{"id":8190,"date":"2024-05-11T06:00:41","date_gmt":"2024-05-11T04:00:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8190"},"modified":"2024-05-10T12:38:20","modified_gmt":"2024-05-10T10:38:20","slug":"11-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/11-may-24\/","title":{"rendered":"La semana en Calculemus (11 de mayo de 2024)"},"content":{"rendered":"\n<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. Producto de potencias de la misma base en monoides<\/a><\/li>\n<li><a href=\"#ej2\">2. Equivalencia de inversos iguales al neutro<\/a><\/li>\n<li><a href=\"#ej3\">3. Unicidad de inversos en monoides<\/a><\/li>\n<li><a href=\"#ej4\">4. Caracterizaci\u00f3n de producto igual al primer factor<\/a><\/li>\n<li><a href=\"#ej5\">5. Unicidad del elemento neutro en los grupos<\/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. Producto de potencias de la misma base en monoides<\/h3>\n<p>En los <a href=\"https:\/\/en.wikipedia.org\/wiki\/Monoid\">monoides<\/a> se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los siguientes lemas:<\/p>\n<pre lang=\"lean\">\n   pow_zero : x^0 = 1\n   pow_succ : x^(succ n) = x * x^n\n<\/pre>\n<p>Demostrar con Lean4 que si &#92;(M&#92;) es un monoide, &#92;(x \u2208 M&#92;) y &#92;(m, n \u2208 \u2115&#92;), entonces<br \/>\n&#92;[ x^{m + n} = x^m  x^n &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (x : M)\nvariable (m n : \u2115)\n\nexample :\n  x^(m + n) = x^m * x^n :=\nby sorry\n<\/pre>\n<h4>1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por inducci\u00f3n en &#92;(m&#92;).<\/p>\n<p><strong>Base<\/strong>:<br \/>\n&#92;begin{align}<br \/>\n   x^{0 + n} &amp;= x^n        &#92;&#92;<br \/>\n             &amp;= 1 \u00b7 x^n    &#92;&#92;<br \/>\n             &amp;= x^0 \u00b7 x^n  &amp;&amp;&#92;text{[por pow_zero]}<br \/>\n&#92;end{align}<\/p>\n<p><strong>Paso<\/strong>: Supongamos que<br \/>\n&#92;[ x^{m + n} = x^m x^n &#92;tag{HI} &#92;]<br \/>\nEntonces<br \/>\n&#92;begin{align}<br \/>\n   x^{(m+1) + n} &amp;= x^{(m + n) + 1}  &#92;&#92;<br \/>\n                 &amp;= x \u00b7 x^{m + n}    &amp;&amp;&#92;text{[por pow_succ]} &#92;&#92;<br \/>\n                 &amp;= x \u00b7 (x^m \u00b7 x^n)  &amp;&amp;&#92;text{[por HI]} &#92;&#92;<br \/>\n                 &amp;= (x \u00b7 x^m) \u00b7 x^n  &#92;&#92;<br \/>\n                 &amp;= x^{m+1} \u00b7 x^n    &amp;&amp;&#92;text{[por pow_succ]}<br \/>\n&#92;end{align}<\/p>\n<h4>2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (x : M)\nvariable (m n : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  x^(m + n) = x^m * x^n :=\nby\n  induction' m with m HI\n  . calc x^(0 + n)\n       = x^n               := congrArg (x ^ .) (Nat.zero_add n)\n     _ = 1 * x^n           := (Monoid.one_mul (x^n)).symm\n     _ = x^0 * x^n         := congrArg (. * (x^n)) (pow_zero x).symm\n  . calc x^(succ m + n)\n       = x^succ (m + n)    := congrArg (x ^.) (succ_add m n)\n     _ = x * x^(m + n)     := pow_succ x (m + n)\n     _ = x * (x^m * x^n)   := congrArg (x * .) HI\n     _ = (x * x^m) * x^n   := (mul_assoc x (x^m) (x^n)).symm\n     _ = x^succ m * x^n    := congrArg (. * x^n) (pow_succ x m).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  x^(m + n) = x^m * x^n :=\nby\n  induction' m with m HI\n  . calc x^(0 + n)\n       = x^n             := by simp only [Nat.zero_add]\n     _ = 1 * x^n         := by simp only [Monoid.one_mul]\n     _ = x^0 * x^n       := by simp only [_root_.pow_zero]\n  . calc x^(succ m + n)\n       = x^succ (m + n)  := by simp only [succ_add]\n     _ = x * x^(m + n)   := by simp only [_root_.pow_succ]\n     _ = x * (x^m * x^n) := by simp only [HI]\n     _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm\n     _ = x^succ m * x^n  := by simp only [_root_.pow_succ]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  x^(m + n) = x^m * x^n :=\nby\n  induction' m with m HI\n  . calc x^(0 + n)\n       = x^n             := by simp [Nat.zero_add]\n     _ = 1 * x^n         := by simp\n     _ = x^0 * x^n       := by simp\n  . calc x^(succ m + n)\n       = x^succ (m + n)  := by simp [succ_add]\n     _ = x * x^(m + n)   := by simp [_root_.pow_succ]\n     _ = x * (x^m * x^n) := by simp [HI]\n     _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm\n     _ = x^succ m * x^n  := by simp [_root_.pow_succ]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n  x^(m + n) = x^m * x^n :=\npow_add x m n\n\n-- Lemas usados\n-- ============\n\n-- variable (y z : M)\n-- #check (Monoid.one_mul x : 1 * x = x)\n-- #check (Nat.zero_add n : 0 + n = n)\n-- #check (mul_assoc x y z : (x * y) * z = x * (y * z))\n-- #check (pow_add x m n : x^(m + n) = x^m * x^n)\n-- #check (pow_succ x n : x ^ succ n = x * x ^ n)\n-- #check (pow_zero x : x ^ 0 = 1)\n-- #check (succ_add n m : succ n + m = succ (n + m))\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\/Producto_de_potencias_de_la_misma_base_en_monoides.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Producto_de_potencias_de_la_misma_base_en_monoides\nimports Main\nbegin\n\ncontext monoid_mult\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"x ^ (m + n) = x ^ m * x ^ n\"\nproof (induct m)\n  have \"x ^ (0 + n) = x ^ n\"                by (simp only: add_0)\n  also have \"\u2026 = 1 * x ^ n\"                 by (simp only: mult_1_left)\n  also have \"\u2026 = x ^ 0 * x ^ n\"             by (simp only: power_0)\n  finally show \"x ^ (0 + n) = x ^ 0 * x ^ n\"\n    by this\nnext\n  fix m\n  assume HI : \"x ^ (m + n) = x ^ m * x ^ n\"\n  have \"x ^ (Suc m + n) = x ^ Suc (m + n)\"   by (simp only: add_Suc)\n  also have \"\u2026 = x *  x ^ (m + n)\"           by (simp only: power_Suc)\n  also have \"\u2026 = x *  (x ^ m * x ^ n)\"       by (simp only: HI)\n  also have \"\u2026 = (x *  x ^ m) * x ^ n\"       by (simp only: mult_assoc)\n  also have \"\u2026 = x ^ Suc m * x ^ n\"          by (simp only: power_Suc)\n  finally show \"x ^ (Suc m + n) = x ^ Suc m * x ^ n\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"x ^ (m + n) = x ^ m * x ^ n\"\nproof (induct m)\n  have \"x ^ (0 + n) = x ^ n\"                 by simp\n  also have \"\u2026 = 1 * x ^ n\"                  by simp\n  also have \"\u2026 = x ^ 0 * x ^ n\"              by simp\n  finally show \"x ^ (0 + n) = x ^ 0 * x ^ n\"\n    by this\nnext\n  fix m\n  assume HI : \"x ^ (m + n) = x ^ m * x ^ n\"\n  have \"x ^ (Suc m + n) = x ^ Suc (m + n)\"   by simp\n  also have \"\u2026 = x *  x ^ (m + n)\"           by simp\n  also have \"\u2026 = x *  (x ^ m * x ^ n)\"       using HI by simp\n  also have \"\u2026 = (x *  x ^ m) * x ^ n\"       by (simp add: mult_assoc)\n  also have \"\u2026 = x ^ Suc m * x ^ n\"          by simp\n  finally show \"x ^ (Suc m + n) = x ^ Suc m * x ^ n\"\n    by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"x ^ (m + n) = x ^ m * x ^ n\"\nproof (induct m)\n  case 0\n  then show ?case\n    by simp\nnext\n  case (Suc m)\n  then show ?case\n    by (simp add: algebra_simps)\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"x ^ (m + n) = x ^ m * x ^ n\"\n  by (induct m) (simp_all add: algebra_simps)\n\n(* 5\u00aa demostraci\u00f3n *)\n\nlemma \"x ^ (m + n) = x ^ m * x ^ n\"\n  by (simp only: power_add)\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Equivalencia de inversos iguales al neutro<\/h3>\n<p>Sea &#92;(M&#92;) un monoide y &#92;(a, b \u2208 M&#92;) tales que &#92;(ab = 1&#92;). Demostrar con Lean4 que &#92;(a = 1&#92;) si y s\u00f3lo si &#92;(b = 1&#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 {M : Type} [Monoid M]\nvariable {a b : M}\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\nby sorry\n<\/pre>\n<h4>1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Demostraremos las dos implicaciones.<\/p>\n<p>(\u27f9) Supongamos que &#92;(a = 1&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   b &amp;= 1\u00b7b    &amp;&amp;&#92;text{[por neutro por la izquierda]} &#92;&#92;<br \/>\n     &amp;= a\u00b7b    &amp;&amp;&#92;text{[por supuesto]} &#92;&#92;<br \/>\n     &amp;= 1      &amp;&amp;&#92;text{[por hip\u00f3tesis]}<br \/>\n&#92;end{align}<\/p>\n<p>(\u27f8) Supongamos que &#92;(b = 1&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   a &amp;= a\u00b71    &amp;&amp;&#92;text{[por neutro por la derecha]} &#92;&#92;<br \/>\n     &amp;= a\u00b7b    &amp;&amp;&#92;text{[por supuesto]} &#92;&#92;<br \/>\n     &amp;= 1      &amp;&amp;&#92;text{[por hip\u00f3tesis]}<br \/>\n&#92;end{align}<\/p>\n<h4>2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\nvariable {a b : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\nby\n  constructor\n  . -- \u22a2 a = 1 \u2192 b = 1\n    intro a1\n    -- a1 : a = 1\n    -- \u22a2 b = 1\n    calc b = 1 * b := (one_mul b).symm\n         _ = a * b := congrArg (. * b) a1.symm\n         _ = 1     := h\n  . -- \u22a2 b = 1 \u2192 a = 1\n    intro b1\n    -- b1 : b = 1\n    -- \u22a2 a = 1\n    calc a = a * 1 := (mul_one a).symm\n         _ = a * b := congrArg (a * .) b1.symm\n         _ = 1     := h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\nby\n  constructor\n  . -- \u22a2 a = 1 \u2192 b = 1\n    intro a1\n    -- a1 : a = 1\n    -- \u22a2 b = 1\n    rw [a1] at h\n    -- h : 1 * b = 1\n    rw [one_mul] at h\n    -- h : b = 1\n    exact h\n  . -- \u22a2 b = 1 \u2192 a = 1\n    intro b1\n    -- b1 : b = 1\n    -- \u22a2 a = 1\n    rw [b1] at h\n    -- h : a * 1 = 1\n    rw [mul_one] at h\n    -- h : a = 1\n    exact h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\nby\n  constructor\n  . -- \u22a2 a = 1 \u2192 b = 1\n    rintro rfl\n    -- h : 1 * b = 1\n    simpa using h\n  . -- \u22a2 b = 1 \u2192 a = 1\n    rintro rfl\n    -- h : a * 1 = 1\n    simpa using h\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\nby constructor <;> (rintro rfl; simpa using h)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : a * b = 1)\n  : a = 1 \u2194 b = 1 :=\neq_one_iff_eq_one_of_mul_eq_one h\n\n-- Lemas usados\n-- ============\n\n-- #check (eq_one_iff_eq_one_of_mul_eq_one : a * b = 1 \u2192 (a = 1 \u2194 b = 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\/Equivalencia_de_inversos_iguales_al_neutro.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Equivalencia_de_inversos_iguales_al_neutro\nimports Main\nbegin\n\ncontext monoid\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows   \"a = 1 \u27f7 b = 1\"\nproof (rule iffI)\n  assume \"a = 1\"\n  have \"b = 1 * b\"      by (simp only: left_neutral)\n  also have \"\u2026 = a * b\" by (simp only: \u2039a = 1\u203a)\n  also have \"\u2026 = 1\"     by (simp only: \u2039a * b = 1\u203a)\n  finally show \"b = 1\"  by this\nnext\n  assume \"b = 1\"\n  have \"a = a * 1\"      by (simp only: right_neutral)\n  also have \"\u2026 = a * b\" by (simp only: \u2039b = 1\u203a)\n  also have \"\u2026 = 1\"     by (simp only: \u2039a * b = 1\u203a)\n  finally show \"a = 1\"  by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows   \"a = 1 \u27f7 b = 1\"\nproof\n  assume \"a = 1\"\n  have \"b = 1 * b\"      by simp\n  also have \"\u2026 = a * b\" using \u2039a = 1\u203a by simp\n  also have \"\u2026 = 1\"     using \u2039a * b = 1\u203a by simp\n  finally show \"b = 1\"  .\nnext\n  assume \"b = 1\"\n  have \"a = a * 1\"      by simp\n  also have \"\u2026 = a * b\" using \u2039b = 1\u203a by simp\n  also have \"\u2026 = 1\"     using \u2039a * b = 1\u203a by simp\n  finally show \"a = 1\"  .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"a * b = 1\"\n  shows   \"a = 1 \u27f7 b = 1\"\n  by (metis assms left_neutral right_neutral)\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Unicidad de inversos en monoides<\/h3>\n<p>Demostrar con Lean4 que si &#92;(M&#92;) es un monoide conmutativo y &#92;(x, y, z \u2208 M&#92;) tales que &#92;(x\u00b7y = 1&#92;) y &#92;(x\u00b7z = 1&#92;), entonces &#92;(y = z&#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 {M : Type} [CommMonoid M]\nvariable {x y z : M}\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\nby sorry\n<\/pre>\n<h4>1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   y &amp;= 1\u00b7y          &amp;&amp;&#92;text{[por neutro a la izquierda]} &#92;&#92;<br \/>\n     &amp;= (x\u00b7z)\u00b7y      &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= (z\u00b7x)\u00b7y      &amp;&amp;&#92;text{[por la conmutativa]} &#92;&#92;<br \/>\n     &amp;= z\u00b7(x\u00b7y)      &amp;&amp;&#92;text{[por la asociativa]} &#92;&#92;<br \/>\n     &amp;= z\u00b71          &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= z            &amp;&amp;&#92;text{[por neutro a la derecha]}<br \/>\n&#92;end{align}<\/p>\n<h4>2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [CommMonoid M]\nvariable {x y z : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\ncalc y = 1 * y       := (one_mul y).symm\n     _ = (x * z) * y := congrArg (. * y) hz.symm\n     _ = (z * x) * y := congrArg (. * y) (mul_comm x z)\n     _ = z * (x * y) := mul_assoc z x y\n     _ = z * 1       := congrArg (z * .) hy\n     _ = z           := mul_one z\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\ncalc y = 1 * y     := by simp only [one_mul]\n   _ = (x * z) * y := by simp only [hz]\n   _ = (z * x) * y := by simp only [mul_comm]\n   _ = z * (x * y) := by simp only [mul_assoc]\n   _ = z * 1       := by simp only [hy]\n   _ = z           := by simp only [mul_one]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\ncalc y = 1 * y     := by simp\n   _ = (x * z) * y := by simp [hz]\n   _ = (z * x) * y := by simp [mul_comm]\n   _ = z * (x * y) := by simp [mul_assoc]\n   _ = z * 1       := by simp [hy]\n   _ = z           := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\nby\n  apply left_inv_eq_right_inv _ hz\n  -- \u22a2 y * x = 1\n  rw [mul_comm]\n  -- \u22a2 x * y = 1\n  exact hy\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hy : x * y = 1)\n  (hz : x * z = 1)\n  : y = z :=\ninv_unique hy hz\n\n-- Lemas usados\n-- ============\n\n-- #check (inv_unique : x * y = 1 \u2192 x * z = 1 \u2192 y = z)\n-- #check (left_inv_eq_right_inv : y * x = 1 \u2192 x * z = 1 \u2192 y = z)\n-- #check (mul_assoc x y z : (x * y) * z = x * (y * z))\n-- #check (mul_comm x y : x * y = y * x)\n-- #check (mul_one x : x * 1 = x)\n-- #check (one_mul x : 1 * x = x)\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_inversos_en_monoides.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Unicidad_de_inversos_en_monoides\nimports Main\nbegin\n\ncontext comm_monoid\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"x * y = 1\"\n          \"x * z = 1\"\n  shows \"y = z\"\nproof -\n  have \"y = 1 * y\"            by (simp only: left_neutral)\n  also have \"\u2026 = (x * z) * y\" by (simp only: \u2039x * z = 1\u203a)\n  also have \"\u2026 = (z * x) * y\" by (simp only: commute)\n  also have \"\u2026 = z * (x * y)\" by (simp only: assoc)\n  also have \"\u2026 = z * 1\"       by (simp only: \u2039x * y = 1\u203a)\n  also have \"\u2026 = z\"           by (simp only: right_neutral)\n  finally show \"y = z\"        by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"x * y = 1\"\n          \"x * z = 1\"\n  shows \"y = z\"\nproof -\n  have \"y = 1 * y\"            by simp\n  also have \"\u2026 = (x * z) * y\" using assms(2) by simp\n  also have \"\u2026 = (z * x) * y\" by simp\n  also have \"\u2026 = z * (x * y)\" by simp\n  also have \"\u2026 = z * 1\"       using assms(1) by simp\n  also have \"\u2026 = z\"           by simp\n  finally show \"y = z\"        by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"x * y = 1\"\n          \"x * z = 1\"\n  shows \"y = z\"\n  using assms\n  by auto\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Caracterizaci\u00f3n de producto igual al primer factor<\/h3>\n<p>Un monoide cancelativo por la izquierda es un monoide &#92;(M&#92;) que cumple la propiedad cancelativa por la izquierda; es decir, para todo &#92;(a, b \u2208 M&#92;)<br \/>\n&#92;[ a\u00b7b = a\u00b7c \u2194 b = c &#92;]<\/p>\n<p>En Lean4 la clase de los monoides cancelativos por la izquierda es <code>LeftCancelMonoid<\/code> y la propiedad cancelativa por la izquierda es<\/p>\n<pre lang=\"lean\">\n   mul_left_cancel : a * b = a * c \u2192 b = c\n<\/pre>\n<p>Demostrar con Lean4 que si &#92;(M&#92;) es un monoide cancelativo por la izquierda y &#92;(a, b \u2208 M&#92;), entonces<br \/>\n&#92;[ a\u00b7b = a \u2194 b = 1 &#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 {M : Type} [LeftCancelMonoid M]\nvariable {a b : M}\n\nexample : a * b = a \u2194 b = 1 :=\nby sorry\n<\/pre>\n<h4>1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Demostraremos las dos implicaciones.<\/p>\n<p>(\u27f9) Supongamos que<br \/>\n&#92;[ a\u00b7b = a  &#92;]<br \/>\nPor la propiedad del neutro por la derecha tenemos<br \/>\n&#92;[ a\u00b71 = a &#92;]<br \/>\nPor tanto,<br \/>\n&#92;[ a\u00b7b = a\u00b71 &#92;]<br \/>\ny, por la propiedad cancelativa,<br \/>\n&#92;[ b = 1 &#92;]<\/p>\n<p>(\u27f8) Supongamos que &#92;(b = 1&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   a\u00b7b &amp;= a\u00b71    &#92;&#92;<br \/>\n       &amp;= a      &amp;&amp;&#92;text{[por el neutro por la derecha]}<br \/>\n&#92;end{align}<\/p>\n<h4>2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [LeftCancelMonoid M]\nvariable {a b : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * b = a \u2194 b = 1 :=\nby\n  constructor\n  . -- \u22a2 a * b = a \u2192 b = 1\n    intro h\n    -- h : a * b = a\n    -- \u22a2 b = 1\n    have h1 : a * b = a * 1 := by\n      calc a * b = a     := by exact h\n               _ = a * 1 := (mul_one a).symm\n    exact mul_left_cancel h1\n  . -- \u22a2 b = 1 \u2192 a * b = a\n    intro h\n    -- h : b = 1\n    -- \u22a2 a * b = a\n    rw [h]\n    -- \u22a2 a * 1 = a\n    exact mul_one a\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * b = a \u2194 b = 1 :=\ncalc a * b = a\n     \u2194 a * b = a * 1 := by rw [mul_one]\n   _ \u2194 b = 1         := mul_left_cancel_iff\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * b = a \u2194 b = 1 :=\nmul_right_eq_self\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * b = a \u2194 b = 1 :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- variable (c : M)\n-- #check (mul_left_cancel : a * b = a * c \u2192 b = c)\n-- #check (mul_one a : a * 1 = a)\n-- #check (mul_right_eq_self : a * b = a \u2194 b = 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\/Caracterizacion_de_producto_igual_al_primer_factor.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Caracterizacion_de_producto_igual_al_primer_factor\nimports Main\nbegin\n\ncontext cancel_comm_monoid_add\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\nproof (rule iffI)\n  assume \"a + b = a\"\n  then have \"a + b = a + 0\"     by (simp only: add_0_right)\n  then show \"b = 0\"             by (simp only: add_left_cancel)\nnext\n  assume \"b = 0\"\n  have \"a + 0 = a\"              by (simp only: add_0_right)\n  with \u2039b = 0\u203a show \"a + b = a\" by (rule ssubst)\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\nproof\n  assume \"a + b = a\"\n  then have \"a + b = a + 0\" by simp\n  then show \"b = 0\"         by simp\nnext\n  assume \"b = 0\"\n  have \"a + 0 = a\"          by simp\n  then show \"a + b = a\"     using \u2039b = 0\u203a by simp\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\nproof -\n  have \"(a + b = a) \u27f7 (a + b = a + 0)\" by (simp only: add_0_right)\n  also have \"\u2026 \u27f7 (b = 0)\"              by (simp only: add_left_cancel)\n  finally show \"a + b = a \u27f7 b = 0\"     by this\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\nproof -\n  have \"(a + b = a) \u27f7 (a + b = a + 0)\" by simp\n  also have \"\u2026 \u27f7 (b = 0)\"              by simp\n  finally show \"a + b = a \u27f7 b = 0\"     .\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\n  by (simp only: add_cancel_left_right)\n\n(* 6\u00aa demostraci\u00f3n *)\n\nlemma \"a + b = a \u27f7 b = 0\"\n  by auto\n\nend\n\nend\n<\/pre>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Unicidad del elemento neutro en los grupos<\/h3>\n<p>Demostrar con Lean4 que un grupo s\u00f3lo posee un elemento neutro.<\/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]\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nsorry\n<\/pre>\n<h4>1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sea &#92;(e \u2208 G&#92;) tal que<br \/>\n&#92;[ (\u2200 x)[x\u00b7e = x] &#92;tag{1} &#92;]<br \/>\nEntonces,<br \/>\n&#92;begin{align}<br \/>\n   e &amp;= 1.e    &amp;&amp;&#92;text{[porque 1 es neutro]} &#92;&#92;<br \/>\n     &amp;= 1      &amp;&amp;&#92;text{[por (1)]}<br \/>\n&#92;end{align}<\/p>\n<h4>2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\ncalc e = 1 * e := (one_mul e).symm\n     _ = 1     := h 1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nby\n  have h1 : e = e * e := (h e).symm\n  exact self_eq_mul_left.mp h1\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nself_eq_mul_left.mp (h e).symm\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : G)\n-- #check (one_mul a : 1 * a = a)\n-- #check (self_eq_mul_left : b = a * b \u2194 a = 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\/Unicidad_del_elemento_neutro_en_los_grupos.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Unicidad_del_elemento_neutro_en_los_grupos\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\nproof -\n  have \"e = 1 * e\"     by (simp only: left_neutral)\n  also have \"\u2026 = 1\"    using assms by (rule allE)\n  finally show \"e = 1\" by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\nproof -\n  have \"e = 1 * e\"     by simp\n  also have \"\u2026 = 1\"    using assms by simp\n  finally show \"e = 1\" .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\n  using assms\n  by (metis left_neutral)\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. Producto de potencias de la misma base en monoides 2. Equivalencia de inversos iguales al neutro 3. Unicidad de inversos en monoides 4. Caracterizaci\u00f3n de producto igual al primer factor 5. Unicidad del elemento neutro en los grupos A continuaci\u00f3n&#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\/8190"}],"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=8190"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8190\/revisions"}],"predecessor-version":[{"id":8191,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8190\/revisions\/8191"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8190"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8190"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8190"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}