coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Continuity of coinductive definitions, Andrej Bauer
- Re: [Coq-Club] Continuity of coinductive definitions, Adam Chlipala
- Re: [Coq-Club] Continuity of coinductive definitions,
Edsko de Vries
- Re: [Coq-Club] Continuity of coinductive definitions, Pierre Casteran
- Re: [Coq-Club] Continuity of coinductive definitions, Andrej Bauer
Archive powered by MhonArc 2.6.16.