Consultas de Práctico

Hola Juan Manuel.

Sin tener información precisa sobre tus definiciones y pruebas, aporto algunos comentarios generales.

Es correcto definir posfijo como una relación inductiva y no como una función booleana. De esta manera, se puede luego hacer inducción en la relación y no solo en los argumentos inductivos (listas) de la relación. La ventaja es que los casos que se plantean son los que corresponden a la definición inductiva y no todos los posibles si hicieras por ejemplo inducción en ambas variables argumentos (de tipo Lista) de la relación.

Se puede usar inversion o inversion_clear, aunque esto lo veremos en el módulo siguiente (práctico 5) y como dije no es imprescindible para el práctico 4 (pero se puede usar, no está prohibido en el práctico 4).

Es importante al aplicar cualquier táctica que las variables que se instancien en el goal y aparecen en las hipótesis, queden isntanciadasa también en las hipótesis, o al menos queden las igualdades para aplicar reescrituras.

Finalmente, hay varias formas de probar ciertas propiedades que involucran elementos inductivos; sean variables de tipo dato, como nat, list, por ejemplo, o relaciones definidas inductivamente. Dependiendo de las definiciones dadas y las propiedades a demostrar, algunas veces conviene más hacer inducción sobre una cosa u otra. Recomiendo pensar primero una estrategia de prueba antes de usar Coq sin mucho criterio, ya que sino las pruebas pueden no salir o ser muy rebuscadas e incomprensibles (como pasa cuando se programa; es similar). Con esto no quiero decir que tengan que buscar la prueba perfecta o minimalista, pero que si siga una estrategia. Por ejemplo, si una función binaria se define por recursión en el primer argumento, conviene hacer inducción en ese argumento y no en el otro, para que se pueda aplicar la definción de la función en la prueba.

Saludos, Carlos