{"id":2485,"date":"2024-05-20T06:00:11","date_gmt":"2024-05-20T04:00:11","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2485"},"modified":"2024-05-16T19:21:46","modified_gmt":"2024-05-16T17:21:46","slug":"20-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/20-may-24\/","title":{"rendered":"Los monoides booleanos son conmutativos"},"content":{"rendered":"\n

Un monoide es un conjunto junto con una operaci\u00f3n binaria que es asociativa y tiene elemento neutro.<\/p>\n

Un monoide \(M\) es booleano si
\n\[ (\u2200 x \u2208 M)[x\u00b7x = 1] \]
\ny es conmutativo si
\n\[ (\u2200 x, y \u2208 M)[x\u00b7y = y\u00b7x] \]<\/p>\n

En Lean4, est\u00e1 definida la clase de los monoides (como Monoid<\/code>) y sus propiedades caracter\u00edsticas son<\/p>\n

\n   mul_assoc : (a * b) * c = a * (b * c)\n   one_mul :   1 * a = a\n   mul_one :   a * 1 = a\n<\/pre>\n
Demostrar con Lean4 que los monoides booleanos son conmutativos.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby sorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sean \(a, b \u2208 M\). Se verifica la siguiente cadena de igualdades
\n\begin{align}
\n   a\u00b7b &= (a\u00b7b)\u00b71               &&\text{[por mul_one]} \\
\n       &= (a\u00b7b)\u00b7(a\u00b7a)           &&\text{[por hip\u00f3tesis, \(a\u00b7a = 1\)]} \\
\n       &= ((a\u00b7b)\u00b7a)\u00b7a           &&\text{[por mul_assoc]} \\
\n       &= (a\u00b7(b\u00b7a))\u00b7a           &&\text{[por mul_assoc]} \\
\n       &= (1\u00b7(a\u00b7(b\u00b7a)))\u00b7a       &&\text{[por one_mul]} \\
\n       &= ((b\u00b7b)\u00b7(a\u00b7(b\u00b7a)))\u00b7a   &&\text{[por hip\u00f3tesis, \(b\u00b7b = 1\)]} \\
\n       &= (b\u00b7(b\u00b7(a\u00b7(b\u00b7a))))\u00b7a   &&\text{[por mul_assoc]} \\
\n       &= (b\u00b7((b\u00b7a)\u00b7(b\u00b7a)))\u00b7a   &&\text{[por mul_assoc]} \\
\n       &= (b\u00b71)\u00b7a               &&\text{[por hip\u00f3tesis, \((b\u00b7a)\u00b7(b\u00b7a) = 1\)]} \\
\n       &= b\u00b7a                   &&\text{[por mul_one]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {M : Type} [Monoid M]\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1\n         := (mul_one (a * b)).symm\n     _ = (a * b) * (a * a)\n         := congrArg ((a*b) * .) (h a).symm\n     _ = ((a * b) * a) * a\n         := (mul_assoc (a*b) a a).symm\n     _ = (a * (b * a)) * a\n         := congrArg (. * a) (mul_assoc a b a)\n     _ = (1 * (a * (b * a))) * a\n         := congrArg (. * a) (one_mul (a*(b*a))).symm\n     _ = ((b * b) * (a * (b * a))) * a\n         := congrArg (. * a) (congrArg (. * (a*(b*a))) (h b).symm)\n     _ = (b * (b * (a * (b * a)))) * a\n         := congrArg (. * a) (mul_assoc b b (a*(b*a)))\n     _ = (b * ((b * a) * (b * a))) * a\n         := congrArg (. * a) (congrArg (b * .) (mul_assoc b a (b*a)).symm)\n     _ = (b * 1) * a\n         := congrArg (. * a) (congrArg (b * .) (h (b*a)))\n     _ = b * a\n         := congrArg (. * a) (mul_one b)\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp only [mul_one]\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = ((a * b) * a) * a             := by simp only [mul_assoc]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * (b * (a * (b * a)))) * a := by simp only [mul_assoc]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp only [mul_one]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp only [mul_one]\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp only [one_mul]\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp only [mul_one]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (h : \u2200 x : M, x * x = 1)\n  : \u2200 x y : M, x * y = y * x :=\nby\n  intros a b\n  calc a * b\n       = (a * b) * 1                   := by simp\n     _ = (a * b) * (a * a)             := by simp only [h a]\n     _ = (a * (b * a)) * a             := by simp only [mul_assoc]\n     _ = (1 * (a * (b * a))) * a       := by simp\n     _ = ((b * b) * (a * (b * a))) * a := by simp only [h b]\n     _ = (b * ((b * a) * (b * a))) * a := by simp only [mul_assoc]\n     _ = (b * 1) * a                   := by simp only [h (b*a)]\n     _ = b * a                         := by simp\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : M)\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
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Los_monoides_booleanos_son_conmutativos\nimports Main\nbegin\n\ncontext monoid\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * 1\"\n    by (simp only: right_neutral)\n  also have \"\u2026 = (a * b) * (a * a)\"\n    by (simp only: assms)\n  also have \"\u2026 = ((a * b) * a) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (a * (b * a)) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (1 * (a * (b * a))) * a\"\n    by (simp only: left_neutral)\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\"\n    by (simp only: assms)\n  also have \"\u2026 = (b * (b * (a * (b * a)))) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\"\n    by (simp only: assoc)\n  also have \"\u2026 = (b * 1) * a\"\n    by (simp only: assms)\n  also have \"\u2026 = b * a\"\n    by (simp only: right_neutral)\n  finally show \"a * b = b * a\"\n    by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * 1\"                    by simp\n  also have \"\u2026 = (a * b) * (a * a)\"             by (simp add: assms)\n  also have \"\u2026 = ((a * b) * a) * a\"             by (simp add: assoc)\n  also have \"\u2026 = (a * (b * a)) * a\"             by (simp add: assoc)\n  also have \"\u2026 = (1 * (a * (b * a))) * a\"       by simp\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\" by (simp add: assms)\n  also have \"\u2026 = (b * (b * (a * (b * a)))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * 1) * a\"                   by (simp add: assms)\n  also have \"\u2026 = b * a\"                         by simp\n  finally show \"a * b = b * a\"                  by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\nproof (rule allI)+\n  fix a b\n  have \"a * b = (a * b) * (a * a)\"              by (simp add: assms)\n  also have \"\u2026 = (a * (b * a)) * a\"             by (simp add: assoc)\n  also have \"\u2026 = ((b * b) * (a * (b * a))) * a\" by (simp add: assms)\n  also have \"\u2026 = (b * ((b * a) * (b * a))) * a\" by (simp add: assoc)\n  also have \"\u2026 = (b * 1) * a\"                   by (simp add: assms)\n  finally show \"a * b = b * a\"                  by simp\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * x = 1\"\n  shows   \"\u2200 x y. x * y = y * x\"\n  by (metis assms assoc right_neutral)\n\nend\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
Un monoide es un conjunto junto con una operaci\u00f3n binaria que es asociativa y tiene elemento neutro. Un monoide \(M\) es booleano si \[ (\u2200 x \u2208 M)[x\u00b7x = 1] \] y es conmutativo si \[ (\u2200 x, y \u2208 M)[x\u00b7y = y\u00b7x] \] En Lean4, est\u00e1 definida la clase de los monoides (como Monoid) y sus propiedades caracter\u00edsticas son mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a Demostrar con Lean4 que los monoides booleanos son conmutativos. Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] example (h : \u2200 x : M, x * x = 1) :…<\/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":[9],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2485"}],"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=2485"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2485\/revisions"}],"predecessor-version":[{"id":2489,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2485\/revisions\/2489"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2485"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2485"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2485"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}