From ba215d5f7f2cd087e6b920e7ea1793e4b114a775 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 18 Sep 2023 13:06:49 +0200
Subject: Add arithmetic lemmas in Scalar.lean

---
 backends/lean/Base/Primitives/Scalar.lean | 191 ++++++++++++++++++++++++++++--
 1 file changed, 179 insertions(+), 12 deletions(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index aa1d452d..1d31b04a 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -491,6 +491,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}
@@ -540,6 +570,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)
@@ -586,6 +646,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}
@@ -639,6 +729,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}
@@ -692,20 +824,55 @@ 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
-def I8.ofIntCore    := @Scalar.ofIntCore .I8
-def I16.ofIntCore   := @Scalar.ofIntCore .I16
-def I32.ofIntCore   := @Scalar.ofIntCore .I32
-def I64.ofIntCore   := @Scalar.ofIntCore .I64
-def I128.ofIntCore  := @Scalar.ofIntCore .I128
-def Usize.ofIntCore := @Scalar.ofIntCore .Usize
-def U8.ofIntCore    := @Scalar.ofIntCore .U8
-def U16.ofIntCore   := @Scalar.ofIntCore .U16
-def U32.ofIntCore   := @Scalar.ofIntCore .U32
-def U64.ofIntCore   := @Scalar.ofIntCore .U64
-def U128.ofIntCore  := @Scalar.ofIntCore .U128
+@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize
+@[reducible] def I8.ofIntCore    := @Scalar.ofIntCore .I8
+@[reducible] def I16.ofIntCore   := @Scalar.ofIntCore .I16
+@[reducible] def I32.ofIntCore   := @Scalar.ofIntCore .I32
+@[reducible] def I64.ofIntCore   := @Scalar.ofIntCore .I64
+@[reducible] def I128.ofIntCore  := @Scalar.ofIntCore .I128
+@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize
+@[reducible] def U8.ofIntCore    := @Scalar.ofIntCore .U8
+@[reducible] def U16.ofIntCore   := @Scalar.ofIntCore .U16
+@[reducible] def U32.ofIntCore   := @Scalar.ofIntCore .U32
+@[reducible] def U64.ofIntCore   := @Scalar.ofIntCore .U64
+@[reducible] def U128.ofIntCore  := @Scalar.ofIntCore .U128
 
 --  ofInt
 -- TODO: typeclass?
-- 
cgit v1.2.3