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

[Luke Palmer]

On Mon, Nov 17, 2008 at 4:10 PM, Vladimir Komendantsky
<komendantsky at gmail.com> wrote:
> Lemma facSn : forall n m, terminates_with (fac n) m ->
>   fac (S n) = Now ((S n) * m).
> Admitted.

Of course this will do it, because it is false!

fac 3 = Later (Later (Later (Now 6)))

Luke

> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>