Both of these close 2 + 2 = 4:
example : 2 + 2 = 4 := rfl
example : 2 + 2 = 4 := ⊢ 2 + 2 = 4 All goals completed! 🐙
So I assumed they were interchangeable for small closed facts. They are not.
rfl fails on 10 < 20:
example : 10 < 20 := Type mismatch
rfl
has type
?m.9 = ?m.9
but is expected to have type
10 < 20rfl
Why
rfl is a proof of a = a. It works on 2 + 2 = 4 because the type checker
can reduce 2 + 2 to 4, so both sides are definitionally equal. But
10 < 20 is not an equation. On Nat, < unfolds to Nat.le, an inductive
proposition, and no amount of reduction turns it into _ = _.
decide works differently. It looks for an instance of Decidable (10 < 20),
evaluates it, and if the result is isTrue h it uses h. Any proposition with
a Decidable instance that computes can be proved this way, whether or not it
is an equation.
theorem ten_lt : 10 < 20 := ⊢ 10 < 20 All goals completed! 🐙
'ten_lt' does not depend on any axioms#print axioms ten_lt
The proof uses no axioms, because the kernel checked the evaluation itself:
'ten_lt' does not depend on any axiomsTo follow up
-
What exactly does the kernel reduce when checking
decide, and why does it get slow on large numbers? (This leads tonative_decide, which is a kernel-and-trust topic.) -
Decidableinstances that do not reduce, for example ones defined with well-founded recursion.