Proof by induction... I don't geddit.

[HarryW]

Does anybody understand this?...



Given the following term signature:

sorts    NAT
ops      zero:	NAT
         succ:	NAT->NAT

+ops     plus:	NAT,NAT->NAT
+defns   (x, y: NAT)
         plus(zero, x) = x
         plus(succ(y), x) = succ(plus(y, x)

Prove that the quotient term structure is associative,

ie. plus(plus(x, y), z) = plus(x, plus(y, z)) for all terms x, y, z.


I am having a lot of trouble with this proof by induction business. Has anyone come across it before?



[Edited by HarryW on 11-05-2000 at 10:30 PM]

[kedaman]

can you explain what does succ, NAT and zeroes mean? I understand the associative rule but i don't even know what the problem is

and i forgot:

[HarryW]

Well, succ(x) is like (x+1), NAT is a data type (a sort) which in this case is analogous to the natural numbers (non-negative integers), and zero is an operator (like a function) which take no parameters and returns a constant value. Zero is basically a constant.

I'm not really sure why we're doing this, it's a bit like number theory for data types, but this particular part of the course I'm doing is about proof by induction. I have to prove that plus(plus(zero, y), z) = plus(zero, plus(y, z)) and also that plus(plus(succ(a), y), z) = plus(succ(a), plus(y, z)).

[kedaman]

Well if you first prooved plus is commutative you could proove its associative next.

but i'm not sure how you can get proof of this at all, maybe by defining addition or soemthing?

[HarryW]

Well, I seem to have already proven that it's assosiative now, and I now have to prove that it's commutative ....anyway I've got at least 3 hours before it has to be handed in - plenty of time

[Sam Finch]

I'll try to explain proof by Induction to you, using a great example with Robin Reliants. (a classic car with only 3 wheels)

The key thing you need to know about Robin Reliants is they have no reverse pedal, ie they can go forwards, but not backwards.


Imagine a Robin Reliant drives up to a wall, so its front bumper touches the wall, it can't go forwards because the wall is in the way, it can't go backwards because it's a Robin Reliant, hence it can't move, if a Robin Reliant can't move we say it is *****ed.

now Imagine a Whole line of Robin Reliants driving bumper to bumper, the first car parks up against a wall, with it's front bumper touching the wall , all the other cars have their front bumpers touching the back bumper of the car in front. Prove that they're all *****ed.


We will prove this by induction.

define the statement P(n), P(n) is true iff the nth car in the line is *****ed.

P(1), the first car has it's bumper up against a wall, by the axiom above it is *****ed, so P(1) is true.


now assume P(k) for some k

the k+1th car has it's bumper up against the kth car, P(k) is true so the kth car is *****ed and can't move. hence the k+1th car can't go forwards, and it can't go backwards because it's a Robin Reliant, so it's *****ed.

Hence P(k+1) is true if P(k) is true
ie P(k) => P(k+1)


we know P(1) is true, so P(2) must be true
we know P(2) is true, so P(3) must be true
we know P(3) is true, so P(4) must be true


we can continue this for as bigger n as we like, so for all n P(n) is true, and hence all the Robin Reliants are *****ed.


that is essentiall ywhat induction is, you prove a theory is true for a particular case, which is easy because you just have to work the sum out, then you prove that if it's true for the kth example it's true for the k+1th example, and so you've proved it for them all.

the example you have looks like it needs 2 inductions, these are the steps you need

1. Show the proposition P(1,1) is true
2. Use an induction to show that P(y,1) is true for all y
3. use a second induction to show that P(y,z) is true

where P(y,z) are the propositions you have to prove.

[HarryW]

Thanks Sam, that has helped clear it up a bit, but that's the bit I more or less understood already. By the way I handed this i this morning with some bullshit written on it, which seemed to be very similar to other people's bullshit so there's a chance of some marks I would definitely still like to understand this though.

What I am having trouble with is the way each case is proven and then the inductive step which we prove that (in this case) the hypothesis holds for succ(a). To try and clarify, I'll type out my supposed proof here:

RTP: plus(x,y) = plus(y, x) for all terms x, y
     (ie. plus is commutative)

base case: x=zero
	
	use induction, for the second argument, over all terms y not involving plus
		base case: y=zero
			plus(zero, zero) = zero  (using def[1])
		
		inductive step: y=succ(s')
			whenever s' does not involve plus and plus(zero, s')=plus(s', zero)
			then plus(zero, y)=y  (using def [1])
			                  =??? (more steps needed?)
			                  =plus(y, zero)
	Thus plus(zero, y)=plus(y, zero) for all terms y which do not involve plus.

Inductive step: x=succ(s)
	whenever plus(s, y)=plus(y, s) for all terms y which do not involve plus
	then use induction, for the second argument, over all terms y not involving plus.

		base case: y=zero
			plus(x, zero)=plus(zero, x)   (already proven above)

		inductive step: y=succ(s')
			whenever plus(succ(s), s')=plus(s', succ(s))

			then plus(x, y)=plus(succ(s), succ(s'))
			               = ??? (more steps here)
			               =plus(y, x)

	This completes the proof that plus(succ(s), y)=plus(y, succ(s))

And so completes the proof by induction of
plus(x, y)=plus(y, x) for all terms x and y which do not involve plus.

Now I have put some of the previously mentioned bullshit into the ??? gaps there, but I am fairly confident that it's wrong. For the second bit I think I wrote something like this:

plus(x, y) = plus(succ(s), succ(s'))
           = succ(plus(s, succ(s')))
           = succ(plus(succ(s'), s))
           = plus(succ(s'), succ(s))
           = plus(y, x)

which seems to be a bit of a pointless set of statements, as although they are all true I don't think some of them are proven when I use them.

How would I establish that plus(x, y) = plus(y, x) in this last bit? I don't really know what kind of things I can legitimately do with the algebra.

Thanks for any/all help.

[HarryW]

Any comments appreciated.... any comments at all.... please

[paulw]

Harry,

I will work on this - I've got a Maths degree but it was a long time ago, but this is interesting.

Cheers,

Paul.

P.S. What the hell is all that info in your profile and what is UO, and what are you studying - and are you in London since I am trying to get tumblingdown out for a beer or six.

[Edited by paulw on 11-07-2000 at 11:48 AM]

[HarryW]

Cheers Paul

UO = Ultima Online, an online game which sucks your life away. The weird symbolic stuff is d00d speak for 'I rocks your arse, newbie'.

I'm in Guildford Studying BSc Computing and Information Technology, but I appreciate the offer

[HarryW]

Anybody got any ideas on the correct way to prove this then? I really need to get this sorted out.

[paulw]

Harry,

I am still grappling with this one

1. Prove for x = zero (easy)

Assume correct for x

2. Prove for Succ(x)

i.e. plus(plus(succ(x),y),z)=plus(succ(x),plus(y,z)) (tough)

Now, two things occur to me, x can be written as plus(zero, x) and any non-zero value of x can be expressed as succ(succ(succ(x))) etc.

I think that that is the way to do it.

I'll keep going, BUT it is YOUR homework. So let me know when you have the solution (or else).

Cheers,

Paul.

[HarryW]

It's handed in already, I'm not getting any marks for this. Seeing as the lecturer already owes us 4 weeks of coursework though, I don't think the solution's coming any time soon.

You say proving plus(zero, y) = plus(y, zero) is easy? Could you explain it then please? Pretty please? It was implied in the coursework that more steps were needed than:

plus(zero, y) = y

= plus(y, zero)


Personally I don't see why you can't just use the inductive hypothesis plus(zero, s')=plus(s', zero) to rewrite it. I am pretty sure you can't though, so what am I missing? Exams are in about 4 weeks I think, and I need to understand this

[Sam Finch]

I keep forgetting about this, I typed almost all of it up for you only to recieve the blue screen of death for no reason at all.

anyway, I'll start again.

Paul's right about his 2 statements, you have to assume the second one, (x = succ(succ(succ(succ(zero)))) etc)

formally
for all x in the set NAT there exists a unique n in the set of natrual numbers s.t. x = succ©ú(zero)

you might want to translate this into maths language if you want to be impressive, for all is written as an upside down A, in the set is a sort of small rounded E, like the euro symbol but with only 1 line, there exists is a backwards E, a unique is an !, and the natrual numbers is a capial N with an extra bar for the diagonal. But I don't know if that's relevent or not.


you would have to prove that plus(x,zero) = x though, fortunatley we don't actually need it, I'll write it out for you, unfortunatley I can't remember the proper formal layout of inductions, but I'll lay it out in a way that would be acceptable.

Define Proposition P(x)  (where x is a NAT)

P(x) is true iff Plus(Plus(x,y), z) = Plus(x, Plus(y,z))
for all NAT y,z 


consider P(zero)

Plus(Plus(zero,y), z) = Plus(y,z) = Plus(zero, Plus(y,z))

Hence P(zero) is true.




now assume P(k) for some NAT k.

Plus(Plus(k,y), z) = Plus(k, Plus(y,z))


consider P(Succ(k))

Plus(Plus(Succ(k),y), z) = Plus(Succ(Plus(k,x)),z)
                         = Succ(Plus(k,y), z)
by P(k)                  = Succ(Plus(k, Plus(y,z))
                         = Plus(Succ(k), Plus(y,z))


and hence P(k) => P(Succ(k))

So we have shown P(zero) and (P(k) => P(Succ(k))
and hence have proved inductivley that P(x) is true for all NAT x

and hence that Plus(Plus(x,y),z) = Plus(x,Plus(y,z)) for all NAT x,y,z

Is that all you have to do or do you have other wierd and wonderful inductions to do.

The key thing with inductions is make sure you understand them. I've inducted for other people in the past and they all got cuaght out for being the cheating scum that they were because they didn't understand what I'd done for them. Read over it and make sure you get what I've done and why it must mean that it works for all x, otherwise you will have trouble if you're asked to do other ones.

[paulw]

Assume x = succ(zero)

defn 1 (x, y :NAT)
defn 2 plus(zero, x) = x

Now plus(zero, x), by defn 2 = x = succ(zero), by assumption.

plus(x, zero), by substitution =
plus(succ(zero), zero), by defn 3 =
succ(plus(zero, zero)), which, by defn 2 =
succ(zero) which was our base assumption

This can be generalised (I think) to show that plus(zero, x) = plus(x, zero) for all values of x

Work on proving for succ(succ(x)), if you can prove it for that, we know it is true for zero and for succ(x). If we can prove for succ(succ(x)) then by induction it is true for all values of x.

Do you get it.

e-mail me a tel.# if you want to talk it through.

Cheers,

Paul.

[paulw]

Now if x is succ(succ(zero))

plus(zero, x) = x
plus(x, zero) = plus(succ(succ(zero)), zero)
= succ(plus(succ(zero), zero))
= succ(succ(plus(zero, zero)))
= succ(succ(zero))
= x (wahey)

so we have proved it for 1, 2 - but we can now say for x we can prove it for succ(x)

This is intuitively true, but I am unsure how to formally prove it. basically I think you can show that the associativity holds for any level of succ(zero) => all NAT

What do you think,


Paul.

P.S. I meant, originally, it was easy to prove that

plus(plus(zero, y), z) = plus(zero, plus(y, z)

[Sam Finch]

BTW do you have to prove that plus(x,y) = plus(y,x), cos that's a really wierd one (I havn't finished it, but it looks like a sort of simultanious induction, or whatver the proper name is. Give me a shout if you want that done.

[HarryW]

Sam:

Thanks a lot, that's cleared up a lot of the confusion in my head. That was for assosiativity though, and I need to prove commutativity It's getting clearer though.

Oh and thanks for the tips about the mathematical notation, I would use it (though obviously not here because I have to use this font) but the lecturer hasn't been using it. Oh and the 'is a member of the set' operator is the Greek letter Epsilon

Paul:

Cheers, I see what you've done there but what you're doing there is proving for individual cases. Instead of proving with x=succ(zero) you need to prove with x=succ(s') where s' is any term not involving plus, ie. succ^n(zero) since we haven't defined any more extensions than plus yet.

So using succ(s'), you can't use defn 2 to rewrite plus(s', zero) as s'



Can you, in these proofs, use x=succ^n(zero) in your algebra? So could you write:

plus(x, zero)
= plus(succ^n(zero), zero)
= succ^n(plus(zero, zero))
= succ^n(zero)
= plus(zero, succ^n(zero)) using defn 2
= plus(zero, x)

?

This looks sensible but I'm not sure if you can legitimately use this kind of notation in these proofs.

Can I use the definition

plus(succ(x), y) = succ(plus(x, y))

and interpret it as

plus(succ^n(x), y) = succ^n(plus(x, y))

?

[HarryW]

Thanks to all for your help by the way, this is getting much clearer

[Sam Finch]

As I said, this one's a bit harder, you don't have to use the wierd double induction I mentioned, but you do need 3 seperate inductions.



the first one is to proove the axiom that

plus(succ(x), y) = plus(x, succ(y))

So put your induction hat on

P(x) <=> plus(succ(x), y) = plus(x, succ(y))

consider p(zero) 

Plus(succ(zero), y) = succ(plus(zero, y))
                    = succ(y)
                    = plus(0,succ(y))



So P(zero) is true

now assume P(k)

Plus(succ(k), y) = plus(k, succ(y))

and consider P(succ(k))
plus(succ(succ(k)), y) = succ(plus(succ(k), y)
                       = succ(plus(k, succ(y))
                       = plus(succ(k), succ(y))

so P(k) => P(succ(k))

and hence we've proved that plus(succ(x), y) = plus(x, succ(y)) for all NAT x,y 


now consider proposition Q(x) <=> Plus(zero,x) = Plus(x,zero)

clearly Q(zero) is true

now assume Q(k) for some NAT k

Plus(zero,k) = plus(k,zero)

plus(zero, succ(k)) = succ(k)
                    = succ(plus(zero,k))
                    = succ(plus(k,zero))
                    = plus(succ(k),zero)

and hence Q(k) => Q(succ(k))
so by induction
plus(x,zero) = plus(zero,x) for all NAT x



now consider proposition R(x) 

plus(x,y) = plus(y,x)

we see that the statement Q(y) above is the same as R(0) and hence R(0) is true.

now assume R(k)
plus(k,y) = plus(y,k)

and consider R(succ(k))

plus(succ(k), y) = plus(k, succ(y))  (by P(k))
                 = Plus(succ(y), k)
                 = plus(y, succ(k))

and hence R(k) => R(succ(k))

and by induction plus(x,y) = plus(y,x) for all NAT x,y

I've bolted through that pretty quickly because I need a ***, but you should be able to follow it and translate that into a more formal layout.

Hope it helps

[HarryW]

Fan-*****ing-tastic, thanks a lot That helps a hell of a lot. I think I see how it works now. I wasn't sure if the definitions could be used backwards (make any sense?), I mean I wasn't sure if you could rewrite the rvalue with the lvalue. I now feel a bit dumb

My only concern is how you did this:

plus(k, succ(y))
= Plus(succ(y), k)

Looking at the rest of your proofs, I think I would have done it like this:

plus(succ(k), y)
= succ(plus(k, y))
= succ(plus(y, k)) {using the inductive hypothesis R(k)}
= plus(succ(y), k)
= plus(y, succ(k)) {using P(x)}

Is that right?

[Sam Finch]

That's right, but completley unneccassery, when I did that I'd already assumed

plus(k,y) = plus(y,k) for all NAT y, so as the value of Y is irrelevent then it also works for succ(y), so It doesn't need proving.

[HarryW]

Ah right.

In that case, why can't you just write:

plus(succ(k), y)
= plus(y, succ(k)) using R(k)

?

Oh dear, confused again

[Sam Finch]

No, you can't do that, R(k) says that plus(k,y) = plus(y,k) for any value of y, for example R(3) says that plus(3,y) = plus(y,3), so If we know R(k) is true we know that plus is commutitive as long as one of the values is k. we then have to prove it for the general case plus(succ(k), y) for all values of y. We can't assume plus(succ(k), y) = plus(y,succ(k)) because that assumes y = k. but we can assume plus(k, succ(y)) = plus(succ(y), k) because one of the parameters is k.

I hope that makes some sense

[HarryW]

Oh and it doesn't matter what k is because we haven't assumed that k is an element of NAT not involving plus?

Sorry I can see you probably feel like you're banging your head against a brick wall here, but it's sinking in slowly I assure you

The proof I gave earlier, that's the way our lecturer gave an outline to do it. Ie. prove the following in order:

plus(zero, zero) = plus(zero, zero)
plus(zero, y) = plus(y, zero)
plus(x, zero) = plus(zero, x)
plus(x, y) = plus(y, x)

Hmm, I'll try and write up a proof in that format, my next post will show how successful I've been....

[Oops, typo]

[Edited by HarryW on 11-09-2000 at 04:40 PM]

[HarryW]

I think I got it! *Crosses fingers* Took me literally hours of tweaking though

How's this?

RTP: plus(x,y) = plus(y, x) for all terms x, y
     (ie. plus is commutative)

base case: x=zero
	
	use induction, for the second argument, over all terms y not involving plus
		base case: y=zero
			plus(zero, zero) = zero  (using def[1])
		
		inductive step: y=succ(s')
			whenever s' does not involve plus and plus(zero, s')=plus(s', zero)
			then plus(zero, y)=y  (using def [1])
			                  =succ(s')
					  =succ(plus(zero, s'))  (using def [2])
					  =succ(plus(s', zero))  (using inductive hypothesis)
			                  =plus(succ(s'), zero)  (using def [1])
					  =plus(y, zero)
	Thus plus(zero, y)=plus(y, zero) for all terms y which do not involve plus.

Inductive step: x=succ(s)
	whenever plus(s, y)=plus(y, s) for all terms y which do not involve plus
	then use induction, for the second argument, over all terms y not involving plus.

		base case: y=zero
			plus(x, zero)=plus(zero, x)   (already proven above)

		inductive step: y=succ(s')
			whenever plus(succ(s), s')=plus(s', succ(s))

			then plus(x, y)=plus(succ(s), succ(s'))
			               =succ(plus(s, succ(s')))
			               =succ(plus(s, succ(plus(zero, s'))))
			               =succ(plus(s, plus(succ(zero), s')))
			               =succ(plus(s, plus(s', succ(zero))))
			               =succ(plus(plus(s, s'), succ(zero)))
			               =plus(succ(plus(s, s')), succ(zero))
			               =plus(plus(succ(s), s'), succ(zero))
			               =plus(plus(s', succ(s)), succ(zero))
			               =plus(s', plus(succ(s), succ(zero)))
			               =plus(s', plus(succ(s), plus(zero, succ(zero))))
			               =plus(s', plus(succ(s), succ(zero))) 
			               =plus(s', succ(plus(s, succ(zero)))) 
			               =plus(s', succ(plus(succ(zero), s))) 
			               =plus(s', succ(succ(plus(zero, s))))
			               =plus(s', succ(succ(s))) 
			               =plus(succ(succ(s)), s') 
			               =succ(plus(succ(s), s')) 
			               =succ(plus(s', succ(s))) 
			               =plus(succ(s'), succ(s)) 
			               =plus(y, x)

	This completes the proof that plus(succ(s), y)=plus(y, succ(s))

And so completes the proof by induction of
plus(x, y)=plus(y, x) for all terms x and y which do not involve plus.

I think that's correct, but I'm not sure it's in its most concise form. It assumes that assosiativity is already proven (which it has been in the previous question). I know Sam's way is easier but I'm trying to follow the guideline.

[paulw]

Harry,

I will check this through. I was trying to show that you could prove for x=1 and x=2 as a general outline of how to approach - NOT as a final proof - I've already got my degree <grin>. I've got to leave you some work!

It is looking good though and the approach is right.

I'm glad you found Sam's stuff more helpful, hope mine helped a bit - even if just to get the juices flowing! It was fun for me 'cos I haven't done that since I was a Freshman in 1984!!!

Cheers,

Paul.

[HarryW]

All help is appreciated Paul, this is a heck of a lot clearer than it was a couple of days ago. Shame that's when the coursework had to be in really Ah well. And I'm sorry for misunderstanding your intentions, I should have guessed you knew what you were doing better than me

[paulw]

I should have guessed you knew what you were doing better than me

Course you should

Cheers,

Paul.