diff options
| author | Ryan Lahfa | 2024-05-15 15:11:42 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-05-21 10:42:15 +0200 |
| commit | 065e60754084ef169fd17bbb7ab1b492fb7497c3 (patch) | |
| tree | a47a7ea9f04c31d197e2c1198bada4c4ac932369 | |
| parent | cbf425d178f9063507585233ebee7ca785567e3a (diff) | |
feat(backends/lean): make `max`-related coercions nicer
Situations where you have `coe (max a b) = max (coe a) (coe b)` are
often stuck during verification because of the lack of this theorem.
With this theorem, `push_cast` works as intended and normalizes even
further.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index dccbcdf2..f08b8dec 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -1419,6 +1419,18 @@ instance (ty: ScalarTy) : LinearOrder (Scalar ty) where right; exact (Scalar.le_equiv _ _).2 H decidableLE := ScalarDecidableLE ty +-- Coercion theorems +-- This is helpful whenever you want to "push" casts to the innermost nodes +-- and make the cast normalization happen more magically. + +@[simp, norm_cast] +theorem coe_max {ty: ScalarTy} (a b: Scalar ty): ↑(Max.max a b) = (Max.max (↑a) (↑b): ℤ) := by + -- TODO: there should be a shorter way to prove this. + rw [max_def, max_def] + split_ifs <;> simp_all + refine' absurd _ (lt_irrefl a) + exact lt_of_le_of_lt (by assumption) ((Scalar.lt_equiv _ _).2 (by assumption)) + -- Leading zeros def core.num.Usize.leading_zeros (x : Usize) : U32 := sorry def core.num.U8.leading_zeros (x : U8) : U32 := sorry |