[Coq-Club] Re: [Agda] Termination proof in partiality monad

[Vladimir Komendantsky]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081117/f99c7fe5/attachment.html