## Stream: new members

### Topic: rewrite only first occurrence?

#### agro1986 (Nov 24 2019 at 14:55):

Hi all. In tactics mode, how do I say rewrite th1 but please do it only on the first occurence k thx? Thanks a lot

#### Mario Carneiro (Nov 24 2019 at 14:57):

you can do it with conv, but I would like to see a use case first

#### agro1986 (Nov 24 2019 at 14:57):

More concretely, I want to change n = n + 1 into n + 0 = n + 1. If I use the proof n = n + 0, rw will change it into n + 0 = n + 0 + 1 :(

#### Mario Carneiro (Nov 24 2019 at 14:58):

example (n : ℕ) : n = n + 1 :=
begin
conv {to_lhs, rw ← add_zero n},
end


#### Mario Carneiro (Nov 24 2019 at 14:59):

it's not changing the first occurrence, but it is rewriting only on the lhs of the equality

#### Mario Carneiro (Nov 24 2019 at 14:59):

which achieves the same effect

#### agro1986 (Nov 24 2019 at 15:01):

@Mario Carneiro thanks. What about the case where I want to change a hypothesis h, not the goal? In rw we say rw th1 at h

#### Mario Carneiro (Nov 24 2019 at 15:02):

at h still works

#### Mario Carneiro (Nov 24 2019 at 15:02):

example (n : ℕ) (h : n = n + 1) : true :=
begin
conv at h {to_lhs, rw ← add_zero n},
end


#### Mario Carneiro (Nov 24 2019 at 15:02):

it goes on the conv because that's the part that figures out where to work

#### agro1986 (Nov 24 2019 at 15:03):

Ahh I see! I tried writing at h at the end of the sentence so it didn't work. Thanks a lot!

#### Mario Carneiro (Nov 24 2019 at 15:04):

if you mouse over the conv it should print conv (at id)? (in expr)? { tactic } which shows the correct order of use

#### agro1986 (Nov 24 2019 at 15:06):

cool! I used it for solving this: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

  rw ← add_one_eq_succ,
assume h,
conv at h {to_lhs, rw ← add_zero n},
have h2 := add_left_cancel _ _ _ h,
apply zero_ne_succ 0,
rw ← one_eq_succ_zero,
exact h2,


#### Mario Carneiro (Nov 24 2019 at 15:13):

what's the theorem?

#### Mario Carneiro (Nov 24 2019 at 15:15):

the natural number game says what theorem you are proving just outside the text box, you need that if you want to quote the theorem outside the game (and some more besides that, depending on how advanced the theorem is, you might have your own definitions and such to rely on)

#### Mario Carneiro (Nov 24 2019 at 15:15):

it's always best to post complete examples here in chat so we can test your work

#### Kevin Buzzard (Nov 24 2019 at 18:46):

Mario surely you can work out the theorem from the proof :-)

#### Kevin Buzzard (Nov 24 2019 at 18:46):

Is that reverse mathematics?

#### Mario Carneiro (Nov 24 2019 at 19:05):

Hm, it's a bit complicated because you made up all the theorem names, but this prelude does the job:

import data.nat.basic
namespace mynat
open nat
theorem add_one_eq_succ (n : ℕ) : n + 1 = nat.succ n := rfl
theorem add_left_cancel (a b c : ℕ) : a + b = a + c → b = c := add_left_cancel
theorem zero_ne_succ (n : ℕ) : 0 ≠ succ n.
theorem one_eq_succ_zero : 1 = succ 0 := rfl

example (n : ℕ) : n ≠ succ n :=
begin
assume h,
conv at h {to_lhs, rw ← add_zero n},
have h2 := add_left_cancel _ _ _ h,
apply zero_ne_succ 0,
rw ← one_eq_succ_zero,
exact h2,
end

end mynat


#### Mario Carneiro (Nov 24 2019 at 19:09):

and golfed:

example (n : ℕ) : n ≠ succ n :=
begin
exact λ h, zero_ne_succ 0 (add_left_cancel n 0 1 h)
end


the best tactic proof is a term proof :P

Last updated: May 14 2021 at 04:22 UTC