diff options
author | Son Ho | 2024-01-26 00:17:59 +0100 |
---|---|---|
committer | Son Ho | 2024-01-26 00:17:59 +0100 |
commit | 9f0e4605e1c8816dbf5ed3e9e893b25e9a2be4a3 (patch) | |
tree | a1bd3885305af5598cab879a0551660a6bcf0492 /backends/lean/Base/Primitives | |
parent | 202f0153dc51983e6bc0eddb65d22c763579850c (diff) |
Improve the Lean backend
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 7 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 11 |
2 files changed, 18 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..2c34774b 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1038,6 +1038,17 @@ instance {ty} : LT (Scalar ty) where instance {ty} : LE (Scalar ty) where le a b := LE.le a.val b.val +theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) : + x < y ↔ x.val < y.val := by simp [LT.lt] + +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 + 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 .. |