Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Continuity of coinductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Continuity of coinductive definitions


chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: Andrej.Bauer AT andrej.com, Coq Mailing List <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Continuity of coinductive definitions
  • Date: Mon, 18 Feb 2008 15:52:53 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.





Archive powered by MhonArc 2.6.16.

Top of Page