Zulip Chat Archive

Stream: new members

Topic: rewrite only first occurrence?


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2019 at 14:57):

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

view this post on Zulip 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 :(

view this post on Zulip Mario Carneiro (Nov 24 2019 at 14:58):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2019 at 14:59):

which achieves the same effect

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2019 at 15:02):

at h still works

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2019 at 15:02):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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,

view this post on Zulip Mario Carneiro (Nov 24 2019 at 15:13):

what's the theorem?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2019 at 18:46):

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

view this post on Zulip Kevin Buzzard (Nov 24 2019 at 18:46):

Is that reverse mathematics?

view this post on Zulip 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

view this post on Zulip 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