20
$\begingroup$

I already know that refl is called a tactic, and that rfl is a term; can you explain with examples how they technically differ? I've read that refl is "more powerful", but I never knew beforehand if one would definitely work where the other may not. Bonus points for by exact rfl explanations. I also wonder if there are significant changes to these between different versions of Lean 3...

$\endgroup$
2
  • 1
    $\begingroup$ I changed the reflexivity tag to equality. Presumably there is no point in splitting equality into reflexivity, symmetry, transitivity, etc. $\endgroup$ Feb 14, 2022 at 13:14
  • $\begingroup$ I can't seem to edit it. I can only edit some tags but not others. Or maybe I don't know how to use the internet. $\endgroup$ Feb 14, 2022 at 22:11

2 Answers 2

18
$\begingroup$

So you are correct that refl is a tactic, and rfl is a term, so for example:

example : 1 = 1 := rfl
example : nat = nat := by refl -- equivalent to putting `rfl`

But refl is more powerful, as it can also apply other lemmas that have the @[refl] attribute on them (like rfl) :

example : true ↔ true := rfl -- error!
example : true ↔ true := by refl -- fine! makes term `iff.rfl`
example : 0 ≤ 0 := by refl -- fine!

There are other similar tactics for symmetry (also symmetry' which is slightly better) and transitivity, both with their related attributes.

by exact rfl is a hack used to deal with the elaborator, which sometimes can infer what you mean wrong, but putting it into a tactic state forces it to realise what's going on. A similar hack is show _, from ... (although it seems this isn't commonly used with rfl)

$\endgroup$
2
  • 2
    $\begingroup$ In the first line, rfl and refl seem like they should be swapped $\endgroup$ Feb 12, 2022 at 19:23
  • 3
    $\begingroup$ It might be worth mentioning that refl is able to prove equalities because eq.refl has the [refl] attribute (i.e., equality isn't a special case). It's also part of a suite of three tactics for applying lemmas for relations: refl, symmetry, and transitivity. $\endgroup$ Feb 12, 2022 at 19:31
9
$\begingroup$

Separately from the rfl (term) vs refl (tactic) distinction, there is also the distinction between rfl and refl in lemma names:

#check @eq.refl  -- ∀ {α : Sort u_2} (a : α), a = a
#check @rfl      -- ∀ {α : Sort u_2} {a : α}, a = a

#check @iff.refl -- ∀ (a : Prop), a ↔ a
#check @iff.rfl  -- ∀ {a : Prop}, a ↔ a

#check @le_refl  -- ∀ {α : Type u_2} [_inst_1 : preorder α] (a : α), a ≤ a
#check @le_rfl   -- ∀ {α : Type u_2} [_inst_1 : preorder α] {a : α}, a ≤ a

The difference here is that that rfl uses an implicit {} binder for a, while refl uses a explicit () binder. So iff.rfl is shorthand for iff.refl _, le_rfl is shorthand for le_refl _, etc.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.