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



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



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