The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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> 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.