Hola, no entendemos que debemos hacer en este ejercicio. A que se refiere exactamente con utilizar los estructuradores de tácticas para escribir una prueba de los teoremas en una sola línea?
Saludos, gracias.
Hola.
Hay una sección en el manual de Coq sobre este tema (Chapter 9 - The tactic language): https://coq.inria.fr/distrib/current/refman/Reference-Manual011.html#hevea_default719.
Esencialmente precisan el estructurador de tácticas ";"
- T1;T2 aplica la táctica T2 a todos los subgoals generados por la aplicación de T1.
- T1;[T2|T3] aplica la táctica T2 al primer subgoal luego de la aplicación de T1, y la táctica T3 al segundo subgoal (luego de la aplicación de T1).
Por más información ver la referencia indicada.
Saludos, Carlos
Bárbaro, lo habíamos hecho con eso pero no estabamos seguros de que fuera lo que pedía el ejercicio.
Gracias!