From 12fe37ee9776e2a882c382922a7f8628bc6283ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Felipe=20P=C3=A9ret?=
 <40478095+felipeperet@users.noreply.github.com>
Date: Thu, 26 Feb 2026 14:26:10 -0300
Subject: [PATCH 1/3] Add rewrite rule: List.any with equality lambda to
 List.elem

---
 Blaster/Optimize/Rewriting/OptimizeApp.lean   |  2 +
 .../Optimize/Rewriting/OptimizeListAny.lean   | 53 +++++++++++++++++++
 Tests/Optimize.lean                           |  4 +-
 Tests/Optimize/OptimizeConst/NormHOF.lean     | 10 ++--
 Tests/Optimize/OptimizeListAny.lean           | 29 ++++++++++
 5 files changed, 90 insertions(+), 8 deletions(-)
 create mode 100644 Blaster/Optimize/Rewriting/OptimizeListAny.lean
 create mode 100644 Tests/Optimize/OptimizeListAny.lean

diff --git a/Blaster/Optimize/Rewriting/OptimizeApp.lean b/Blaster/Optimize/Rewriting/OptimizeApp.lean
index dbfe971..36ccd94 100644
--- a/Blaster/Optimize/Rewriting/OptimizeApp.lean
+++ b/Blaster/Optimize/Rewriting/OptimizeApp.lean
@@ -7,6 +7,7 @@ import Blaster.Optimize.Rewriting.OptimizeDecideBoolBinary
 import Blaster.Optimize.Rewriting.OptimizeExists
 import Blaster.Optimize.Rewriting.OptimizeInt
 import Blaster.Optimize.Rewriting.OptimizeITE
+import Blaster.Optimize.Rewriting.OptimizeListAny
 import Blaster.Optimize.Rewriting.OptimizeNat
 import Blaster.Optimize.Rewriting.OptimizeString
 import Blaster.Optimize.OptimizeStack
@@ -64,6 +65,7 @@ def optimizeAppAux (f : Expr) (args: Array Expr) : TranslateEnvT Expr := do
   if let some e ← optimizePropBinary? f args then return e
   if let some e ← optimizeBoolNot? f args then return e
   if let some e ← optimizeBoolBinary? f args then return e
+  if let some e ← optimizeListAny? f args then return e
   if let some e ← optimizeEquality? f args then return e
   if let some e ← optimizeNat? f args then return e
   if let some e ← optimizeInt? f args then return e
diff --git a/Blaster/Optimize/Rewriting/OptimizeListAny.lean b/Blaster/Optimize/Rewriting/OptimizeListAny.lean
new file mode 100644
index 0000000..0eb2073
--- /dev/null
+++ b/Blaster/Optimize/Rewriting/OptimizeListAny.lean
@@ -0,0 +1,53 @@
+import Lean
+import Blaster.Optimize.Rewriting.Utils
+
+open Lean Meta
+namespace Blaster.Optimize
+
+/-- Detect `List.any l (λ x => BEq.beq x k)` or `List.any l (λ x => BEq.beq k x)`
+    and rewrite to `List.elem k l`.
+
+    @List.any : {α : Type} → List α → (α → Bool) → Bool
+    args[0] = α, args[1] = l, args[2] = f
+
+    @BEq.beq : {α : Type} → [inst : BEq α] → α → α → Bool
+    beqArgs[0] = α, beqArgs[1] = inst, beqArgs[2] = lhs, beqArgs[3] = rhs
+
+    @List.elem : {α : Type} → [inst : BEq α] → α → List α → Bool
+-/
+
+def optimizeListAny? (f : Expr) (args : Array Expr) : TranslateEnvT (Option Expr) := do
+  let Expr.const ``List.any _ := f | return none
+  if args.size != 3 then return none
+  let α := args[0]!
+  let l := args[1]!
+  let lam := args[2]!
+  let Expr.lam binderName binderType body binderInfo := lam | return none
+  withLocalDecl binderName binderInfo binderType λ x => do
+    let body := body.instantiate1 x
+    let beqType := mkApp (mkConst ``BEq [levelZero]) α
+    let inst ← try synthInstance beqType
+      catch _ => do
+      return none
+    let kMVar ← mkFreshExprMVar α
+    let rhs_candidate := mkAppN (mkConst ``BEq.beq [levelZero]) #[α, inst, x, kMVar]
+    let rhs_matches ← isDefEq body rhs_candidate
+    let k ← if rhs_matches then do
+        let k ← instantiateMVars kMVar
+        pure k
+      else do
+        let kMVar2 ← mkFreshExprMVar α
+        let lhs_candidate := mkAppN (mkConst ``BEq.beq [levelZero]) #[α, inst, kMVar2, x]
+        let lhs_matches ← isDefEq body lhs_candidate
+        if lhs_matches then do
+          let k ← instantiateMVars kMVar2
+          pure k
+        else do
+          return none
+    if k.hasLooseBVars then return none
+    setRestart
+    let u <- getLevel α
+    let u' := u.normalize.dec.getD Lean.Level.zero
+    return mkAppN (mkConst ``List.elem [u']) #[α, inst, k, l]
+
+end Blaster.Optimize
diff --git a/Tests/Optimize.lean b/Tests/Optimize.lean
index 200e9bd..f7f2094 100644
--- a/Tests/Optimize.lean
+++ b/Tests/Optimize.lean
@@ -1,15 +1,15 @@
-
 import Tests.Optimize.FunPropagation
 import Tests.Optimize.NormChoiceApp
 import Tests.Optimize.OptimizeBEq
 import Tests.Optimize.OptimizeBool
 import Tests.Optimize.OptimizeConst
+import Tests.Optimize.OptimizeDecide
 import Tests.Optimize.OptimizeEq
 import Tests.Optimize.OptimizeExists
-import Tests.Optimize.OptimizeDecide
 import Tests.Optimize.OptimizeForAll
 import Tests.Optimize.OptimizeITE
 import Tests.Optimize.OptimizeLet
+import Tests.Optimize.OptimizeListAny
 import Tests.Optimize.OptimizeMatch
 import Tests.Optimize.OptimizeNat
 import Tests.Optimize.OptimizeProp
diff --git a/Tests/Optimize/OptimizeConst/NormHOF.lean b/Tests/Optimize/OptimizeConst/NormHOF.lean
index e80d48b..a2d9ae7 100644
--- a/Tests/Optimize/OptimizeConst/NormHOF.lean
+++ b/Tests/Optimize/OptimizeConst/NormHOF.lean
@@ -441,12 +441,12 @@ def mapOptionDefault (x : Nat) (y : Option Nat) : Nat :=
 -- ∀ (x : Nat) (xs : List Nat),
 --   List.any xs (λ a => a == x) → ∃ (p : Prop), p ∈ (List.map (Eq x) xs) ∧ p ===>
 -- ∀ (x : Nat) (xs : List Nat),
---   true = List.any xs (λ a => x == a) → ∃ (p : Prop), p ∧ List.Mem p (List.map (λ a => Eq x a) xs)
+--   true = List.elem x xs → ∃ (p : Prop), p ∧ List.Mem p (List.map (λ a => x = a) xs)
 #testOptimize [ "ConstPartialFunArg_4" ]
     ∀ (x : Nat) (xs : List Nat),
       List.any xs (λ a => a == x) → ∃ (p : Prop), p ∈ (List.map (Eq x) xs) ∧ p ===>
     ∀ (x : Nat) (xs : List Nat),
-      true = List.any xs (λ a => x == a) → ∃ (p : Prop), p ∧ List.Mem p (List.map (λ a => Eq x a) xs)
+      true = List.elem x xs → ∃ (p : Prop), p ∧ List.Mem p (List.map (λ a => Eq x a) xs)
 
 /-! Test cases to ensure that opaque functions passed as arguments are properly normalized. -/
 
@@ -473,11 +473,9 @@ def mapOptionDefault (x : Nat) (y : Option Nat) : Nat :=
 
 def boolWapper (f : Nat → Nat → Bool) (x : Nat) (y : Nat) := f x y
 
--- ∀ (x : Nat) (xs : List Nat), List.any xs (beqWapper Nat.beq x) → List.contains xs x ===>
--- ∀ (x : Nat) (xs : List Nat), true = List.any xs (λ a => x == a) → true = List.elem x xs
+-- ∀ (x : Nat) (xs : List Nat), List.any xs (beqWapper Nat.beq x) → List.contains xs x ===> True
 #testOptimize [ "ConstNormOpaqueFunArg_5" ]
-  ∀ (x : Nat) (xs : List Nat), List.any xs (boolWapper Nat.beq x) → List.contains xs x ===>
-  ∀ (x : Nat) (xs : List Nat), true = List.any xs (λ a => x == a) → true = List.elem x xs
+  ∀ (x : Nat) (xs : List Nat), List.any xs (boolWapper Nat.beq x) → List.contains xs x ===> True
 
 -- ∀ (x : Nat) (xs : List Nat), List.any (λ a => x ≤ a) xs = List.any xs (Nat.ble x)  ===> True
 #testOptimize [ "ConstNormOpaqueFunArg_6" ]
diff --git a/Tests/Optimize/OptimizeListAny.lean b/Tests/Optimize/OptimizeListAny.lean
new file mode 100644
index 0000000..f3603c7
--- /dev/null
+++ b/Tests/Optimize/OptimizeListAny.lean
@@ -0,0 +1,29 @@
+import Lean
+import Tests.Utils
+import Tests.Smt.Benchmarks.ValidatorsExamples.PlutusLedgerAPI.VDummy
+
+open Lean Elab Command Term
+open Tests.ValidatorsExamples.PlutusLedgerAPI
+
+namespace Test.OptimizeListAny
+
+-- Another approach: Specializing new recursive function
+
+-- List.any l (λ x => x == k) ===> true = List.elem k l
+#testOptimize [ "ListAnyElem_1" ]
+  ∀ (l : List Nat) (k : Nat), List.any l (λ x => x == k) ===>
+  ∀ (l : List Nat) (k : Nat), true = List.elem k l
+
+-- List.any l (λ x => k == x) ===> true = List.elem k l
+#testOptimize [ "ListAnyElem_2" ]
+  ∀ (l : List Nat) (k : Nat), List.any l (λ x => k == x) ===>
+  ∀ (l : List Nat) (k : Nat), true = List.elem k l
+
+-- Custom type with deriving BEq
+#testOptimize [ "ListAnyElem_3" ]
+  ∀ (l : List VerificationKeyHash) (k : VerificationKeyHash),
+    List.any l (λ x => x == k) ===>
+  ∀ (l : List VerificationKeyHash) (k : VerificationKeyHash),
+    true = List.elem k l
+
+end Test.OptimizeListAny

From 7153436dc267b0e3f94ac9505b89cbd786771a04 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Felipe=20P=C3=A9ret?=
 <40478095+felipeperet@users.noreply.github.com>
Date: Thu, 26 Feb 2026 14:29:33 -0300
Subject: [PATCH 2/3] docs: clarify List.any rewrite rule uses definitional
 equality checking

---
 Blaster/Optimize/Rewriting/OptimizeListAny.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Blaster/Optimize/Rewriting/OptimizeListAny.lean b/Blaster/Optimize/Rewriting/OptimizeListAny.lean
index 0eb2073..fafb451 100644
--- a/Blaster/Optimize/Rewriting/OptimizeListAny.lean
+++ b/Blaster/Optimize/Rewriting/OptimizeListAny.lean
@@ -14,6 +14,9 @@ namespace Blaster.Optimize
     beqArgs[0] = α, beqArgs[1] = inst, beqArgs[2] = lhs, beqArgs[3] = rhs
 
     @List.elem : {α : Type} → [inst : BEq α] → α → List α → Bool
+
+    Uses definitional equality checking to handle custom types with derived BEq
+    instances, where the elaborator may expand (==) into primitive constructs.
 -/
 
 def optimizeListAny? (f : Expr) (args : Array Expr) : TranslateEnvT (Option Expr) := do

From 0e57eac264277353cbb97b1c27016b7596dc9d7d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Felipe=20P=C3=A9ret?=
 <40478095+felipeperet@users.noreply.github.com>
Date: Thu, 26 Feb 2026 14:35:34 -0300
Subject: [PATCH 3/3] remove leftover comment from Jean's suggestion during
 discussion

---
 Tests/Optimize/OptimizeListAny.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Tests/Optimize/OptimizeListAny.lean b/Tests/Optimize/OptimizeListAny.lean
index f3603c7..2aca987 100644
--- a/Tests/Optimize/OptimizeListAny.lean
+++ b/Tests/Optimize/OptimizeListAny.lean
@@ -7,8 +7,6 @@ open Tests.ValidatorsExamples.PlutusLedgerAPI
 
 namespace Test.OptimizeListAny
 
--- Another approach: Specializing new recursive function
-
 -- List.any l (λ x => x == k) ===> true = List.elem k l
 #testOptimize [ "ListAnyElem_1" ]
   ∀ (l : List Nat) (k : Nat), List.any l (λ x => x == k) ===>