refactor: Offset.lean and related files (#3614)

Motivation: avoid the unfold and check idiom.
This commit also minimize dependencies at `Offset.lean`.

closes #2615

src/Lean/Elab/Syntax.lean

@@ -382,7 +382,6 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
   let name ← match name? with
     | some name => pure name.getId
     | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
-  trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
   let stxNodeKind := (← getCurrNamespace) ++ name

src/Lean/Expr.lean

@@ -2003,4 +2003,34 @@ def mkEM (p : Expr) : Expr := mkApp (mkConst ``Classical.em) p
 /-- Return `p ↔ q` -/
 def mkIff (p q : Expr) : Expr := mkApp2 (mkConst ``Iff) p q
 
+private def natAddFn : Expr :=
+  let nat := mkConst ``Nat
+  mkApp4 (mkConst ``HAdd.hAdd [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHAdd [0]) nat (mkConst ``instAddNat))
+
+private def natMulFn : Expr :=
+  let nat := mkConst ``Nat
+  mkApp4 (mkConst ``HMul.hMul [0, 0, 0]) nat nat nat (mkApp2 (mkConst ``instHMul [0]) nat (mkConst ``instMulNat))
+
+/-- Given `a b : Nat`, returns `a + b` -/
+def mkNatAdd (a b : Expr) : Expr :=
+  mkApp2 natAddFn a b
+
+/-- Given `a b : Nat`, returns `a * b` -/
+def mkNatMul (a b : Expr) : Expr :=
+  mkApp2 natMulFn a b
+
+private def natLEPred : Expr :=
+  mkApp2 (mkConst ``LE.le [0]) (mkConst ``Nat) (mkConst ``instLENat)
+
+/-- Given `a b : Nat`, return `a ≤ b` -/
+def mkNatLE (a b : Expr) : Expr :=
+  mkApp2 natLEPred a b
+
+private def natEqPred : Expr :=
+  mkApp (mkConst ``Eq [1]) (mkConst ``Nat)
+
+/-- Given `a b : Nat`, return `a = b` -/
+def mkNatEq (a b : Expr) : Expr :=
+  mkApp2 natEqPred a b
+
 end Lean

src/Lean/Meta/Coe.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.Meta.WHNF
 import Lean.Meta.Transform
 import Lean.Meta.SynthInstance
 import Lean.Meta.AppBuilder

src/Lean/Meta/NatInstTesters.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+/-!
+Functions for testing whether expressions are canonical `Nat` instances.
+-/
+
+def isInstOfNatNat (e : Expr) : MetaM Bool := do
+  let_expr instOfNatNat _ ← e | return false
+  return true
+def isInstAddNat (e : Expr) : MetaM Bool := do
+  let_expr instAddNat ← e | return false
+  return true
+def isInstSubNat (e : Expr) : MetaM Bool := do
+  let_expr instSubNat ← e | return false
+  return true
+def isInstMulNat (e : Expr) : MetaM Bool := do
+  let_expr instMulNat ← e | return false
+  return true
+def isInstDivNat (e : Expr) : MetaM Bool := do
+  let_expr Nat.instDivNat ← e | return false
+  return true
+def isInstModNat (e : Expr) : MetaM Bool := do
+  let_expr Nat.instModNat ← e | return false
+  return true
+def isInstNatPowNat (e : Expr) : MetaM Bool := do
+  let_expr instNatPowNat ← e | return false
+  return true
+def isInstPowNat (e : Expr) : MetaM Bool := do
+  let_expr instPowNat _ i ← e | return false
+  isInstNatPowNat i
+def isInstHAddNat (e : Expr) : MetaM Bool := do
+  let_expr instHAdd _ i ← e | return false
+  isInstAddNat i
+def isInstHSubNat (e : Expr) : MetaM Bool := do
+  let_expr instHSub _ i ← e | return false
+  isInstSubNat i
+def isInstHMulNat (e : Expr) : MetaM Bool := do
+  let_expr instHMul _ i ← e | return false
+  isInstMulNat i
+def isInstHDivNat (e : Expr) : MetaM Bool := do
+  let_expr instHDiv _ i ← e | return false
+  isInstDivNat i
+def isInstHModNat (e : Expr) : MetaM Bool := do
+  let_expr instHMod _ i ← e | return false
+  isInstModNat i
+def isInstHPowNat (e : Expr) : MetaM Bool := do
+  let_expr instHPow _ _ i ← e | return false
+  isInstPowNat i
+def isInstLTNat (e : Expr) : MetaM Bool := do
+  let_expr instLTNat ← e | return false
+  return true
+def isInstLENat (e : Expr) : MetaM Bool := do
+  let_expr instLENat ← e | return false
+  return true
+
+end Lean.Meta

src/Lean/Meta/Offset.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Data.LBool
 import Lean.Meta.InferType
-import Lean.Meta.AppBuilder
+import Lean.Meta.NatInstTesters
 
 namespace Lean.Meta
 
@@ -17,12 +17,6 @@ private abbrev withInstantiatedMVars (e : Expr) (k : Expr → OptionT MetaM α)
   else
     k eNew
 
-def isNatProjInst (declName : Name) (numArgs : Nat) : Bool :=
-    (numArgs == 4 && (declName == ``Add.add || declName == ``Sub.sub || declName == ``Mul.mul || declName == ``Div.div || declName == ``Mod.mod || declName == ``NatPow.pow))
- || (numArgs == 5 && (declName == ``Pow.pow))
- || (numArgs == 6 && (declName == ``HAdd.hAdd || declName == ``HSub.hSub || declName == ``HMul.hMul || declName == ``HDiv.hDiv || declName == ``HMod.hMod || declName == ``HPow.hPow))
- || (numArgs == 3 && declName == ``OfNat.ofNat)
-
 /--
   Evaluate simple `Nat` expressions.
   Remark: this method assumes the given expression has type `Nat`. -/
@@ -37,20 +31,28 @@ partial def evalNat (e : Expr) : OptionT MetaM Nat := do
 where
   visit e := do
     match_expr e with
+    | OfNat.ofNat _ n i => guard (← isInstOfNatNat i); evalNat n
     | Nat.succ a => return (← evalNat a) + 1
     | Nat.add a b => return (← evalNat a) + (← evalNat b)
+    | Add.add _ i a b => guard (← isInstAddNat i); return (← evalNat a) + (← evalNat b)
+    | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddNat i); return (← evalNat a) + (← evalNat b)
     | Nat.sub a b => return (← evalNat a) - (← evalNat b)
+    | Sub.sub _ i a b => guard (← isInstSubNat i); return (← evalNat a) - (← evalNat b)
+    | HSub.hSub _ _ _ i a b => guard (← isInstHSubNat i); return (← evalNat a) - (← evalNat b)
     | Nat.mul a b => return (← evalNat a) * (← evalNat b)
+    | Mul.mul _ i a b => guard (← isInstMulNat i); return (← evalNat a) * (← evalNat b)
+    | HMul.hMul _ _ _ i a b => guard (← isInstHMulNat i); return (← evalNat a) * (← evalNat b)
     | Nat.div a b => return (← evalNat a) / (← evalNat b)
+    | Div.div _ i a b => guard (← isInstDivNat i); return (← evalNat a) / (← evalNat b)
+    | HDiv.hDiv _ _ _ i a b => guard (← isInstHDivNat i); return (← evalNat a) / (← evalNat b)
     | Nat.mod a b => return (← evalNat a) % (← evalNat b)
+    | Mod.mod _ i a b => guard (← isInstModNat i); return (← evalNat a) % (← evalNat b)
+    | HMod.hMod _ _ _ i a b => guard (← isInstHModNat i); return (← evalNat a) % (← evalNat b)
     | Nat.pow a b => return (← evalNat a) ^ (← evalNat b)
-    | _ =>
-      let e ← instantiateMVarsIfMVarApp e
-      let f := e.getAppFn
-      if f.isConst && isNatProjInst f.constName! e.getAppNumArgs then
-        evalNat (← unfoldProjInst? e)
-      else
-        failure
+    | NatPow.pow _ i a b => guard (← isInstNatPowNat i); return (← evalNat a) ^ (← evalNat b)
+    | Pow.pow _ _ i a b => guard (← isInstPowNat i); return (← evalNat a) ^ (← evalNat b)
+    | HPow.hPow _ _ _ i a b => guard (← isInstHPowNat i); return (← evalNat a) ^ (← evalNat b)
+    | _ => failure
 
 mutual
 
@@ -66,25 +68,17 @@ private partial def getOffset (e : Expr) : MetaM (Expr × Nat) :=
 Similar to `getOffset` but returns `none` if the expression is not syntactically an offset.
 -/
 private partial def isOffset? (e : Expr) : OptionT MetaM (Expr × Nat) := do
-  match e with
-  | .app _ a => do
-    let f := e.getAppFn
-    match f with
-    | .mvar .. => withInstantiatedMVars e isOffset?
-    | .const c _ =>
-      let nargs := e.getAppNumArgs
-      if c == ``Nat.succ && nargs == 1 then
-        let (s, k) ← getOffset a
-        pure (s, k+1)
-      else if c == ``Nat.add && nargs == 2 then
-        let v ← evalNat (e.getArg! 1)
-        let (s, k) ← getOffset (e.getArg! 0)
-        pure (s, k+v)
-      else if (c == ``Add.add && nargs == 4) || (c == ``HAdd.hAdd && nargs == 6) then
-        isOffset? (← unfoldProjInst? e)
-      else
-        failure
-    | _ => failure
+  let add (a b : Expr) := do
+    let v ← evalNat b
+    let (s, k) ← getOffset a
+    return (s, k+v)
+  match_expr e with
+  | Nat.succ a =>
+    let (s, k) ← getOffset a
+    return (s, k+1)
+  | Nat.add a b => add a b
+  | Add.add _ i a b => guard (← isInstAddNat i); add a b
+  | HAdd.hAdd _ _ _ i a b => guard (← isInstHAddNat i); add a b
   | _ => failure
 
 end
@@ -100,7 +94,7 @@ private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
   else if (← isNatZero e) then
     return mkNatLit offset
   else
-    mkAdd e (mkNatLit offset)
+    return mkNatAdd e (mkNatLit offset)
 
 def isDefEqOffset (s t : Expr) : MetaM LBool := do
   let ifNatExpr (x : MetaM LBool) : MetaM LBool := do

src/Lean/Meta/SynthInstance.lean

@@ -10,7 +10,6 @@ import Init.Data.Array.InsertionSort
 import Lean.Meta.Basic
 import Lean.Meta.Instances
 import Lean.Meta.AbstractMVars
-import Lean.Meta.WHNF
 import Lean.Meta.Check
 import Lean.Util.Profile
 

src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Check
 import Lean.Meta.Offset
+import Lean.Meta.AppBuilder
 import Lean.Meta.KExprMap
 
 namespace Lean.Meta.Linear.Nat
@@ -43,15 +44,15 @@ def LinearExpr.toArith (ctx : Array Expr) (e : LinearExpr) : MetaM Expr := do
   match e with
   | num v    => return mkNatLit v
   | var i    => return ctx[i]!
-  | add a b  => mkAdd (← toArith ctx a) (← toArith ctx b)
-  | mulL k a => mkMul (mkNatLit k) (← toArith ctx a)
-  | mulR a k => mkMul (← toArith ctx a) (mkNatLit k)
+  | add a b  => return mkNatAdd (← toArith ctx a) (← toArith ctx b)
+  | mulL k a => return mkNatMul (mkNatLit k) (← toArith ctx a)
+  | mulR a k => return mkNatMul (← toArith ctx a) (mkNatLit k)
 
 def LinearCnstr.toArith (ctx : Array Expr) (c : LinearCnstr) : MetaM Expr := do
   if c.eq then
-    mkEq (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
+    return mkNatEq (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
   else
-    return mkApp4 (mkConst ``LE.le [levelZero]) (mkConst ``Nat) (mkConst ``instLENat) (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
+    return mkNatLE (← LinearExpr.toArith ctx c.lhs) (← LinearExpr.toArith ctx c.rhs)
 
 namespace ToLinear
 
@@ -82,57 +83,55 @@ partial def toLinearExpr (e : Expr) : M LinearExpr := do
   | _                     => addAsVar e
 where
   visit (e : Expr) : M LinearExpr := do
-    match_expr e with
-    | Nat.succ a => return inc (← toLinearExpr a)
-    | Nat.add a b => return add (← toLinearExpr a) (← toLinearExpr b)
-    | Nat.mul a b =>
+    let mul (a b : Expr) := do
       match (← evalNat a |>.run) with
       | some k => return mulL k (← toLinearExpr b)
       | none => match (← evalNat b |>.run) with
         | some k => return mulR (← toLinearExpr a) k
         | none => addAsVar e
-    | _ =>
-      let e ← instantiateMVarsIfMVarApp e
-      let f := e.getAppFn
-      if f.isConst && isNatProjInst f.constName! e.getAppNumArgs then
-        let some e ← unfoldProjInst? e | addAsVar e
-        toLinearExpr e
-      else
-        addAsVar e
+    match_expr e with
+    | OfNat.ofNat _ n i =>
+      if (← isInstOfNatNat i) then toLinearExpr n
+      else addAsVar e
+    | Nat.succ a => return inc (← toLinearExpr a)
+    | Nat.add a b => return add (← toLinearExpr a) (← toLinearExpr b)
+    | Add.add _ i a b =>
+      if (← isInstAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
+      else addAsVar e
+    | HAdd.hAdd _ _ _ i a b =>
+      if (← isInstHAddNat i) then return add (← toLinearExpr a) (← toLinearExpr b)
+      else addAsVar e
+    | Nat.mul a b => mul a b
+    | Mul.mul _ i a b =>
+      if (← isInstMulNat i) then mul a b
+      else addAsVar e
+    | HMul.hMul _ _ _ i a b =>
+      if (← isInstHMulNat i) then mul a b
+      else addAsVar e
+    | _ => addAsVar e
 
-partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := do
-  let f := e.getAppFn
-  match f with
-  | Expr.mvar .. =>
-    let eNew ← instantiateMVars e
-    if eNew != e then
-      toLinearCnstr? eNew
-    else
-      return none
-  | Expr.const declName .. =>
-    let numArgs := e.getAppNumArgs
-    if declName == ``Eq && numArgs == 3 then
-      return some { eq := true, lhs := (← toLinearExpr (e.getArg! 1)), rhs := (← toLinearExpr (e.getArg! 2)) }
-    else if declName == ``Nat.le && numArgs == 2 then
-      return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)), rhs := (← toLinearExpr (e.getArg! 1)) }
-    else if declName == ``Nat.lt && numArgs == 2 then
-      return some { eq := false, lhs := (← toLinearExpr (e.getArg! 0)).inc, rhs := (← toLinearExpr (e.getArg! 1)) }
-    else if numArgs == 4 && (declName == ``GE.ge || declName == ``GT.gt) then
-      if let some e ← unfoldDefinition? e then
-        toLinearCnstr? e
-      else
-        return none
-    else if numArgs == 4 && (declName == ``LE.le || declName == ``LT.lt) then
-      if (← isDefEq (e.getArg! 0) (mkConst ``Nat)) then
-        if let some e ← unfoldProjInst? e then
-          toLinearCnstr? e
-        else
-          return none
-      else
-        return none
-    else
-      return none
-  | _ => return none
+partial def toLinearCnstr? (e : Expr) : M (Option LinearCnstr) := OptionT.run do
+  match_expr e with
+  | Eq α a b =>
+    let_expr Nat ← α | failure
+    return { eq := true, lhs := (← toLinearExpr a), rhs := (← toLinearExpr b) }
+  | Nat.le a b =>
+    return { eq := false, lhs := (← toLinearExpr a), rhs := (← toLinearExpr b) }
+  | Nat.lt a b =>
+    return { eq := false, lhs := (← toLinearExpr a).inc, rhs := (← toLinearExpr b) }
+  | LE.le _ i a b =>
+    guard (← isInstLENat i)
+    return { eq := false, lhs := (← toLinearExpr a), rhs := (← toLinearExpr b) }
+  | LT.lt _ i a b =>
+    guard (← isInstLTNat i)
+    return { eq := false, lhs := (← toLinearExpr a).inc, rhs := (← toLinearExpr b) }
+  | GE.ge _ i a b =>
+    guard (← isInstLENat i)
+    return { eq := false, lhs := (← toLinearExpr b), rhs := (← toLinearExpr a) }
+  | GT.gt _ i a b =>
+    guard (← isInstLTNat i)
+    return { eq := false, lhs := (← toLinearExpr b).inc, rhs := (← toLinearExpr a) }
+  | _ => failure
 
 def run (x : M α) : MetaM (α × Array Expr) := do
   let (a, s) ← x.run {}

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -45,7 +45,6 @@ Helper function for reducing homogenous binary bitvector operators.
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
   if h : v₁.n = v₂.n then
-    trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
     return .done <| toExpr (op v₁.value (h ▸ v₂.value))
   else
     return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -20,7 +20,6 @@ builtin_dsimproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
   return .done <| toExpr (a ++ b)
 
 private partial def reduceListChar (e : Expr) (s : String) : SimpM DStep := do
-  trace[Meta.debug] "reduceListChar {e}, {s}"
   if e.isAppOfArity ``List.nil 1 then
     return .done <| toExpr s
   else if e.isAppOfArity ``List.cons 3 then

src/Lean/ParserCompiler.lean

@@ -5,6 +5,7 @@ Authors: Sebastian Ullrich
 -/
 prelude
 import Lean.Meta.ReduceEval
+import Lean.Meta.WHNF
 import Lean.KeyedDeclsAttribute
 import Lean.ParserCompiler.Attribute
 import Lean.Parser.Extension

tests/lean/run/2615.lean

@@ -0,0 +1,7 @@
+-- `simp_arith` does not support `Int` yet.
+-- But, the weird error message at #2615 is not generated anymore
+/--
+error: simp made no progress
+-/
+#guard_msgs (error) in
+theorem huh (x : Int) : x + 1 = 1 + x := by simp_arith