The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

This is probably way too simplistic, and if so, I apologise :) but why
is 'halts' CoInductive? If you make 'halts' Inductive, then your proof
becomes trivial:

CoInductive sigma : Set :=
  | Finished : sigma
  | NotYet : sigma -> sigma.

Inductive halts : sigma -> Prop :=
  | isFinished : halts Finished
  | isNotYet : forall x : sigma, halts x -> halts (NotYet x).

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.

Lemma continuity :
  forall p : sigma, halts p -> exists n : nat, haltsWithin n p.
Proof.
  induction 1 ; intros.
  exists (S 0) ; simpl ; auto.
  elim IHhalts ; intros n ?.
  exists (S n) ; simpl ; auto.
Qed.

(By the way, presumably you know of the Delay monad? Very similar to
your 'sigma' type).

Edsko