The Coq mailing list

[Andrej Bauer <Andrej.Bauer AT fmf.uni-lj.si>]

(*
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
*)