Ao tentar provar algumas propriedades básicas usando tipos coindutores no Coq, continuo com o seguinte problema e não consigo contorná-lo. Eu destilei o problema em um script Coq simples da seguinte maneira.
O tipo de árvore define árvores possivelmente infinitas com ramos rotulados com elementos do tipo A . Um ramo não precisa ser definido para todos os elementos A . O valor Univ é a árvore infinita com todos os ramos A sempre definidos. O isUniv testa se uma determinada árvore é igual à Univ . O lema afirma que o Univ realmente satisfaz o 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.
Neste ponto, desisto da prova. O objetivo atual é:
CH : isUniv Univ
============================
isUniv (cofix Univ : Tree := Node (fun _ : A => Some Univ))
Não sei qual tática aplicar para eliminar o cofix no objetivo de produzir (Nó alguma coisa) para que eu possa aplicar isiv .
Alguém pode ajudar a provar esse lema?
Quais são as formas padrão de eliminar o cofix em tal situação?
fonte
Respostas:
Você pode eliminar o cofix usando uma função auxiliar que corresponda ao padrão em Árvore.
Você obterá esse objetivo, que é um passo livre.
Eu adaptei essa técnica em http://adam.chlipala.net/cpdt/html/Coinductive.html
fonte
fonte