The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon 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?
>

Hi Venanzio,

  Yes, it seems to be a problem with the CoFixpoint ... with construct.
  Your example works perfectly if you replace the mutual cofixpoint
  with a function with a boolean parameter :

CoFixpoint zigzag (b:bool) :tree :=
 if b then node (zigzag false) leaf
      else node leaf (zigzag true).

Lemma unfold_l : zigzag true = node (zigzag false) leaf.
Proof.
  rewrite (tree_decompose (zigzag true)).
  simpl.
  trivial.
Qed.

 Lemma Infinite_lr : forall b, Infinite (zigzag b).
 cofix H.
 intro b; case b; rewrite tree_decompose; simpl.
 constructor 1.
 auto.
 constructor 2;auto.
Qed.

 Notice that with Coq 8.0pl2, The first lemma :

(* 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.
apply refl_equal.

 Could not be proved (an error message occurred at the tactic call
"apply refl_equal").


Cheers,
Pierre





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


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.