diff options
author | Ryan Lahfa | 2024-05-15 15:42:18 +0200 |
---|---|---|
committer | Ryan Lahfa | 2024-05-24 16:07:33 +0200 |
commit | 3ff6d93822fe5b2e233d4b12b88b38839c8533c5 (patch) | |
tree | 9ea5aa8be6ba2f0f2af035d10cc50f8f05d43047 /backends/lean/Base/Primitives | |
parent | 3c8ea6df20f92be9c341bbfb748f65d6c598fead (diff) |
feat: add small pieces of max theory
`0#ty` is neutral for `max` for unsigned integers.
Without the `Fact` instances, those theorems are not as automatic as
they could be.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index f08b8dec..8fb067e1 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -146,6 +146,25 @@ def ScalarTy.isSigned (ty : ScalarTy) : Bool := | U64 | U128 => false +-- FIXME(chore): bulk prove them via macro? +instance : Fact (¬ ScalarTy.isSigned .Usize) where + out := by decide + +instance : Fact (¬ ScalarTy.isSigned .U8) where + out := by decide + +instance : Fact (¬ ScalarTy.isSigned .U16) where + out := by decide + +instance : Fact (¬ ScalarTy.isSigned .U32) where + out := by decide + +instance : Fact (¬ ScalarTy.isSigned .U64) where + out := by decide + +instance : Fact (¬ ScalarTy.isSigned .U128) where + out := by decide + def Scalar.smin (ty : ScalarTy) : Int := match ty with @@ -386,6 +405,10 @@ theorem Scalar.tryMk_eq (ty : ScalarTy) (x : Int) : simp [tryMk, ofOption, tryMkOpt] split_ifs <;> simp +instance (ty: ScalarTy) : InBounds ty 0 where + hInBounds := by + induction ty <;> simp [Scalar.cMax, Scalar.cMin, Scalar.max, Scalar.min] <;> decide + def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val) -- Our custom remainder operation, which satisfies the semantics of Rust @@ -1431,6 +1454,22 @@ theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (↠refine' absurd _ (lt_irrefl a) exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption)) +-- Max theory +-- TODO: do the min theory later on. + +theorem Scalar.zero_le_unsigned {ty} (s: ¬ ty.isSigned) (x: Scalar ty): Scalar.ofInt 0 ≤ x := by + apply (Scalar.le_equiv _ _).2 + convert x.hmin + cases ty <;> simp [ScalarTy.isSigned] at s <;> simp [Scalar.min] + +@[simp] +theorem Scalar.max_unsigned_left_zero_eq {ty} [s: Fact (¬ ty.isSigned)] (x: Scalar ty): + Max.max (Scalar.ofInt 0) x = x := max_eq_right (Scalar.zero_le_unsigned s.out x) + +@[simp] +theorem Scalar.max_unsigned_right_zero_eq {ty} [s: Fact (¬ ty.isSigned)] (x: Scalar ty): + Max.max x (Scalar.ofInt 0) = x := max_eq_left (Scalar.zero_le_unsigned s.out x) + -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry |