From c1c33de85906bda71cac098ddba0e5dfc98c85d2 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Fri, 12 Apr 2024 20:01:18 +0200 Subject: 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 --- backends/lean/Base/Primitives/Scalar.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'backends') 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 -- cgit v1.2.3