diff options
| author | Ryan Lahfa | 2024-04-12 20:01:18 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-04-12 20:01:18 +0200 |
| commit | c1c33de85906bda71cac098ddba0e5dfc98c85d2 (patch) | |
| tree | 7feb40276bbfc54e682bbdff2c7db4d287f5a0e4 | |
| parent | 67eaff0b90d693c86d9848cbf598e7c86caba4c4 (diff) | |
lean: scalars form a preorder
Via the canonical injection, we can easily define an induced preorder on
scalars and inherit all nice properties.
It's useful to reason on specific scalar preorders w.r.t. Ordering, see
the binary search tree verification example.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index b8d93d30..be930754 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1394,6 +1394,16 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by simp [eq_equiv] +instance (ty: ScalarTy) : Preorder (Scalar ty) where + le_refl := fun a => by simp + le_trans := fun a b c => by + intro Hab Hbc + exact (le_trans ((Scalar.le_equiv _ _).1 Hab) ((Scalar.le_equiv _ _).1 Hbc)) + lt_iff_le_not_le := fun a b => by + trans (a: Int) < (b: Int); exact (Scalar.lt_equiv _ _) + trans (a: Int) ≤ (b: Int) ∧ ¬ (b: Int) ≤ (a: Int); exact lt_iff_le_not_le + repeat rewrite [← Scalar.le_equiv]; rfl + -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry |