Demostrar con Lean4 que un n\u00famero es par si y solo si lo es su cuadrado.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Int.Parity\nimport Mathlib.Tactic\nopen Int\n\nvariable (n : \u2124)\n\nexample :\n Even (n^2) \u2194 Even n :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(n \u2208 \u2124\). Tenemos que demostrar que \(n^2\) es par si y solo si n es par. Lo haremos probando las dos implicaciones.<\/p>\n
(\u27f9) Lo demostraremos por contraposici\u00f3n. Para ello, supongamos que \(n\) no es par. Entonces, existe un \(k \u2208 Z\) tal que
\n\[ n = 2k+1 \tag{1} \]
\nLuego,
\n\begin{align}
\n n^2 &= (2k+1)^2 &&\text{[por (1)]} \\
\n &= 4k^2+4k+1 \\
\n &= 2(2k(k+1))+1
\n\end{align}
\nPor tanto, \(n^2\) es impar.<\/p>\n
(\u27f8) Supongamos que \(n\) es par. Entonces, existe un \(k \u2208 \u2124\) tal que
\n\[ n = 2k \tag{2} \]
\nLuego,
\n\begin{align}
\n n^2 &= (2k)^2 &&\text{[por (2)]} \\
\n &= 2(2k^2)
\n\end{align}
\nPor tanto, \(n^2\) es par.<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Int.Parity\nimport Mathlib.Tactic\nopen Int\n\nvariable (n : \u2124)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n Even (n^2) \u2194 Even n :=\nby\n constructor\n . -- \u22a2 Even (n ^ 2) \u2192 Even n\n contrapose\n -- \u22a2 \u00acEven n \u2192 \u00acEven (n ^ 2)\n intro h\n -- h : \u00acEven n\n -- \u22a2 \u00acEven (n ^ 2)\n rw [\u2190odd_iff_not_even] at *\n -- h : Odd n\n -- \u22a2 Odd (n ^ 2)\n cases' h with k hk\n -- k : \u2124\n -- hk : n = 2 * k + 1\n use 2*k*(k+1)\n -- \u22a2 n ^ 2 = 2 * (2 * k * (k + 1)) + 1\n calc n^2\n = (2*k+1)^2 := by rw [hk]\n _ = 4*k^2+4*k+1 := by ring\n _ = 2*(2*k*(k+1))+1 := by ring\n . -- \u22a2 Even n \u2192 Even (n ^ 2)\n intro h\n -- h : Even n\n -- \u22a2 Even (n ^ 2)\n cases' h with k hk\n -- k : \u2124\n -- hk : n = k + k\n use 2*k^2\n -- \u22a2 n ^ 2 = 2 * k ^ 2 + 2 * k ^ 2\n calc n^2\n = (k + k)^2 := by rw [hk]\n _ = 2*k^2 + 2*k^2 := by ring\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n Even (n^2) \u2194 Even n :=\nby\n constructor\n . -- \u22a2 Even (n ^ 2) \u2192 Even n\n contrapose\n -- \u22a2 \u00acEven n \u2192 \u00acEven (n ^ 2)\n rw [\u2190odd_iff_not_even]\n -- \u22a2 Odd n \u2192 \u00acEven (n ^ 2)\n rw [\u2190odd_iff_not_even]\n -- \u22a2 Odd n \u2192 Odd (n ^ 2)\n unfold Odd\n -- \u22a2 (\u2203 k, n = 2 * k + 1) \u2192 \u2203 k, n ^ 2 = 2 * k + 1\n intro h\n -- h : \u2203 k, n = 2 * k + 1\n -- \u22a2 \u2203 k, n ^ 2 = 2 * k + 1\n cases' h with k hk\n -- k : \u2124\n -- hk : n = 2 * k + 1\n use 2*k*(k+1)\n -- \u22a2 n ^ 2 = 2 * (2 * k * (k + 1)) + 1\n rw [hk]\n -- \u22a2 (2 * k + 1) ^ 2 = 2 * (2 * k * (k + 1)) + 1\n ring\n . -- \u22a2 Even n \u2192 Even (n ^ 2)\n unfold Even\n -- \u22a2 (\u2203 r, n = r + r) \u2192 \u2203 r, n ^ 2 = r + r\n intro h\n -- h : \u2203 r, n = r + r\n -- \u22a2 \u2203 r, n ^ 2 = r + r\n cases' h with k hk\n -- k : \u2124\n -- hk : n = k + k\n use 2*k^2\n -- \u22a2 n ^ 2 = 2 * k ^ 2 + 2 * k ^ 2\n rw [hk]\n -- \u22a2 (k + k) ^ 2 = 2 * k ^ 2 + 2 * k ^ 2\n ring\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n Even (n^2) \u2194 Even n :=\nby\n constructor\n . -- \u22a2 Even (n ^ 2) \u2192 Even n\n contrapose\n -- \u22a2 \u00acEven n \u2192 \u00acEven (n ^ 2)\n rw [\u2190odd_iff_not_even]\n -- \u22a2 Odd n \u2192 \u00acEven (n ^ 2)\n rw [\u2190odd_iff_not_even]\n -- \u22a2 Odd n \u2192 Odd (n ^ 2)\n rintro \u27e8k, rfl\u27e9\n -- k : \u2124\n -- \u22a2 Odd ((2 * k + 1) ^ 2)\n use 2*k*(k+1)\n -- \u22a2 (2 * k + 1) ^ 2 = 2 * (2 * k * (k + 1)) + 1\n ring\n . -- \u22a2 Even n \u2192 Even (n ^ 2)\n rintro \u27e8k, rfl\u27e9\n -- k : \u2124\n -- \u22a2 Even ((k + k) ^ 2)\n use 2*k^2\n -- \u22a2 (k + k) ^ 2 = 2 * k ^ 2 + 2 * k ^ 2\n ring\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n Even (n^2) \u2194 Even n :=\ncalc Even (n^2)\n \u2194 Even (n * n) := iff_of_eq (congrArg Even (sq n))\n _ \u2194 (Even n \u2228 Even n) := even_mul\n _ \u2194 Even n := or_self_iff (Even n)\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n Even (n^2) \u2194 Even n :=\ncalc Even (n^2)\n \u2194 Even (n * n) := by ring_nf\n _ \u2194 (Even n \u2228 Even n) := even_mul\n _ \u2194 Even n := by simp\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : Prop)\n-- variable (m : \u2124)\n-- #check (even_mul : Even (m * n) \u2194 Even m \u2228 Even n)\n-- #check (iff_of_eq : a = b \u2192 (a \u2194 b))\n-- #check (odd_iff_not_even : Odd n \u2194 \u00acEven n)\n-- #check (or_self_iff a : a \u2228 a \u2194 a)\n<\/pre>\n