# Zulip Chat Archive

## 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 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, 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