# Zulip Chat Archive

## Stream: general

### Topic: modeq.refl

#### Kevin Buzzard (Apr 30 2018 at 20:31):

`@[refl] protected theorem refl (a : ℕ) : a ≡ a [MOD n] := @rfl _ _`

#### Kevin Buzzard (Apr 30 2018 at 20:31):

looks funny because `rfl`

unfolds to exactly `@rfl _ _`

#### Kevin Buzzard (Apr 30 2018 at 20:32):

but it's one of those situations where you can't prove the result by the exact three letter combination `rfl`

#### Kevin Buzzard (Apr 30 2018 at 20:32):

because you get the error `not a rfl-lemma, even though marked as rfl`

#### Kenny Lau (Apr 30 2018 at 20:32):

do you know what the `@[refl]`

`@[symm]`

`@[trans]`

are for (as a sidenote)?

#### Kevin Buzzard (Apr 30 2018 at 20:32):

but the funny thing is, it is tagged `[refl]`

anyway

#### Kevin Buzzard (Apr 30 2018 at 20:33):

what is the difference between being `a rfl-lemma`

and being tagged with `@[refl]`

?

#### Kevin Buzzard (Apr 30 2018 at 20:33):

Kenny here are some ramblings

#### Kenny Lau (Apr 30 2018 at 20:33):

they are for the reflexivity symmetry transitivty tactics respectively

#### Kenny Lau (Apr 30 2018 at 20:33):

(refl = reflexivity)

#### Kevin Buzzard (Apr 30 2018 at 20:33):

If you are in calc mode then calc will use any lemma tagged `trans`

#### Kenny Lau (Apr 30 2018 at 20:34):

that also

#### Kevin Buzzard (Apr 30 2018 at 20:34):

to concatenate `a R b`

and `b R c`

#### Kevin Buzzard (Apr 30 2018 at 20:34):

or even `b S c`

#### Chris Hughes (Apr 30 2018 at 20:34):

le_refl is refl but not rfl

#### Gabriel Ebner (May 01 2018 at 08:07):

`rfl`

-lemmas show definitional equalities (i.e. `a = b`

where `a`

and `b`

are def-eq). The three letters `rfl`

are essentially hardcoded into the parser for this purpose. The reason is that typically lemmas are completely independent of their proofs, (well-founded recursion aside) it should not matter what proof you use for a lemma. However whether an equality is proved by definitional equality has important consequences: for example, `dsimp`

can only use definitional equalities. Hence we have an easy syntactic criterion to determine whether a lemma is proven by definitional equality.

Last updated: Aug 03 2023 at 10:10 UTC