Programación funcional y métodos elementales de demostración en Coq
En este tema se introduce mediante ejemplos la programación funcional en Coq y la demostración de las propiedades de las funciones definidas usando los métodos elementales de programación en Coq.
Su contenido es
- Datos y funciones
- Tipos enumerados
- Booleanos
- Tipos de las funciones
- Tipos compuestos
- Módulos
- Números naturales
- Métodos elementales de demostración
- Demostraciones por simplificación
- Demostraciones por reescritura
- Demostraciones por análisis de casos
La teoría correspondiente es