The Coq mailing list

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

In fact, if we'd keep the coinductive definition of "halts", we could  
prove
that the infinite repetition of NotYet halts :-(

Pierre


CoInductive sigma : Set :=
 | Finished : sigma
 | NotYet : sigma -> sigma.

(* should be Inductive *)

CoInductive halts : sigma -> Prop :=
 | isFinished : halts Finished
 | isNotYet : forall x : sigma, halts x -> halts (NotYet x).


CoFixpoint loopsforever : sigma :=
 NotYet(loopsforever).


Definition sigma_decompose (l:sigma) : sigma :=
 match l with Finished => Finished
            | NotYet l' => NotYet l'
 end.

Lemma sigma_dec_lemma : forall l, l= sigma_decompose l.
destruct l;auto.
Qed.


Lemma L: halts(loopsforever).
 cofix.
rewrite (sigma_dec_lemma loopsforever).
simpl.
constructor.
auto.
Qed.