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


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