4 files changed, 46 insertions, 14 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 1d3e82be..068d6f2f 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -21,6 +21,11 @@ class HasIntProp (a : Sort u) where
   prop_ty : a → Prop
   prop : ∀ x:a, prop_ty x
 
+/- Terms that induces predicates: if we can find the term `x`, we can introduce `concl` in the context. -/
+class HasIntPred {a: Sort u} (x: a) where
+  concl : Prop
+  prop : concl
+
 /- Proposition with implications: if we find P we can introduce Q in the context -/
 class PropHasImp (x : Sort u) where
   concl : Prop
@@ -106,36 +111,52 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
-  let hs ← decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs
+  let hs ← decls.foldlM (fun hs d => do 
+    -- Collect instances over all subexpressions in the context.
+    -- Note that we explore the *type* of the local declarations: if we have
+    -- for instance `h : A ∧ B` in the context, the expression itself is simply
+    -- `h`; the information we are interested in is its type.
+    let ty ← Lean.Meta.inferType d.toExpr
+    collectInstances k hs ty
+  ) hs
   -- Also explore the goal
   collectInstances k hs (← Tactic.getMainTarget)
 
 -- Helper
-def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do
+def lookupProp (fName : String) (className : Name) (e : Expr)
+  (instantiateClassFn : Expr → MetaM (Array Expr))
+  (instantiateProjectionFn : Expr → MetaM (Array Expr)) : MetaM (Option Expr) := do
   trace[Arith] fName
   -- TODO: do we need Lean.observing?
   -- This actually eliminates the error messages
   trace[Arith] m!"{fName}: {e}"
   Lean.observing? do
     trace[Arith] m!"{fName}: observing: {e}"
-    let ty ← Lean.Meta.inferType e
-    let hasProp ← mkAppM className #[ty]
+    let hasProp ← mkAppM className (← instantiateClassFn e)
     let hasPropInst ← trySynthInstance hasProp
     match hasPropInst with
     | LOption.some i =>
       trace[Arith] "Found {fName} instance"
       let i_prop ← mkProjection i (Name.mkSimple "prop")
-      some (← mkAppM' i_prop #[e])
+      some (← mkAppM' i_prop (← instantiateProjectionFn e))
     | _ => none
 
 -- Return an instance of `HasIntProp` for `e` if it has some
 def lookupHasIntProp (e : Expr) : MetaM (Option Expr) :=
-  lookupProp "lookupHasIntProp" ``HasIntProp e
+  lookupProp "lookupHasIntProp" ``HasIntProp e (fun e => do pure #[← Lean.Meta.inferType e]) (fun e => pure #[e])
 
 -- Collect the instances of `HasIntProp` for the subexpressions in the context
 def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
   collectInstancesFromMainCtx lookupHasIntProp
 
+-- Return an instance of `HasIntPred` for `e` if it has some
+def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
+  lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
+
+-- Collect the instances of `HasIntPred` for the subexpressions in the context
+def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do 
+  collectInstancesFromMainCtx lookupHasIntPred
+
 -- Return an instance of `PropHasImp` for `e` if it has some
 def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do
   trace[Arith] m!"lookupPropHasImp: {e}"
@@ -193,6 +214,13 @@ def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
 elab "intro_has_int_prop_instances" : tactic => do
   let _ ← introHasIntPropInstances
 
+def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do 
+  trace[Arith] "Introducing the HasIntPred instances"
+  introInstances ``HasIntPred.concl lookupHasIntPred
+
+elab "intro_has_int_pred_instances" : tactic => do
+  let _ ← introHasIntPredInstances
+
 def introPropHasImpInstances : Tactic.TacticM (Array Expr) := do
   trace[Arith] "Introducing the PropHasImp instances"
   introInstances ``PropHasImp.concl lookupPropHasImp
@@ -208,6 +236,8 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
   Tactic.withMainContext do
   -- Introduce the instances of `HasIntProp`
   let _ ← introHasIntPropInstances
+  -- Introduce the instances of `HasIntPred`
+  let _ ← introHasIntPredInstances
   -- Introduce the instances of `PropHasImp`
   let _ ← introPropHasImpInstances
   -- Extra preprocessing
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a1897191..96843f55 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -18,9 +18,11 @@ theorem len_pos : 0 ≤ (ls : List α).len := by
   induction ls <;> simp [*]
   omega
 
-instance (a : Type u) : Arith.HasIntProp (List a) where
-  prop_ty := λ ls => 0 ≤ ls.len
-  prop := λ ls => ls.len_pos
+instance (l: List a) : Arith.HasIntPred (l.len) where
+   concl := 0 ≤ l.len
+   prop := l.len_pos
+
+example (l: List a): 0 ≤ l.len := by scalar_tac
 
 -- Remark: if i < 0, then the result is none
 def indexOpt (ls : List α) (i : Int) : Option α :=
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index de2e22cd..aa2349c2 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/lean/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05",
+   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "659d35143a857ceb5ba7c02a0e1530a1c7aec70c",
+   "rev": "77e1ea0a339a4663eced9cacc3a46eb45f967b51",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index 0ba3faf8..29c0cea4 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0-rc1
+leanprover/lean4:v4.9.0-rc2