rewrite and reflexivity

Stream: new members

[Thorsten Altenkirch]

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 :=
begin
  assume x y p,
  rewrite p,
end

[Ruben Van de Velde]

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

[Alex Peattie]

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
end

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
end

to finish the proof, or:

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

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

[Alex J. Best]

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.