While trying to prove some basic properties using coinductive types in Coq, I keep running into the following problem and I cannot get around it. I've distilled the problem into a simple Coq script as follows.
The type Tree defines possibly infinite trees with branches labelled with elements of type A. A branch need not be defined for all elements of A. The value Univ is the infinite tree with all A branches always defined. isUniv tests whether a given tree is equal to the Univ. The lemma states that Univ does indeed satisfy 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.
At this point I give up the proof. The current goal is:
CH : isUniv Univ ============================ isUniv (cofix Univ : Tree := Node (fun _ : A => Some Univ))
I do not know which tactic to apply to eliminate the cofix in the goal to produce (Node something) so that I can apply isuniv.
Can anyone help prove this lemma?
What are the standard ways of eliminating cofix in such a situation?