<p>You can eliminate cofix using an auxiliary function that pattern matches Tree.</p>

<pre><code>Definition TT (t:Tree) :=
  match t with
    | Node o =&gt; 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.
</code></pre>

<p>You will obtain this goal, which is a step unwinded.</p>

<pre><code>  UnivIsUniv : isUniv Univ
  ============================
   isUniv
     (Node
        (fun _ : A =&gt;
         Some (cofix Univ  : Tree := Node (fun _ : A =&gt; Some Univ))))
</code></pre>

<p>I adapted this technique from <a href="http://adam.chlipala.net/cpdt/html/Coinductive.html" rel="nofollow">http://adam.chlipala.net/cpdt/html/Coinductive.html</a></p>

CC BY-SA 2.5
2010-09-02T15:02:29.497Z
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
CC BY-SA 2.5
2010-09-02T13:13:16.120Z
2010-09-02T13:13:16.120Z
yhirai
<pre><code>(* 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 -&gt; option (Tree A)) -&gt; Tree A.

Definition child (A : Set) (t : Tree A) (a : A) :=
  match t with
    Node f =&gt; 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 _ =&gt; Some (Univ A)).

CoFixpoint Thread : Tree (bool) :=
  Node (fun (b : bool) =&gt; 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 -&gt; Prop :=
  haspath : forall (f : A -&gt; option (Tree A)) (a : A) (t : Tree A),
    f a = Some t -&gt;
    hasInfinitePath t -&gt; 
    hasInfinitePath (Node f).

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

(* Technicalities that allow us to get coinductive proofs done. *)
Definition TT (A : Set) (t : Tree A) :=
  match t with
    | Node o =&gt; 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. *)
Lemma ThreadHasInfinitePath : hasInfinitePath Thread.
Proof.
  cofix H.
  rewrite TTid.
  unfold TT.
  unfold Thread.
  (* 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 -&gt; (child t a &lt;&gt; None).
Proof.
  intros A t a [f H].
  destruct (H a) as [u [G _]].
  unfold child.
  rewrite G.
  discriminate.
Qed.

(* Thread is not universal. *)
Lemma ThreadNotUniversal: ~ (isUniv Thread).
Proof.
  unfold not.
  intro H.
  eapply univChildNotNone with (t := Thread) (a := false).
  auto.
  unfold Thread, child.
  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) &lt;-&gt; 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.
</code></pre>

CC BY-SA 2.5
2010-09-04T09:06:05.207Z
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
CC BY-SA 2.5
2010-09-04T16:54:58.287Z
Well, I am not embarrassed by my response :-) I thought I might as well give a comprehensive response if I give one.
Andrej Bauer
CC BY-SA 2.5
2010-09-04T22:41:33.650Z
Your response was embarrassing for me. But certainly highly appreciated.
Dave Clarke
CC BY-SA 2.5
2010-09-05T10:59:40.090Z
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
CC BY-SA 2.5
2010-09-04T05:46:05.910Z
2010-09-04T08:15:12.603Z
2010-09-04T08:15:12.603Z
Andrej Bauer
<p>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. </p>

<p>The type <strong>Tree</strong> defines possibly infinite trees with branches labelled with elements of type <em>A</em>. A branch need not be defined for all elements of <em>A</em>. The value <em>Univ</em> is the infinite tree with all <em>A</em> branches always defined. <em>isUniv</em> tests whether a given tree is equal to the <em>Univ</em>. The lemma states that <em>Univ</em> does indeed satisfy <em>isUniv</em>.</p>

<pre><code>Parameter A : Set.

CoInductive Tree: Set := Node : (A -&gt; option Tree) -&gt; Tree.

Definition derv (a : A) (t: Tree): option Tree :=
  match t with Node f =&gt; f a end.

CoFixpoint Univ : Tree := Node (fun _ =&gt; Some Univ).

CoInductive isUniv : Tree -&gt; Prop :=
  isuniv : forall (nf : A -&gt; option Tree) (a : A) (t : Tree), 
    nf a = Some t -&gt; 
    isUniv t -&gt; 
    isUniv (Node nf).

Lemma UnivIsUniv : isUniv Univ.
Proof.
  cofix CH.    (* this application of cofix is fine *)
  unfold Univ. 

Admitted.
</code></pre>

<p>At this point I give up the proof. The current goal is:</p>

<pre><code>CH : isUniv Univ
============================
isUniv (cofix Univ  : Tree := Node (fun _ : A =&gt; Some Univ))
</code></pre>

<p>I do not know which tactic to apply to eliminate the <strong>cofix</strong> in the goal to produce <strong>(Node something)</strong> so that I can apply <strong>isuniv</strong>. </p>

<p>Can anyone help prove this lemma?<br>
What are the standard ways of eliminating <strong>cofix</strong> in such a situation?</p>

CC BY-SA 2.5
2010-09-01T22:34:27.987Z
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
CC BY-SA 2.5
2010-09-02T06:51:20.077Z
Fixed, using "proof-assistants"
Dave Clarke
<coq><proof-assistants>
Eliminating cofix in Coq proof
Dave Clarke
# Eliminating cofix in Coq proof

(Asked by: username_0 on 2010-09-01)

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?

**Tags:** coq, proof-assistants

> **Comments:**
> **username_1**: 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".  
> **username_0**: Fixed, using "proof-assistants"  

---

## 2 answers

### Answer by username_2 on 2010-09-02. Score: 6 | Accepted answer

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))))

I adapted this technique from http://adam.chlipala.net/cpdt/html/Coinductive.html

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_3 on 2010-09-04. Score: 9

(* 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. *)
Lemma ThreadHasInfinitePath : hasInfinitePath Thread.
Proof.
  cofix H.
  rewrite TTid.
  unfold TT.
  unfold Thread.
  (* 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. *)
Lemma ThreadNotUniversal: ~ (isUniv Thread).
Proof.
  unfold not.
  intro H.
  eapply univChildNotNone with (t := Thread) (a := false).
  auto.
  unfold Thread, child.
  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.

> **Comments:**
> **username_0**: 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.  
> **username_3**: Well, I am not embarrassed by my response :-) I thought I might as well give a comprehensive response if I give one.  
> **username_0**: Your response was embarrassing for me. But certainly highly appreciated.  
> **username_3**: 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.  

---

