Email Gateway (Aug 22 2022 at 11:37): Email Gateway (Aug 22 2022 at 11:37):From: Johannes Hölzl <hoelzl@in.tum.de>
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
Email Gateway (Aug 22 2022 at 11:38):From: Alfio Martini <alfio.martini@acm.org>
Hi Johannes,
If you just want to have induction which follows the rewrite steps of
Email Gateway (Aug 22 2022 at 11:43):From: Alfio Martini <alfio.martini@acm.org>
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!
Email Gateway (Aug 22 2022 at 11:43):From: Johannes Hölzl <hoelzl@in.tum.de>
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,
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 thatP(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)
doneTwo 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!
Email Gateway (Aug 22 2022 at 11:44):From: Alfio Martini <alfio.martini@acm.org>
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
Last updated: Apr 24 2024 at 08:20 UTC