The Coq mailing list

["Vladimir Komendantsky" <komendantsky AT gmail.com>]

Let me remind the relaxed termination relation:

Inductive terminates_with (A:Set) : Delay A -> A -> Prop :=
  | terminates_now_with : forall a:A, terminates_with (Now a) a
  | terminates_later_with : forall (a a':A) (d:Delay A), (terminates_with d a) ->
      terminates_with (Later d) a.

I did try to weaken termination to a terminated_with relation, but I still get stuck. Vladimir, why do you think it might help?

Because you need the result of [fac n] as a plain value and not as a monadic one. This is because you don't prove continuity of lfp in your development. Can you prove the equality in [facSn] below? If not, see 3.1 in [Cristine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq] for an example how to define a flat order on your [Delay A]. You will still be able to prove a weaker equivalence relation derived from this flat order: x == y := x<=y /\ y<=x.

Lemma fac0 : fac 0 = Now 1.
rewrite (unfold_delay_id 1 (fac 0)); reflexivity.
Qed.

Lemma facSn : forall n m, terminates_with (fac n) m ->
  fac (S n) = Now ((S n) * m).
Admitted.

Lemma fac_terminates_with : forall (n:nat), exists m, terminates_with (fac n) m.
intros.
induction n.
  (* base case *)
rewrite fac0.
exists 1.
constructor.
  (* inductive step *)
destruct IHn as [m Hfacn].
exists ((S n) * m).
rewrite (facSn n Hfacn).
constructor.
Qed.


All the best,
V