The Coq mailing list

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

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.