{"id":7976,"date":"2023-07-29T12:30:22","date_gmt":"2023-07-29T10:30:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7976"},"modified":"2023-07-29T12:41:45","modified_gmt":"2023-07-29T10:41:45","slug":"29-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/29-jul-23\/","title":{"rendered":"La semana en Calculemus (29 de julio de 2023)"},"content":{"rendered":"<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si c = da+b y b = ad, entonces c = 2ad<\/a><\/li>\n<li><a href=\"#ej2\">2. Si a+b = c, entonces (a+b)(a+b) = ac+ bc<\/a><\/li>\n<li><a href=\"#ej3\">3. Si R es un anillo y a \u2208 R, entonces a + 0 = a<\/a><\/li>\n<li><a href=\"#ej4\">4. Si R es un anillo y a \u2208 R, entonces a + -a = 0<\/a><\/li>\n<li><a href=\"#ej5\">5. Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b<\/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 c = da+b y b = ad, entonces c = 2ad<\/h3>\n<p>Demostrar con Lean4 que si a, b, c y d son n\u00fameros reales tales que<\/p>\n<pre lang=\"text\">\n   c = d * a + b\n   b = a * d\n<\/pre>\n<p>entonces<\/p>\n<pre lang=\"text\">\n   c = 2 * a * d\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (a b c d : \u211d)\n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><br \/>\nPor la siguiente cadena de igualdades<br \/>\n\\begin{align}<br \/>\n   c &amp;= da + b     &amp;&amp;\\text{[por la primera hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= da + ad    &amp;&amp;\\text{[por la segunda hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= ad + ad    &amp;&amp;\\text{[por la conmutativa]} &#92;&#92;<br \/>\n     &amp;= 2(ad)      &amp;&amp;\\text{[por la def. de doble]} &#92;&#92;<br \/>\n     &amp;= 2ad        &amp;&amp;\\text{[por la asociativa]}<br \/>\n\\end{align}<\/p>\n<p><b>Demostraciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (a b c d : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\ncalc\n  c = d * a + b     := by rw [h1]\n  _ = d * a + a * d := by rw [h2]\n  _ = a * d + a * d := by rw [mul_comm d a]\n  _ = 2 * (a * d)   := by rw [\u2190 two_mul (a * d)]\n  _ = 2 * a * d     := by rw [mul_assoc]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby\n  rw [h2] at h1\n  clear h2\n  rw [mul_comm d a] at h1\n  rw [\u2190 two_mul (a*d)] at h1\n  rw [\u2190 mul_assoc 2 a d] at h1\n  exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby rw [h1, h2, mul_comm d a, \u2190 two_mul (a * d), mul_assoc]\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby\n  rw [h1]\n  rw [h2]\n  ring\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby\n  rw [h1, h2]\n  ring\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby rw [h1, h2] ; ring\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : c = d * a + b)\n  (h2 : b = a * d)\n  : c = 2 * a * d :=\nby linarith\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Si_c_eq_da%252Bb_y_b_eq_ad_entonces_c_eq_2ad.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 8.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si a+b = c, entonces (a+b)(a+b) = ac+ bc<\/h3>\n<p>Demostrar con Lean4 que si a, b y c son n\u00fameros reales tales que<\/p>\n<pre lang=\"text\">\n   a + b = c,\n<\/pre>\n<p>entonces<\/p>\n<pre lang=\"text\">\n   (a + b) * (a + b) = a * c + b * c\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (a b c : \u211d)\n\nexample\n  (h : a + b = c)\n  : (a + b) * (a + b) = a * c + b * c :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><br \/>\nPor la siguiente cadena de igualdades<br \/>\n\\begin{align}<br \/>\n   (a + b)(a + b)<br \/>\n   &amp;= (a + b)c        &amp;&amp;\\text{[por la hip\u00f3tesis]}   &#92;&#92;<br \/>\n   &amp;= ac + bc         &amp;&amp;\\text{[por la distributiva]}<br \/>\n\\end{align}<\/p>\n<p><b>Demostraciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Tactic\n\nvariable (a b c : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : a + b = c)\n  : (a + b) * (a + b) = a * c + b * c :=\ncalc\n  (a + b) * (a + b)\n    = (a + b) * c   := by exact congrArg (HMul.hMul (a + b)) h\n  _ = a * c + b * c := by rw [add_mul]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : a + b = c)\n  : (a + b) * (a + b) = a * c + b * c :=\nby\n  nth_rewrite 2 [h]\n  rw [add_mul]\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Sia%2Bb_eq_c_entonces_(a%2Bb)(a%2Bb)_eq_ac%2Bbc.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 9.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si R es un anillo y a \u2208 R, entonces a + 0 = a<\/h3>\n<p>En Lean4, se declara que &#40;R&#41; es un anillo mediante la expresi\u00f3n<\/p>\n<pre lang=\"text\">\n   variable {R : Type _} [Ring R]\n<\/pre>\n<p>Como consecuencia, se tiene 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 &#40;R&#41; es un anillo, entonces<\/p>\n<pre lang=\"text\">\n   \u2200 a : R, a + 0 = a\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Ring.Defs\n\nvariable {R : Type _} [Ring R]\nvariable (a : R)\n\nexample : a + 0 = a :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><br \/>\nPor la siguiente cadena de igualdades<br \/>\n\\begin{align}<br \/>\n   a + 0 &amp;= 0 + a    &amp;&amp;\\text{[por la conmutativa de la suma]} &#92;&#92;<br \/>\n         &amp;= a        &amp;&amp;\\text{[por el axioma del cero por la izquierda]}<br \/>\n\\end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\n-- 1\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\ncalc a + 0\n     = 0 + a := by rw [add_comm]\n   _ = a     := by rw [zero_add]\n\n-- 2\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\nby\n  rw [add_comm]\n  rw [zero_add]\n\n-- 3\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\nby rw [add_comm, zero_add]\n\n-- 4\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\nby exact add_zero a\n\n-- 5\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\n  add_zero a\n\n-- 5\u00aa demostraci\u00f3n\nexample : a + 0 = a :=\nby simp\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_con_cero.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 10.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si R es un anillo y a \u2208 R, entonces a + -a = 0<\/h3>\n<p>Demostrar con Lean4 que si &#40;R&#41; es un anillo, entonces<\/p>\n<pre lang=\"text\">\n   \u2200 a : R, a + -a = 0\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Ring.Defs\n\nvariable {R : Type _} [Ring R]\nvariable (a : R)\n\nexample : a + -a = 0 :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><br \/>\nPor la siguiente cadena de igualdades<br \/>\n\\begin{align}<br \/>\n   a + -a &amp;= -a + a    &amp;&amp;\\text{[por la conmutativa de la suma]} &#92;&#92;<br \/>\n          &amp;= 0         &amp;&amp;\\text{[por el axioma de inverso por la izquierda]}<br \/>\n\\end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Ring.Defs\n\nvariable {R : Type _} [Ring R]\nvariable (a : R)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\ncalc a + -a = -a + a := by rw [add_comm]\n          _ = 0      := by rw [add_left_neg]\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\nby\n  rw [add_comm]\n  rw [add_left_neg]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\nby rw [add_comm, add_left_neg]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\nby exact add_neg_self a\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\n  add_neg_self a\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a + -a = 0 :=\nby simp\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Suma_con_opuesto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 10.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si R es un anillo y a, b \u2208 R, entonces -a + (a + b) = b<\/h3>\n<p>Demostrar en Lean4 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 Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Ring.Defs\n\nvariable {R : Type _} [Ring R]\nvariable (a b : R)\n\nexample : -a + (a + b) = b :=\nsorry\n<\/pre>\n<p><b>Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n<p><br \/>\nPor la siguiente cadena de igualdades<br \/>\n\\begin{align}<br \/>\n   -a + (a + b) &amp;= (-a + a) + b    &amp;&amp;\\text{[por la asociativa]} &#92;&#92;<br \/>\n                &amp;= 0 + b           &amp;&amp;\\text{[por inverso por la izquierda]} &#92;&#92;<br \/>\n                &amp;= b               &amp;&amp;\\text{[por cero por la izquierda]}<br \/>\n\\end{align}<\/p>\n<p><b>Demostraciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">\n-- 1\u00aa demostraci\u00f3n\nexample : -a + (a + b) = b :=\ncalc -a + (a + b) = (-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 : -a + (a + b) = b :=\nby\n  rw [\u2190add_assoc]\n  rw [add_left_neg]\n  rw [zero_add]\n\n-- 3\u00aa demostraci\u00f3n\nexample : -a + (a + b) = b :=\nby rw [\u2190add_assoc, add_left_neg, zero_add]\n\n-- 4\u00aa demostraci\u00f3n\nexample : -a + (a + b) = b :=\nby exact neg_add_cancel_left a b\n\n-- 5\u00aa demostraci\u00f3n\nexample : -a + (a + b) = b :=\n  neg_add_cancel_left a b\n\n-- 6\u00aa demostraci\u00f3n\nexample : -a + (a + b) = b :=\nby simp\n<\/pre>\n<p><b>Demostraciones interactivas<\/b><\/p>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/lean.math.hhu.de\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Opuesto_se_cancela_con_la_suma_por_la_izquierda.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 10.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si c = da+b y b = ad, entonces c = 2ad 2. Si a+b = c, entonces (a+b)(a+b) = ac+ bc 3. Si R es un anillo y a \u2208 R, entonces a + 0 = a 4. Si&#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\/7976"}],"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=7976"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7976\/revisions"}],"predecessor-version":[{"id":7983,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7976\/revisions\/7983"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7976"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7976"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7976"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}