The Coq mailing list

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

Hi,
 When I define two terms by mutual corecursion, I seem to get the wrong 
reductions when doing the proofs and strange errors at the end of the proof.
In the attached example I define a coinductve type of binary trees and 
then two trees by mutual corecursion:
 inf_l = node inf_r leaf
 inf_r = node leaf inf_l

When I try to prove something about them, inf_l is unfolded not as (node 
inf_r leaf) as expected, but as (node inf_l leaf), which is wrong.
Fortunately (?!) at the end of a proof that exploits this wrong 
unfolding, Coq rejects the final term.
Notice that the proof of inf_l_unfold is not by coinduction, so I expect 
that when I have the message "Proof completed." I can "Qed" safely. 
Instead I get a type-checking error.

This appears to be a bug in the implementation of "CoFixpoint ... with ...".
Is there a way around it?

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.

(* I shouldn't be able to prove this. *)
Lemma inf_l_unfold: inf_l = node inf_l leaf.
Proof.
pattern inf_l at 1.
rewrite tree_decompose.
simpl.
trivial.
Qed.

(* Why is the final proof rejected? *)
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 tree_decompose; simpl;
  [apply Inf_l | apply Inf_r]; apply H; auto.
Qed.