En el ejercicio 6 se nos pide implementar algunas funciones sobre listas de naturales y luego generalizarlas a listas de cualquier tipo de set. Para la primera parte recurrí a la función Nat.eqb que, dados dos naturales, retorna el booleano true si son iguales o el booleano false si no lo son.
Para generalizar las funciones para que acepten listas de A (siendo A : Set) necesitaría una un comparador booleano genérico de tipo A -> A -> bool tal que retornara "true" sii sus dos argumentos son iguales. ¿Existe una manera de hacer eso en Coq? Sino la alternativa que se me ocurre es exigir que las funciones generalizadas tomaran una función A -> A -> bool como argumento.
Quizá existe una manera de resolver el problema utilizando el operador de igualdad de coq (que funciona como un A -> A -> Prop) pero no he encontrado cómo.
Gracias y saludos.
[Practico 4] Igualdad de objetos como booleano
Número de respuestas: 1
En respuesta a Jose Diego Suarez Hernandez
Re: [Practico 4] Igualdad de objetos como booleano
de Carlos Luna -
Hola José.
Te recomiendo la opción de recibir como parámetro una función de tipo A -> A -> bool, para la igualdad sobre elemento de un tipo genérico A. No es correcto usar Prop para definir funciones con significado computacional.
Saludos, Carlos