Skip to content

jaalonso/DAO_con_Lean

BranchesTags

Repository files navigation

DAO (Demostración Asistida por Ordenador) con Lean

1 Introducción

El objetivo de este trabajo es presentar una introducción a la DAO (Demostración Asistida con Ordenador) usando Lean para usarla en las clases de la asignatura de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla. Por tanto, el único prerrequisito es, como en el Máster, cierta madurez matemática como la que deben tener los alumnos de los Grados de Matemática y de Informática.

La exposición se hará mediante una colección de ejercicios. En cada ejercicios se mostrarán distintas pruebas del mismo resultado y se comentan las tácticas conforme se van usando y los lemas utilizados en las demostraciones.

Además, en cada ejercicio hay tres enlaces: uno al código, otro que al pulsarlo abre el ejercicio en Lean Web (en una sesión del navegador) de forma que se puede navegar por las pruebas y editar otras alternativas, y el tercero es un enlace a un vídeo explicando las soluciones del ejercicio.

El trabajo se presenta en 2 formas:

Además, los vídeos correspondientes a cada uno de los ejercicios se encuentran en YouTube.

El trabajo se basa fundamentalmente en el proyecto lean-tutorials de la Comunidad Lean que, a su vez, se basa en el curso Introduction aux mathématiques formalisées de Patrick Massot.

El proyecto se crea con

leanproject new DAO_con_Lean

2 Igualdad

En este capítulos se presenta el razonamiento con igualdades mediante reescritura.

2.1 Prueba mediante reescritura

2.2 Prueba con lemas y mediante encadenamiento de ecuaciones

2.3 Teorema aritmético con hipótesis y uso de lemas

2.4 Ejercicios sobre aritmética real

3 Conectivas: implicación, equivalencia, conjunción y disyunción

3.1 Reglas de la implicación

3.1.1 Eliminación de la implicación

3.1.2 Introducción de la implicación

3.2 Reglas de la equivalencia

3.2.1 Eliminación de la equivalencia

3.3 Reglas de la conjunción

3.3.1 Eliminación de la conjunción

3.3.2 Introducción de la conjunción

3.4 Reglas de la disyunción

3.4.1 Eliminación de la disyunción

3.5 Ejercicios

3.5.1 Monotonía de la suma por la izquierda

3.5.2 Monotonía de la suma por la derecha

3.5.3 La suma de no negativos es expansiva

3.5.4 Suma de no negativos

3.5.5 Suma de desigualdades

3.5.6 Monotonía de la multiplicación por no negativo

3.5.7 Monotonía de la multiplicación por no positivo

3.5.8 Conectivas y desigualdades

3.5.9 Conmutatividad de la conjunción

3.5.10 Formulación equivalente de lemas con dos hipótesis

3.5.11 En los naturales, mcd(x,y) = x syss x divide a y

4 Cuantificadores

4.1 Cuantificador universal

4.1.1 Eliminación del cuantificador universal

4.1.2 Introducción del cuantificador universal: La función cuadrado es par

4.1.3 Renombramiento de variables

4.2 Ejercicios sobre el cuantificador universal

4.2.1 La suma de dos funciones pares es una función par

4.2.2 La composición con una función par es par

4.2.3 La composición de funciones impares es impar

4.2.4 La composición de funciones crecientes es creciente

4.2.5 La composición de una función creciente y una decreciente es decreciente

4.2.6 f es creciente syss ∀ x y, x < y → f x ≤ f y

4.2.7 Una función creciente e involutiva es la identidad

4.2.8 Propiedad: ∀ a b : ℝ, a = a * b → a = 0 ∨ b = 1

4.2.9 Propiedad: ∀ x : ℝ, x^2 = 1 → x = 1 ∨ x = -1

4.2.10 Propiedad: ∀ x y : ℝ, x^2 = y^2 → x = y ∨ x = -y

4.3 Cuantificador existencial

4.3.1 Eliminación del cuantificador existencial

4.3.2 Introducción del cuantificador existencial

4.4 Ejercicios con el cuantificador existencial

4.4.1 Propiedad: ∃ k, n = k + 1 ⊢ n > 0

4.4.2 Propiedad transitiva de la divisibilidad

4.4.3 Propiedad: Si divide a los sumandos divide a la suma

4.4.4 Propiedad: Si divide a los sumandos divide a la suma (con condicionales)

4.4.5 CNS de divisible por cero

4.4.6 Propiedad: Si (g ∘ f) es suprayectiva, entonces g es suprayectiva

4.4.7 Propiedad: La composición de funciones suprayectivas es suprayectiva

5 Límites de sucesiones

5.1 Límites de sucesiones

5.1.1 Límite de sucesiones constantes

5.1.2 Si el límite de la sucesión u es c y c > 0, entonces u(n) ≥ c/2 a partir de un N

5.1.3 Límite de la suma de dos sucesiones convergentes

5.1.4 Teorema del emparedado

5.1.5 Si |x| < ε, para todo ε > 0, entonces x = 0

5.1.6 Si |x| ≤ ε, para todo ε > 0, entonces x = 0

5.1.7 Si |x - y| ≤ ε, para todo ε > 0, entonces x = y

5.1.8 Unicidad del límite de las sucesiones

5.1.9 Los supremos de las sucesiones no decrecientes son sus límites

5.2 Subsucesiones

5.2.1 La función identidad es menor o igual que la función de extracción

5.2.2 Las funciones de extracción no están acotadas

5.2.3 Si a es un punto de acumulación de u, entonces ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε

5.2.4 Las subsucesiones tienen el mismo límite que la sucesión

5.2.5 El punto de acumulación de las convergentes es su límite

5.2.6 Toda sucesión convergente es una sucesión de Cauchy

5.2.7 Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

6 Negación

6.1 Falso y negación

6.1.1 Principio de no contradicción

6.1.2 Introducción de la doble negación

6.1.3 La relación menor es irreflexiva en los reales

6.1.4 Demostración con hipótesis inconsistentes

6.2 Principio del tercio excluso y reducción al absurdo

6.2.1 Eliminación de la doble negación

6.2.2 Demostración por casos: P → R, ¬P → Q, Q → R ⊢ R

6.2.3 Demostración de P ∨ Q, ¬(P ∧ Q) ⊢ ¬P ↔ Q

6.2.4 Principio de contraposición

6.2.5 Definición del condicional mediante la negación y la disyunción

6.2.6 Un número es par syss lo es su cuadrado

6.2.7 Pruebas de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

6.2.8 Negación del existencial: Caracterización de números no pares.

6.2.9 Negación del universal: Caracterización de funciones no pares

6.2.10 La función duplicadora no es par

6.2.11 La función identidad no está acotada superiormente

6.2.12 CS menor o igual que cero

6.2.13 Equivalencia de definiciones de creciente

7 Límites y negaciones

8 Ampliación de límites

9 Apéndices

9.1 Resumen de tácticas usadas

9.2 Resumen de teoremas usados

9.3 Estilos de demostración

9.4 Nomenclatura

About

DAO (Demostración Asistida por Ordenador) con Lean

github.com/jaalonso/DAO_con_Lean/raw/master/DAO_con_Lean.pdf

Topics

logic theorem-proving mathematics interactive-theorem-proving leanprover

Resources

Readme

License

GPL-3.0 license
Activity

Stars

0 stars

Watchers

1 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published

Languages