summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2024-04-12 08:33:21 +0200
committerSon Ho2024-04-12 08:33:21 +0200
commitba7462d7da5185456298f240f2e6f6dac240cc7e (patch)
tree9dfccfe7582ddbe2886d5428054a891f10a9f860 /backends
parentb6421bc01df278f625a8c95b4ea36ad2e4355718 (diff)
Update the core.num.checked_* definitions
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean264
1 files changed, 233 insertions, 31 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 53bc7854..d1f7bee7 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -325,33 +325,65 @@ instance [Decide (Scalar.cMin ty ≤ v ∧ v ≤ Scalar.cMax ty)] : InBounds ty
@[reducible, match_pattern] def Scalar.ofInt {ty : ScalarTy} (x : Int) [InBounds ty x] : Scalar ty :=
Scalar.ofIntCore x (Scalar.bound_suffices ty x InBounds.hInBounds)
-@[simp] def Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
+@[simp] abbrev Scalar.in_bounds (ty : ScalarTy) (x : Int) : Prop :=
+ Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
+
+@[simp] abbrev Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
(Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty)
-theorem Scalar.check_bounds_prop {ty : ScalarTy} {x : Int} (h: Scalar.check_bounds ty x) :
- Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by
+theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
+ (h: Scalar.check_bounds ty x) :
+ Scalar.in_bounds ty x := by
simp at *
have ⟨ hmin, hmax ⟩ := h
have hbmin := Scalar.cMin_bound ty
have hbmax := Scalar.cMax_bound ty
cases hmin <;> cases hmax <;> apply And.intro <;> linarith
+theorem Scalar.check_bounds_eq_in_bounds (ty : ScalarTy) (x : Int) :
+ Scalar.check_bounds ty x ↔ Scalar.in_bounds ty x := by
+ constructor <;> intro h
+ . apply (check_bounds_imp_in_bounds h)
+ . simp_all
+
-- Further thoughts: look at what has been done here:
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Basic.lean
-- and
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
-- which both contain a fair amount of reasoning already!
-def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
+def Scalar.tryMkOpt (ty : ScalarTy) (x : Int) : Option (Scalar ty) :=
if h:Scalar.check_bounds ty x then
-- If we do:
-- ```
- -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_prop h)
+ -- let ⟨ hmin, hmax ⟩ := (Scalar.check_bounds_imp_in_bounds h)
-- Scalar.ofIntCore x hmin hmax
-- ```
-- then normalization blocks (for instance, some proofs which use reflexivity fail).
-- However, the version below doesn't block reduction (TODO: investigate):
- ok (Scalar.ofIntCore x (Scalar.check_bounds_prop h))
- else fail integerOverflow
+ some (Scalar.ofIntCore x (Scalar.check_bounds_imp_in_bounds h))
+ else none
+
+def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a :=
+ match x with
+ | some x => ok x
+ | none => fail e
+
+def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
+ Result.ofOption (tryMkOpt ty x) integerOverflow
+
+theorem Scalar.tryMk_eq (ty : ScalarTy) (x : Int) :
+ match tryMk ty x with
+ | ok y => y.val = x ∧ in_bounds ty x
+ | fail _ => ¬ (in_bounds ty x)
+ | _ => False := by
+ simp [tryMk, ofOption, tryMkOpt, ofIntCore]
+ have h := check_bounds_eq_in_bounds ty x
+ split_ifs <;> simp_all
+
+@[simp] theorem Scalar.tryMk_eq_div (ty : ScalarTy) (x : Int) :
+ tryMk ty x = div ↔ False := by
+ simp [tryMk, ofOption, tryMkOpt]
+ split_ifs <;> simp
def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
@@ -583,42 +615,117 @@ instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where
/- A helper function that converts failure to none and success to some
TODO: move up to Base module? -/
-@[simp] abbrev Option.ofResult : Result (Scalar ty) → Result (Option (Scalar ty))
- | Result.ret z => Result.ret (some z)
- | Result.fail _ => Result.ret none
- | Result.div => Result.div
+def Option.ofResult {a : Type u} (x : Result a) :
+ Option a :=
+ match x with
+ | ok x => some x
+ | _ => none
/- [core::num::{T}::checked_add] -/
-def core.num.checked_add (x y : Scalar ty) : Result (Option (Scalar ty)) :=
+def core.num.checked_add (x y : Scalar ty) : Option (Scalar ty) :=
Option.ofResult (x + y)
+def U8.checked_add (x y : U8) : Option U8 := core.num.checked_add x y
+def U16.checked_add (x y : U16) : Option U16 := core.num.checked_add x y
+def U32.checked_add (x y : U32) : Option U32 := core.num.checked_add x y
+def U64.checked_add (x y : U64) : Option U64 := core.num.checked_add x y
+def U128.checked_add (x y : U128) : Option U128 := core.num.checked_add x y
+def Usize.checked_add (x y : Usize) : Option Usize := core.num.checked_add x y
+def I8.checked_add (x y : I8) : Option I8 := core.num.checked_add x y
+def I16.checked_add (x y : I16) : Option I16 := core.num.checked_add x y
+def I32.checked_add (x y : I32) : Option I32 := core.num.checked_add x y
+def I64.checked_add (x y : I64) : Option I64 := core.num.checked_add x y
+def I128.checked_add (x y : I128) : Option I128 := core.num.checked_add x y
+def Isize.checked_add (x y : Isize) : Option Isize := core.num.checked_add x y
+
/- [core::num::{T}::checked_sub] -/
-def core.num.checked_sub (x y : Scalar ty) : Result (Option (Scalar ty)) :=
+def core.num.checked_sub (x y : Scalar ty) : Option (Scalar ty) :=
Option.ofResult (x - y)
+def U8.checked_sub (x y : U8) : Option U8 := core.num.checked_sub x y
+def U16.checked_sub (x y : U16) : Option U16 := core.num.checked_sub x y
+def U32.checked_sub (x y : U32) : Option U32 := core.num.checked_sub x y
+def U64.checked_sub (x y : U64) : Option U64 := core.num.checked_sub x y
+def U128.checked_sub (x y : U128) : Option U128 := core.num.checked_sub x y
+def Usize.checked_sub (x y : Usize) : Option Usize := core.num.checked_sub x y
+def I8.checked_sub (x y : I8) : Option I8 := core.num.checked_sub x y
+def I16.checked_sub (x y : I16) : Option I16 := core.num.checked_sub x y
+def I32.checked_sub (x y : I32) : Option I32 := core.num.checked_sub x y
+def I64.checked_sub (x y : I64) : Option I64 := core.num.checked_sub x y
+def I128.checked_sub (x y : I128) : Option I128 := core.num.checked_sub x y
+def Isize.checked_sub (x y : Isize) : Option Isize := core.num.checked_sub x y
+
/- [core::num::{T}::checked_mul] -/
-def core.num.checked_mul (x y : Scalar ty) : Result (Option (Scalar ty)) :=
+def core.num.checked_mul (x y : Scalar ty) : Option (Scalar ty) :=
Option.ofResult (x * y)
+def U8.checked_mul (x y : U8) : Option U8 := core.num.checked_mul x y
+def U16.checked_mul (x y : U16) : Option U16 := core.num.checked_mul x y
+def U32.checked_mul (x y : U32) : Option U32 := core.num.checked_mul x y
+def U64.checked_mul (x y : U64) : Option U64 := core.num.checked_mul x y
+def U128.checked_mul (x y : U128) : Option U128 := core.num.checked_mul x y
+def Usize.checked_mul (x y : Usize) : Option Usize := core.num.checked_mul x y
+def I8.checked_mul (x y : I8) : Option I8 := core.num.checked_mul x y
+def I16.checked_mul (x y : I16) : Option I16 := core.num.checked_mul x y
+def I32.checked_mul (x y : I32) : Option I32 := core.num.checked_mul x y
+def I64.checked_mul (x y : I64) : Option I64 := core.num.checked_mul x y
+def I128.checked_mul (x y : I128) : Option I128 := core.num.checked_mul x y
+def Isize.checked_mul (x y : Isize) : Option Isize := core.num.checked_mul x y
+
/- [core::num::{T}::checked_div] -/
-def core.num.checked_div (x y : Scalar ty) : Result (Option (Scalar ty)) :=
+def core.num.checked_div (x y : Scalar ty) : Option (Scalar ty) :=
Option.ofResult (x / y)
-/- [core::num::{T}::checked_mod] -/
-def core.num.checked_mod (x y : Scalar ty) : Result (Option (Scalar ty)) :=
+def U8.checked_div (x y : U8) : Option U8 := core.num.checked_div x y
+def U16.checked_div (x y : U16) : Option U16 := core.num.checked_div x y
+def U32.checked_div (x y : U32) : Option U32 := core.num.checked_div x y
+def U64.checked_div (x y : U64) : Option U64 := core.num.checked_div x y
+def U128.checked_div (x y : U128) : Option U128 := core.num.checked_div x y
+def Usize.checked_div (x y : Usize) : Option Usize := core.num.checked_div x y
+def I8.checked_div (x y : I8) : Option I8 := core.num.checked_div x y
+def I16.checked_div (x y : I16) : Option I16 := core.num.checked_div x y
+def I32.checked_div (x y : I32) : Option I32 := core.num.checked_div x y
+def I64.checked_div (x y : I64) : Option I64 := core.num.checked_div x y
+def I128.checked_div (x y : I128) : Option I128 := core.num.checked_div x y
+def Isize.checked_div (x y : Isize) : Option Isize := core.num.checked_div x y
+
+/- [core::num::{T}::checked_rem] -/
+def core.num.checked_rem (x y : Scalar ty) : Option (Scalar ty) :=
Option.ofResult (x % y)
+def U8.checked_rem (x y : U8) : Option U8 := core.num.checked_rem x y
+def U16.checked_rem (x y : U16) : Option U16 := core.num.checked_rem x y
+def U32.checked_rem (x y : U32) : Option U32 := core.num.checked_rem x y
+def U64.checked_rem (x y : U64) : Option U64 := core.num.checked_rem x y
+def U128.checked_rem (x y : U128) : Option U128 := core.num.checked_rem x y
+def Usize.checked_rem (x y : Usize) : Option Usize := core.num.checked_rem x y
+def I8.checked_rem (x y : I8) : Option I8 := core.num.checked_rem x y
+def I16.checked_rem (x y : I16) : Option I16 := core.num.checked_rem x y
+def I32.checked_rem (x y : I32) : Option I32 := core.num.checked_rem x y
+def I64.checked_rem (x y : I64) : Option I64 := core.num.checked_rem x y
+def I128.checked_rem (x y : I128) : Option I128 := core.num.checked_rem x y
+def Isize.checked_rem (x y : Isize) : Option Isize := core.num.checked_rem x y
+
+theorem Scalar.add_equiv {ty} {x y : Scalar ty} :
+ match x + y with
+ | ok z => Scalar.in_bounds ty (↑x + ↑y) ∧ (↑z : Int) = ↑x + ↑y
+ | fail _ => ¬ (Scalar.in_bounds ty (↑x + ↑y))
+ | _ => ⊥ := by
+ -- Applying the unfoldings only inside the match
+ conv in _ + _ => unfold HAdd.hAdd instHAddScalarResult; simp [add]
+ have h := tryMk_eq ty (↑x + ↑y)
+ simp [in_bounds] at h
+ split at h <;> simp_all [check_bounds_eq_in_bounds]
+
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.add_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ ↑x + y.val)
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
(∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
- -- Applying the unfoldings only on the left
- conv => congr; ext; lhs; unfold HAdd.hAdd instHAddScalarResult; simp [add, tryMk]
- split
- . simp [pure]; rfl
- . tauto
+ have h := @add_equiv ty x y
+ split at h <;> simp_all
+ apply h
theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x + ↑y ≤ Scalar.max ty) :
@@ -684,17 +791,36 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
+theorem core.num.checked_add_spec {ty} {x y : Scalar ty} :
+ match core.num.checked_add x y with
+ | some z => Scalar.in_bounds ty (↑x + ↑y) ∧ ↑z = (↑x + ↑y : Int)
+ | none => ¬ (Scalar.in_bounds ty (↑x + ↑y)) := by
+ have h := Scalar.tryMk_eq ty (↑x + ↑y)
+ simp only [checked_add, Option.ofResult]
+ cases heq: x + y <;> simp_all <;> simp [HAdd.hAdd, Scalar.add] at heq
+ <;> simp [Add.add] at heq
+ <;> simp_all
+
+theorem Scalar.sub_equiv {ty} {x y : Scalar ty} :
+ match x - y with
+ | ok z => Scalar.in_bounds ty (↑x - ↑y) ∧ (↑z : Int) = ↑x - ↑y
+ | fail _ => ¬ (Scalar.in_bounds ty (↑x - ↑y))
+ | _ => ⊥ := by
+ -- Applying the unfoldings only inside the match
+ conv in _ - _ => unfold HSub.hSub instHSubScalarResult; simp [sub]
+ have h := tryMk_eq ty (↑x - ↑y)
+ simp [in_bounds] at h
+ split at h <;> simp_all [check_bounds_eq_in_bounds]
+
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.sub_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ ↑x - ↑y)
(hmax : ↑x - ↑y ≤ Scalar.max ty) :
∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
- conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub]
- split
- . simp [pure]
- rfl
- . tauto
+ have h := @sub_equiv ty x y
+ split at h <;> simp_all
+ apply h
theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
{x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
@@ -768,12 +894,33 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty}
(hmax : ↑x * ↑y ≤ Scalar.max ty) :
∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
conv => congr; ext; lhs; simp [HMul.hMul]
- simp [mul, tryMk]
- split
+ simp [mul, tryMk, tryMkOpt, ofOption]
+ split_ifs
. simp [pure]
rfl
. tauto
+theorem core.num.checked_sub_spec {ty} {x y : Scalar ty} :
+ match core.num.checked_sub x y with
+ | some z => Scalar.in_bounds ty (↑x - ↑y) ∧ ↑z = (↑x - ↑y : Int)
+ | none => ¬ (Scalar.in_bounds ty (↑x - ↑y)) := by
+ have h := Scalar.tryMk_eq ty (↑x - ↑y)
+ simp only [checked_sub, Option.ofResult]
+ have add_neg_eq : x.val + (-y.val) = x.val - y.val := by omega -- TODO: why do we need this??
+ cases heq: x - y <;> simp_all <;> simp only [HSub.hSub, Scalar.sub, Sub.sub, Int.sub] at heq
+ <;> simp_all
+
+theorem Scalar.mul_equiv {ty} {x y : Scalar ty} :
+ match x * y with
+ | ok z => Scalar.in_bounds ty (↑x * ↑y) ∧ (↑z : Int) = ↑x * ↑y
+ | fail _ => ¬ (Scalar.in_bounds ty (↑x * ↑y))
+ | _ => ⊥ := by
+ -- Applying the unfoldings only inside the match
+ conv in _ * _ => unfold HMul.hMul instHMulScalarResult; simp [mul]
+ have h := tryMk_eq ty (↑x * ↑y)
+ simp [in_bounds] at h
+ split at h <;> simp_all [check_bounds_eq_in_bounds]
+
theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
(hmax : ↑x * ↑y ≤ Scalar.max ty) :
∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
@@ -838,6 +985,29 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
+theorem core.num.checked_mul_spec {ty} {x y : Scalar ty} :
+ match core.num.checked_mul x y with
+ | some z => Scalar.in_bounds ty (↑x * ↑y) ∧ ↑z = (↑x * ↑y : Int)
+ | none => ¬ (Scalar.in_bounds ty (↑x * ↑y)) := by
+ have h := Scalar.tryMk_eq ty (↑x * ↑y)
+ simp only [checked_mul, Option.ofResult]
+ have : Int.mul ↑x ↑y = ↑x * ↑y := by simp -- TODO: why do we need this??
+ cases heq: x * y <;> simp_all <;> simp only [HMul.hMul, Scalar.mul, Mul.mul] at heq
+ <;> simp [add_neg_eq] at heq
+ <;> simp_all
+
+theorem Scalar.div_equiv {ty} {x y : Scalar ty} :
+ match x / y with
+ | ok z => y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_div ↑x ↑y) ∧ (↑z : Int) = scalar_div ↑x ↑y
+ | fail _ => ¬ (y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_div ↑x ↑y))
+ | _ => ⊥ := by
+ -- Applying the unfoldings only inside the match
+ conv in _ / _ => unfold HDiv.hDiv instHDivScalarResult; simp [div]
+ have h := tryMk_eq ty (scalar_div ↑x ↑y)
+ simp [in_bounds] at h
+ split_ifs <;> simp <;>
+ split at h <;> simp_all [check_bounds_eq_in_bounds]
+
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.div_spec {ty} {x y : Scalar ty}
@@ -846,7 +1016,7 @@ theorem Scalar.div_spec {ty} {x y : Scalar ty}
(hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) :
∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
simp [HDiv.hDiv, div, Div.div]
- simp [tryMk, *]
+ simp [tryMk, tryMkOpt, ofOption, *]
rfl
theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
@@ -932,6 +1102,28 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
+theorem core.num.checked_div_spec {ty} {x y : Scalar ty} :
+ match core.num.checked_div x y with
+ | some z => y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_div ↑x ↑y) ∧ ↑z = (scalar_div ↑x ↑y : Int)
+ | none => ¬ (y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_div ↑x ↑y)) := by
+ have h := Scalar.tryMk_eq ty (scalar_div ↑x ↑y)
+ simp only [checked_div, Option.ofResult]
+ cases heq0: (y.val = 0 : Bool) <;>
+ cases heq1: x / y <;> simp_all <;> simp only [HDiv.hDiv, Scalar.div, Div.div] at heq1
+ <;> simp_all
+
+theorem Scalar.rem_equiv {ty} {x y : Scalar ty} :
+ match x % y with
+ | ok z => y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_rem ↑x ↑y) ∧ (↑z : Int) = scalar_rem ↑x ↑y
+ | fail _ => ¬ (y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_rem ↑x ↑y))
+ | _ => ⊥ := by
+ -- Applying the unfoldings only inside the match
+ conv in _ % _ => unfold HMod.hMod instHModScalarResult; simp [rem]
+ have h := tryMk_eq ty (scalar_rem ↑x ↑y)
+ simp [in_bounds] at h
+ split_ifs <;> simp <;>
+ split at h <;> simp_all [check_bounds_eq_in_bounds]
+
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.rem_spec {ty} {x y : Scalar ty}
@@ -940,7 +1132,7 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty}
(hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) :
∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
simp [HMod.hMod, rem]
- simp [tryMk, *]
+ simp [tryMk, tryMkOpt, ofOption, *]
rfl
theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
@@ -1019,6 +1211,16 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
+theorem core.num.checked_rem_spec {ty} {x y : Scalar ty} :
+ match core.num.checked_rem x y with
+ | some z => y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_rem ↑x ↑y) ∧ ↑z = (scalar_rem ↑x ↑y : Int)
+ | none => ¬ (y.val ≠ 0 ∧ Scalar.in_bounds ty (scalar_rem ↑x ↑y)) := by
+ have h := Scalar.tryMk_eq ty (scalar_rem ↑x ↑y)
+ simp only [checked_rem, Option.ofResult]
+ cases heq0: (y.val = 0 : Bool) <;>
+ cases heq1: x % y <;> simp_all <;> simp only [HMod.hMod, Scalar.rem, Mod.mod] at heq1
+ <;> simp_all
+
-- ofIntCore
-- TODO: typeclass?
def Isize.ofIntCore := @Scalar.ofIntCore .Isize