Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: "Luke Palmer" <lrpalmer AT gmail.com>
  • To: "Vladimir Komendantsky" <komendantsky AT gmail.com>
  • Cc: "Edsko de Vries" <devriese AT cs.tcd.ie>, "Agda mailing list" <agda AT lists.chalmers.se>, coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad
  • Date: Mon, 17 Nov 2008 18:00:57 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=EipoyF5JaibsNc/7hKtQVOkgTNlUd0CWy/msi5PRRlSbbD4ibqLCaqSMRahc10MovQ AU3d2pFhQtBuEzZQ6DYJNseEvpH+bAaEMCJpS4DmrdBrKTFILzHtRPe1TzVmQApeGpYh 9KxypolD6253jqtGnzeMxAP8gz550l5zHoyjo=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
>
>



Archive powered by MhonArc 2.6.16.

Top of Page