ForMatUS: Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R
He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R en el que se comentan 5 pruebas en Lean de
P, P → Q, P → (Q → R) ⊢ R
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 |
-- Pruebas de P, P → Q, P → (Q → R) ⊢ R -- ==================================== -- Ej 1. Demostrar que -- P, P → Q, P → (Q → R) ⊢ R import tactic variables (P Q R : Prop) -- 1ª demostración example (h1 : P) (h2 : P → Q) (h3 : P → (Q → R)) : R := have h4 : Q, from h2 h1, have h5 : Q → R, from h3 h1, show R, from h5 h4 -- 2ª demostración example (h1 : P) (h2 : P → Q) (h3 : P → (Q → R)) : R := have h4 : Q := h2 h1, have h5 : Q → R := h3 h1, show R, from h5 h4 -- 3ª demostración example (h1 : P) (h2 : P → Q) (h3 : P → (Q → R)) : R := show R, from (h3 h1) (h2 h1) -- 4ª demostración example (h1 : P) (h2 : P → Q) (h3 : P → (Q → R)) : R := (h3 h1) (h2 h1) -- 5ª demostración example (h1 : P) (h2 : P → Q) (h3 : P → (Q → R)) : R := by finish |