What is the difference between refl and rfl in Lean 3?

Question

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...

Answer 1

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)

Answer 2

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.