coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrej Bauer <Andrej.Bauer AT fmf.uni-lj.si>
- To: Coq Mailing List <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Continuity of coinductive definitions
- Date: Mon, 18 Feb 2008 15:14:08 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
(*
I apologize if this is an FAQ. Consider these definition. I am putting the text of this message in comments so that you can just cut and paste into Coq:
*)
CoInductive sigma : Set :=
| Finished : sigma
| NotYet : sigma -> sigma.
(*
We can think of type sigma as consisting of elements of the form:
Finished
NotYet Finished
NotYet (NotYet Finished)
NotYet (NotYet (NotYet Finished))
...
NotYet (NotYet (NotYet (...)) (* not yet forever *)
These might represent the running time of a machine, where the last one represents a machine that never halts. We define the coinductive predicate:
*)
CoInductive halts : sigma -> Prop :=
| isFinished : halts Finished
| isNotYet : forall x : sigma, halts x -> halts (NotYet x).
(*
Presumably, it is safe to imagine that "halts p" means that p is a finite number of nestings of NotYet which end with a Finished. To verify that this is really the case, we define a predicate "haltsWithin n p" which says that p halts within n steps.
*)
Fixpoint haltsWithin (n : nat) (p : sigma) {struct n} : Prop :=
match n with
| O => False
| S m =>
(match p with Finished => True | NotYet q => haltsWithin m q end)
end.
(*
But now I get stuck trying to prove the lemma which would confirm my expectations:
*)
Lemma continuity :
forall p : sigma, halts p -> exists n : nat, haltsWithin n p.
(*
It looks like I am hitting against a classical "trick" in Coq. How do I relate the coinductive nature of sigma to the inductive nature of nat?
I can actually imagine that the lemma is not provable without further assumptions. If this is the case, a model-theoretic explanation would
help.
Best regards,
Andrej
*)
- [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.