# Zulip Chat Archive

## Stream: new members

### Topic: Specific selection of terms with rw

#### Martin Kleiven (Feb 20 2020 at 13:20):

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 (Feb 20 2020 at 13:24):

You can do `rw add_assoc (a * b) a (a * c)`

. Not sure if this is what you wanted.

#### Martin Kleiven (Feb 20 2020 at 13:29):

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 (Feb 20 2020 at 13:32):

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 (Feb 20 2020 at 13:35):

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 (Feb 20 2020 at 13:37):

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 (Feb 20 2020 at 13:54):

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 (Feb 20 2020 at 13:54):

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 (Feb 20 2020 at 13:56):

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 (Feb 20 2020 at 13:58):

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 (Feb 20 2020 at 14:03):

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 (Feb 20 2020 at 14:47):

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

Last updated: May 16 2021 at 20:13 UTC