{"id":7784,"date":"2022-09-04T08:52:05","date_gmt":"2022-09-04T06:52:05","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7784"},"modified":"2022-09-04T08:52:05","modified_gmt":"2022-09-04T06:52:05","slug":"dao-la-semana-en-calculemus-2-de-septiembre-de-2022","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/dao-la-semana-en-calculemus-2-de-septiembre-de-2022\/","title":{"rendered":"DAO: La semana en Calculemus (2 de septiembre de 2022)"},"content":{"rendered":"<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b<\/a><\/li>\n<li><a href=\"#ej2\">2. Si R es un anillo y a, b \u2208 R, entonces (a + b) + -b = a<\/a><\/li>\n<li><a href=\"#ej3\">3. Si R es un anillo y a, b, c \u2208 R tales que a + b = a + c, entonces b = c<\/a><\/li>\n<li><a href=\"#ej4\">4. Si R es un anillo y a, b, c \u2208 R tales que a + b = c + b, entonces a = c<\/a><\/li>\n<li><a href=\"#ej5\">5. Si R es un anillo y a \u2208 R, entonces a * 0 = 0<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b<\/h3>\n<p>En Lean, se declara que R es un anillo mediante la expresi\u00f3n<\/p>\n<pre lang=\"text\">\n   variables {R : Type*} [ring R]\n<\/pre>\n<p>y, como consecuencia, se tienen los siguientes axiomas<\/p>\n<pre lang=\"text\">\n   add_assoc    : \u2200 a b c : R, (a + b) + c = a + (b + c)\n   add_comm     : \u2200 a b : R,   a + b = b + a\n   zero_add     : \u2200 a : R,     0 + a = a\n   add_left_neg : \u2200 a : R,     -a + a = 0\n   mul_assoc    : \u2200 a b c : R, a * b * c = a * (b * c)\n   mul_one      : \u2200 a : R,     a * 1 = a\n   one_mul      : \u2200 a : R,     1 * a = a\n   mul_add      : \u2200 a b c : R, a * (b + c) = a * b + a * c\n   add_mul      : \u2200 a b c : R, (a + b) * c = a * c + b * c\n<\/pre>\n<p>Demostrar que si R es un anillo, entonces<\/p>\n<pre lang=\"text\">\n   \u2200 a b : R, -a + (a + b) = b\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\nexample\n  : -a + (a + b) = b :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\ncalc -a + (a + b)\n     = (-a + a) + b : by rw \u2190 add_assoc\n ... = 0 + b        : by rw add_left_neg\n ... = b            : by rw zero_add\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\nbegin\n  rw \u2190add_assoc,\n  rw add_left_neg,\n  rw zero_add,\nend\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\nby rw [\u2190add_assoc, add_left_neg, zero_add]\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\n-- by library_search\nneg_add_cancel_left a b\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  : -a + (a + b) = b :=\n-- by hint\nby finish\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Opuesto_se_cancela_con_la_suma_por_la_izquierda.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<\/p>\n<h3>2. Si R es un anillo y a, b \u2208 R, entonces (a + b) + -b = a<\/h3>\n<p>Demostrar que si R es un anillo, entonces<\/p>\n<pre lang=\"text\">\n   \u2200 a b : R, (a + b) + -b = a\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\nexample : (a + b) + -b = a :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariables a b : R\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\ncalc (a + b) + -b\n     = a + (b + -b) : by rw add_assoc\n ... = a + 0        : by rw add_right_neg\n ... = a            : by rw add_zero\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\nbegin\n  rw add_assoc,\n  rw add_right_neg,\n  rw add_zero,\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\nby rw [add_assoc, add_right_neg, add_zero]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\n-- by library_search\nadd_neg_eq_of_eq_add rfl\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a + b) + -b = a :=\n-- by hint\nby finish\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Opuesto_se_cancela_con_la_suma_por_la_derecha.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<h3>3. Si R es un anillo y a, b, c \u2208 R tales que a + b = a + c, entonces b = c<\/h3>\n<p>Demostrar que si R es un anillo y a, b, c \u2208 R tales que<\/p>\n<pre lang=\"text\">\n   a + b = a + c\n<\/pre>\n<p>entonces<\/p>\n<pre lang=\"text\">\n   b = c\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables {a b c : R}\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables {a b c : R}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\ncalc b\n     = 0 + b        : by rw zero_add\n ... = (-a + a) + b : by rw add_left_neg\n ... = -a + (a + b) : by rw add_assoc\n ... = -a + (a + c) : by rw h\n ... = (-a + a) + c : by rw \u2190add_assoc\n ... = 0 + c        : by rw add_left_neg\n ... = c            : by rw zero_add\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\ncalc b\n     = 0 + b        : by simp\n ... = (-a + a) + b : by simp\n ... = -a + (a + b) : by simp\n ... = -a + (a + c) : by rw h\n ... = (-a + a) + c : by simp\n ... = 0 + c        : by simp\n ... = c            : by simp\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nlemma aux : -a + (a + b) = b :=\nby finish\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\ncalc b\n     = -a + (a + b) : aux.symm\n ... = -a + (a + c) : congr_arg (\u03bb x, -a + x) h\n ... = c            : aux\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\n-- by library_search\n(add_right_inj a).mp h\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = a + c)\n  : b = c :=\n-- by hint\nby finish\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Cancelativa_de_la_suma_por_la_izquierda.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<h3>4. Si R es un anillo y a, b, c \u2208 R tales que a + b = c + b, entonces a = c<\/h3>\n<p>Demostrar que si R es un anillo y a, b, c \u2208 R tales que<\/p>\n<pre lang=\"text\">\n   a + b = c + b\n<\/pre>\n<p>entonces<\/p>\n<pre lang=\"text\">\n   a = c\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables {a b c : R}\n\nexample\n  (h : a + b = c + b)\n  : a = c :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport algebra.ring\nimport tactic\n\nvariables {R : Type*} [ring R]\nvariables {a b c : R}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = c + b)\n  : a = c :=\ncalc a\n     = a + 0        : by rw add_zero\n ... = a + (b + -b) : by rw add_right_neg\n ... = (a + b) + -b : by rw add_assoc\n ... = (c + b) + -b : by rw h\n ... = c + (b + -b) : by rw \u2190 add_assoc\n ... = c + 0        : by rw \u2190 add_right_neg\n ... = c            : by rw add_zero\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = c + b)\n  : a = c :=\ncalc a\n     = a + 0        : by simp\n ... = a + (b + -b) : by simp\n ... = (a + b) + -b : by simp\n ... = (c + b) + -b : by rw h\n ... = c + (b + -b) : by simp\n ... = c + 0        : by simp\n ... = c            : by simp\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nlemma aux : (a + b) + -b = a :=\nby finish\n\nexample\n  (h : a + b = c + b)\n  : a = c :=\ncalc a\n     = (a + b) + -b : aux.symm\n ... = (c + b) + -b : congr_arg (\u03bb x, x + -b) h\n ... = c            : aux\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a + b = c + b)\n  : a = c :=\nby finish\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Cancelativa_de_la_suma_por_la_derecha.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<h3>5. Si R es un anillo y a \u2208 R, entonces a * 0 = 0<\/h3>\n<p>Demostrar que Si R es un anillo y a \u2208 R, entonces<\/p>\n<pre lang=\"text\">\na * 0 = 0\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariable  a : R\n\nexample : a * 0 = 0 :=\nsorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport algebra.ring\n\nvariables {R : Type*} [ring R]\nvariable  a : R\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : (mul_add a 0 0).symm\n     ... = a * 0       : congr_arg (\u03bb x, a * x) (add_zero 0)\n     ... = a * 0 + 0   : (add_zero (a * 0)).symm,\n  rw add_left_cancel h\nend\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : by rw \u2190mul_add\n     ... = a * 0       : by rw add_zero\n     ... = a * 0 + 0   : by rw add_zero,\n  rw add_left_cancel h\nend\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n  { rw [\u2190mul_add, add_zero, add_zero] },\n  rw add_left_cancel h\nend\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nbegin\n  have h : a * 0 + a * 0 = a * 0 + 0,\n    calc a * 0 + a * 0\n         = a * (0 + 0) : by simp\n     ... = a * 0       : by simp\n     ... = a * 0 + 0   : by simp,\n  simp,\nend\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\nby simp\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 0 = 0 :=\n-- by library_search\nmul_zero a\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Producto_por_cero.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades: 1. Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b 2. Si R es un anillo y a, b \u2208 R, entonces (a + b) + -b = a 3. Si R&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7784"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7784"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7784\/revisions"}],"predecessor-version":[{"id":7785,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7784\/revisions\/7785"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7784"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7784"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7784"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}