Email Gateway (Aug 18 2022 at 15:04): Email Gateway (Aug 18 2022 at 15:04):From: Andrei Borac <zerosum42@gmail.com>
I am looking for someone who will answer these kinds of beginner
questions for pay. I am thinking something like $10 / question,
payment would be over paypal or similar. This does not constitute an
offer to pay $10 for an answer to this particular question. If you are
interested in answering questions for pay, please contact me and we'll
figure out some basic terms.
Ok, so I'm trying to get started. So far I've only been doing things
that can be proven by auto. Now I'm trying induction and things aren't
working. I'm trying to prove that "successor" can be "factored" out of
add:
datatype n =
Z
| S n
primrec add :: "n => n => n"
where
"(add x Z) = x"
| "(add x (S y)) = (add (S x) y)"
lemma desired: "!!y. !!x. ((add x (S y)) = (S (add x y)))"
I can write out the steps of the induction I'm trying to do:
!!x. add x sz = add sx z = s (add x z) # this is the base case y=Z
!!x. add x ssz = add sx sz = s (add sx z) = s (add x sz)
!!x. add x sssz = add sx ssz = s (add sx sz) = s (add x ssz)
So the general idea is to do a "forward step" (where an s is shifted
left), an "inductive step" and a "backward step" (where an s is
shifted right). The base case and the inductive step can be proven
with auto:
lemma bascase: "(!!x. (add x (S Z)) = (S (add x Z)))"
apply(auto)
done
lemma indstep [simp]: "(!!x. (add x (S y)) = (S (add x y))) ==> (!!x.
(add x (S (S y))) = (S (S (add x y))))"
apply(auto)
done
However, if I try to apply induct_tac on the desired lemma:
lemma desired: "!!y. !!x. ((add x (S y)) = (S (add x y)))"
apply(induct_tac y)
apply(auto)
I get:
proof (prove): step 2
goal (1 subgoal):
This is not what I want. My induction is based on !!y (!!x p(x,y)) ->
(!!x p'(x,y)) but what it is asking me to prove is !!y !!x (p(x,y) ->
p'(x,y)). How do I get back on track?
-Andrei
Email Gateway (Aug 18 2022 at 15:04):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Andrei Borac wrote:
I think this is not the right inductive step, but that you want
(add x (S (S y))) = (S (add x (S y)))
In any event, given this problem, you should have not declared your
inductive step
as [simp]. Then, after doing the induct_tac step, you would see what
the required lemmas are.
Regards,
Jeremy
Email Gateway (Aug 18 2022 at 15:04):From: Andrei Borac <zerosum42@gmail.com>
Well, I have solved this particular problem. Still looking for someone
to answer questions (starting with "what is the difference between
induct and induct_tac" ...).
-Andrei
datatype n =
Z
| S n
primrec add :: "n => n => n"
where
"(add x Z) = x"
| "(add x (S y)) = (add (S x) y)"
lemma desired: "!!x. ((add x (S y)) = (S (add x y)))"
apply(induct y)
apply(auto)
done
Email Gateway (Aug 18 2022 at 15:04):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Andrei,
You've got the problem on your hands that you've got some variables
bound in the lemma itself, which doesn't work well with induct_tac. When
I was taught to do this for induction, I was told these rules of thumb:
if you use induct_tac, use \<forall> (!) and --> (object
quantification and object implication)
if you use induct, use \<And> (!!) and ==> (meta quantification and
meta implication)
Also, when you do an induction proof, you might want to leave the
variable you're inducting over free. With your example (shortened for
the email):
datatype n = Z | S n
primrec add :: "n => n => n" where
"add x Z = x"
| "add x (S y) = add (S x) y"
lemma simple_desired: "\<And>x. add x (S y) = S (add x y)"
by (induct y, simp_all)
lemma desired: "\<And>x y. add x (S y) = S (add x y)"
by (rule simple_desired)
As far as I can see, these two lemmas are identical after you prove them.
A more exploratory way with a lot more steps which maybe illustrates the
problem a bit better for you:
lemma desired: "add x (S y) = S (add x y)"
proof (induct y arbitrary: x)
fix x
show "add x (S Z) = S (add x Z)" by simp
next
fix y x
assume IH: "\<And>x. add x (S y) = S (add x y)"
hence "add (S x) (S y) = S (add (S x) y)" .
thus "add x (S (S y)) = S (add x (S y))" by simp
qed
Note that induct will be happy if the "y" in the lemma is bound. If x is
bound we don't need the "arbitrary: x".
Finally, a personal observation: there's no need to meta-quantify
variables in top-level proofs. Usually you get problems because
variables are fixed (hence the "arbitrary: x" above). When you prove a
top-level lemma they become schematic variables, which can already be
substituted with anything.
Anyway, I hope this helps,
Rafal Kolanski.
Andrei Borac wrote:
Email Gateway (Aug 18 2022 at 15:04):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi there,
first of all, save your money :), answers on this list are for free.
Your example works with
datatype n = Z | S n
primrec add :: "n => n => n" where
"add x Z = x" |
"add x (S y) = add (S x) y"
lemma desired: "add x (S y) = S (add x y)"
by (induct y arbitrary: x) simp_all
The "trick" is generalization over x (otherwise the IH does only hold
for the specific x in the lemma and not for all x's). You could do the
same thing by stating your lemma as:
lemma desired: "ALL x. add x (S y) = S (add x y)"
And then doing an induction prove over y.
cheers
chris
Email Gateway (Aug 18 2022 at 15:04):From: Andrei Borac <zerosum42@gmail.com>
Wow, thanks everyone, lots of good info. So far I am impressed with
proofgeneral/isabelle/hol (have just finished doing the commutativity
of add). Especially Rafal Kolanski's detailed proof I will have to go
over carefully. Might take a while ;-)
-Andrei
Email Gateway (Aug 18 2022 at 15:05):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Feel free to ask questions about it, it's only there to show you more
internal steps of what's going on. The simple proof in my email is more
than adequate for the task and is, in fact, identical to Christian's.
Christian's explanation is better than mine, I think. Less rambling,
straight to the point. It's a shame we don't get to see each other's
posts until the next round of moderation ;)
Anyway, I'm glad you got your problem sorted.
Sincerely,
Rafal Kolanski.
Andrei Borac wrote:
Last updated: Apr 30 2024 at 04:19 UTC