{"id":2449,"date":"2024-05-06T06:00:49","date_gmt":"2024-05-06T04:00:49","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2449"},"modified":"2024-05-05T20:30:30","modified_gmt":"2024-05-05T18:30:30","slug":"06-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/06-may-24\/","title":{"rendered":"Producto de potencias de la misma base en monoides"},"content":{"rendered":"\n

En los monoides<\/a> se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los siguientes lemas:<\/p>\n

\n   pow_zero : x^0 = 1\n   pow_succ : x^(succ n) = x * x^n\n<\/pre>\n
Demostrar con Lean4 que si \(M\) es un monoide, \(x \u2208 M\) y \(m, n \u2208 \u2115\), entonces
\n\[ x^{m + n} = x^m  x^n \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\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
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por inducci\u00f3n en \(m\).<\/p>\n
Base<\/strong>:
\n\begin{align}
\n   x^{0 + n} &= x^n        \\
\n             &= 1 \u00b7 x^n    \\
\n             &= x^0 \u00b7 x^n  &&\text{[por pow_zero]}
\n\end{align}<\/p>\n
Paso<\/strong>: Supongamos que
\n\[ x^{m + n} = x^m x^n \tag{HI} \]
\nEntonces
\n\begin{align}
\n   x^{(m+1) + n} &= x^{(m + n) + 1}  \\
\n                 &= x \u00b7 x^{m + n}    &&\text{[por pow_succ]} \\
\n                 &= x \u00b7 (x^m \u00b7 x^n)  &&\text{[por HI]} \\
\n                 &= (x \u00b7 x^m) \u00b7 x^n  \\
\n                 &= x^{m+1} \u00b7 x^n    &&\text{[por pow_succ]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\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
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\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","protected":false},"excerpt":{"rendered":"
En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los siguientes lemas: pow_zero : x^0 = 1 pow_succ : x^(succ n) = x * x^n Demostrar con Lean4 que si \(M\) es un monoide, \(x \u2208 M\) y \(m, n \u2208 \u2115\), entonces \[ x^{m + n} = x^m x^n \] Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Algebra.Group.Defs import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (x : M) variable (m n : \u2115) example : x^(m + n) = x^m * x^n := by sorry<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[1],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2449"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=2449"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2449\/revisions"}],"predecessor-version":[{"id":2452,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2449\/revisions\/2452"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2449"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2449"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2449"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}