Hola a todos,
Escribo para hacer algunas consultas.
1. En general intento llevar un esquema mental de lo que voy escribiendo, para no caer en la mala práctica de simplemente mezclar símbolos. En el caso de Coq voy imaginando un esquema de derivación con forma de árbol (al estilo deducción natural / cálculo lambda tipado), y creo que no es del todo adecuado. Entiendo que lo ideal sería estudiar un poco del cálculo de secuentes, y creo que lo veremos luego en la materia. ¿Alguna recomendación sobre cómo pensar, por ejemplo, la táctica apply (es la que más me cuesta "meter" en mi esquema mental)?
2. En la clase anterior se habló de la indecidibilidad de las pruebas automáticas en Coq cuando se usa el axioma del tercero excluido. Me hace recordar a la no reversibilidad de los argumentos en Prolog cuando no queda claro cómo se construyen los términos, por esta noción de construcción que "quita" el tercero excluido. ¿Hay alguna conexión a nivel conceptual o es imaginación mía nomás?
3. También se habló en la clase anterior sobre dos diferentes formas de plantear una prueba: desde el uso de una prueba como objeto al aplicar la táctica `exact`, y desde la lógica aplicando `assumption`. Me interesa, ¿veremos más sobre esta dualidad? En caso de que no, ¿recomiendan algún material para profundizar?
¡Gracias!
Saludos,
Cristian