*To*: Johannes HÃlzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Induction on the length of computation sequences (in Isabelle)*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Wed, 28 Oct 2015 10:51:21 -0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1446030574.2334.221.camel@in.tum.de>*References*: <CAAPnxw1+xhX7NG5EK8pbqrWo6chi0h-vcOUeLUZ1-fNdKDNhmQ@mail.gmail.com> <1444641081.12063.21.camel@in.tum.de> <CAAPnxw2Kz-N10_aUmsvfTUzKTDbw3vU-21dCUBbNJBCnd-PT1A@mail.gmail.com> <1446030574.2334.221.camel@in.tum.de>*Sender*: alfio.martini at gmail.com

Hi Johannes, If you just want to have induction which follows the rewrite steps of > your function, then use the induction rule by the fun-package. > > with this you can even show equality with Q: >> > Yes, this is it. What I wanted is an induction on the length of the rewrite steps of the function, which is just what computation induction provides. For some unknown reason, I was not convinced about that before. But shortly after, I realized that this is exactly what I wanted. In the case of this simple example, even the standard induction method would do the job. Best! On Wed, Oct 28, 2015 at 9:09 AM, Johannes HÃlzl <hoelzl at in.tum.de> wrote: > Hi Alfio, > > I'm still not sure why you insist on the length of the computation > sequence. Do you want to reason about the _runtime complexity_ of your > algorithm? Then you need to model "time" explicitly, and you need > semantics handling time. > > If you just want to have induction which follows the rewrite steps of > your function, then use the induction rule by the fun-package. > > with this you can even show equality with Q: > > lemma "tail_multn m n a = r = Q(m,n,a,r)" > by (induction m n a rule: tail_multn.induct) auto > > > - Johannes > > Am Montag, den 12.10.2015, 15:38 -0300 schrieb Alfio Martini: > > Hi Johannes, > > > > > > Thank you for your feedback. > > > > > > I wanted actually to perform induction on the length of computation > > sequences of the tail recursive > > > > function, so I chose to use the rule f.induct. But I was not really > > sure if using that that rule I > > > > was really doing this kind of induction. So I decided to make an > > explicit definition of > > > > the tail function as an inductive set of quadruples. This time I was > > more convinced that I was > > > > performing induction on the the length of the computation sequences. > > But maybe this > > > > was the ugly way. I am not sure. > > > > > > I will be glad to receive more comments about this. This is the > > alternative code, defining > > > > the multiplication as an inductive predicate. > > > > inductive > > imultn :: "nat x nat x nat x nat => bool" > > where > > base : "imultn(0,n,a,a)" | > > ind : "imultn(m, n, a+n, value) ==> imultn(Suc m,n,a,value)" > > > > > > fun Q::"nat x nat x nat x nat =>bool" where > > "Q(x,y,z,w) = (x*y+z = w)" > > > > lemma "imultn(m,n,a,r) ==>Q(m,n,a,r)" (* consistency *) > > proof (induct rule:imultn.induct) > > fix n a > > show "Q(0,n,a,a)" by simp > > next > > fix m n a v > > assume h1: "imultn(m,n,a+n,v)" > > assume h2: "Q(m,n,a+n,v)" > > show "Q(Suc m, n,a,v)" > > proof - > > from h2 have "m*n+(a+n)=v" by simp > > then have "m*n+n +a=v" by simp > > then have "(m+1)*n+a=v" by simp > > then show ?thesis by simp > > qed > > qed > > > > lemma "Q(m,n,a,r) ==> imultn(m,n,a,r)" (* completeness *) > > proof (induction m arbitrary:n a r) > > fix n a r > > assume h:"Q(0,n,a,r)" > > show "imultn(0,n,a,r)" > > proof - > > from h have "a=r" by simp > > have "imultn(0,n,a,a)" by (rule base) > > then show ?thesis using h by simp > > qed > > next > > fix m n a r > > assume IH:" /\ i n a r. Q (m, n, a, r) ==>imultn (m, n, a, r)" > > assume h2: "Q (Suc m, n, a, r)" > > show "imultn (Suc m, n, a, r)" > > proof (rule ind) > > from h2 have "m*n + (n+a) = r" by simp > > then have "Q(m,n,a+n,r)" by simp > > then show "imultn(m,n,a+n,r)" using IH by simp > > qed > > qed > > > > > > fun tail_multn::"nat => nat => nat => nat" where > > "tail_multn 0 n a = a" | > > "tail_multn (Suc m) n a = tail_multn m n (a+n)" > > > > lemma "tail_multn m n a = r ==> Q(m,n,a,r)" > > apply(induction m n a rule:tail_multn.induct) > > apply (simp) > > apply(simp) > > done > > > > > > On Mon, Oct 12, 2015 at 6:11 AM, Johannes HÃlzl <hoelzl at in.tum.de> > > wrote: > > Hi Alfio, > > > > To answer your two questions: > > > > > 1) Is this a correct way to encode a proof of an invariant > > of a tail > > > recursive function? > > > > Yes, to use the induction-scheme by the function method is the > > usual way > > in Isabelle/HOL. of course, the induction-scheme is > > independent of the > > function itself: you can use other induction-schemes (like > > nat_induct), > > and you can also use the induction scheme tail_multn.induct to > > prove > > theorems no involving tail_multn. > > > > > 2) Is there a more elegant way to approach this problem? > > > > I find it quite elegant. Do you have anything more elegant in > > mind? > > Obviously, if you have more specific theorems to prove you > > might use a > > different approach. > > > > Btw, sometimes when defining tail-recursive functions the > > function-package is not enough and you might want to use > > partial_function. > > > > Greetings, > > - Johannes > > > > Am Freitag, den 09.10.2015, 14:46 -0300 schrieb Alfio Martini: > > > Dear Users, > > > > > > Whenever I want to (manually) prove that an invariant of a > > tail recursive > > > function is true, > > > I perform induction on the length of computation sequences. > > For instance, > > > consider the following > > > example: > > > > > > fun tail_multn::"nat => nat => nat => nat" where > > > "tail_multn 0 n a = a" | > > > "tail_multn (Suc m) n a = tail_multn m n (a+n)" > > > > > > Thus, a state s_ k (0<=k<=n) for a computation of this > > function is a triple > > > s_k=(m_k,n_k,a_k) in nat x nat x nat. > > > Now, using induction on k, I can prove that > > > > > > P(k)=def all m,n,a:nat. tail_multn m n a = m_k*n_k+ a_k > > > > > > The only way I was able to encode this proof in Isabelle was > > using > > > computation induction, > > > after reading carefully the presentation of this material in > > "Programming > > > and Proving". > > > > > > So, my proof in Isabelle is given by: > > > > > > lemma "tail_inv": "tail_multn x y a = x*y +a" > > > apply (induction x y a rule: tail_multn.induct) > > > apply (simp_all) > > > done > > > > > > Two questions: > > > > > > 1) Is this a correct way to encode a proof of an invariant > > of a tail > > > recursive function? > > > 2) Is there a more elegant way to approach this problem? > > > > > > Best! > > > > > > > > > > > > > > > > > -- > > Alfio Ricardo Martini > > PhD in Computer Science (TU Berlin) > > Associate Professor at Faculty of Informatics (PUCRS) > > www.inf.pucrs.br/alfio > > Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica > > 90619-900 -Porto Alegre - RS - Brasil > > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**References**:**[isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Alfio Martini

**Re: [isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Johannes Hölzl

**Re: [isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Alfio Martini

**Re: [isabelle] Induction on the length of computation sequences (in Isabelle)***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Document Preparation System - Windows
- Next by Date: [isabelle] Programming Languages Meeting (S-REPLS 2) at Middlesex University London, Nov 20th
- Previous by Thread: Re: [isabelle] Running Isabelle in batch mode
- Next by Thread: [isabelle] Mirroring Isabelle
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list