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
He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 2 de 2) en el que se completa el estudio de las definiciones por recursión en Haskell comenzado en el vídeo anterior. Concretamente, hemos visto ejemplos de
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.
He añadido a la lista Programación funcional con Haskell el vídeo Definiciones por recursión en Haskell (Parte 1 de 2) en el que se e,pieza el estudio de las definiciones por recursión en Haskell. Concretamente, hemos visto ejemplos de
El vídeo es
Los apuntes correspondientes son
Una versión interactiva de los apuntes en IHaskell se encuentra aquí.