feat: keep haves above a split match in equation lemmas

src/Lean/Meta/Match/Rewrite.lean

@@ -65,14 +65,16 @@ In the `onAlt` handler of a `MatcherApp.transform`, you can use this function on
 substituted matcher application with the alternative `altIdx`.
 
 If it fails, it returns a rewrite with `proof? := none` and the unchanged expression.
+If the matcher is applied to more arguments than its arity, the rewrite applies to the matcher
+application and carries the extra arguments along.
 
 "Properly substituted" here means that the discriminants have been substituted according to the
 alternative; otherwise, the rewrite might fail because some hypothesis of the congruence
 equation theorem cannot be discharged by assumption or reflixivity.
 See `Lean.Meta.Tactic.FunInd.buildInductionBody` and `Lean.Elab.Tactic.Do.VCGen.Split` for examples
 of how to coerce `MatherApp.transform` into doing the substitution on the motive for you.
 -/
-def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
+partial def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
   if e.isAppOf ``PSum.casesOn || e.isAppOf ``PSigma.casesOn then
     let mut e := e
     while true do
@@ -90,6 +92,11 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
       trace[Meta.Match.debug] "Not a matcher application:{indentExpr e}"
       return { expr := e }
     let matcherDeclName := e.getAppFn.constName!
+    let some info ← getMatcherInfo? matcherDeclName | return { expr := e }
+    let args := e.getAppArgs
+    if info.arity < args.size then
+      let r ← rwMatcher altIdx (mkAppN e.getAppFn (args.extract 0 info.arity))
+      return ← r.addExtraArgs (args.extract info.arity)
     let eqns ← Match.genMatchCongrEqns matcherDeclName
     unless altIdx < eqns.size do
       trace[Meta.Match.debug] "When trying to reduce arm {altIdx}, only {eqns.size} equations for {.ofConstName matcherDeclName}"
@@ -128,7 +135,9 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
           else if hType.isEq then
             h.assumption <|> h.refl <|> throwError m!"Failed to resolve `{h}`"
           else if hType.isHEq then
-            h.assumption <|> h.hrefl <|> throwError m!"Failed to resolve `{h}`"
+            -- Splitting may provide an `Eq` hypothesis where the matcher equation requires `HEq`.
+            h.assumption <|> h.hrefl <|> (do (← h.heqOfEq).assumption) <|>
+              throwError m!"Failed to resolve `{h}`"
       let unassignedHyps ← hyps.filterM fun h => return !(← h.isAssigned)
       unless unassignedHyps.isEmpty do
         throwError m!"Not all hypotheses of `{.ofConstName eqnThm}` could be discharged: {unassignedHyps}"

src/Lean/Meta/Tactic/Split.lean

@@ -10,6 +10,7 @@ public import Lean.Meta.Match.MatcherApp.Basic
 public import Lean.Meta.Tactic.Apply
 public import Lean.Meta.Tactic.Generalize
 public import Lean.Meta.Tactic.Simp.Types
+import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.SplitIf
 
@@ -249,17 +250,18 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs :
       | none => mvarId := mvarId'
   return mvarId
 
-def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := do
+private def applyMatchSplitterCore (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level)
+    (params : Array Expr) (discrs : Array Expr)
+    (generalize : MVarId → Expr → Array Expr → MetaM (Array FVarId × Array FVarId × MVarId)) :
+    MetaM (List MVarId) := do
   let some info ← getMatcherInfo? matcherDeclName | throwInternalMisuseError m!"Internal error in `split` tactic: `{matcherDeclName}` is not an auxiliary declaration used to encode `match`-expressions"
   let matchEqns ← Match.getEquationsFor matcherDeclName
   -- splitterPre does not have the correct universe elimination level, but this is fine, we only use it to compute the `motiveType`,
   -- and we only care about the `motiveType` arguments, and not the resulting `Sort u`.
   let splitterPre := mkAppN (mkConst matchEqns.splitterName us.toList) params
   let motiveType := (← whnfForall (← inferType splitterPre)).bindingDomain!
   trace[split.debug] "applyMatchSplitter\n{mvarId}"
-  let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs
-  trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}"
-  let (discrFVarIds, discrEqs, mvarId) ← generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs
+  let (discrFVarIds, discrEqs, mvarId) ← generalize mvarId motiveType discrs
   trace[split.debug] "after generalizeMatchDiscrs\n{mvarId}"
   let mvarId ← generalizeTargetsEq mvarId motiveType (discrFVarIds.map mkFVar)
   mvarId.withContext do trace[split.debug] "discrEqs after generalizeTargetsEq: {discrEqs.map mkFVar}"
@@ -303,6 +305,40 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le
         return (i+1, mvarId::mvarIds)
     return mvarIds.reverse
 
+def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) :=
+  applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs => do
+    let (discrs, mvarId) ← generalizeMatchPropDiscrs mvarId discrs
+    trace[split.debug] "after generalizeMatchPropDiscrs\n{mvarId}"
+    generalizeMatchDiscrs mvarId matcherDeclName motiveType discrs
+
+/--
+Refines a goal into the cases of a matcher applied to `params` and `discrs`, without replacing
+matcher occurrences in the target. The arguments must be well-typed in the goal's context, but
+the matcher application need not occur in the target.
+
+Computed discriminants are linked to fresh variables by equalities. After splitting, these
+equalities specialize the goal where possible. Contradictory branches are closed; unresolved
+conditions remain as hypotheses. The target is not simplified.
+-/
+def refineMatch (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level)
+    (params : Array Expr) (discrs : Array Expr) : MetaM (List MVarId) := mvarId.withContext do
+  let mvarIds ← applyMatchSplitterCore mvarId matcherDeclName us params discrs fun mvarId motiveType discrs =>
+    mvarId.withContext do
+      if ← discrs.allM fun discr => do
+        unless discr.isFVar do return false
+        return !(← discr.fvarId!.getDecl).isLet
+      then
+        return (discrs.map (·.fvarId!), #[], mvarId)
+      let mvarId ← generalizeTargetsEq mvarId motiveType discrs
+      let (discrFVarIds, mvarId) ← mvarId.introN discrs.size
+      let (discrEqs, mvarId) ← mvarId.introN discrs.size
+      return (discrFVarIds, discrEqs, mvarId)
+  /- Substitution can expose contradictions in the generalized discriminant equalities
+     (e.g. `0 = n.succ`) or overlap exclusions (e.g. `0 = 0 → False`). These hypotheses
+     are already in the local context, so `Cases.unifyEqs?` does not process them. -/
+  mvarIds.filterM fun mvarId => do
+    return !(← mvarId.contradictionCore { useDecide := false, emptyType := false, genDiseq := true })
+
 def mkDiscrGenErrorMsg (e : Expr) : MessageData :=
   m!"`split` tactic failed to generalize discriminant(s) at{indentExpr e}\nresulting expression was not type correct\npossible solution: generalize discriminant(s) manually before using `split`"
 

tests/elab/1074a.lean

@@ -1,3 +1,5 @@
+/-! Equation generation for recursive elimination of proofs. -/
+
 inductive Term : Type
 | id2: Term -> Term -> Term
 
@@ -19,10 +21,7 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp
   }
 
 /--
-info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) :
-  H_2.interp =
-    match ⋯ with
-    | ⋯ => Hz.interp
+info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) : H_2.interp = ⋯.interp
 -/
 #guard_msgs in
 #check Brx.interp.eq_1

tests/elab/5667.lean

@@ -1,3 +1,5 @@
+/-! Equation generation for structural and mutual recursion with multiple discriminants (#5667). -/
+
 inductive Expr where
   | const (i : BitVec 32)
   | op (op : Unit) (e1 : Expr)
@@ -25,10 +27,10 @@ info: optimize.eq_def (x✝ : Expr) :
 /--
 info: equations:
 @[backward_defeq] theorem optimize.eq_1 : ∀ (i : BitVec 32), optimize (Expr.const i) = Expr.const i
-theorem optimize.eq_2 : ∀ (e1 : Expr) (bop : Unit) (i : BitVec 32),
-  optimize e1 = Expr.const i → optimize (Expr.op bop e1) = Expr.op bop (Expr.const 0)
-theorem optimize.eq_3 : ∀ (e1 : Expr) (bop : Unit),
-  (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop e1) = Expr.const 0
+theorem optimize.eq_2 : ∀ (e1 : Expr) (bop_1 : Unit) (i : BitVec 32),
+  optimize e1 = Expr.const i → optimize (Expr.op bop_1 e1) = Expr.op bop_1 (Expr.const 0)
+theorem optimize.eq_3 : ∀ (e1 : Expr) (bop_1 : Unit),
+  (∀ (i : BitVec 32), optimize e1 = Expr.const i → False) → optimize (Expr.op bop_1 e1) = Expr.const 0
 -/
 #guard_msgs in
 #print equations optimize

tests/elab/ack.lean

@@ -16,8 +16,8 @@ trace: [simp] Diagnostics
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---
 trace: [diag] Diagnostics
-  [kernel] unfolded declarations (max: 86, num: 1):
-    [kernel] OfNat.ofNat ↦ 86
+  [kernel] unfolded declarations (max: 91, num: 1):
+    [kernel] OfNat.ofNat ↦ 91
   use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 -/
 #guard_msgs in

tests/elab/byteSliceIssue.lean

@@ -1,3 +1,5 @@
+/-! Equation generation for a well-founded monadic byte-slice loop. -/
+
 def Nat.Up (ub a i : Nat) := i < a ∧ i < ub
 
 theorem Nat.Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩

tests/elab/byteSliceIssue.lean.out.expected

@@ -5,7 +5,5 @@
       let __do_lift ← f (arr.get! i) b
       match __do_lift with
         | ForInStep.done b => pure b
-        | ForInStep.yield b =>
-          have this := ⋯;
-          forIn.loop f arr off _end (i + 1) b
+        | ForInStep.yield b => forIn.loop f arr off _end (i + 1) b
     else pure b

tests/elab/eqns_have_invariant.lean

@@ -0,0 +1,115 @@
+module
+
+/-! Simplifying generated equations must preserve the `have` abstraction invariant (#16122). -/
+
+def dependentMatcher : Nat :=
+  have a := 0
+  have q : { n : Nat // n = a } :=
+    match a with
+    | 0 => ⟨0, rfl⟩
+    | n+1 => ⟨n+1, rfl⟩
+  q.val
+
+example (n : Nat) : dependentMatcher = 0 := by
+  simp -zeta only [dependentMatcher.eq_1, ← Nat.sub_self n]
+  simp -zeta only [Nat.sub_self]
+  rfl
+
+opaque usesProof (n : Nat) (h : n = 0) : Nat
+
+-- The dependency occurs inside a proof argument, while the result type remains `Nat`.
+def namedMatcher : Nat :=
+  have a := 0
+  match h : a with
+  | 0 => usesProof a h
+  | _+1 => 0
+
+example (n : Nat) : namedMatcher = usesProof 0 rfl := by
+  simp -zeta only [namedMatcher.eq_1, ← Nat.sub_self n] <;>
+    simp -zeta only [Nat.sub_self] <;> rfl
+
+-- The dependent `let` makes equation normalization use `dsimp` for `n`'s value.
+set_option cleanup.letToHave false in
+def fixedHave : Nat :=
+  have n :=
+    have a := 0
+    have q : {n : Nat // n = a} := match a with
+      | 0 => ⟨0, rfl⟩
+      | n+1 => ⟨n+1, rfl⟩
+    q.val
+  let v : Fin (n+1) := ⟨0, Nat.zero_lt_succ n⟩
+  n + v.val
+
+example (m : Nat) : fixedHave = 0 := by
+  simp -zeta only [fixedHave.eq_1, ← Nat.sub_self m]
+  simp -zeta only [Nat.sub_self]
+  rfl
+
+/- The second and fourth alternatives are impossible because `a = 0`. Equation generation
+must eliminate them, including the contradiction in the second alternative's overlap condition. -/
+def depMatch (x : Nat) : Nat :=
+  have a := 0
+  have q : { n : Nat // n ≤ x + a } :=
+    match x, a with
+    | 0, 0 => ⟨0, by simp⟩
+    | 0, a => ⟨0, by simp⟩
+    | x+1, 0 => ⟨x, by simp⟩
+    | x+1, a+1 => ⟨x+a, by lia⟩
+  q.val
+
+/--
+info: depMatch.eq_1 :
+  depMatch 0 =
+    let a := 0;
+    have q := ⟨0, depMatch._proof_1⟩;
+    q.val
+-/
+#guard_msgs in #check depMatch.eq_1
+
+/--
+info: depMatch.eq_2 (x_3 : Nat) :
+  depMatch x_3.succ =
+    let a := 0;
+    have q := ⟨x_3, ⋯⟩;
+    q.val
+-/
+#guard_msgs in #check depMatch.eq_2
+
+example : depMatch 0 = 0 := depMatch.eq_1
+example (n : Nat) : depMatch (n+1) = n := depMatch.eq_2 n
+
+/-- error: Unknown identifier `depMatch.eq_3` -/
+#guard_msgs in #check depMatch.eq_3
+
+-- Constant discriminants must eliminate impossible alternatives without any local bindings.
+def constantDiscr (x : Nat) : Nat :=
+  match x, (0 : Nat) with
+  | 0, 0 => 0
+  | 0, _ => 0
+  | n+1, 0 => n
+  | n+1, k+1 => n+k
+
+example : constantDiscr 0 = 0 := constantDiscr.eq_1
+example (n : Nat) : constantDiscr (n+1) = n := constantDiscr.eq_2 n
+
+/-- error: Unknown identifier `constantDiscr.eq_3` -/
+#guard_msgs in #check constantDiscr.eq_3
+
+-- The impossible overlap condition quantifies over the payload of `some`.
+def constructorDiscr (x : Nat) : Nat :=
+  match x, (some 0 : Option Nat) with
+  | 0, some n => n
+  | 0, _ => 0
+  | n+1, _ => n
+
+example : constructorDiscr 0 = 0 := constructorDiscr.eq_1
+example (n : Nat) : constructorDiscr (n+1) = n := constructorDiscr.eq_2 n
+
+/-- info: constructorDiscr.eq_1 : constructorDiscr 0 = 0 -/
+#guard_msgs in #check constructorDiscr.eq_1
+
+/-- info: constructorDiscr.eq_2 (n : Nat) : constructorDiscr n.succ = n -/
+#guard_msgs in #check constructorDiscr.eq_2
+
+/-- error: Unknown identifier `constructorDiscr.eq_3` -/
+#guard_msgs in #check constructorDiscr.eq_3