He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Formulación equivalente de lemas con dos hipótesis en el que se comentan 5 demostraciones en Lean de la fórmula
(P ∧ Q → R) ↔ (P → (Q → R))
usando distintos estilos de prueba,
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conmutatividad de la conjunción en Lean en el que se comentan 9 demostraciones en Lean de la conmutatividad de la conjunción usando los distintos estilos: aplicativa con táctica, declarativa estructurada, funcional con término de prueba y automática.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conectivas y desigualdades en Lean en el se comentan las demostraciones en Lean de algunas de las propiedades de las desigualdades de los números reales estudiadas en vídeos anteriores, pero formuladas con conectivas. Concretamente, se demuestran las 5 propiedades siguientes:
Sean a, b y c números reales.
- 0 ≤ a → b ≤ a + b
- 0 ≤ b → a ≤ a + b
- (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b
- 0 ≤ a → (0 ≤ b → 0 ≤ a + b)
- Si (0 ≤ a ∧ 0 ≤ b) → 0 ≤ a + b, entonces 0 ≤ a → (0 ≤ b → 0 ≤ a + b)
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo