# Eliminating cofix in Coq proof

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.



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?

• The tag "interactive-proofs" is not adequate, as it generally refers to interactive proof systems in their complexity-theoretic sense. The correct term I suppose is "interactive-theorem-proving", or "theorem-proving". – Iddo Tzameret Sep 1 '10 at 22:34
• Fixed, using "proof-assistants" – Dave Clarke Sep 2 '10 at 6:51

You can eliminate cofix using an auxiliary function that pattern matches Tree.

Definition TT (t:Tree) :=
match t with
| Node o => Node o
end.

Lemma TTid : forall t: Tree, t = TT t.
intro t.
destruct t.
reflexivity.
Qed.

Lemma UnivIsUniv : isUniv Univ.
Proof.
cofix.
rewrite TTid.
unfold TT.
unfold Univ.


You will obtain this goal, which is a step unwinded.

  UnivIsUniv : isUniv Univ
============================
isUniv
(Node
(fun _ : A =>
Some (cofix Univ  : Tree := Node (fun _ : A => Some Univ))))


• Thanks for this. I was looking at that page at about the same time your answer came in. Crazy, but it seems to work ... and then I get stuck a little further, but I'll bash my head against that for a little longer. – Dave Clarke Sep 2 '10 at 15:02
(* I post my answer as a Coq file. In it I show that supercoooldave's
definition of a universal tree is not what he intended. His isUniv
means "the tree has an infinite branch". I provide the correct
definition, show that the universal tree is universal according to
the new definition, and I provide counter-examples to
supercooldave's definition. I also point out that the universal
tree of branching type A has an infinite path iff A is inhabited.
*)

Set Implicit Arguments.

CoInductive Tree (A : Set): Set := Node : (A -> option (Tree A)) -> Tree A.

Definition child (A : Set) (t : Tree A) (a : A) :=
match t with
Node f => f a
end.

(* We consider two trees, one is the universal tree on A (always
branches out fully), and the other is a binary tree which always
branches to one side and not to the other, so it is like an
infinite path with branches of length 1 shooting off at each node.  *)

CoFixpoint Univ (A : Set) : Tree A := Node (fun _ => Some (Univ A)).

CoFixpoint Thread : Tree (bool) :=
Node (fun (b : bool) => if b then Some Thread else None).

(* The original definition of supercooldave should be called "has an
infinite path", so we rename it to "hasInfinitePath". *)
CoInductive hasInfinitePath (A : Set) : Tree A -> Prop :=
haspath : forall (f : A -> option (Tree A)) (a : A) (t : Tree A),
f a = Some t ->
hasInfinitePath t ->
hasInfinitePath (Node f).

(* The correct definition of universal tree. *)
CoInductive isUniv (A : Set) : Tree A -> Prop :=
isuniv : forall (f : A -> option (Tree A)),
(forall  a, exists t, f a = Some t /\ isUniv t) ->
isUniv (Node f).

(* Technicalities that allow us to get coinductive proofs done. *)
Definition TT (A : Set) (t : Tree A) :=
match t with
| Node o => Node o
end.

Lemma TTid (A : Set) : forall t: Tree A, t = TT t.
intros A t.
destruct t.
reflexivity.
Qed.

(* Thread has an infinite path. *)
Proof.
cofix H.
rewrite TTid.
unfold TT.
(* there is a path down the "true" branch leading to Thread. *)
apply haspath with (a := true) (t := Thread).
auto.
auto.
Qed.

(* Auxiliary lemma *)
Lemma univChildNotNone (A : Set) (t : Tree A) (a : A):
isUniv t -> (child t a <> None).
Proof.
intros A t a [f H].
destruct (H a) as [u [G _]].
unfold child.
rewrite G.
discriminate.
Qed.

(* Thread is not universal. *)
Proof.
unfold not.
intro H.
eapply univChildNotNone with (t := Thread) (a := false).
auto.
auto.
Qed.

(* Now let us show that Univ is universal. *)
Lemma univIsuniv (A : Set): isUniv (Univ A).
Proof.
intro A.
cofix H.
rewrite TTid.
unfold TT.
unfold Univ.
apply isuniv.
intro a.
exists (Univ A).
auto.
Qed.

(* By the way, it need not be the case that a universal tree has
an infinite path! In fact, the universal tree of branching type
A has an infinite path iff A is inhabited. *)

Lemma whenUnivHasInfiniteBranch (A : Set):
hasInfinitePath (Univ A) <-> exists a : A, True.
Proof.
intro A.
split.
intro H.
destruct H as [f a t _].
exists a.
trivial.
intros [a _].
cofix H.
rewrite TTid.
unfold TT.
unfold Univ.
apply haspath with (t := Univ A); auto.
Qed.

• Thanks for this somewhat embarrassing response. I did run into the problem with A being inhabited, but managed to finesse my way around that. Surprisingly, the universe didn't unfold. – Dave Clarke Sep 4 '10 at 9:06
• Well, I am not embarrassed by my response :-) I thought I might as well give a comprehensive response if I give one. – Andrej Bauer Sep 4 '10 at 16:54
• Your response was embarrassing for me. But certainly highly appreciated. – Dave Clarke Sep 4 '10 at 22:41
• I was joking... Anyhow, there's nothing to be embarrassed about. I've made worse mistakes. Also, the web invites people to post before they think. I myself posted an erroneous fix of your definition here, but luckily I noticed it before you did. – Andrej Bauer Sep 5 '10 at 10:59