Specific selection of terms with rw

Stream: new members

[Martin Kleiven]

Hey I'm going through the Nat Num Game, currently working through mul_add, I wonder first and foremost if it fundementally matters which variable we perform induction on? It seems some are much harder.

a(b + c) = ab + ac

Solving for a was my first shot but this got very hard fast, I did manage to solve for b and c however.

Q2: Is it possible to provide a selector for specific terms?

I know we can say rw add_assoc a b c, but is rw add_assoc (ab) + a + (ac) possible?

[Chris Hughes]

You can do rw add_assoc (a * b) a (a * c). Not sure if this is what you wanted.

[Martin Kleiven]

Okay so it does indeed work. Turned out I wanted right_add_comm but that's alright.

Solving for a, is that possible as well?

[Anne Baanen]

The set of variables you perform induction on does matter, but given the set it shouldn't matter in which order you do induction.

[Anne Baanen]

In this case, if you start by induction on a in a * (b + c), you should be able to solve the base case, but there is no lemma succ_mul equivalent to mul_succ (yet!)

[Martin Kleiven]

If I understand correctly the choice on which variable to perform induction on is determined by previous lemmas that are proved, and ultimately what I choose depends on this. But any choice of variable are valid?

[Anne Baanen]

I'm sorry, I don't understand the question. Indeed, the set of variables you do induction on is determined by the previous lemmas, and ultimately by the definitions. (For example, * is defined by recursion on the right-hand argument, so to prove things about a * b you probably want to do induction on the right-hand argument b.) But given that the variables you want to do induction on are correct, you can pick any one of the variables to start with, and you shouldn't get stuck.

[Donald Sebastian Leung]

Not in general. For example, suppose you want to prove some property about exponentiation (on the natural numbers), e.g. a ^ (b + c) = (a ^ b) * (a ^ c), which is defined as follows:

• a ^ 0 = 1
• a ^ (S n) = a * (a ^ n)

Since exponentiation is defined by induction on its second argument, attempting to prove the statement by induction on a (the first argument) would fail miserably.

[Anne Baanen]

Perhaps it's clearer to say that doing induction on only a would fail, but if the next command is induction b, you should be able to solve it anyway.

[Donald Sebastian Leung]

Anne Baanen said:

Perhaps it's clearer to say that doing induction on only a would fail, but if the next command is induction b, you should be able to solve it anyway.

But you probably won't be able to use the induction hypothesis generated by induction a anyway so you're technically not really performing induction on a

[Anne Baanen]

That's also a reasonable view. But up to definitional equality, rw [add_zero] (where add_zero reduces to eq.refl) then also isn't really doing rewriting :P

[Martin Kleiven]

Okay thanks, still not quite there but its starting to make sense to me, got some reading to do. Thank you both!