15
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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". $\endgroup$ – Iddo Tzameret Sep 1 '10 at 22:34
  • $\begingroup$ Fixed, using "proof-assistants" $\endgroup$ – Dave Clarke Sep 2 '10 at 6:51
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Dave Clarke Sep 2 '10 at 15:02
9
$\begingroup$
(* 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.
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Dave Clarke Sep 4 '10 at 9:06
  • $\begingroup$ Well, I am not embarrassed by my response :-) I thought I might as well give a comprehensive response if I give one. $\endgroup$ – Andrej Bauer Sep 4 '10 at 16:54
  • $\begingroup$ Your response was embarrassing for me. But certainly highly appreciated. $\endgroup$ – Dave Clarke Sep 4 '10 at 22:41
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 5 '10 at 10:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.