feat: ensure projections are not reducing at DiscrTree V (simpleReduce := true)

Now, the `simp` discrimination tree does not perform `iota` nor reduce
projections.

src/Lean/Meta/DiscrTree.lean

@@ -225,23 +225,12 @@ def hasNoindexAnnotation (e : Expr) : Bool :=
 
 /--
 Reduction procedure for the discrimination tree indexing.
-It only unfolds reducible definitions, and does not perform iota reduction.
-
-We disable iota reduction because of simp theorems such as
-```
-@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
-    Quot.liftOn (Quot.mk r a) f h = f a := rfl
-```
-If we use iota, the lhs becomes `f a`
-
-We have considered disabling other reductions (e.g., projection reduction), but
-we could not even compile `Init` with this setup.
-
-Remark: rnote it is not sufficient to just unfold reducible definitions and perform
-beta-reduction, we must also instantiate assgined metavariables, and perform zeta-reduction.
+The parameter `simpleReduce` controls how aggressive the term is reduced.
+The parameter at type `DiscrTree` controls this value.
+See comment at `DiscrTree`.
 -/
 partial def reduce (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
-  let e ← whnfCore e (iota := !simpleReduce)
+  let e ← whnfCore e (simpleReduceOnly := simpleReduce)
   match (← unfoldDefinition? e) with
   | some e => reduce e simpleReduce
   | none => match e.etaExpandedStrict? with
@@ -267,21 +256,21 @@ private def isBadKey (fn : Expr) : Bool :=
   Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
   is a bad key (see comment at `isBadKey`).
   We use this method instead of `reduce` for root terms at `pushArgs`. -/
-private partial def reduceUntilBadKey (e : Expr) : MetaM Expr := do
+private partial def reduceUntilBadKey (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
   let e ← step e
   match e.etaExpandedStrict? with
-  | some e => reduceUntilBadKey e
+  | some e => reduceUntilBadKey e simpleReduce
   | none   => return e
 where
   step (e : Expr) := do
-    let e ← whnfCore e (iota := false)
+    let e ← whnfCore e (simpleReduceOnly := simpleReduce)
     match (← unfoldDefinition? e) with
     | some e' => if isBadKey e'.getAppFn then return e else step e'
     | none    => return e
 
 /-- whnf for the discrimination tree module -/
 def reduceDT (e : Expr) (root : Bool) (simpleReduce : Bool) : MetaM Expr :=
-  if root then reduceUntilBadKey e else reduce e simpleReduce
+  if root then reduceUntilBadKey e simpleReduce else reduce e simpleReduce
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 

src/Lean/Meta/WHNF.lean

@@ -485,14 +485,17 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
     return none
 
 /--
-  Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
-  expand let-expressions, expand assigned meta-variables.
+Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
+expand let-expressions, expand assigned meta-variables.
 
-  The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
-  then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
-  We only set this flag to `false` when implementing `isDefEq`.
+The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
+then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
+We only set this flag to `false` when implementing `isDefEq`.
+
+If `simpleReduceOnly`, then `iota` and projection reduction are not performed.
+Note that the value of `deltaAtProj` is irrelevant if `simpleReduceOnly = true`.
 -/
-partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) (iota := true) : MetaM Expr :=
+partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) (simpleReduceOnly := false) : MetaM Expr :=
   go e
 where
   go (e : Expr) : MetaM Expr :=
@@ -511,14 +514,14 @@ where
           go eNew
         else
           let e := if f == f' then e else e.updateFn f'
-          match (← reduceMatcher? e) with
-          | ReduceMatcherResult.reduced eNew => go eNew
-          | ReduceMatcherResult.partialApp   => pure e
-          | ReduceMatcherResult.stuck _      => pure e
-          | ReduceMatcherResult.notMatcher   =>
-            if !iota then
-              return e
-            else
+          if simpleReduceOnly then
+            return e
+          else
+            match (← reduceMatcher? e) with
+            | ReduceMatcherResult.reduced eNew => go eNew
+            | ReduceMatcherResult.partialApp   => pure e
+            | ReduceMatcherResult.stuck _      => pure e
+            | ReduceMatcherResult.notMatcher   =>
               matchConstAux f' (fun _ => return e) fun cinfo lvls =>
                 match cinfo with
                 | ConstantInfo.recInfo rec    => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
@@ -530,10 +533,13 @@ where
                     return e
                 | _ => return e
       | Expr.proj _ i c =>
-        let c ← if deltaAtProj then whnf c else whnfCore c
-        match (← projectCore? c i) with
-        | some e => go e
-        | none => return e
+        if simpleReduceOnly then
+          return e
+        else
+          let c ← if deltaAtProj then whnf c else whnfCore c
+          match (← projectCore? c i) with
+          | some e => go e
+          | none => return e
       | _ => unreachable!
 
 /--

tests/lean/973.lean.expected.out

@@ -1,2 +0,0 @@
-973.lean:4:2-4:6: error: invalid `simp` theorem, equation is equivalent to
-  x = x

tests/lean/run/946.lean

@@ -76,7 +76,7 @@ theorem consistentConcatOfConsistentRow
   match df with
     | ⟨_, rows, hr⟩ => by
       induction rows with
-        | nil         => simp [hc] -- breaks here
+        | nil         => simp at hc; simp [hc]
         | cons _ _ hi => exact ⟨hr.1, hi hr.2 hc⟩
 
 def addRow (df : DataFrame) (row : List DataEntry)