norm_num for USize

Stream: lean4

[Tomas Skrivan]

How do I make norm_num work for USize? I'm working with fixed size arrays where the size is USize and I want to simplify the array size in the type with norm_num.

[Shreyas Srinivas]

Lots of USize functions are implemented natively and implementation + system dependent. So even if you prove something about the function, it may not apply to the implementation. See USize.usize which depends on architecture and decEq which defers to implementation

See this example below. The two values are definitionally unequal but in the implementation they are equal:

import Mathlib.Tactic

example : (18446744073709552000 : USize) = (384 : USize) := by decide -- error as expected
example : (18446744073709552000 : USize) = (384 : USize) := by native_decide -- no error

#eval (18446744073709552000 : USize) -- most likely why there is no error

So would it make sense to prove anything about them?

[Tomas Skrivan]

I do not see the problem USize wraps around on overflow similar to Fin

example : (5 : Fin 10) = (15 : Fin 10) := by decide
example : (5 : Fin 10) = (15 : Fin 10) := by native_decide
example : (18446744073709552000 : Fin USize.size) = (384 : Fin USize.size) := by decide -- failed to reduce to 'true'
example : (18446744073709552000 : Fin USize.size) = (384 : Fin USize.size) := by native_decide

The by decide fails probably just because the numbers are so large.

[Tomas Skrivan]

In fact the spec of USize is just Fin USize.size

[Henrik Böving]

Do we have an axiom or w/e that claims we always have a 32 or 64 bit USize.size?

[Henrik Böving]

That way you could case split and norm_num individually right?

[Shreyas Srinivas]

example : 18446744073709552000 = 384 := by norm_num -- goal state False because it upcasts to Nat

[Shreyas Srinivas]

Wouldn't a time out would cause a maxHeartbeats error?

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Sorry : typo. I meant to type 6 instead of 3. Inequalities do seem to work for Fin. Still, its correspondence to execution may be poor for USize.

[Tomas Skrivan]

Ok this might be a XY problem

I have Expr e.g. (10*2 / 4 : USize) and I want to turn it into 5 : USize and proof that they are equal.

I though I would call conv norm_num on 10*2 / 4and get 5. Then I can call either norm_num or native_decide on 10*2/4 = 5.

[Tomas Skrivan]

I'm dealing with concrete and small enough numbers such that all the overflow nonsens is completely irrelevant

[Shreyas Srinivas]

I did a show term on two examples

import Mathlib

example : ((10 * 2/4) : USize) = (5 : USize) := by
  show_term norm_num

/-
refine
    Eq.mpr
      (id
        (congrFun
          (congrArg Eq
            (congrFun
              (congrArg HDiv.hDiv
                (Mathlib.Meta.NormNum.IsNat.to_eq
                  (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
                    (Mathlib.Meta.NormNum.isNat_ofNat USize (Eq.refl 10))
                    (Mathlib.Meta.NormNum.isNat_ofNat USize (Eq.refl 2)) (Eq.refl 20))
                  (Eq.refl 20)))
              4))
          5))
      ?_
-/
example : ((10 * 2/4)) = (5) := by
  show_term norm_num

/-
   exact
    of_eq_true
      (eq_true
        (Mathlib.Meta.NormNum.isNat_eq_true
          (Mathlib.Meta.NormNum.isNat_natDiv
            (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul)
              (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 10))
              (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl 20))
            (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 4)) (Eq.refl 5))
          (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 5))))
-/

[Tomas Skrivan]

But I need norm_num as a conv tactic not as proving tactic

[Shreyas Srinivas]

It doesn't work even outside conv. Because it can't figure out nat division in the Usize example even though it has converted the Usizes to Nats. EDIT: Inside conv it does the same thing for the USize example

[Eric Wieser]

I think the answer to your original question is "find or define the Ring instance"

[Shreyas Srinivas]

Why? Nat is not a ring and norm_num works for Nat.

[Shreyas Srinivas]

I think based on examining the terms that norm_num is recasting the multiplication of 10*2 back to USize. So it rules out natDiv for the next step.

[Shreyas Srinivas]

a solution might be to provide a Div instance or a div function for USize and tag it with norm_num's attribute somehow (not entirely sure how instances can be tagged).

[Kyle Miller]

norm_num only knows about Nat and Int division

[Kyle Miller]

If you want to get norm_num to work with USize division, either you have to write a @[norm_num] plugin for this operation, or you have to transform your expression into Nat arithmetic and run norm_num, if that's possible.

[Kyle Miller]

Kyle Miller said:

norm_num only knows about Nat and Int division

Oops, that's incorrect. It also knows about DivisionRing

[Kyle Miller]

I'm not sure this is documented anywhere, so I'll mention what else I found here. It appears to get norm_num to handle addition you just need docs#AddMonoidWithOne, and for multiplication you just need docs#Semiring

That's for natural number literals. To handle integer literals too, you need docs#Ring for both.

[Shreyas Srinivas]

Can confirm the issue with USize division:

UPDATE: The issue is with Fin division. See last example.

import Mathlib

example : (20 : USize) * (5 : USize) = (100 : USize) := by norm_num -- works
example : (20 : USize) + (5 : USize) = (25 : USize) := by norm_num -- works
example : (20 : USize) - (5 : USize) = (15 : USize) := by norm_num -- works
example : (20 : USize) / (5 : USize) = (4 : USize) := by norm_num -- doesn't work

example : (20 / 5) = 4 := by norm_num --  works for Nat division

def usizeDiv (x y : USize) := ((x.toNat : ℕ) / (y.toNat : ℕ)).toUSize

#eval usizeDiv 1 2

example : usizeDiv (20 : USize) (5 : USize) = (4 : USize) := by
  norm_num [usizeDiv] -- also doesn't work

example :  (20 : Fin 100) / (5 : Fin 100) = (4 : Fin 100) := by
  norm_num -- doesn't work

example :  (20 : Fin 89) / (5 : Fin 89) = (4 : Fin 89) := by
  norm_num -- doesn't work

[Shreyas Srinivas]

The issue is with Fin division.

[Shreyas Srinivas]

Probably because of the division being ill-defined in general modulo composites (though it also doesn't work for Fin 87 for example).

[Michael Stoll]

87 = 3 * 29

[Shreyas Srinivas]

Sorry 89

[Shreyas Srinivas]

Copy pasted the 89 version in the code sample above.

[Kyle Miller]

Here's a way to write your demonstrations to protect against it accidentally using rfl.

/- 100 -/
#norm_num (20 : USize) * (5 : USize)
/- 25 -/
#norm_num (20 : USize) + (5 : USize)
/- 15 -/
#norm_num (20 : USize) - (5 : USize)
/- 20 / 5 -/
#norm_num (20 : USize) / (5 : USize)

[Shreyas Srinivas]

That looks neater too. But yeah the reason norm_num doesn't work inside or outside conv on USize with Tomas's example is clearly because of division on Fins not being meaningfully defined

[Kyle Miller]

In particular, it's neither Nat, Int, nor a type with a docs#DivisionRing instance.

[Kyle Miller]

@Tomas Skrivan I didn't finish it (there's a missing proof), but here's a norm_num extension for USize division:

import Mathlib

/- 20 / 5 -/
#norm_num (20 : USize) / (5 : USize)

namespace Mathlib.Meta.NormNum
open Qq Lean Meta

theorem isNat_USizeDiv : {a b : USize} → {a' b' c : ℕ} →
    IsNat a a' → IsNat b b' → Nat.div (a' % USize.size) (b' % USize.size) = c → IsNat (a / b) c
  | _, _, a', b', _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨sorry⟩

@[norm_num (_ : USize) / (_ : USize)]
def evalUSizeDiv : NormNumExt where eval {u α} e := do
  let .app (.app f (a : Q($α))) (b : Q($α)) ← whnfR e | failure
  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q USize := ⟨⟩
  haveI' : $e =Q $a / $b := ⟨⟩
  guard <|← withNewMCtxDepth <| isDefEq f q(HDiv.hDiv (α := USize))
  let sUSize : Q(AddMonoidWithOne USize) := q(inferInstance)
  let ⟨na, pa⟩ ← deriveNat a sUSize; let ⟨nb, pb⟩ ← deriveNat b sUSize
  have nc : Q(ℕ) := mkRawNatLit ((na.natLit! % USize.size) / (nb.natLit! % USize.size))
  have pf : Q(Nat.div ($na % USize.size) ($nb % USize.size) = $nc) := (q(Eq.refl $nc) : Expr)
  return .isNat sUSize nc q(isNat_USizeDiv $pa $pb $pf)

end Mathlib.Meta.NormNum

/- 4 -/
#norm_num (20 : USize) / (5 : USize)
/- 5 -/
#norm_num (10*2 / 4 : USize)

You could extend it to be for Fin division in general.

[Tomas Skrivan]

Thanks, will look into it!

[Kyle Miller]

The sorry isn't so bad:

a' b' : ℕ
⊢ (↑a' / ↑b' : USize) = ↑(Nat.div (a' % USize.size) (b' % USize.size))

[Tomas Skrivan]

I might be still in XY problem, what I'm trying to do is to fill the hole in

2 * ?k + 1 = 3 * n + n + 1

and give a proof of it.

My idea is to run norm_num on (3* n + n + 1 - 1) / 2. Get 2*n and then prove 2 * (2*n) = 3 * n + n + 1 with norm_num again.

[Kyle Miller]

Hmm, a warning, my code is apparently buggy.

/-
application type mismatch
  Mathlib.Meta.NormNum.isNat_USizeDiv (Mathlib.Meta.NormNum.isNat_ofNat USize (Eq.refl 20))
    (Mathlib.Meta.NormNum.isNat_ofNat USize (Eq.refl 5)) (Eq.refl 4)
argument has type
  4 = 4
but function has type
  Nat.div (20 % USize.size) (5 % USize.size) = 4 → Mathlib.Meta.NormNum.IsNat (20 / 5) 4
-/
example : (20 : USize) / (5 : USize) = (4 : USize) := by
  norm_num

I'm not sure why the Nat.div isn't reducing here.

[Kyle Miller]

I'm not sure norm_num is the right tactic for that, since it's not designed for normalize expressions with free variables. Maybe you want to apply ring_nf to LHS - RHS = 0 and then try to solve for ?k?

[Tomas Skrivan]

Ahh using ring_nf on LHS - RHS is great idea!

[Shreyas Srinivas]

I think I have an idea what the issue with the code might be. See below:

import Mathlib

#eval USize.size

example : USize.size = 18446744073709551616 := by
  norm_num -- fails

[Kyle Miller]

Ah, System.Platform.numBits is opaque

[Kyle Miller]

I guess the norm_num extension could use docs#System.Platform.numBits_eq and create proofs in the special case that division gives the same result both in 32-bit and 64-bit systems.

[Shreyas Srinivas]

Kyle Miller said:

Ah, System.Platform.numBits is opaque

Yep

[Shreyas Srinivas]

Kyle Miller said:

I guess the norm_num extension could use docs#System.Platform.numBits_eq and create proofs in the special case that division gives the same result both in 32-bit and 64-bit systems.

A slightly weird and tedious to provide solution would be to hardcode the constant into platform specific releases of lean rather than get it from CPP code. Then it wouldn't have to be opaque.

[Shreyas Srinivas]

Maybe still have the native implementation but use it to tag the hardcoded version with an implemented_by attribute as with much of the Usize API for execution purposes.

[Shreyas Srinivas]

I hesitated to suggest this because any library dependent on this constant will be potentially bugged if run on a system with a different value, unless we provide some weird cmake style syntactic wizardry to modify lean files by lake when it builds or fetches caches. It is just a totally hideous solution.

[Kyle Miller]

How would proofs about USize carry over from one system to another? I think the purpose of it being opaque is to make it so the proof environment is oblivious to the word size.

[Kyle Miller]

I got the USize division to work for constants that fit inside Fin (2^32). Pasting it here:

import Mathlib

/- 20 / 5 -/
#norm_num (20 : USize) / (5 : USize)

namespace Mathlib.Meta.NormNum
open Qq Lean Meta

@[simp]
theorem succ_pow_numBits :
    Nat.succ (2 ^ System.Platform.numBits - 1) = 2 ^ System.Platform.numBits := by
  obtain (hbits | hbits) := System.Platform.numBits_eq <;> norm_num [hbits]

theorem isNat_USizeDiv : {a b : USize} → {a' b' c : ℕ} →
    IsNat a a' → IsNat b b' →
    Nat.div (a' % 2^32) (b' % 2^32) = c →
    Nat.div (a' % 2^64) (b' % 2^64) = c →
    IsNat (a / b) c
  | _, _, a', b', _, ⟨rfl⟩, ⟨rfl⟩, h32, h64 => by
    constructor
    unfold_projs
    unfold USize.div
    unfold_projs
    unfold Fin.div
    unfold_projs
    simp [USize.size]
    obtain (hbits | hbits) := System.Platform.numBits_eq
     <;> · simp [hbits, *]
           generalize_proofs h
           apply USize.eq_of_val_eq
           ext; rename_i x; change x = (x : Fin USize.size)
           rw [Fin.val_cast_of_lt h]

@[norm_num (_ : USize) / (_ : USize)]
def evalUSizeDiv : NormNumExt where eval {u α} e := do
  let .app (.app f (a : Q($α))) (b : Q($α)) ← whnfR e | failure
  haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q USize := ⟨⟩
  haveI' : $e =Q $a / $b := ⟨⟩
  guard <|← withNewMCtxDepth <| isDefEq f q(HDiv.hDiv (α := USize))
  let sUSize : Q(AddMonoidWithOne USize) := q(inferInstance)
  let ⟨na, pa⟩ ← deriveNat a sUSize; let ⟨nb, pb⟩ ← deriveNat b sUSize
  have nc32 : Q(ℕ) := mkRawNatLit ((na.natLit! % 2^32) / (nb.natLit! % 2^32))
  have nc64 : Q(ℕ) := mkRawNatLit ((na.natLit! % 2^64) / (nb.natLit! % 2^64))
  guard <| nc32 == nc64
  haveI' : $nc32 =Q $nc64 := ⟨⟩
  have pf32 : Q(Nat.div ($na % 2 ^ 32) ($nb % 2 ^ 32) = $nc32) := (q(Eq.refl $nc32) : Expr)
  have pf64 : Q(Nat.div ($na % 2 ^ 64) ($nb % 2 ^ 64) = $nc64) := (q(Eq.refl $nc64) : Expr)
  haveI' : Nat.div ($na % 2 ^ 64) ($nb % 2 ^ 64) =Q $nc64 := ⟨⟩
  return .isNat sUSize nc64 q(isNat_USizeDiv $pa $pb $pf32 $pf64)

end Mathlib.Meta.NormNum

/- 4 -/
#norm_num (20 : USize) / (5 : USize)
/- 5 -/
#norm_num (10*2 / 4 : USize)

example : (20 / 5 : USize) = 4 := by norm_num1
example : (10*2 / 4 : USize) = 5 := by norm_num1

[Shreyas Srinivas]

Kyle Miller said:

How would proofs about USize carry over from one system to another? .

It wouldn't. That is what I mean by "any library dependent on this constant will be potentially bugged if run on a system with a different value"

[Mario Carneiro]

it's worse than that, if you use oleans to ship compiled libraries (as mathlib does) then the downstream code running on another target architecture can prove False by combining what it knows about the constant with what mathlib proved about it on another target

[Mario Carneiro]

Then again, oleans are definitely not portable between 64 bit and 32 bit systems, and mathlib cache does not support 32 bit arches

[Shreyas Srinivas]

mixing 32 bit and 64 bit oleans should lead to ABI incompatibilities, ruling out the compilation of such programs.

[Shreyas Srinivas]

There is a more basic question I don't know the answer to: Do we even support any 32 bit systems?

[Mario Carneiro]

Besides compression, another advantage of .ltar files is their cross-platform compatibility. The packing / unpacking process can produce compatible oleans across systems

[Mario Carneiro]

Shreyas Srinivas said:

There is a more basic question I don't know the answer to: Do we even support any 32 bit systems?

Lean is technically compilable on 32 bit but I don't think there is much support

[Sebastian Ullrich]

https://lean-lang.org/lean4/doc/setup.html#supported-platforms

[Shreyas Srinivas]

Sebastian Ullrich said:

https://lean-lang.org/lean4/doc/setup.html#supported-platforms

This I know. I recently read FPIL. I am thinking about lean as whole (i.e. vscode + lean + lake + elan...) . For example here's this announcement on the vscode page that they are not supporting 32 bit linux since 2019: https://code.visualstudio.com/updates/v1_32 (scroll down to the Engineering section)

[Mario Carneiro]

like it says, tier 2 support means that it's not tested

[Mario Carneiro]

so the stuff is there in principle but it might not all work together

[Sebastian Ullrich]

In practice the only 32-bit platform we're interested in is wasm. Whether a standard setup for it, which does not exist yet, will consist of cross-compiling from x86-64 or x86 is an open question.