Stuck on nat game

Stream: new members

[J. O.]

I’m doing the natural number game, and im stuck on how to prove the first goal. Is using induction the right approach? AB39A285-F83B-42C6-81E3-03E0F791CA3F.jpeg

[Mario Carneiro]

do induction on b not a

[Mario Carneiro]

because addition is defined by recursion on the second argument

[J. O.]

Hmm i think i see

[Daniel Roca González]

zero_add doesn't work because your term is not of the form 0 + x. You should be able to use the lemmas you have of you use induction on b.

[J. O.]

Mario Carneiro said:

because addition is defined by recursion on the second argument

I think they said that in the game somewhere

[J. O.]

I dont really understand the recursion part of the reasoning (sorry if i sound stupid)

[J. O.]

Do you keep adding one until the second number is zero?

[J. O.]

I’m going to recreate such a function to understand

[Daniel Roca González]

yes, that is how addition on nats is defined. You should have used that in the proof of add_succ.

[Kyle Miller]

J. O. said:

because addition is defined by recursion on the second argument

I think they said that in the game somewhere

It's easy to miss this, but the key is the two theorems you get at the beginning:

image.png

It means that if you have, say a + 3, you can compute that it's succ (succ (succ a)) by repeatedly applying the second theorem and then the first theorem at the end.

[Kyle Miller]

If you had 3 + a with an unknown a, then there's nothing you can do with only those two theorems.

[Kyle Miller]

(These two theorems actually are the definition for addition.)

[J. O.]

So why did I have to do induction in b instead of a

[Stuart Presnell]

"Do you keep adding one until the second number is zero?"

Essentially addition is defined by "keep moving succ to the left past the addition until the second number is zero".

For example, how do we evaluate a + 3? Since 3 is succ (succ (succ zero)), by repeatedly rewriting with add_succ we have:

a + succ (succ (succ zero))
=
succ (a + succ (succ zero))
=
succ (succ (a + succ zero))
=
succ (succ (succ (a + zero)))

and then by add_zero this is equal to succ (succ (succ a))

[Stuart Presnell]

Notice that a stays the same here, while b keeps decrementing: a + 3 = succ(a + 2) = succ(succ(a + 1)) = succ(succ(succ(a + 0))).

[Stuart Presnell]

Since this is how addition is defined — "by recursion on the second argument" — when we want to prove something about addition we often do it by an induction on the second (or more generally, the rightmost) argument.

[J. O.]

Ah ok. So it’s something more generally used

[Stuart Presnell]

So in a theorem like succ(a) + b = succ(a + b) as in Level 3/6, we let a be arbitrary since it's going to be held fixed by these rewrites, and then we have to prove that for this arbitrary a the theorem holds for all b.

[J. O.]

after that, I call rw add_zero?

[J. O.]

Stuart Presnell said:

So in a theorem like succ(a) + b = succ(a + b) as in Level 3/6, we let a be arbitrary since it's going to be held fixed by these rewrites, and then we have to prove that for this arbitrary a the theorem holds for all b.

This is because b is the recursive argument, right?

[Mario Carneiro]

If we do induction on b we get a goal like succ(a) + 0 = succ(a + 0) and add_zero works on that. If you do induction on a you would get succ(0) + b = succ(0 + b) and you would need zero_add which you don't have yet

[Stuart Presnell]

When we use induction b it produces two goals: prove that the theorem holds for b=0 (the base case), and prove that if it hold for some number b' then it also holds for succ b' (the inductive step).

[Stuart Presnell]

We know how to deal with an addition where the second argument is of the form succ b' — that's just what we were looking at above with the chain of rewrites by add_succ.

[Stuart Presnell]

So when we're asked to prove something involving succ a + succ b' we know we can rewrite it with add_succ to turn it into succ(succ a + b'). Again, the first argument to the addition remains unchanged, and the succ on the second argument is moved to the left.

[Stuart Presnell]

And now the "inductive hypothesis" comes to the rescue. We're assuming that the theorem holds for b' (that's the "inductive hypothesis") and trying to prove it for succ b'. So we can use the inductive hypothesis to rewrite the thing inside the brackets.

[Patrick Johnson]

So why did I have to do induction in b instead of a

Since mynat is an inductive datatype, we can use induction/recursion to construct something involving mynat. Addition is defined using recursion on the second argument. If we want to prove something about addition, we should induct on the second argument. Induction is basically a recursion that constructs a proof term.

[J. O.]

Thanks everyone for these great answers

[J. O.]

I was able to prove the first goal with

induction b with d hd,
rw add_zero,
rw add_zero,
refl,

But im a bit unsure about the second goal

case mynat.succ
a d : mynat,
hd : succ a + d = succ (a + d)
⊢ succ a + succ d = succ (a + succ d)

Any hints would be appreciated

I did this so far:

rw add_succ,
rw add_succ,

And i get

case mynat.succ
a d : mynat,
hd : succ a + d = succ (a + d)
⊢ succ (succ a + d) = succ (succ (a + d))

I dont know how to continue really

[Mario Carneiro]

notice that hd matches the left side

[Kevin Buzzard]

Do you know what induction is and how it works? Did you see this in class yet?

The way induction works is that you get an inductive hypothesis which almost always is an essential part of the proof.

The game is designed for people who are already familiar with mathematical induction (in fact it's designed for maths undergraduates at my university), so I don't explain the ins and outs of how it works -- apologies if this is not a good fit for you.

[Hans Parshall]

(deleted)