Merge remote-tracking branch 'origin/joachim/simp-underLambda' into joachim/issue5667

Author: nomeata

src/Init/MetaTypes.lean

@@ -114,6 +114,12 @@ structure Config where
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  When `underLambda` (default: `true`) is `false`, then `simp` will not rewrite under lambdas
+  (so in particular not in the arms of a `match` expressoin), and not in the cases of an
+  `if-then-else.`
+  -/
+  underLambda       : Bool := true
   deriving Inhabited, BEq
 
 end DSimp
@@ -224,7 +230,7 @@ structure Config where
   -/
   zetaDelta         : Bool := false
   /--
-  When `index` (default : `true`) is `false`, `simp` will only use the root symbol
+  When `index` (default: `true`) is `false`, `simp` will only use the root symbol
   to find candidate `simp` theorems. It approximates Lean 3 `simp` behavior.
   -/
   index             : Bool := true
@@ -238,6 +244,12 @@ structure Config where
   `let x := v; e` simplifies to `e` when `x` does not occur in `e`.
   -/
   zetaUnused : Bool := true
+  /--
+  When `underLambda` (default: `true`) is `false`, then `simp` will not rewrite under lambdas
+  (so in particular not in the arms of a `match` expressoin), and not in the cases of an
+  `if-then-else.`
+  -/
+  underLambda       : Bool := true
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -296,7 +296,9 @@ def simpProj (e : Expr) : SimpM Result := do
 def simpConst (e : Expr) : SimpM Result :=
   return { expr := (← reduce e) }
 
-def simpLambda (e : Expr) : SimpM Result :=
+def simpLambda (e : Expr) : SimpM Result := do
+  unless (← getConfig).underLambda do
+      return { expr := e }
   withParent e <| lambdaTelescopeDSimp e fun xs e => withNewLemmas xs do
     let r ← simp e
     let eNew ← mkLambdaFVars xs r.expr
@@ -456,13 +458,32 @@ Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 
+/-- The dsimp implementation of `underLambda := false` -/
+private def doNotVisitLambda : DSimproc := fun e => do
+  if e.isLambda then
+    return .done e
+  if e.isApp && e.isAppOf ``ite then
+    -- dsimp is using `Meta.transform`, which we cannot tell to only
+    -- traverse into some subterms.
+    -- So recurse into `dsimp` here. Unfortunately sets up a fresh transform cache.
+    e.withApp fun f args => do
+      let args' ← args.mapIdxM fun i a =>
+        if i < 3 || i > 4 then
+          dsimp a
+        else
+          pure a
+      return .done (mkAppN f args')
+  else
+    return .continue
+
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
     return e
   let m ← getMethods
   let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific >> doNotVisitCharLit
+  let pre := if cfg.underLambda then pre else doNotVisitLambda >> pre
   let post := m.dpost >> dsimpReduce
   withInDSimp do
   transform (usedLetOnly := cfg.zeta || cfg.zetaUnused) e (pre := pre) (post := post)
@@ -490,7 +511,10 @@ def congrDefault (e : Expr) : SimpM Result := do
 
 /-- Process the given congruence theorem hypothesis. Return true if it made "progress". -/
 def processCongrHypothesis (h : Expr) : SimpM Bool := do
+  trace[Debug.Meta.Tactic.simp.congr] "Processing {h} of type {←inferType h}"
   forallTelescopeReducing (← inferType h) fun xs hType => withNewLemmas xs do
+    unless (← getConfig).underLambda || xs.isEmpty do
+      return false
     let lhs ← instantiateMVars hType.appFn!.appArg!
     let r ← simp lhs
     let rhs := hType.appArg!
@@ -546,6 +570,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
       let x := xs[i]!
       try
         if (← processCongrHypothesis x) then
+          trace[Debug.Meta.Tactic.simp.congr] "modified!"
           modified := true
       catch _ =>
         trace[Meta.Tactic.simp.congr] "processCongrHypothesis {c.theoremName} failed {← inferType x}"

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -586,11 +586,15 @@ def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
   else
     let cfg ← getConfig
     let infos := (← getFunInfoNArgs r.expr args.size).paramInfo
+    let noIteArms := !cfg.underLambda && r.expr.isConstOf ``ite
     let mut r := r
     let mut i := 0
     for arg in args do
-      if h : i < infos.size then
-        trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
+      if noIteArms && (i == 3 || i == 4) then
+        -- Do not traverse then/else arguments when underLambda := false
+        r ← mkCongrFun r arg
+      else if h : i < infos.size then
+        trace[Debug.Meta.Tactic.simp] "app [{i+1}/{infos.size}] {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
         let info := infos[i]
         if cfg.ground && info.isInstImplicit then
           -- We don't visit instance implicit arguments when we are reducing ground terms.
@@ -645,6 +649,7 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
   let args := e.getAppArgs
   let infos := (← getFunInfoNArgs f args.size).paramInfo
   let config ← getConfig
+  let noIteArms := !config.underLambda && f.isConstOf ``ite
   let mut simplified := false
   let mut hasProof   := false
   let mut hasCast    := false
@@ -659,6 +664,11 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
         argsNew := argsNew.push arg
         i := i + 1
         continue
+    if noIteArms && (i = 3 || i = 4) then
+        -- Do not visit arms of an ite when `underLambda := false`
+        argsNew := argsNew.push arg
+        i := i + 1
+        continue
     match kind with
     | CongrArgKind.fixed =>
       let argNew ← dsimp arg

tests/lean/run/simpUnderLambda.lean

@@ -0,0 +1,95 @@
+import Lean
+/-!
+Tests for `simp -underlambda`
+
+(Not using #check_simp because it does not support simp arguments)
+-/
+
+opaque P : {α : Type} → α → Prop
+
+-- Like sorry, but no warning
+axiom abort {α : Prop} : α
+macro "abort" : tactic => `(tactic |exact abort)
+
+/-- info: ⊢ P fun x => x -/
+#guard_msgs in
+example : P (fun (x : Nat) => id x) := by
+  simp; trace_state; abort
+
+/-- info: ⊢ P fun x => id x -/
+#guard_msgs in
+example : P (id (fun (x : Nat) => id x)) :=
+  by simp -underLambda; trace_state; abort
+
+/--
+info: o : Option Nat
+⊢ P
+    (match o with
+    | some val => id true
+    | none => id false)
+-/
+#guard_msgs in
+example (o : Option Nat) : P (id (match id o with | some _ => id true | none => id false)) := by
+  simp -underLambda; trace_state; abort
+
+/--
+info: b : Bool
+⊢ P (if b = true then id 5 else id 6)
+-/
+#guard_msgs in
+example (b : Bool) : P (id (if id b then id 5 else id 6)) := by
+  simp -underLambda; trace_state; abort
+
+/--
+info: b : Bool
+⊢ P (if b = true then id 5 else id 6)
+-/
+#guard_msgs in
+example (b : Bool) : P (id (if id b then id 5 else id 6)) := by
+  dsimp -underLambda; trace_state; abort
+
+/--
+info: b : Bool
+g : {b : Bool} → b = true → Nat
+⊢ P (if h : b = true then id (g h) else id 7)
+-/
+#guard_msgs in
+set_option pp.proofs true in
+example (b : Bool) (g : {b : Bool} → b = true → Nat) :
+    P (id (if h : b then id (g h) else id 7)) := by
+  simp -underLambda; trace_state; abort
+
+
+/--
+info: xs : List Nat
+⊢ P (List.map (fun x => 0 + x) xs)
+-/
+#guard_msgs in
+example (xs : List Nat) :
+    P (id (xs.map (fun x => 0 + x))) := by
+  simp -underLambda; trace_state; abort
+
+-- The following rewrite works because
+-- List.map_id_fun
+-- applies definitionally
+
+/--
+info: xs : List Nat
+⊢ P (id xs)
+-/
+#guard_msgs in
+example (xs : List Nat) :
+    P (xs.map (fun x => id x)) := by
+  simp -underLambda only [List.map_id_fun]; trace_state; abort
+
+
+attribute [congr] List.map_congr_left
+
+/--
+info: xs : List Nat
+⊢ P (List.map (fun x => 0 + x) xs)
+-/
+#guard_msgs in
+example (xs : List Nat) :
+    P (id (xs.map (fun x => 0 + x))) := by
+  simp -underLambda; trace_state; abort

tests/lean/run/simpUnderLambdaFind.lean

@@ -0,0 +1,32 @@
+/-!
+This uses `simp -underLambda` to perform a calculation that involves well-founded
+recursion and is thus hard to do with `decide`. It needs the `-underLambda` flag
+as otherwise the well-founded function's equation lemmas cause it to loop.
+-/
+
+def find (P : Nat → Prop) [DecidablePred P] (i : Nat) (h : ∃ n, i ≤ n ∧ P n) : Nat :=
+  if hi : P i then
+    i
+  else
+    find P (i+1) (by
+      obtain ⟨w, hle, h⟩ := h
+      have : w ≠ i := fun heq => by cases heq; contradiction
+      exact ⟨w, by omega, h⟩;
+     )
+decreasing_by sorry
+
+-- Without -underLambda, the following example will unroll the `find` equation
+-- very very often
+
+/--
+error: tactic 'fail' failed
+P : Nat → Bool
+h0 : ∀ (i : Nat), i < 10 → ¬P i = true
+h1 : P 100 = true
+⊢ (if hi : P 10 = true then 10 else find (fun n => P n = true) (10 + 1) ⋯) = 100
+-/
+#guard_msgs in
+example (P : Nat → Bool) (h0 : ∀ i, i < 10 → ¬ P i) (h1 : P 100) :
+    find (fun n => P n) 0 ⟨100, by omega, h1⟩ = 100 := by
+  simp -underLambda [find, *]
+  fail