He añadido a la lista Lógica con Lean el vídeo Presentación de “Lógica con Lean” en el que se se comenta el proyecto de “Lógica con Lean”. Concretamente sus objetivos, bases y método de desarrollo.
Los enlaces correspondientes son:
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 El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean) en el que se comenta la prueba en Lean de la siguiente propiedad de los números naturales: el máximo común divisor de a y b es igual a a si, y sólo si, a divide a b. Más concretamente,
Sean m y n son números naturales. Entonces, son equivalentes
- mcd(m,n) = n
- m divide a n
Su enunciado en Lean es
|
1 2 3 4 5 6 7 8 |
import data.nat.gcd open nat variables (a b : ℕ) example : a ∣ b ↔ gcd a b = a := sorry |
En la demostración se utilizan los siguientes propiedades de los números naturales:
|
1 2 3 4 |
dvd_refl: a ∣ a dvd_antisymm : a ∣ b → b ∣ a → a = b dvd_gcd_iff : c ∣ gcd a b ↔ c ∣ a ∧ c ∣ b gcd_dvd : gcd a b ∣ a ∧ gcd a b ∣ b |
Los enlaces correspondientes son:
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 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