Demostrar que un n\u00famero es par si y solo si lo es su cuadrado.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.int.parity\nimport tactic\nopen int\n\nvariable (n : \u2124)\n\nexample :\n even (n^2) \u2194 even n :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport data.int.parity\r\nimport tactic\r\nopen int\r\n\r\nvariable (n : \u2124)\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\nbegin\r\n split,\r\n { contrapose,\r\n rw \u2190 odd_iff_not_even,\r\n rw \u2190 odd_iff_not_even,\r\n unfold odd,\r\n intro h,\r\n cases h with k hk,\r\n use 2*k*(k+1),\r\n rw hk,\r\n ring, },\r\n { unfold even,\r\n intro h,\r\n cases h with k hk,\r\n use 2*k^2,\r\n rw hk,\r\n ring, },\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\nbegin\r\n split,\r\n { contrapose,\r\n rw \u2190 odd_iff_not_even,\r\n rw \u2190 odd_iff_not_even,\r\n rintro \u27e8k, rfl\u27e9,\r\n use 2*k*(k+1),\r\n ring, },\r\n { rintro \u27e8k, rfl\u27e9,\r\n use 2*k^2,\r\n ring, },\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\niff.intro\r\n ( have h : \u00aceven n \u2192 \u00aceven (n^2),\r\n { assume h1 : \u00aceven n,\r\n have h2 : odd n,\r\n from odd_iff_not_even.mpr h1,\r\n have h3: odd (n^2), from\r\n exists.elim h2\r\n ( assume k,\r\n assume hk : n = 2*k+1,\r\n have h4 : n^2 = 2*(2*k*(k+1))+1, from\r\n calc n^2\r\n = (2*k+1)^2 : by rw hk\r\n ... = 4*k^2+4*k+1 : by ring\r\n ... = 2*(2*k*(k+1))+1 : by ring,\r\n show odd (n^2),\r\n from exists.intro (2*k*(k+1)) h4),\r\n show \u00aceven (n^2),\r\n from odd_iff_not_even.mp h3 },\r\n show even (n^2) \u2192 even n,\r\n from not_imp_not.mp h )\r\n ( assume h1 : even n,\r\n show even (n^2), from\r\n exists.elim h1\r\n ( assume k,\r\n assume hk : n = 2*k ,\r\n have h2 : n^2 = 2*(2*k^2), from\r\n calc n^2\r\n = (2*k)^2 : by rw hk\r\n ... = 2*(2*k^2) : by ring,\r\n show even (n^2),\r\n from exists.intro (2*k^2) h2 ))\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\ncalc even (n^2)\r\n \u2194 even (n * n) : iff_of_eq (congr_arg even (sq n))\r\n ... \u2194 (even n \u2228 even n) : int.even_mul\r\n ... \u2194 even n : or_self (even n)\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\ncalc even (n^2)\r\n \u2194 even (n * n) : by ring_nf\r\n ... \u2194 (even n \u2228 even n) : int.even_mul\r\n ... \u2194 even n : by simp\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n even (n^2) \u2194 even n :=\r\nbegin\r\n split,\r\n { contrapose,\r\n intro h,\r\n rw \u2190 odd_iff_not_even at *,\r\n cases h with k hk,\r\n use 2*k*(k+1),\r\n calc n^2\r\n = (2*k+1)^2 : by rw hk\r\n ... = 4*k^2+4*k+1 : by ring\r\n ... = 2*(2*k*(k+1))+1 : by ring, },\r\n { intro h,\r\n cases h with k hk,\r\n use 2*k^2,\r\n calc n^2\r\n = (2*k)^2 : by rw hk\r\n ... = 2*(2*k^2) : by ring, },\r\nend\r\n<\/pre>\n