Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Continuity of coinductive definitions


chronological Thread 
  • 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
*)





Archive powered by MhonArc 2.6.16.

Top of Page