summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2023-10-16 11:20:57 +0200
committerSon Ho2023-10-16 11:20:57 +0200
commit2ec2e374302c772ff2c6a26e39451b4e49e13a16 (patch)
treeda523de2f105f28c995ef8da01b320074b63f366 /backends/lean/Base/Primitives
parentcbb2d05e0db6bedf9d6844f29ee25b95429b994c (diff)
parent40ed38216499ea1bf58b8acbcd05b2cd97329830 (diff)
Merge branch 'main' into son_traits and fix some issues
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean226
1 files changed, 198 insertions, 28 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 9e65d3c0..ec9665a5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -533,6 +533,36 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+@[cepspec] theorem Isize.add_spec {x y : Isize}
+ (hmin : Isize.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ Isize.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I8.add_spec {x y : I8}
+ (hmin : I8.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I8.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I16.add_spec {x y : I16}
+ (hmin : I16.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I16.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I32.add_spec {x y : I32}
+ (hmin : I32.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I32.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I64.add_spec {x y : I64}
+ (hmin : I64.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I64.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I128.add_spec {x y : I128}
+ (hmin : I128.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I128.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.sub_spec {ty} {x y : Scalar ty}
@@ -582,6 +612,36 @@ theorem Scalar.sub_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+@[cepspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ Isize.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I8.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I16.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I32.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I64.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I128.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
theorem Scalar.mul_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val * y.val)
@@ -628,6 +688,36 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+@[cepspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ Isize.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I8.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I16.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I32.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I64.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I128.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.div_spec {ty} {x y : Scalar ty}
@@ -681,6 +771,48 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+@[cepspec] theorem Isize.div_spec (x : Isize) {y : Isize}
+ (hnz : y.val ≠ 0)
+ (hmin : Isize.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ Isize.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I8.div_spec (x : I8) {y : I8}
+ (hnz : y.val ≠ 0)
+ (hmin : I8.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I8.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I16.div_spec (x : I16) {y : I16}
+ (hnz : y.val ≠ 0)
+ (hmin : I16.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I16.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I32.div_spec (x : I32) {y : I32}
+ (hnz : y.val ≠ 0)
+ (hmin : I32.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I32.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I64.div_spec (x : I64) {y : I64}
+ (hnz : y.val ≠ 0)
+ (hmin : I64.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I64.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I128.div_spec (x : I128) {y : I128}
+ (hnz : y.val ≠ 0)
+ (hmin : I128.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I128.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.rem_spec {ty} {x y : Scalar ty}
@@ -734,6 +866,41 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
+@[cepspec] theorem I8.rem_spec (x : I8) {y : I8}
+ (hnz : y.val ≠ 0)
+ (hmin : I8.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I8.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
+
+@[cepspec] theorem I16.rem_spec (x : I16) {y : I16}
+ (hnz : y.val ≠ 0)
+ (hmin : I16.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I16.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
+
+@[cepspec] theorem I32.rem_spec (x : I32) {y : I32}
+ (hnz : y.val ≠ 0)
+ (hmin : I32.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I32.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
+
+@[cepspec] theorem I64.rem_spec (x : I64) {y : I64}
+ (hnz : y.val ≠ 0)
+ (hmin : I64.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I64.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
+
+@[cepspec] theorem I128.rem_spec (x : I128) {y : I128}
+ (hnz : y.val ≠ 0)
+ (hmin : I128.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I128.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
+
-- ofIntCore
-- TODO: typeclass?
def Isize.ofIntCore := @Scalar.ofIntCore .Isize
@@ -751,33 +918,34 @@ def U128.ofIntCore := @Scalar.ofIntCore .U128
-- ofInt
-- TODO: typeclass?
-def Isize.ofInt := @Scalar.ofInt .Isize
-def I8.ofInt := @Scalar.ofInt .I8
-def I16.ofInt := @Scalar.ofInt .I16
-def I32.ofInt := @Scalar.ofInt .I32
-def I64.ofInt := @Scalar.ofInt .I64
-def I128.ofInt := @Scalar.ofInt .I128
-def Usize.ofInt := @Scalar.ofInt .Usize
-def U8.ofInt := @Scalar.ofInt .U8
-def U16.ofInt := @Scalar.ofInt .U16
-def U32.ofInt := @Scalar.ofInt .U32
-def U64.ofInt := @Scalar.ofInt .U64
-def U128.ofInt := @Scalar.ofInt .U128
-
-postfix:74 "%isize" => Isize.ofInt
-postfix:74 "%i8" => I8.ofInt
-postfix:74 "%i16" => I16.ofInt
-postfix:74 "%i32" => I32.ofInt
-postfix:74 "%i64" => I64.ofInt
-postfix:74 "%i128" => I128.ofInt
-postfix:74 "%usize" => Usize.ofInt
-postfix:74 "%u8" => U8.ofInt
-postfix:74 "%u16" => U16.ofInt
-postfix:74 "%u32" => U32.ofInt
-postfix:74 "%u64" => U64.ofInt
-postfix:74 "%u128" => U128.ofInt
-
-example : Result U32 := 1%u32 + 2%u32
+abbrev Isize.ofInt := @Scalar.ofInt .Isize
+abbrev I8.ofInt := @Scalar.ofInt .I8
+abbrev I16.ofInt := @Scalar.ofInt .I16
+abbrev I32.ofInt := @Scalar.ofInt .I32
+abbrev I64.ofInt := @Scalar.ofInt .I64
+abbrev I128.ofInt := @Scalar.ofInt .I128
+abbrev Usize.ofInt := @Scalar.ofInt .Usize
+abbrev U8.ofInt := @Scalar.ofInt .U8
+abbrev U16.ofInt := @Scalar.ofInt .U16
+abbrev U32.ofInt := @Scalar.ofInt .U32
+abbrev U64.ofInt := @Scalar.ofInt .U64
+abbrev U128.ofInt := @Scalar.ofInt .U128
+
+postfix:max "#isize" => Isize.ofInt
+postfix:max "#i8" => I8.ofInt
+postfix:max "#i16" => I16.ofInt
+postfix:max "#i32" => I32.ofInt
+postfix:max "#i64" => I64.ofInt
+postfix:max "#i128" => I128.ofInt
+postfix:max "#usize" => Usize.ofInt
+postfix:max "#u8" => U8.ofInt
+postfix:max "#u16" => U16.ofInt
+postfix:max "#u32" => U32.ofInt
+postfix:max "#u64" => U64.ofInt
+postfix:max "#u128" => U128.ofInt
+
+-- Testing the notations
+example : Result Usize := 0#usize + 1#usize
-- TODO: factor those lemmas out
@[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
@@ -819,7 +987,6 @@ example : Result U32 := 1%u32 + 2%u32
@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
apply Scalar.ofInt_val_eq h
-
-- Comparisons
instance {ty} : LT (Scalar ty) where
lt a b := LT.lt a.val b.val
@@ -847,6 +1014,9 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
coe := λ v => v.val
+@[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
+ intro i j; cases i; cases j; simp
+
-- -- We now define a type class that subsumes the various machine integer types, so
-- -- as to write a concise definition for scalar_cast, rather than exhaustively
-- -- enumerating all of the possible pairs. We remark that Rust has sane semantics