{"id":1957,"date":"2024-01-22T06:00:46","date_gmt":"2024-01-22T04:00:46","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1957"},"modified":"2024-01-17T13:56:58","modified_gmt":"2024-01-17T11:56:58","slug":"22-ene-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/22-ene-24\/","title":{"rendered":"En \u211d, x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -y"},"content":{"rendered":"\n

Demostrar con Lean4 que en \\(\u211d\\),
\n\\[x\u00b2 = y\u00b2 \u2192 x = y \u2228 x = -y\\]<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\r\nimport Mathlib.Data.Real.Basic\r\nvariable (x y : \u211d)\r\n\r\nexample\r\n  (h : x^2 = y^2)\r\n  : x = y \u2228 x = -y :=\r\nby sorry\r\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Usaremos los siguientes lemas
\n\\begin{align}
\n   &(\u2200 x \u2208 \u211d)[x – x = 0]                                           \\tag{L1} \\\\
\n   &(\u2200 x, y \u2208 \u211d)[xy = 0 \u2192 x = 0 \u2228 y = 0]                           \\tag{L2} \\\\
\n   &(\u2200 x, y \u2208 \u211d)[x – y = 0 \u2194 x = y]                                \\tag{L3} \\\\
\n   &(\u2200 x, y \u2208 \u211d)[x + y = 0 \u2192 x = -y]                               \\tag{L4}
\n\\end{align}<\/p>\n
Se tiene que
\n\\begin{align}
\n   (x – y)(x + y) &= x\u00b2 – y\u00b2    \\\\
\n                  &= y\u00b2 – y\u00b2    &&\\text{[por la hip\u00f3tesis]} \\\\
\n                  &= 0          &&\\text{[por L1]}
\n\\end{align}
\ny, por el lema L2, se tiene que
\n\\[ x – y = 0 \u2228 x + y = 0 \\]<\/p>\n
Acabaremos la demostraci\u00f3n por casos.<\/p>\n
Primer caso:
\n\\begin{align}
\n  x – y = 0 &\u27f9 x = y             &&\\text{[por L3]} \\\\
\n            &\u27f9 x = y \u2228 x = -y
\n\\end{align}<\/p>\n
Segundo caso:
\n\\begin{align}
\n  x + y = 0 &\u27f9 x = -y            &&\\text{[por L4]} \\\\
\n            &\u27f9 x = y \u2228 x = -y
\n\\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\r\nimport Mathlib.Data.Real.Basic\r\nvariable (x y : \u211d)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : x^2 = y^2)\r\n  : x = y \u2228 x = -y :=\r\nby\r\n  have h1 : (x - y) * (x + y) = 0 := by\r\n    calc (x - y) * (x + y) = x^2 - y^2 := by ring\r\n                         _ = y^2 - y^2 := by rw [h]\r\n                         _ = 0         := sub_self (y ^ 2)\r\n  have h2 : x - y = 0 \u2228 x + y = 0 := by\r\n    apply eq_zero_or_eq_zero_of_mul_eq_zero h1\r\n  rcases h2 with h3 | h4\r\n  . -- h3 : x - y = 0\r\n    left\r\n    -- \u22a2 x = y\r\n    exact sub_eq_zero.mp h3\r\n  . -- h4 : x + y = 0\r\n    right\r\n    -- \u22a2 x = -y\r\n    exact eq_neg_of_add_eq_zero_left h4\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : x^2 = y^2)\r\n  : x = y \u2228 x = -y :=\r\nby\r\n  have h1 : (x - y) * (x + y) = 0 := by nlinarith\r\n  have h2 : x - y = 0 \u2228 x + y = 0 := by aesop\r\n  rcases h2 with h3 | h4\r\n  . -- h3 : x - y = 0\r\n    left\r\n    -- \u22a2 x = y\r\n    linarith\r\n  . -- h4 : x + y = 0\r\n    right\r\n    -- \u22a2 x = -y\r\n    linarith\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (h : x^2 = y^2)\r\n  : x = y \u2228 x = -y :=\r\nsq_eq_sq_iff_eq_or_eq_neg.mp h\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (eq_neg_of_add_eq_zero_left : x + y = 0 \u2192 x = -y)\r\n-- #check (eq_zero_or_eq_zero_of_mul_eq_zero : x * y = 0 \u2192 x = 0 \u2228 y = 0)\r\n-- #check (sq_eq_sq_iff_eq_or_eq_neg : x ^ 2 = y ^ 2 \u2194 x = y \u2228 x = -y)\r\n-- #check (sub_eq_zero : x - y = 0 \u2194 x = y)\r\n-- #check (sub_self x : x - x = 0)\r\n<\/pre>\n
Demostraciones interactivas<\/h3>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/h3>\n