From 065e60754084ef169fd17bbb7ab1b492fb7497c3 Mon Sep 17 00:00:00 2001
From: Ryan Lahfa
Date: Wed, 15 May 2024 15:11:42 +0200
Subject: 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>
---
 backends/lean/Base/Primitives/Scalar.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'backends/lean/Base/Primitives/Scalar.lean')

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
-- 
cgit v1.2.3

