How to prove 20 < 42 ?

Stream: general

[Andrej Bauer]

What is the idiomatic way to prove 20 < 42? Is it to write nat.lt_of_sub_eq_succ rfl?

More generally, I am implementing binary search trees and need to generate lots of proofs of the form n < m where n and m are concrete natural numbers (numerals). To illustrate what I am looking for, suppose we have

def f (a b : ℕ) (p : a < b) : ℕ := a + b

I would like a smart_f such that if I write auto_f 20 42 then it will apply f 20 42 p where p is an auto-generated proof of 20 < 42. (The idea is to then have smart constructors for binary search trees.) Is this doable? With tactics?

[Floris van Doorn]

by norm_num

[Andrej Bauer]

Hmm, nat.lt_of_sub_eq_succ rfl seems to be linear in the size of the arguments. Is there a way to use fast subtraction or something to accomplish this?

[Mario Carneiro]

norm_num uses binary arithmetic

[Mario Carneiro]

and here is smart_f :

meta def by_norm_num := `[norm_num]
def auto_f (a b : ℕ) (p : a < b . by_norm_num) : ℕ := a + b

#check auto_f 20 42 -- auto_f 20 42 _ : ℕ

[Mario Carneiro]

(we have to work around some silly restrictions in auto params here; you can just use (h : a < b := by norm_num) in lean 4)