# Re: [isabelle] Induction on the length of computation sequences (in Isabelle)

```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.
> >
> >
> > 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,
> >
> >
> >         > 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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.