Pruebas en Lean de “La relación menor es irreflexiva en los reales”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 16 pruebas en Lean de la propiedad
La relación menor es irreflexiva en los reales
usando los estilos declarativo, funcional, 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 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 |
import data.real.basic import tactic variable {x : ℝ} -- ---------------------------------------------------- -- Ejercicio. Demostrar que la relación menor es -- irreflexiva en los reales. -- ---------------------------------------------------- -- 1ª demostración example : ¬ x < x := begin intro h1, rw lt_iff_le_and_ne at h1, cases h1 with h2 h3, -- clear h2, -- change x = x → false at h3, apply h3, refl, end -- 2ª demostración example : ¬ x < x := begin intro h1, rw lt_iff_le_and_ne at h1, cases h1 with h2 h3, apply h3, refl, end -- 3ª demostración example : ¬ x < x := begin intro h1, cases (lt_iff_le_and_ne.mp h1) with h2 h3, apply h3, refl, end -- 4ª demostración example : ¬ x < x := begin intro h1, apply (lt_iff_le_and_ne.mp h1).2, refl, end -- 5ª demostración example : ¬ x < x := begin intro h1, exact absurd rfl (lt_iff_le_and_ne.mp h1).2, end -- 6ª demostración example : ¬ x < x := λ h, absurd rfl (lt_iff_le_and_ne.mp h).2 -- 7ª demostración example : ¬ x < x := assume h1 : x < x, have h2 : x ≤ x ∧ x ≠ x, from lt_iff_le_and_ne.mp h1, have h3 : x ≠ x, from and.right h2, have h4 : x = x, from rfl, show false, from absurd h4 h3 -- 8ª demostración example : ¬ x < x := assume h1 : x < x, have h2 : x ≤ x ∧ x ≠ x, from lt_iff_le_and_ne.mp h1, absurd rfl (and.right h2) -- 9ª demostración example : ¬ x < x := assume h1 : x < x, absurd rfl (and.right (lt_iff_le_and_ne.mp h1)) -- 10ª demostración example : ¬ x < x := assume h1 : x < x, absurd rfl (lt_iff_le_and_ne.mp h1).2 -- 11ª demostración example : ¬ x < x := λ h, absurd rfl (lt_iff_le_and_ne.mp h).2 -- 12ª demostración example : ¬ x < x := -- by library_search irrefl x -- 12ª demostración example : ¬ x < x := -- by hint by simp -- 13ª demostración example : ¬ x < x := by finish -- 14ª demostración example : ¬ x < x := by norm_num -- 15ª demostración example : ¬ x < x := by linarith -- 16ª demostración example : ¬ x < x := by nlinarith |