Re: [isabelle] can't hack induction



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

On Tue, Apr 13, 2010 at 2:04 AM, Christian Sternagel
<christian.sternagel at uibk.ac.at> wrote:
> 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
>
>
> On 04/13/2010 03:20 AM, Andrei Borac wrote:
>>
>> 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):
>>  1. !!x n. add (S x) n = S (add x n) ==>  add (S (S x)) n = S (S (add x
>> n))
>>
>> 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
>>
>
>





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