Porting Nat/Digits

Stream: mathlib4

[Ryan Lahfa]

Hello there, I'm trying to port Nat/Digits in Lean 4, I would like to extend normNum to support inequalities, if I understand well, it requires to recognize f.isConstOf ``Nat.ble and dispatch to some evaluation which will provide a couple (term value of truth, term proof of the value of truth), I am just uncertain on how to handle the stuff regarding the orders as it seems like the actual code supports numerals from semiring and I am confused about semirings/numerals/(lt|le) orders ; should I lift the numerals to Nat and think only over these types? Can I read more about this, except the original tactic?

Also, is the plan:

• proving that a numeral is > 0
• proving that a numeral is ≥ x
• proving that a numeral is > x

is the good one?

In the same vein, I would like to work on rcases, but I wonder if that's needed at all, it looks like match x with is enough (at least, that's how I replaced most of rcases I encountered in Lean 3's code)

And last question for now, here's this little theorem:

def ofDigits {α: Type} [Semiring α] (b: α) : List ℕ → α
| [] => 0
| h :: t => Numeric.ofNat h + b * ofDigits b t -- should have auto-coercions?

In Lean 3, there is no need to specify the explicit Numeric.ofNat, shouldn't there be some coe lemma for this too?

Thanks in advance!

[Ryan Lahfa]

Also, I realize there is no instance : Semiring N, should I lift one from simpler structures to get auto-simplification in the natural integers semiring?

[Kevin Buzzard]

Somebody once posted some "lean 4 natural number game levels" but probably proving semiring isn't hard, it's inequalities which can get subtle

[Mario Carneiro]

I think rcases should be ported, with the lean 3 syntax

[Mario Carneiro]

there are some possible syntax refinements but match is not a complete replacement, since it doesn't generalize arguments in the same way as cases and generates lots of inaccessible names

[Mario Carneiro]

The goal for normNum inequalities would be to prove that (a < b) = True or (a < b) = False where a and b are numerals

[Mario Carneiro]

this would be done by reducing the problem to Nat.ble and using rfl

[Chris B]

Mario Carneiro said:

The goal for normNum inequalities would be to prove that (a < b) = True or (a < b) = False where a and b are numerals

What typeclass should introduce (<=) to normNum? It looks like it was linear_ordered_semiring in lean 3.

[Mario Carneiro]

If you want to start working on it now, feel free to invent your own typeclass that includes whatever norm_num uses. Later it will probably be replaced with LinearOrderedSemiring

[Mario Carneiro]

I guess the main thing the new norm_num needs to know is that ofNat a < ofNat b <-> a < b and then the rhs is evaluated in the kernel

[Chris B]

Ok, the second part is what I had in mind.