Buenas,
Salen los ejercicios y las definiciones con Fixpoint pero hay algo que no estoy entendiendo bien. Me resulta redundante que tengas que escribir `{struct x}` y también `match y with` con x = y.
Hay algún ejemplo que uses x /= y ? Ni siquiera entiendo mucho qué querría decir eso, jaja.
Saludos!
Hola Julián.
No tengo la computadora ahora.
No estoy seguro de entender tu duda.
El match es para hacer análisis de casos en una definición, usando los constructores del tipo de dato (si es nat: 0 y S ; si es una lista: nil y cons, por ejemplo).
El struct es para fijar el parámetro a ser chequeado en una recursion, para ver que estructuralmente es mas pequeño (constructivamente).
Podrías tener funciones recursivas como la igualdad (que retorna un bool) entre listas o naturales, donde es necesario hacer análisis de casos en los dos parámetros pero donde alcanzaría con chequear (uso de struct) la terminación en uno de ellos.
Por otro lado, podes hacer strcuct x, y luego match x en la definición. No entiendo lo de la y...
Si esto no resuelve tu consulta, volvé a escribir.
Saludos Carlos
Hola.
Para definir funciones por recursion estructural usamos Fixpoint, no Defintion.
Fixpoint permite asegurar la terminación pero para ello es necesario establecer un argumento en el cual Coq chequee que es estrictamente mas pequeño en base a exclusivamente los constructores del tipo de dato. No funciona si por ejemplo llamas recursivamente con el resultado de cierta función, como - (n-1), ya que en general habría que demostrar que el resultado de la función es estructuralmente mas pequeño; esto con Fixpoint no es posible.
En el último módulo del curso veremos como definir funciones recursivas generales, pero para esto se requerirá demostrar terminación sobre órdenes bien fundados (con Fixpoint la terminación se asegura, pero con las restricciones vistas).
Saludos
El struct es para eso, si. Si no se pone, Coq toma uno por defecto.
El match, como puse en una respuesta anterior, es para hacer análisis de casos en los constructores. Dado que Fixpoint chequea recursión estructural, llamar con un término estructuralmente mas pequeño permite asegurar terminación sobre el parámetro elegido con struct (explícita o implicitamente).
Podes hacer match en más de un parámetro (como puse en un mensaje anterior), como en el ejemplo de leBool. Notar que en el llamado recursivo (leBool k j) ambos parámetros son estructuralmente mas pequeños (tienen un sucesor menos).
Saludos