The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>]

Hi Pierre,
 thank you for your answer.
Yes, replacing the mutual definition with a function works, but I was 
wandering what's wrong with the "CoFixpoint ... with ..." construction.
It seems to be a problem with the reduction tactics: If you give the 
proof of the unfolding lemma directly instead of using tactics, you 
don't get any error. See the attached file.

To Frederic: the problem doesn't seem to be related with the fact that 
you don't get the correct induction principle for mutual inductive 
types, since here you define mutual functions, not types.

Cheers,
 Venanzio

--
Venanzio Capretta
Department of Mathematics
          and Statistics
University of Ottawa, Canada
http://www.science.uottawa.ca/~vcapr396/


CoInductive tree: Set :=
  leaf: tree
| node: tree -> tree -> tree.


Definition tree_decomp (t:tree): tree :=
match t with
  leaf => leaf
| (node t1 t2) => node t1 t2
end.

Lemma tree_decompose: forall (t:tree), t = tree_decomp t.
Proof.
intro t; case t; trivial.
Qed.

CoInductive Infinite: tree -> Prop :=
  Inf_l: forall (t1 t2:tree), Infinite t1 -> Infinite (node t1 t2)
| Inf_r: forall (t1 t2:tree), Infinite t2 -> Infinite (node t1 t2).

CoFixpoint inf_l: tree := node inf_r leaf
      with inf_r: tree := node leaf inf_l.


Lemma inf_l_unfold: inf_l = node inf_r leaf.
Proof eq_ind_r (fun t : tree => t = node inf_r leaf)
               (refl_equal (node inf_r leaf))
               (tree_decompose inf_l).

Lemma inf_r_unfold: inf_r = node leaf inf_l.
Proof eq_ind_r (fun t : tree => t = node leaf inf_l)
               (refl_equal (node leaf inf_l))
               (tree_decompose inf_r).

Lemma Infinite_lr:
  forall t:tree, t=inf_l \/ t=inf_r -> Infinite t.
Proof.
cofix H; intros t Ht; case Ht; intro H1; rewrite H1.
rewrite inf_l_unfold; apply Inf_l; apply H; auto.
rewrite inf_r_unfold; apply Inf_r; apply H; auto.
Qed.