modeq.refl

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

looks funny because rfl unfolds to exactly @rfl _ _

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

do you know what the @[refl] @[symm] @[trans] are for (as a sidenote)?

[Kevin Buzzard]

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

[Kevin Buzzard]

what is the difference between being a rfl-lemma and being tagged with @[refl]?

[Kevin Buzzard]

Kenny here are some ramblings

[Kenny Lau]

they are for the reflexivity symmetry transitivty tactics respectively

[Kenny Lau]

(refl = reflexivity)

[Kevin Buzzard]

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

[Kenny Lau]

that also

[Kevin Buzzard]

to concatenate a R b and b R c

[Kevin Buzzard]

or even b S c

[Chris Hughes]

le_refl is refl but not rfl

[Gabriel Ebner]

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.