Pruebas en Lean de “La función identidad no está acotada superiormente”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad
La función identidad no está acotada superiormente
usando los estilos aplicativo, declarativo, y funcional.
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 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 |
import data.real.basic -- ---------------------------------------------------- -- Ejercicio 1. Definir la función -- acotada_superiormente : (ℝ → ℝ) → Prop -- tal que (acotada_superiormente f) expresa que la -- función f está acotada superiormente. -- ---------------------------------------------------- def acotada_superiormente : (ℝ → ℝ) → Prop | f := ∃ M, ∀ x, f x ≤ M -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que la función identidad no -- está acotada superiormente. -- ---------------------------------------------------- -- 1ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente, unfold id, by_contradiction h, cases h with M hM, specialize hM (M+1), contrapose hM, simp only [not_le], exact lt_add_one M, end -- 2ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente id, push_neg, intro M, use M + 1, linarith, end -- 3ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente id, push_neg, exact no_top, end -- 4ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), have h4 : ¬(M < M + 1), from not_lt.mpr h3, have h5 : M < M + 1, from lt_add_one M, show false, from h4 h5) -- 5ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), have h4 : ¬(M < M + 1), from not_lt.mpr h3, have h5 : M < M + 1, from lt_add_one M, h4 h5) -- 6ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), (not_lt.mpr h3) (lt_add_one M)) -- 7ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 8ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 9ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, exists.elim h2 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 10ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 11ª demostración example : ¬acotada_superiormente id := λ h1, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) |