Demostrar con Lean4 la transitividad de la divisibilidad.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\n\nvariable {a b c : \u2115}\n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSupongamos que \(a | b\) y \(b | c\). Entonces, existen \(d\) y \(e\) tales que
\n\begin{align}
\n b &= ad \tag{1} \\
\n c &= be \tag{2}
\n\end{align}
\nPor tanto,
\n\begin{align}
\n c &= be &&\text{[por (2)]} \\
\n &= (ad)e &&\text{[por (1)]} \\
\n &= a(de)
\n\end{align}
\nPor consiguiente, \(a | c\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\n\nvariable {a b c : \u2115}\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby\n rcases divab with \u27e8d, beq : b = a * d\u27e9\n rcases divbc with \u27e8e, ceq : c = b * e\u27e9\n have h1 : c = a * (d * e) :=\n calc c = b * e := ceq\n _ = (a * d) * e := congrArg (. * e) beq\n _ = a * (d * e) := mul_assoc a d e\n show a \u2223 c\n exact Dvd.intro (d * e) h1.symm\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby\n rcases divab with \u27e8d, beq : b = a * d\u27e9\n rcases divbc with \u27e8e, ceq : c = b * e\u27e9\n use (d * e)\n -- \u22a2 c = a * (d * e)\n rw [ceq, beq]\n -- \u22a2 (a * d) * e = a * (d * e)\n exact mul_assoc a d e\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby\n rcases divbc with \u27e8e, rfl\u27e9\n -- \u22a2 a \u2223 b * e\n rcases divab with \u27e8d, rfl\u27e9\n -- \u22a2 a \u2223 a * d * e\n use (d * e)\n -- \u22a2 a * d * e = a * (d * e)\n ring\n\n-- 4\u00aa demostraci\u00f3n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby\n cases' divab with d beq\n -- d : \u2115\n -- beq : b = a * d\n cases' divbc with e ceq\n -- e : \u2115\n -- ceq : c = b * e\n rw [ceq, beq]\n -- \u22a2 a \u2223 a * d * e\n use (d * e)\n -- \u22a2 (a * d) * e = a * (d * e)\n exact mul_assoc a d e\n\n-- 5\u00aa demostraci\u00f3n\nexample\n (divab : a \u2223 b)\n (divbc : b \u2223 c) :\n a \u2223 c :=\nby exact dvd_trans divab divbc\n\n-- Lemas usados\n-- ============\n\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (Dvd.intro c : a * c = b \u2192 a \u2223 b)\n-- #check (dvd_trans : a \u2223 b \u2192 b \u2223 c \u2192 a \u2223 c)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n