summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Base.lean7
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean21
2 files changed, 28 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 3d70c84a..9dbaf133 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -116,6 +116,13 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
@[simp] theorem bind_tc_div (f : α → Result β) :
(do let y ← div; f y) = div := by simp [Bind.bind, bind]
+@[simp] theorem bind_assoc_eq {a b c : Type u}
+ (e : Result a) (g : a → Result b) (h : b → Result c) :
+ (Bind.bind (Bind.bind e g) h) =
+ (Bind.bind e (λ x => Bind.bind (g x) h)) := by
+ simp [Bind.bind]
+ cases e <;> simp
+
----------
-- MISC --
----------
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index a8eda6d5..fe8dc8ec 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1038,6 +1038,27 @@ instance {ty} : LT (Scalar ty) where
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
+ 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
+
+theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
+ x < y ↔ x.val < y.val := 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
+
+theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
+ x ≤ y ↔ x.val ≤ y.val := 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
+
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 ..