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: Dec 20 2023 at 11:08 UTC