summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2024-02-09 17:19:51 +0100
committerSon Ho2024-02-09 17:19:51 +0100
commitc285a3ff4fa6e7f8de182e574a7eb6d164cbee46 (patch)
tree22cf28a3c36ba53f445a89047214fafa1aa8eebd /backends/lean/Base/Primitives
parent08707b6c64d6487e5cb038a802f8ebb97ba6c975 (diff)
Cleanup a bit Scalar.lean
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean396
1 files changed, 198 insertions, 198 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index b11bd2a1..285bc7fb 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -271,6 +271,9 @@ structure Scalar (ty : ScalarTy) where
hmax : val ≤ Scalar.max ty
deriving Repr
+instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
+ coe := λ v => v.val
+
theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
@@ -535,9 +538,9 @@ instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.add_spec {ty} {x y : Scalar ty}
- (hmin : Scalar.min ty ≤ x.val + y.val)
- (hmax : x.val + y.val ≤ Scalar.max ty) :
- (∃ z, x + y = ret z ∧ z.val = x.val + y.val) := by
+ (hmin : Scalar.min ty ≤ ↑x + y.val)
+ (hmax : ↑x + ↑y ≤ Scalar.max ty) :
+ (∃ z, x + y = ret 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
@@ -545,75 +548,75 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
. tauto
theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
- (hmax : x.val + y.val ≤ Scalar.max ty) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
- have hmin : Scalar.min ty ≤ x.val + y.val := by
+ (hmax : ↑x + ↑y ≤ Scalar.max ty) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+ have hmin : Scalar.min ty ≤ ↑x + ↑y := by
have hx := x.hmin
have hy := y.hmin
cases ty <;> simp [min, ScalarTy.isSigned] at * <;> linarith
apply add_spec <;> assumption
/- Fine-grained theorems -/
-@[pspec] theorem Usize.add_spec {x y : Usize} (hmax : x.val + y.val ≤ Usize.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
-@[pspec] theorem U8.add_spec {x y : U8} (hmax : x.val + y.val ≤ U8.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
-@[pspec] theorem U16.add_spec {x y : U16} (hmax : x.val + y.val ≤ U16.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
-@[pspec] theorem U32.add_spec {x y : U32} (hmax : x.val + y.val ≤ U32.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
-@[pspec] theorem U64.add_spec {x y : U64} (hmax : x.val + y.val ≤ U64.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
-@[pspec] theorem U128.add_spec {x y : U128} (hmax : x.val + y.val ≤ U128.max) :
- ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+@[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
@[pspec] 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 :=
+ (hmin : Isize.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ Isize.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] 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 :=
+ (hmin : I8.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I8.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] 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 :=
+ (hmin : I16.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I16.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] 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 :=
+ (hmin : I32.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I32.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] 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 :=
+ (hmin : I64.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I64.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
@[pspec] 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 :=
+ (hmin : I128.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I128.max) :
+ ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
Scalar.add_spec hmin hmax
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.sub_spec {ty} {x y : Scalar ty}
- (hmin : Scalar.min ty ≤ x.val - y.val)
- (hmax : x.val - y.val ≤ Scalar.max ty) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+ (hmin : Scalar.min ty ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ Scalar.max ty) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub]
split
. simp [pure]
@@ -621,9 +624,9 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
. tauto
theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
- {x y : Scalar ty} (hmin : Scalar.min ty ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
- have : x.val - y.val ≤ Scalar.max ty := by
+ {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+ have : ↑x - ↑y ≤ Scalar.max ty := by
have hx := x.hmin
have hxm := x.hmax
have hy := y.hmin
@@ -632,65 +635,65 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
apply sub_spec <;> assumption
/- Fine-grained theorems -/
-@[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ x.val - y.val) :
- ∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
+@[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
-@[pspec] 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 :=
+@[pspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ Isize.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ I8.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ I16.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ I32.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ I64.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
Scalar.sub_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ ↑x - ↑y)
+ (hmax : ↑x - ↑y ≤ I128.max) :
+ ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
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)
- (hmax : x.val * y.val ≤ Scalar.max ty) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+ (hmin : Scalar.min ty ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ Scalar.max ty) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
conv => congr; ext; lhs; simp [HMul.hMul]
simp [mul, tryMk]
split
@@ -699,91 +702,91 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty}
. tauto
theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
- (hmax : x.val * y.val ≤ Scalar.max ty) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
- have : Scalar.min ty ≤ x.val * y.val := by
+ (hmax : ↑x * ↑y ≤ Scalar.max ty) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+ have : Scalar.min ty ≤ ↑x * ↑y := by
have hx := x.hmin
have hy := y.hmin
cases ty <;> simp [ScalarTy.isSigned] at * <;> apply mul_nonneg hx hy
apply mul_spec <;> assumption
/- Fine-grained theorems -/
-@[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : x.val * y.val ≤ Usize.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] theorem U8.mul_spec {x y : U8} (hmax : x.val * y.val ≤ U8.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] theorem U16.mul_spec {x y : U16} (hmax : x.val * y.val ≤ U16.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] theorem U32.mul_spec {x y : U32} (hmax : x.val * y.val ≤ U32.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] theorem U64.mul_spec {x y : U64} (hmax : x.val * y.val ≤ U64.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] theorem U128.mul_spec {x y : U128} (hmax : x.val * y.val ≤ U128.max) :
- ∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
+@[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
-@[pspec] 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 :=
+@[pspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ Isize.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ I8.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ I16.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ I32.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ I64.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-@[pspec] 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 :=
+@[pspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ ↑x * ↑y)
+ (hmax : ↑x * ↑y ≤ I128.max) :
+ ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
Scalar.mul_spec hmin hmax
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.div_spec {ty} {x y : Scalar ty}
- (hnz : y.val ≠ 0)
- (hmin : Scalar.min ty ≤ scalar_div x.val y.val)
- (hmax : scalar_div x.val y.val ≤ Scalar.max ty) :
- ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val := by
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : Scalar.min ty ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
simp [HDiv.hDiv, div, Div.div]
simp [tryMk, *]
simp [pure]
rfl
theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
- (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+ (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
have hx := x.hmin
have hy := y.hmin
simp [h] at hx hy
- have hmin : 0 ≤ x.val / y.val := Int.ediv_nonneg hx hy
- have hmax : x.val / y.val ≤ Scalar.max ty := by
- have := Int.ediv_le_self y.val hx
+ have hmin : 0 ≤ ↑x / ↑y := Int.ediv_nonneg hx hy
+ have hmax : ↑x / ↑y ≤ Scalar.max ty := by
+ have := Int.ediv_le_self ↑y hx
have := x.hmax
linarith
have hs := @div_spec ty x y hnz
@@ -791,158 +794,158 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
apply hs
/- Fine-grained theorems -/
-@[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : y.val ≠ 0) :
- ∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
+@[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : Isize.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ Isize.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I8.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ I8.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I16.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ I16.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I32.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ I32.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I64.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ I64.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I128.min ≤ scalar_div ↑x ↑y)
+ (hmax : scalar_div ↑x ↑y ≤ I128.max):
+ ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
Scalar.div_spec hnz hmin hmax
-- Generic theorem - shouldn't be used much
@[pspec]
theorem Scalar.rem_spec {ty} {x y : Scalar ty}
- (hnz : y.val ≠ 0)
- (hmin : Scalar.min ty ≤ scalar_rem x.val y.val)
- (hmax : scalar_rem x.val y.val ≤ Scalar.max ty) :
- ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val := by
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : Scalar.min ty ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
simp [HMod.hMod, rem]
simp [tryMk, *]
simp [pure]
rfl
theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
- (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+ (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
have hx := x.hmin
have hy := y.hmin
simp [h] at hx hy
- have hmin : 0 ≤ x.val % y.val := Int.emod_nonneg x.val hnz
- have hmax : x.val % y.val ≤ Scalar.max ty := by
- have h : 0 < y.val := by int_tac
- have h := Int.emod_lt_of_pos x.val h
+ have hmin : (0 : Int) ≤ x % y := Int.emod_nonneg ↑x hnz
+ have hmax : ↑x % ↑y ≤ Scalar.max ty := by
+ have h : (0 : Int) < y := by int_tac
+ have h := Int.emod_lt_of_pos ↑x h
have := y.hmax
linarith
have hs := @rem_spec ty x y hnz
simp [*] at hs
simp [*]
-@[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
-@[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : y.val ≠ 0) :
- ∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
+@[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
+ ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I8.min ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ I8.max):
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I16.min ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ I16.max):
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I32.min ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ I32.max):
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I64.min ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ I64.max):
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
@[pspec] 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 :=
+ (hnz : ↑y ≠ (0 : Int))
+ (hmin : I128.min ≤ scalar_rem ↑x ↑y)
+ (hmax : scalar_rem ↑x ↑y ≤ I128.max):
+ ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
Scalar.rem_spec hnz hmin hmax
-- ofIntCore
@@ -1039,24 +1042,24 @@ instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val
-- Not marking this one with @[simp] on purpose
theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
- x = y ↔ x.val = y.val := by
+ x = y ↔ (↑x : Int) = ↑y := by
cases x; cases y; simp_all
-- This is sometimes useful when rewriting the goal with the local assumptions
@[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
- x = y → x.val = y.val := (eq_equiv x y).mp
+ x = y → (↑x : Int) = ↑y := (eq_equiv x y).mp
theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
- x < y ↔ x.val < y.val := by simp [LT.lt]
+ x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
@[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
- x < y → x.val < y.val := (lt_equiv x y).mp
+ x < y → (↑x : Int) < ↑y := (lt_equiv x y).mp
theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
- x ≤ y ↔ x.val ≤ y.val := by simp [LE.le]
+ x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
@[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
- x ≤ y → x.val ≤ y.val := (le_equiv x y).mp
+ x ≤ y → (↑x : Int) ≤ ↑y := (le_equiv x y).mp
instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
@@ -1076,9 +1079,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
| isTrue h => isTrue (Scalar.eq_of_val_eq h)
| isFalse h => isFalse (Scalar.ne_of_val_ne h)
-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