From 794228a982aa55cd320d5e289c80b8839f8418b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 Mar 2024 19:40:15 -0800 Subject: [PATCH] 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 | 1 - src/Lean/Expr.lean | 30 ++++++ src/Lean/Meta/Coe.lean | 1 - src/Lean/Meta/NatInstTesters.lean | 63 ++++++++++++ src/Lean/Meta/Offset.lean | 62 ++++++------ src/Lean/Meta/SynthInstance.lean | 1 - .../Meta/Tactic/LinearArith/Nat/Basic.lean | 99 +++++++++---------- .../Tactic/Simp/BuiltinSimprocs/BitVec.lean | 1 - .../Tactic/Simp/BuiltinSimprocs/String.lean | 1 - src/Lean/ParserCompiler.lean | 1 + tests/lean/run/2615.lean | 7 ++ 11 files changed, 178 insertions(+), 89 deletions(-) create mode 100644 src/Lean/Meta/NatInstTesters.lean create mode 100644 tests/lean/run/2615.lean diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index e9c7b8316e..f02e62a9c1 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/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 diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index ba853af364..7854c15c85 100644 --- a/src/Lean/Expr.lean +++ b/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 diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean index 001e2e150d..2d51e2d60a 100644 --- a/src/Lean/Meta/Coe.lean +++ b/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 diff --git a/src/Lean/Meta/NatInstTesters.lean b/src/Lean/Meta/NatInstTesters.lean new file mode 100644 index 0000000000..ee4b81d3c4 --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index 402afec72b..695eb177d3 100644 --- a/src/Lean/Meta/Offset.lean +++ b/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 diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 6233a8eb75..3e597da6ff 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean index 6290ec44fe..c3f88147b2 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean +++ b/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 {} diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean index cf5cec5447..bc120154e1 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean index 229b535fcb..0cc24f8359 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean +++ b/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 diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 8d51add2f2..3d15ea6436 100644 --- a/src/Lean/ParserCompiler.lean +++ b/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 diff --git a/tests/lean/run/2615.lean b/tests/lean/run/2615.lean new file mode 100644 index 0000000000..2d09b11815 --- /dev/null +++ b/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