ForMatUS: Pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas usando los estilos declarativos, aplicativos, funcional y automático.
A continuación, se muestra el vídeo
|
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 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar que las relaciones irreflexivas y -- transitivas son asimétricas. -- ---------------------------------------------------- variable A : Type variable R : A → A → Prop -- #reduce irreflexive R -- #reduce transitive R -- 1ª demostración example (h1 : irreflexive R) (h2 : transitive R) : ∀ x y, R x y → ¬ R y x := begin intros x y h3 h4, apply h1 x, apply h2 h3 h4, end -- 2ª demostración example (h1 : irreflexive R) (h2 : transitive R) : ∀ x y, R x y → ¬ R y x := begin intros x y h3 h4, apply (h1 x) (h2 h3 h4), end -- 3ª demostración example (h1 : irreflexive R) (h2 : transitive R) : ∀ x y, R x y → ¬ R y x := λ x y h3 h4, (h1 x) (h2 h3 h4) -- 4ª demostración example (h1 : irreflexive R) (h2 : transitive R) : ∀ x y, R x y → ¬ R y x := assume x y, assume h3 : R x y, assume h4 : R y x, have h5 : R x x, from h2 h3 h4, have h6 : ¬ R x x, from h1 x, show false, from h6 h5 |