{"id":8203,"date":"2024-05-18T12:32:26","date_gmt":"2024-05-18T10:32:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8203"},"modified":"2024-05-18T12:32:26","modified_gmt":"2024-05-18T10:32:26","slug":"18-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/18-may-24\/","title":{"rendered":"La semana en Calculemus (18 de mayo de 2024)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/jaalonso.github.io\/calculemus\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Si G es un grupo y a, b \u2208 G tales que ab = 1 entonces a\u207b\u00b9 = b<\/a><\/li>\n<li><a href=\"#ej2\">2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9<\/a><\/li>\n<li><a href=\"#ej3\">3. Si G un grupo y a \u2208 G, entonces (a\u207b\u00b9)\u207b\u00b9 = a<\/a><\/li>\n<li><a href=\"#ej4\">4. Si G es un grupo y a, b, c \u2208 G tales que a\u00b7b = a\u00b7c, entonces b = c<\/a><\/li>\n<li><a href=\"#ej5\">5. Si M es un monoide, a \u2208 M y m, n \u2208 \u2115, entonces a^(m\u00b7n) = (a^m)^n<\/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 G es un grupo y a, b \u2208 G tales que ab = 1 entonces a\u207b\u00b9 = b<\/h3>\n<p>Demostrar con Lean4 que si &#92;(a&#92;) es un elemento de un grupo &#92;(G&#92;), entonces &#92;(a&#92;) tiene un \u00fanico inverso; es decir, si &#92;(b&#92;) es un elemento de &#92;(G&#92;) tal que &#92;(a\u00b7b = 1&#92;), entonces &#92;(a\u207b\u00b9 = b&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b : G}\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\nby sorry\n<\/pre>\n<h4>1.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   a\u207b\u00b9 &amp;= a\u207b\u00b9\u00b71        &amp;&amp;&#92;text{[porque 1 es neutro]} &#92;&#92;<br \/>\n       &amp;= a\u207b\u00b9\u00b7(a\u00b7b)    &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n       &amp;= (a\u207b\u00b9\u00b7a)\u00b7b    &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n       &amp;= 1\u00b7b          &amp;&amp;&#92;text{[porque a\u207b\u00b9 es el inverso de a]} &#92;&#92;<br \/>\n       &amp;= b            &amp;&amp;&#92;text{[porque 1 es neutro]}<br \/>\n&#92;end{align}<\/p>\n<h4>1.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1  := (mul_one a\u207b\u00b9).symm\n  _ = a\u207b\u00b9 * (a * b) := congrArg (a\u207b\u00b9 * .) h.symm\n  _ = (a\u207b\u00b9 * a) * b := (mul_assoc a\u207b\u00b9 a b).symm\n  _ = 1 * b         := congrArg (. * b) (inv_mul_self a)\n  _ = b             := one_mul b\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1       := by simp only [mul_one]\n       _ = a\u207b\u00b9 * (a * b) := by simp only [h]\n       _ = (a\u207b\u00b9 * a) * b := by simp only [mul_assoc]\n       _ = 1 * b         := by simp only [inv_mul_self]\n       _ = b             := by simp only [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1       := by simp\n       _ = a\u207b\u00b9 * (a * b) := by simp [h]\n       _ = (a\u207b\u00b9 * a) * b := by simp\n       _ = 1 * b         := by simp\n       _ = b             := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * (a * b) := by simp [h]\n       _ = b             := by simp\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : b * a = 1)\n  : b = a\u207b\u00b9 :=\neq_inv_iff_mul_eq_one.mpr h\n\n-- Lemas usados\n-- ============\n\n-- variable (c : G)\n-- #check (eq_inv_iff_mul_eq_one : a = b\u207b\u00b9 \u2194 a * b = 1)\n-- #check (inv_mul_self a : a\u207b\u00b9 * a = 1)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Unicidad_de_los_inversos_en_los_grupos.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>1.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Unicidad_de_los_inversos_en_los_grupos\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows \"inverse a = b\"\nproof -\n  have \"inverse a = inverse a * 1\"    by (simp only: right_neutral)\n  also have \"\u2026 = inverse a * (a * b)\" by (simp only: assms(1))\n  also have \"\u2026 = (inverse a * a) * b\" by (simp only: assoc [symmetric])\n  also have \"\u2026 = 1 * b\"               by (simp only: left_inverse)\n  also have \"\u2026 = b\"                   by (simp only: left_neutral)\n  finally show \"inverse a = b\"        by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows \"inverse a = b\"\nproof -\n  have \"inverse a = inverse a * 1\"    by simp\n  also have \"\u2026 = inverse a * (a * b)\" using assms by simp\n  also have \"\u2026 = (inverse a * a) * b\" by (simp add: assoc [symmetric])\n  also have \"\u2026 = 1 * b\"               by simp\n  also have \"\u2026 = b\"                   by simp\n  finally show \"inverse a = b\"        .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows \"inverse a = b\"\nproof -\n  from assms have \"inverse a * (a * b) = inverse a\"\n    by simp\n  then show \"inverse a = b\"\n    by (simp add: assoc [symmetric])\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows \"inverse a = b\"\n  using assms\n  by (simp only: inverse_unique)\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9<\/h3>\n<p>Demostrar con Lean4 que si &#92;(G&#92;) es un grupo y &#92;(a, b &#92;in G&#92;), entonces &#92;((ab)^{-1} = b^{-1}a^{-1}&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nsorry\n<\/pre>\n<h4>2.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p><br \/>\nTeniendo en cuenta la propiedad<br \/>\n   &#92;[(\u2200 a, b \u2208 G)[ab = 1 \u2192 a\u207b\u00b9 = b] &#92;]<br \/>\nbasta demostrar que<br \/>\n   &#92;[(a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) = 1.&#92;]<br \/>\nque se demuestra mediante la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   (a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) &amp;= a\u00b7(b\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9))   &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7((b\u00b7b\u207b\u00b9)\u00b7a\u207b\u00b9)   &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7(1\u00b7a\u207b\u00b9)         &amp;&amp;&#92;text{[por producto con inverso]} &#92;&#92;<br \/>\n                   &amp;= a\u00b7a\u207b\u00b9             &amp;&amp;&#92;text{[por producto con uno]} &#92;&#92;<br \/>\n                   &amp;= 1                 &amp;&amp;&#92;text{[por producto con<br \/>\n                   inverso]}<br \/>\n&#92;end{align}<\/p>\n<h4>2.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nlemma aux : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\ncalc\n  (a * b) * (b\u207b\u00b9 * a\u207b\u00b9)\n    = a * (b * (b\u207b\u00b9 * a\u207b\u00b9)) := by rw [mul_assoc]\n  _ = a * ((b * b\u207b\u00b9) * a\u207b\u00b9) := by rw [mul_assoc]\n  _ = a * (1 * a\u207b\u00b9)         := by rw [mul_right_inv]\n  _ = a * a\u207b\u00b9               := by rw [one_mul]\n  _ = 1                     := by rw [mul_right_inv]\n\n-- 1\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n  exact inv_eq_of_mul_eq_one_right h1\n\n-- 3\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n  simp [h1]\n\n-- 4\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n    aux a b\n  simp [h1]\n\n-- 5\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n  apply inv_eq_of_mul_eq_one_right\n  rw [aux]\n\n-- 6\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby exact mul_inv_rev a b\n\n-- 7\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby simp\n<\/pre>\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\/Inverso_del_producto.lean\" rel=\"noopener noreferrer\" target=\"_blank\">Lean 4 Web<\/a>.<\/p>\n<h4>2.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Inverso_del_producto\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (a * b) = inverse b * inverse a\"\nproof (rule inverse_unique)\n  have \"(a * b) * (inverse b * inverse a) =\n        ((a * b) * inverse b) * inverse a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * (b * inverse b)) * inverse a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * 1) * inverse a\"\n    by (simp only: right_inverse)\n  also have \"\u2026 = a * inverse a\"\n    by (simp only: right_neutral)\n  also have \"\u2026 = 1\"\n    by (simp only: right_inverse)\n  finally show \"a * b * (inverse b * inverse a) = 1\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (a * b) = inverse b * inverse a\"\nproof (rule inverse_unique)\n  have \"(a * b) * (inverse b * inverse a) =\n        ((a * b) * inverse b) * inverse a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * (b * inverse b)) * inverse a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * 1) * inverse a\"\n    by simp\n  also have \"\u2026 = a * inverse a\"\n    by simp\n  also have \"\u2026 = 1\"\n    by simp\n  finally show \"a * b * (inverse b * inverse a) = 1\"\n    .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (a * b) = inverse b * inverse a\"\nproof (rule inverse_unique)\n  have \"a * b * (inverse b * inverse a) =\n        a * (b * inverse b) * inverse a\"\n    by (simp only: assoc)\n  also have \"\u2026 = 1\"\n    by simp\n  finally show \"a * b * (inverse b * inverse a) = 1\" .\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (a * b) = inverse b * inverse a\"\n  by (simp only: inverse_distrib_swap)\n\nend\n\nend\n<\/pre>\n<h4>Referencias<\/h4>\n<ul>\n<li> J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 12.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Si G un grupo y a \u2208 G, entonces (a\u207b\u00b9)\u207b\u00b9 = a<\/h3>\n<p>Demostrar con Lean4 que si &#92;(G&#92;) un grupo y &#92;(a \u2208 G&#92;), entonces<br \/>\n&#92;[(a\u207b\u00b9)\u207b\u00b9 = a&#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a : G}\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nsorry\n<\/pre>\n<h4>3.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   (a\u207b\u00b9)\u207b\u00b9 &amp;= (a\u207b\u00b9)\u207b\u00b9\u00b71          &amp;&amp;&#92;text{[porque &#92;(1&#92;) es neutro]} &#92;&#92;<br \/>\n           &amp;= (a\u207b\u00b9)\u207b\u00b9\u00b7(a\u207b\u00b9\u00b7a)    &amp;&amp;&#92;text{[porque &#92;(a\u207b\u00b9&#92;) es el inverso de &#92;(a&#92;)]} &#92;&#92;<br \/>\n           &amp;= ((a\u207b\u00b9)\u207b\u00b9\u00b7a\u207b\u00b9)\u00b7a    &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n           &amp;= 1\u00b7a                &amp;&amp;&#92;text{[porque &#92;((a\u207b\u00b9)\u207b\u00b9&#92;) es el inverso de &#92;(a\u207b\u00b9&#92;)]} &#92;&#92;<br \/>\n           &amp;= a                  &amp;&amp;&#92;text{[porque &#92;(1&#92;) es neutro]}<br \/>\n&#92;end{align}<\/p>\n<h4>3.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n     = (a\u207b\u00b9)\u207b\u00b9 * 1         := (mul_one (a\u207b\u00b9)\u207b\u00b9).symm\n   _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := congrArg ((a\u207b\u00b9)\u207b\u00b9 * .) (inv_mul_self a).symm\n   _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := (mul_assoc _ _ _).symm\n   _ = 1 * a               := congrArg (. * a) (inv_mul_self a\u207b\u00b9)\n   _ = a                   := one_mul a\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n     = (a\u207b\u00b9)\u207b\u00b9 * 1         := by simp only [mul_one]\n   _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := by simp only [inv_mul_self]\n   _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := by simp only [mul_assoc]\n   _ = 1 * a               := by simp only [inv_mul_self]\n   _ = a                   := by simp only [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\ncalc (a\u207b\u00b9)\u207b\u00b9\n     = (a\u207b\u00b9)\u207b\u00b9 * 1         := by simp\n   _ = (a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a) := by simp\n   _ = ((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a := by simp\n   _ = 1 * a               := by simp\n   _ = a                   := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nby\n  apply mul_eq_one_iff_inv_eq.mp\n  -- \u22a2 a\u207b\u00b9 * a = 1\n  exact mul_left_inv a\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a :=\nmul_eq_one_iff_inv_eq.mp (mul_left_inv a)\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a:=\ninv_inv a\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (a\u207b\u00b9)\u207b\u00b9 = a:=\nby simp\n\n-- Lemas usados\n-- ============\n\n-- variable (b c : G)\n-- #check (inv_inv a : (a\u207b\u00b9)\u207b\u00b9 = a)\n-- #check (inv_mul_self a : a\u207b\u00b9 * a = 1)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_eq_one_iff_inv_eq : a * b = 1 \u2194 a\u207b\u00b9 = b)\n-- #check (mul_left_inv a : a\u207b\u00b9  * a = 1)\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Inverso_del_inverso_en_grupos.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Inverso_del_inverso_en_grupos\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\nproof -\n  have \"inverse (inverse a) =\n        (inverse (inverse a)) * 1\"\n    by (simp only: right_neutral)\n  also have \"\u2026 = inverse (inverse a) * (inverse a * a)\"\n    by (simp only: left_inverse)\n  also have \"\u2026 = (inverse (inverse a) * inverse a) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = 1 * a\"\n    by (simp only: left_inverse)\n  also have \"\u2026 = a\"\n    by (simp only: left_neutral)\n  finally show \"inverse (inverse a) = a\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\nproof -\n  have \"inverse (inverse a) =\n        (inverse (inverse a)) * 1\"                       by simp\n  also have \"\u2026 = inverse (inverse a) * (inverse a * a)\" by simp\n  also have \"\u2026 = (inverse (inverse a) * inverse a) * a\" by simp\n  also have \"\u2026 = 1 * a\"                                 by simp\n  finally show \"inverse (inverse a) = a\"                 by simp\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\nproof (rule inverse_unique)\n  show \"inverse a * a = 1\"\n    by (simp only: left_inverse)\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\nproof (rule inverse_unique)\n  show \"inverse a * a = 1\" by simp\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\n  by (rule inverse_unique) simp\n\n(* 6\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\n  by (simp only: inverse_inverse)\n\n(* 7\u00aa demostraci\u00f3n *)\n\nlemma \"inverse (inverse a) = a\"\n  by simp\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Si G es un grupo y a, b, c \u2208 G tales que a\u00b7b = a\u00b7c, entonces b = c<\/h3>\n<p>Demostrar con Lean4 que si &#92;(G&#92;) es un grupo y &#92;(a, b, c \u2208 G&#92;) tales que &#92;(a\u00b7b = a\u00b7c&#92;), entonces &#92;(b = c&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b c : G}\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\nsorry\n<\/pre>\n<h4>4.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   b &amp;= 1\u00b7b          &amp;&amp;&#92;text{[porque &#92;(1&#92;) es neutro]} &#92;&#92;<br \/>\n     &amp;= (a\u207b\u00b9\u00b7a)\u00b7b    &amp;&amp;&#92;text{[porque &#92;(a\u207b\u00b9&#92;) es el inverso de &#92;(a&#92;)]} &#92;&#92;<br \/>\n     &amp;= a\u207b\u00b9\u00b7(a\u00b7b)    &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n     &amp;= a\u207b\u00b9\u00b7(a\u00b7c)    &amp;&amp;&#92;text{[por la hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= (a\u207b\u00b9\u00b7a)\u00b7c    &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n     &amp;= 1\u00b7c          &amp;&amp;&#92;text{[porque &#92;(a\u207b\u00b9&#92;) es el inverso de &#92;(a&#92;)]} &#92;&#92;<br \/>\n     &amp;= c            &amp;&amp;&#92;text{[porque 1 es neutro]}<br \/>\n&#92;end{align}<\/p>\n<h4>4.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b c : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\ncalc b = 1 * b         := (one_mul b).symm\n     _ = (a\u207b\u00b9 * a) * b := congrArg (. * b) (inv_mul_self a).symm\n     _ = a\u207b\u00b9 * (a * b) := mul_assoc a\u207b\u00b9 a b\n     _ = a\u207b\u00b9 * (a * c) := congrArg (a\u207b\u00b9 * .) h\n     _ = (a\u207b\u00b9 * a) * c := (mul_assoc a\u207b\u00b9 a c).symm\n     _ = 1 * c         := congrArg (. * c) (inv_mul_self a)\n     _ = c             := one_mul c\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\ncalc b = 1 * b         := by rw [one_mul]\n     _ = (a\u207b\u00b9 * a) * b := by rw [inv_mul_self]\n     _ = a\u207b\u00b9 * (a * b) := by rw [mul_assoc]\n     _ = a\u207b\u00b9 * (a * c) := by rw [h]\n     _ = (a\u207b\u00b9 * a) * c := by rw [mul_assoc]\n     _ = 1 * c         := by rw [inv_mul_self]\n     _ = c             := by rw [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\ncalc b = 1 * b         := by simp\n     _ = (a\u207b\u00b9 * a) * b := by simp\n     _ = a\u207b\u00b9 * (a * b) := by simp\n     _ = a\u207b\u00b9 * (a * c) := by simp [h]\n     _ = (a\u207b\u00b9 * a) * c := by simp\n     _ = 1 * c         := by simp\n     _ = c             := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\ncalc b = a\u207b\u00b9 * (a * b) := by simp\n     _ = a\u207b\u00b9 * (a * c) := by simp [h]\n     _ = c             := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\nmul_left_cancel h\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h: a * b = a  * c)\n  : b = c :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- #check (inv_mul_self a : a\u207b\u00b9 * a = 1)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_left_cancel : a * b = a * c \u2192 b = c)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Propiedad_cancelativa_en_grupos.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>4.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Propiedad_cancelativa_en_grupos\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"b = 1 * b\"                    by (simp only: left_neutral)\n  also have \"\u2026 = (inverse a * a) * b\" by (simp only: left_inverse)\n  also have \"\u2026 = inverse a * (a * b)\" by (simp only: assoc)\n  also have \"\u2026 = inverse a * (a * c)\" by (simp only: \u2039a * b = a * c\u203a)\n  also have \"\u2026 = (inverse a * a) * c\" by (simp only: assoc)\n  also have \"\u2026 = 1 * c\"               by (simp only: left_inverse)\n  also have \"\u2026 = c\"                   by (simp only: left_neutral)\n  finally show \"b = c\"                by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"b = 1 * b\"                    by simp\n  also have \"\u2026 = (inverse a * a) * b\" by simp\n  also have \"\u2026 = inverse a * (a * b)\" by (simp only: assoc)\n  also have \"\u2026 = inverse a * (a * c)\" using \u2039a * b = a * c\u203a by simp\n  also have \"\u2026 = (inverse a * a) * c\" by (simp only: assoc)\n  also have \"\u2026 = 1 * c\"               by simp\n  finally show \"b = c\"                by simp\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"b = (inverse a * a) * b\"      by simp\n  also have \"\u2026 = inverse a * (a * b)\" by (simp only: assoc)\n  also have \"\u2026 = inverse a * (a * c)\" using \u2039a * b = a * c\u203a by simp\n  also have \"\u2026 = (inverse a * a) * c\" by (simp only: assoc)\n  finally show \"b = c\"                by simp\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"inverse a * (a * b) = inverse a * (a * c)\"\n    by (simp only: \u2039a * b = a * c\u203a)\n  then have \"(inverse a * a) * b = (inverse a * a) * c\"\n    by (simp only: assoc)\n  then have \"1 * b = 1 * c\"\n    by (simp only: left_inverse)\n  then show \"b = c\"\n    by (simp only: left_neutral)\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"inverse a * (a * b) = inverse a * (a * c)\"\n    by (simp only: \u2039a * b = a * c\u203a)\n  then have \"(inverse a * a) * b = (inverse a * a) * c\"\n    by (simp only: assoc)\n  then have \"1 * b = 1 * c\"\n    by (simp only: left_inverse)\n  then show \"b = c\"\n    by (simp only: left_neutral)\nqed\n\n(* 6\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\nproof -\n  have \"inverse a * (a * b) = inverse a * (a * c)\"\n    using \u2039a * b = a * c\u203a by simp\n  then have \"(inverse a * a) * b = (inverse a * a) * c\"\n    by (simp only: assoc)\n  then have \"1 * b = 1 * c\"\n    by simp\n  then show \"b = c\"\n    by simp\nqed\n\n(* 7\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = a * c\"\n  shows   \"b = c\"\n  using assms\n  by (simp only: left_cancel)\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si M es un monoide, a \u2208 M y m, n \u2208 \u2115, entonces a^(m\u00b7n) = (a^m)^n<\/h3>\n<p>Demostrar con Lean4 que si &#92;(M&#92;) es un monoide, &#92;(a \u2208 M&#92;) y &#92;(m, n \u2208 \u2115&#92;), entonces<br \/>\n&#92;[ a^{m\u00b7n} = (a^m)^n &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (a : M)\nvariable (m n : \u2115)\n\nexample : a^(m * n) = (a^m)^n :=\nby sorry\n<\/pre>\n<h4>5.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por inducci\u00f3n en &#92;(n&#92;).<\/p>\n<p><strong>Caso base<\/strong>: Supongamos que &#92;(n = 0&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   a^{m\u00b70} &amp;= a^0       &#92;&#92;<br \/>\n           &amp;= 1         &amp;&amp;&#92;text{[por pow_zero]} &#92;&#92;<br \/>\n           &amp;= (a^m)^0   &amp;&amp;&#92;text{[por pow_zero]}<br \/>\n&#92;end{align}<\/p>\n<p>Paso de induci\u00f3n: Supogamos que se verifica para &#92;(n&#92;); es decir,<br \/>\n&#92;[ a^{m\u00b7n} = (a^m)^n &#92;tag{HI} &#92;]<br \/>\nEntonces,<br \/>\n&#92;begin{align}<br \/>\n   a^{m\u00b7(n+1)} &amp;= a^{m\u00b7n + m}    &#92;&#92;<br \/>\n               &amp;= a^{m\u00b7n}\u00b7a^m    &#92;&#92;<br \/>\n               &amp;= (a^m)^n\u00b7a^m    &amp;&amp;&#92;text{[por HI]} &#92;&#92;<br \/>\n               &amp;= (a^m)^{n+1}    &amp;&amp;&#92;text{[por pow_succ&#8217;]}<br \/>\n&#92;end{align}<\/p>\n<h4>5.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (a : M)\nvariable (m n : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . calc a^(m * 0)\n         = a^0             := congrArg (a ^ .) (Nat.mul_zero m)\n       _ = 1               := pow_zero a\n       _ = (a^m)^0         := (pow_zero (a^m)).symm\n  . calc a^(m * succ n)\n         = a^(m * n + m)   := congrArg (a ^ .) (Nat.mul_succ m n)\n       _ = a^(m * n) * a^m := pow_add a (m * n) m\n       _ = (a^m)^n * a^m   := congrArg (. * a^m) HI\n       _ = (a^m)^(succ n)  := (pow_succ' (a^m) n).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . calc a^(m * 0)\n         = a^0             := by simp only [Nat.mul_zero]\n       _ = 1               := by simp only [_root_.pow_zero]\n       _ = (a^m)^0         := by simp only [_root_.pow_zero]\n  . calc a^(m * succ n)\n         = a^(m * n + m)   := by simp only [Nat.mul_succ]\n       _ = a^(m * n) * a^m := by simp only [pow_add]\n       _ = (a^m)^n * a^m   := by simp only [HI]\n       _ = (a^m)^succ n    := by simp only [_root_.pow_succ']\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . calc a^(m * 0)\n         = a^0             := by simp [Nat.mul_zero]\n       _ = 1               := by simp\n       _ = (a^m)^0         := by simp\n  . calc a^(m * succ n)\n         = a^(m * n + m)   := by simp [Nat.mul_succ]\n       _ = a^(m * n) * a^m := by simp [pow_add]\n       _ = (a^m)^n * a^m   := by simp [HI]\n       _ = (a^m)^succ n    := by simp [_root_.pow_succ']\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . simp [Nat.mul_zero]\n  . simp [Nat.mul_succ,\n          pow_add,\n          HI,\n          _root_.pow_succ']\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . -- \u22a2 a ^ (m * zero) = (a ^ m) ^ zero\n    rw [Nat.mul_zero]\n    -- \u22a2 a ^ 0 = (a ^ m) ^ zero\n    rw [_root_.pow_zero]\n    -- \u22a2 1 = (a ^ m) ^ zero\n    rw [_root_.pow_zero]\n  . -- \u22a2 a ^ (m * succ n) = (a ^ m) ^ succ n\n    rw [Nat.mul_succ]\n    -- \u22a2 a ^ (m * n + m) = (a ^ m) ^ succ n\n    rw [pow_add]\n    -- \u22a2 a ^ (m * n) * a ^ m = (a ^ m) ^ succ n\n    rw [HI]\n    -- \u22a2 (a ^ m) ^ n * a ^ m = (a ^ m) ^ succ n\n    rw [_root_.pow_succ']\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n  induction' n with n HI\n  . rw [Nat.mul_zero, _root_.pow_zero, _root_.pow_zero]\n  . rw [Nat.mul_succ, pow_add, HI, _root_.pow_succ']\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\npow_mul a m n\n\n-- Lemas usados\n-- ============\n\n-- #check (Nat.mul_succ n m : n * succ m = n * m + n)\n-- #check (Nat.mul_zero m : m * 0 = 0)\n-- #check (pow_add a m n : a ^ (m + n) = a ^ m * a ^ n)\n-- #check (pow_mul a m n : a ^ (m * n) = (a ^ m) ^ n)\n-- #check (pow_succ' a n : a ^ (n + 1) = a ^ n * a)\n-- #check (pow_zero a : a ^ 0 = 1)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Potencias_de_potencias_en_monoides.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>5.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Potencias_de_potencias_en_monoides\nimports Main\nbegin\n\ncontext monoid_mult\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma  \"a^(m * n) = (a^m)^n\"\nproof (induct n)\n  have \"a ^ (m * 0) = a ^ 0\"\n    by (simp only: mult_0_right)\n  also have \"\u2026 = 1\"\n    by (simp only: power_0)\n  also have \"\u2026 = (a ^ m) ^ 0\"\n    by (simp only: power_0)\n  finally show \"a ^ (m * 0) = (a ^ m) ^ 0\"\n    by this\nnext\n  fix n\n  assume HI : \"a ^ (m * n) = (a ^ m) ^ n\"\n  have \"a ^ (m * Suc n) = a ^ (m + m * n)\"\n    by (simp only: mult_Suc_right)\n  also have \"\u2026 = a ^ m * a ^ (m * n)\"\n    by (simp only: power_add)\n  also have \"\u2026 = a ^ m * (a ^ m) ^ n\"\n    by (simp only: HI)\n  also have \"\u2026 = (a ^ m) ^ Suc n\"\n    by (simp only: power_Suc)\n  finally show \"a ^ (m * Suc n) = (a ^ m) ^ Suc n\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma  \"a^(m * n) = (a^m)^n\"\nproof (induct n)\n  have \"a ^ (m * 0) = a ^ 0\"               by simp\n  also have \"\u2026 = 1\"                        by simp\n  also have \"\u2026 = (a ^ m) ^ 0\"              by simp\n  finally show \"a ^ (m * 0) = (a ^ m) ^ 0\" .\nnext\n  fix n\n  assume HI : \"a ^ (m * n) = (a ^ m) ^ n\"\n  have \"a ^ (m * Suc n) = a ^ (m + m * n)\" by simp\n  also have \"\u2026 = a ^ m * a ^ (m * n)\"      by (simp add: power_add)\n  also have \"\u2026 = a ^ m * (a ^ m) ^ n\"      using HI by simp\n  also have \"\u2026 = (a ^ m) ^ Suc n\"          by simp\n  finally show \"a ^ (m * Suc n) =\n                (a ^ m) ^ Suc n\"           .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma  \"a^(m * n) = (a^m)^n\"\nproof (induct n)\n  case 0\n  then show ?case by simp\nnext\n  case (Suc n)\n  then show ?case by (simp add: power_add)\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma  \"a^(m * n) = (a^m)^n\"\n  by (induct n) (simp_all add: power_add)\n\n(* 5\u00aa demostraci\u00f3n *)\n\nlemma \"a^(m * n) = (a^m)^n\"\n  by (simp only: power_mult)\n\nend\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Si G es un grupo y a, b \u2208 G tales que ab = 1 entonces a\u207b\u00b9 = b 2. Si G es un grupo y a, b \u2208 G, entonces (ab)\u207b\u00b9 = b\u207b\u00b9a\u207b\u00b9 3. Si G un grupo y&#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":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_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":[1],"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\/8203"}],"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=8203"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8203\/revisions"}],"predecessor-version":[{"id":8204,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8203\/revisions\/8204"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8203"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8203"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8203"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}