Negación del universal en Lean: Caracterización de funciones no pares
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 6 pruebas en Lean de la propiedad
¬par f ↔ ∃ x, f (-x) ≠ f x
usando los estilos declarativo, aplicativo y automático.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
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 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 |
import data.real.basic variable (f : ℝ → ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la función -- par : (ℝ → ℝ) → Prop -- tal que (par f) expresa que f es par. -- ---------------------------------------------------- def par : (ℝ → ℝ) → Prop | f := ∀ x, f (-x) = f x -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que -- ¬par f ↔ ∃ x, f (-x) ≠ f x -- ---------------------------------------------------- -- 1ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin split, { contrapose, intro h1, rw not_not, unfold par, intro x, by_contradiction h2, apply h1, use x, }, { intro h1, intro h2, unfold par at h2, cases h1 with x hx, apply hx, exact h2 x, }, end -- 2ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin split, { contrapose, intro h1, rw not_not, intro x, by_contradiction h2, apply h1, use x, }, { rintros ⟨x, hx⟩ h', exact hx (h' x) }, end -- 3ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin unfold par, push_neg, end -- 4ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := iff.intro ( have h1 : ¬(∃ x, f (-x) ≠ f x) → ¬¬par f, { assume h2 : ¬(∃ x, f (-x) ≠ f x), have h3 : par f, { assume x, have h4 : ¬(f (-x) ≠ f x), { assume h5 : f (-x) ≠ f x, have h6 : ∃ x, f (-x) ≠ f x, from exists.intro x h5, show false, from h2 h6, }, show f (-x) = f x, from not_not.mp h4}, show ¬¬par f, from not_not.mpr h3 }, show ¬par f → (∃ x, f (-x) ≠ f x), from not_imp_not.mp h1) ( assume h1 : ∃ x, f (-x) ≠ f x, show ¬par f, { assume h2 : par f, show false, from exists.elim h1 ( assume x, assume hx : f (-x) ≠ f x, have h3 : f (-x) = f x, from h2 x, show false, from hx h3)}) -- 5ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := -- by suggest not_forall -- 6ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := -- by hint by simp [par] |