rewrite only first occurrence?

Stream: new members

[agro1986]

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]

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

[agro1986]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

which achieves the same effect

[agro1986]

@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]

at h still works

[Mario Carneiro]

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

[Mario Carneiro]

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

[agro1986]

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

[Mario Carneiro]

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

[agro1986]

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]

what's the theorem?

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Is that reverse mathematics?

[Mario Carneiro]

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]

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