what rfl does

Stream: lean4

[Asei Inoue]

I want to understand what rfl tactic does.

“if the outputs of #reduce A and #reduce B are equal, then A = B is provable by rfl” is correct?

[Edward van de Meent]

I suspect it calls docs#Lean.Meta.isDefEq

[Kyle Miller]

It can do a number of things. If the goal is an equality though, it's equivalent to exact rfl. Unfolding all the processes involved, this is "if A is definitionally equal to B, then it closes the goal A = B".

The rfl tactic is able to handle reflexive relations too. Roughly speaking, the way it works is that it uses the registered @[refl] lemma for the relation R to convert the goal R A B to A = B, and then it does exact rfl.

[Kyle Miller]

What's (likely) true is that if #reduce A and #reduce B are equal then rfl proves A = B, but definitional equality is complicated, and there are almost certainly cases where A = B is provable by rfl even if the #reduces aren't the same.

[Asei Inoue]

Thank you!!