chore: update stage0

closes #2835

src/Lean/Meta/DiscrTree.lean

@@ -69,21 +69,36 @@ instance : LT Key := ⟨fun a b => Key.lt a b⟩
 instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
 
 def Key.format : Key → Format
-  | .star                   => "*"
-  | .other                  => "◾"
-  | .lit (Literal.natVal v) => Std.format v
-  | .lit (Literal.strVal v) => repr v
-  | .const k _              => Std.format k
-  | .proj s i _             => Std.format s ++ "." ++ Std.format i
-  | .fvar k _               => Std.format k.name
-  | .arrow                  => "→"
+  | .star            => "*"
+  | .other           => "◾"
+  | .lit (.natVal v) => Std.format v
+  | .lit (.strVal v) => repr v
+  | .const k _       => Std.format k
+  | .proj s i _      => Std.format s ++ "." ++ Std.format i
+  | .fvar k _        => Std.format k.name
+  | .arrow           => "→"
 
 instance : ToFormat Key := ⟨Key.format⟩
 
 def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a
-  | .arrow      => 2
+  /-
+  Remark: `.arrow` used to have arity 2, and was used to encode non-dependent arrows.
+  However, this feature was a recurrent source of bugs. For example, a theorem about
+  a dependent arrow can be applied to a non-dependent one. The reverse direction may
+  also happen. See issue #2835.
+  ```
+  -- A theorem about the non-dependent arrow `a → a`
+  theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
+
+  -- can be applied to the dependent one `(h : P a) → P (f h)`.
+  example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
+    simp only [imp_self']
+  ```
+  Thus, we now index dependent and non-dependent arrows using the key `.arrow` with arity 0.
+  -/
+  | .arrow      => 0
   | .proj _ _ a => 1 + a
   | _           => 0
 
@@ -270,39 +285,12 @@ partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
 -/
 private def isBadKey (fn : Expr) : Bool :=
   match fn with
-  | .lit ..   => false
-  | .const .. => false
-  | .fvar ..  => false
-  | .proj ..  => false
-  | .forallE _ _ b _ => b.hasLooseBVars
-  | _ => true
-
-/--
-  Try to eliminate loose bound variables by performing beta-reduction.
-  We use this method when processing terms in discrimination trees.
-  These trees distinguish dependent arrows from nondependent ones.
-  Recall that dependent arrows are indexed as `.other`, but nondependent arrows as `.arrow ..`.
-  Motivation: we want to "discriminate" implications and simple arrows in our index.
-
-  Now suppose we add the term `Foo (Nat → Nat)` to our index. The nested arrow appears as
-  `.arrow ..`. Then, suppose we want to check whether the index contains
-  `(x : Nat) → (fun _ => Nat) x`, but it will fail to retrieve `Foo (Nat → Nat)` because
-  it assumes the nested arrow is a dependent one and uses `.other`.
-
-  We use this method to address this issue by beta-reducing terms containing loose bound variables.
-  See issue #2232.
-
-  Remark: we expect the performance impact will be minimal.
--/
-private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
-  Core.transform e
-    (pre := fun e => do
-      if !e.hasLooseBVars then
-        return .done e
-      else if e.isHeadBetaTarget then
-        return .visit e.headBeta
-      else
-        return .continue)
+  | .lit ..     => false
+  | .const ..   => false
+  | .fvar ..    => false
+  | .proj ..    => false
+  | .forallE .. => false
+  | _           => true
 
 /--
   Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
@@ -326,7 +314,6 @@ def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
-
 /--
 Append `n` wildcards to `todo`
 -/
@@ -390,15 +377,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
         return (.other, todo)
       else
         return (.star, todo)
-    | .forallE _ d b _ =>
-      -- See comment at elimLooseBVarsByBeta
-      let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
-      if b.hasLooseBVars then
-        return (.other, todo)
-      else
-        return (.arrow, todo.push d |>.push b)
-    | _ =>
-      return (.other, todo)
+    | .forallE .. => return (.arrow, todo)
+    | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
 partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
@@ -556,15 +536,8 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .proj s i a .. =>
     let nargs := e.getAppNumArgs
     return (.proj s i nargs, #[a] ++ e.getAppRevArgs)
-  | .forallE _ d b _ =>
-    -- See comment at elimLooseBVarsByBeta
-    let b ← if b.hasLooseBVars then elimLooseBVarsByBeta b else pure b
-    if b.hasLooseBVars then
-      return (.other, #[])
-    else
-      return (.arrow, #[d, b])
-  | _ =>
-    return (.other, #[])
+  | .forallE .. => return (.arrow, #[])
+  | _ => return (.other, #[])
 
 private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
   getKeyArgs e (isMatch := true) (root := root) (config := config)
@@ -608,12 +581,6 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       let result ← visitStar result
       match k with
       | .star  => return result
-      /-
-        Note: dep-arrow vs arrow
-        Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are `(Key.arrow, #[a, b])`.
-        A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`). Thus, we also visit the `Key.other` child.
-      -/
-      | .arrow => visitNonStar .other #[] (← visitNonStar k args result)
       | _      => visitNonStar k args result
 
 private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) :=
@@ -627,8 +594,6 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig)
     let (k, args) ← getMatchKeyArgs e (root := true) config
     match k with
     | .star  => return (k, result)
-    /- See note about "dep-arrow vs arrow" at `getMatchLoop` -/
-    | .arrow => return (k, (← getMatchRoot d k args (← getMatchRoot d .other #[] result config) config))
     | _      => return (k, (← getMatchRoot d k args result config))
 
 /--
@@ -708,8 +673,6 @@ where
           | some c => process 0 (todo ++ args) c.2 result
         match k with
         | .star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
-        -- See comment a `getMatch` regarding non-dependent arrows vs dependent arrows
-        | .arrow => visitNonStar .other #[] (← visitNonStar k args (← visitStar result))
         | _      => visitNonStar k args (← visitStar result)
 
 namespace Trie

tests/lean/run/2835.lean

@@ -0,0 +1,6 @@
+@[simp] theorem imp_self' {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩
+
+example {P : Prop} : P → P := by simp only [imp_self']
+
+example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
+  simp only [imp_self']