lt.base

Stream: general

[Sebastien Gouezel]

Can someone explain the reason for

def lt.base (n : ℕ) : n < succ n := nat.le_refl (succ n)

lemma lt_succ_self (n : ℕ) : n < succ n := lt.base n

with two identical statements, the first one being a def and the second a lemma. (This is in core).

[Mario Carneiro]

Of the two, lt.base is definitely the odd one out. Possibly https://github.com/leanprover-community/lean/blob/master/tests/lean/run/eq9.lean may have something to do with it

open nat
attribute [pattern] lt.base
attribute [pattern] lt.step

theorem lt_succ {a : nat} : ∀ {b : nat}, a < b → succ a < succ b
| .(succ a) (lt.base .(a))       := lt.base (succ a)
| .(succ b) (@lt.step .(a) b h)  := lt.step (lt_succ h)

[Mario Carneiro]

I don't know whether being a def affects its being used in pattern matching like this

[Gabriel Ebner]

Because Lean won't unfold theorems.

[Gabriel Ebner]

And you want to pattern-match on the constructors of <.