From d8247d99520738188bbd160be7de03550f8156ce Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 27 Jan 2024 21:31:52 +0100
Subject: Add some lemmas to the Lean backend

---
 backends/lean/Base/Primitives/Scalar.lean | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 2c34774b..fe8dc8ec 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -1038,16 +1038,26 @@ 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]
 
--- 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
+@[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 ..
-- 
cgit v1.2.3