El producto por un par es par
Demostrar que los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import data.nat.parity import tactic open nat example : ∀ m n : ℕ, even n → even (m * n) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 |
import data.nat.parity import tactic open nat -- 1ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin intros m n hn, unfold even at *, cases hn with k hk, use m * k, calc m * n = m * (k + k) : congr_arg (has_mul.mul m) hk ... = m * k + m * k : mul_add m k k end -- 2ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin intros m n hn, cases hn with k hk, use m * k, calc m * n = m * (k + k) : congr_arg (has_mul.mul m) hk ... = m * k + m * k : mul_add m k k end -- 3ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin rintros m n ⟨k, hk⟩, use m * k, calc m * n = m * (k + k) : congr_arg (has_mul.mul m) hk ... = m * k + m * k : mul_add m k k end -- 4ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin rintros m n ⟨k, hk⟩, use m * k, rw hk, exact mul_add m k k, end -- 5ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin rintros m n ⟨k, hk⟩, use m * k, rw [hk, mul_add] end -- 6ª demostración example : ∀ m n : ℕ, even n → even (m * n) := begin rintros m n ⟨k, hk⟩, exact ⟨m * k, by rw [hk, mul_add]⟩ end -- 7ª demostración example : ∀ m n : ℕ, even n → even (m * n) := λ m n ⟨k, hk⟩, ⟨m * k, by rw [hk, mul_add]⟩ -- 8ª demostración example : ∀ m n : ℕ, even n → even (m * n) := assume m n ⟨k, (hk : n = k + k)⟩, have hmn : m * n = m * k + m * k, by rw [hk, mul_add], show ∃ l, m * n = l + l, from ⟨_, hmn⟩ |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean p. 2.
