ForMatUS: Pruebas del silogismo hipotético: P → Q, Q → R ⊢ P → R
He añadido a la lista Lógica con Lean el vídeo Pruebas del silogismo hipotético en el que se se comentan 11 pruebas en Lean del silogismo hipotético
P → Q, Q → R ⊢ P → R.
Se comienza con pruebas declarativas, con razonamiento hacia adelante, que se reducen a funcionales; a continuación, se hacen pruebas aplicativas, con razonamiento hacia atrás, que también se reducen a funcionales y, finalmente, se buscan las pruebas automáticas.
A continuación, se muestra el vídeo
El código es
|
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 |
-- Pruebas del silogismo hipotético -- -------------------------------- import tactic variables (P Q R : Prop) -- Ej. 1. Demostrar que -- P → Q, Q → R ⊢ P → R -- 1º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := assume h : P, have h3 : Q, from h1 h, show R, from h2 h3 -- 2º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := assume h : P, have h3 : Q := h1 h, show R, from h2 h3 -- 3º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := assume h : P, show R, from h2 (h1 h) -- 4º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := assume h : P, h2 (h1 h) -- 5º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := λ h, h2 (h1 h) -- 6º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := h2 ∘ h1 -- 7º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := begin intro h, apply h2, apply h1, exact h, end -- 8º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := begin intro h, apply h2, exact h1 h, end -- 9º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := begin intro h, exact h2 (h1 h), end -- 10º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := λ h, h2 (h1 h) -- 11º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := h2 ∘ h1 -- 12º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := by tauto -- 13º demostración example (h1 : P → Q) (h2 : Q → R) : P → R := by finish |