fix: missing withIncRecDepth and unifyEqs? and add support for of…

…fsets at `unifyEq?` (#4224)

Given `h` with type `x + k = y + k'` (or `h : k = k')`, `cases h`
produced a proof of size linear in `min k k'`. `isDefEq` has support for
offset, but `unifyEq?` did not have it, and a stack overflow occurred
while processing the resulting proof. This PR fixes this issue.

closes #4219

src/Init/Data/Nat/Linear.lean

@@ -714,4 +714,10 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 
-end Nat.Linear
+end Linear
+
+def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
+  simp_arith at h₁
+  exact h₂ h₁
+
+end Nat

src/Lean/Meta/Tactic/Cases.lean

@@ -200,7 +200,7 @@ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name
     { ctorName           := ctorName,
       toInductionSubgoal := s }
 
-partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := do
+partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
   if numEqs == 0 then
     return some (mvarId, subst)
   else

src/Lean/Meta/Tactic/UnifyEq.lean

@@ -21,6 +21,11 @@ structure UnifyEqResult where
   subst     : FVarSubst
   numNewEqs : Nat := 0
 
+private def toOffset? (e : Expr) : MetaM (Option (Expr × Nat)) := do
+  match (← evalNat e) with
+  | some k => return some (mkNatLit 0, k)
+  | none => isOffset? e
+
 /--
   Helper method for methods such as `Cases.unifyEqs?`.
   Given the given goal `mvarId` containing the local hypothesis `eqFVarId`, it performs the following operations:
@@ -69,7 +74,30 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {})
             return none -- this alternative has been solved
           else
             throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}"
+        /- Special support for offset equalities -/
+        let injectionOffset? (a b : Expr) := do
+          unless (← getEnv).contains ``Nat.elimOffset do return none
+          let some (xa, ka) ← toOffset? a | return none
+          let some (xb, kb) ← toOffset? b | return none
+          if ka == 0 || kb == 0 then return none -- use default noConfusion
+          let (x, y, k) ← if ka < kb then
+            pure (xa, (← mkAdd xb (mkNatLit (kb - ka))), ka)
+          else if ka = kb then
+            pure (xa, xb, ka)
+          else
+            pure ((← mkAdd xa (mkNatLit (ka - kb))), xb, kb)
+          let target ← mvarId.getType
+          let u ← getLevel target
+          let newTarget ← mkArrow (← mkEq x y) target
+          let tag ← mvarId.getTag
+          let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
+          let val := mkAppN (mkConst ``Nat.elimOffset [u]) #[target, x, y, mkNatLit k, eqDecl.toExpr, newMVar]
+          mvarId.assign val
+          let mvarId ← newMVar.mvarId!.tryClear eqDecl.fvarId
+          return some mvarId
         let rec injection (a b : Expr) := do
+          if let some mvarId ← injectionOffset? a b then
+            return some { mvarId, numNewEqs := 1, subst }
           if (← isConstructorApp a <&&> isConstructorApp b) then
             /- ctor_i ... = ctor_j ... -/
             match (← injectionCore mvarId eqFVarId) with

tests/lean/run/4219.lean

@@ -0,0 +1,9 @@
+example (h : 2000 = 2001) : False := by
+  cases h
+
+example (h : 20000 = 20001) : False := by
+  cases h
+
+example (h : x + 20000 = 20001) : x = 1 := by
+  cases h
+  rfl