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

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

```

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