# 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 :=
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