Mientras trato de probar algunas propiedades básicas usando tipos coinductores en Coq, sigo encontrando el siguiente problema y no puedo solucionarlo. He destilado el problema en un simple script Coq de la siguiente manera.
El tipo de árbol define árboles posiblemente infinitos con ramas marcadas con elementos de tipo A . Una rama no tiene que estar definida para todos los elementos de A . El valor Univ es el árbol infinito con todas las ramas A siempre definidas. isUniv prueba si un árbol dado es igual a Univ . El lema dice que Univ realmente satisface a isUniv .
Parameter A : Set.
CoInductive Tree: Set := Node : (A -> option Tree) -> Tree.
Definition derv (a : A) (t: Tree): option Tree :=
match t with Node f => f a end.
CoFixpoint Univ : Tree := Node (fun _ => Some Univ).
CoInductive isUniv : Tree -> Prop :=
isuniv : forall (nf : A -> option Tree) (a : A) (t : Tree),
nf a = Some t ->
isUniv t ->
isUniv (Node nf).
Lemma UnivIsUniv : isUniv Univ.
Proof.
cofix CH. (* this application of cofix is fine *)
unfold Univ.
Admitted.
En este punto renuncio a la prueba. El objetivo actual es:
CH : isUniv Univ
============================
isUniv (cofix Univ : Tree := Node (fun _ : A => Some Univ))
No sé qué táctica aplicar para eliminar el cofix en el objetivo de producir (Nodo algo) para poder aplicar isuniv .
¿Alguien puede ayudar a probar este lema?
¿Cuáles son las formas estándar de eliminar el cofix en tal situación?
fuente
Respuestas:
Puede eliminar el cofix usando una función auxiliar que coincida con el patrón Tree.
Obtendrás este objetivo, que es un paso sin cuerda.
Adapté esta técnica de http://adam.chlipala.net/cpdt/html/Coinductive.html
fuente
fuente