Zulip Chat Archive

Stream: new members

Topic: rewrite and reflexivity

Thorsten Altenkirch (Sep 12 2020 at 12:37):

I am just preparing my lectures and hence I am doing some very simple proofs. I noticed that if after rewrite reflexivity is automatically applied if possible. Is this actually explained somewhere?

theorem sym_eq :  x y : A, x=y  y=x :=
  assume x y p,
  rewrite p,

Ruben Van de Velde (Sep 12 2020 at 12:40):

I would've expected https://leanprover-community.github.io/mathlib_docs/tactics.html#rw%20/%20rewrite to mention it, but apparently not

Alex Peattie (Sep 12 2020 at 12:57):

I'm not sure that reflexivity is applied, at least in terms of being the same as applying the reflexivity tactic. It seems like rw will close a goal if the left and right hand side are literally the same (not just definitionally equal). For example, if you do:

example { c :  } (h: c = 0) : int.nat_abs c = 0 := begin
  rw h

the rw doesn't complete the proof, even though 0.nat_abs = 0 is true by definition. But you can do:

example { c :  } (h: c = 0) : int.nat_abs c = 0 := begin
  rw h, refl

to finish the proof, or:

example { c :  } (h: c = 0) : int.nat_abs c = 0 := begin
  rw [h, int.nat_abs_zero]

which converts the goal to 0 = 0 which is then closed automatically.

Alex J. Best (Sep 12 2020 at 13:05):

I don't know about explained (i.e. a docstring mentioning it or a deeper reason why it is set up this way) but the source for rw_core is

private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
match loca with
| loc.wildcard := loca.try_apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
| _            := loca.apply (rw_hyp cfg rs.rules) (rw_goal cfg rs.rules)
end >> try (reflexivity reducible)
    >> (returnopt rs.end_pos >>= save_info <|> skip)

note try (reflexivity reducible), so perhaps the difference Alex is seeing is due to the reducibility setting being set to reducible here.

Last updated: Dec 20 2023 at 11:08 UTC