The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Jason,

That's because Coq is checking if [loop] is a legal recursive argument 
for a constructor, but in the wrong type, here [CoFalse] instead of 
[Pandora].

This is the reason why I said I was not sure if it was an implementation 
bug or something deeper. However, the second variation does not rely on 
the same behavior, I believe. More precisely, even fixing this bug, 
Omega would still have a legitimate recursive argument.

Maxime.

On 02/27/2014 12:12 AM, Jason Gross wrote:
> I thought that your extra CoFalse argument to CF was redundant, so I 
> tried removing it.  Then I got
>
> Error:
> Recursive definition of loop is ill-formed.
> In environment
> loop : CoFalse
> Recursive call on a non-recursive argument of constructor
> "loop".
> Recursive definition is:
> "match foo in (_ = T) return T with
>  | eq_refl => C loop
>  end".
>
>
> What does this mean?  Does Coq somehow think that "loop" is a 
> constructor?  And why is whether or not "loop" is valid for a 
> recursive call dependent on whether or not there's a dummy CoFalse 
> hypothesis of CF?
>
> -Jason
>
>
> On Wed, Feb 26, 2014 at 11:56 PM, Maxime Dénès <mail AT maximedenes.fr 
> <mailto:mail AT maximedenes.fr>> wrote:
>
>     Hello there,
>
>     As some of you may have been expecting, episode two is out. This
>     time featuring co-inductive types!
>
>     
> ---------------------------------------------------------------------------------
>     CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse.
>
>     CoInductive Pandora : Prop := C : CoFalse -> Pandora.
>
>     Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q.
>
>     Lemma foo : Pandora = CoFalse.
>     apply prop_ext.
>     constructor.
>     intro x; destruct x; assumption.
>     exact C.
>     Qed.
>
>     CoFixpoint loop : CoFalse :=
>     match foo in (_ = T) return T with eq_refl => C loop end.
>
>     Definition ff : False := match loop with CF _ t => t end.
>     
> ---------------------------------------------------------------------------------
>
>     I am still not sure if this is an implementation bug of the guard
>     for cofixpoints or something more fundamental.
>
>     Below is a variation done with Arthur Azevedo de Amorim (requires
>     some of the definitions above):
>
>     
> ---------------------------------------------------------------------------------
>     Inductive omega := Omega : omega -> omega.
>
>     Lemma H : omega = CoFalse.
>     Proof.
>     apply prop_ext; constructor.
>       induction 1; assumption.
>     destruct 1; destruct H0.
>     Qed.
>
>     CoFixpoint loop' : CoFalse :=
>       match H in _ = T return T with
>         eq_refl =>
>         Omega match eq_sym H in _ = T return T with eq_refl => loop' end
>       end.
>
>     Definition ff' : False := match loop' with CF _ t => t end.
>     
> ---------------------------------------------------------------------------------
>
>     We'll work on a fix before the next Coq release.
>
>     Maxime.