diff options
| author | Son Ho | 2024-01-27 21:31:52 +0100 |
|---|---|---|
| committer | Son Ho | 2024-01-27 21:31:52 +0100 |
| commit | d8247d99520738188bbd160be7de03550f8156ce (patch) | |
| tree | 0e801b5e01eda423d49bdb0a43cff11d65e78bb1 /backends | |
| parent | c709eadb14e2ecd21c9c4a6a9def39334f27552b (diff) | |
Add some lemmas to the Lean backend
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 18 |
1 files changed, 14 insertions, 4 deletions
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 .. |