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

```Hi Johannes,

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.

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.