fix: FunInd: preserve have (#10519)

This PR improves FunInd by preserving the `nondep` flag on `.letE`,
which makes it more likely that subsequent matcher transformations work.
Fixes #10516.

Author: nomeata

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -285,9 +285,8 @@ def transform
     let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
-    unless (← isTypeCorrect aux1) do
-      prependError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\nfailed with" do
-        check aux1
+    prependError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\nfailed with" do
+      check aux1
     let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1
 
     -- We replace the matcher with the splitter

src/Lean/Meta/Tactic/FunInd.lean

@@ -377,6 +377,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           mkForallFVars #[x] body'
 
     | .letE n t v b nondep =>
+      trace[Meta.FunInd] "Let-binding {n} with (nondep := {nondep})"
       let t' ← foldAndCollect oldIH newIH isRecCall t
       let v' ← foldAndCollect oldIH newIH isRecCall v
       withLetDecl n t' v' (nondep := nondep) fun x => do
@@ -520,7 +521,7 @@ def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr)
 Like `mkLambdaFVars (usedOnly := true)`, but
 
  * silently skips expression in `xs` that are not `.isFVar`
- * also skips let-bound variabls
+ * also skips let-bound variables
  * returns a mask (same size as `xs`) indicating which variables have been abstracted
    (`true` means was abstracted).
 
@@ -631,11 +632,17 @@ public def rwIfWith (hc : Expr) (e : Expr) : MetaM Simp.Result := do
     return { expr := e }
 
 def rwLetWith (h : Expr) (e : Expr) : MetaM Simp.Result := do
-  if e.isLet then
-    if (← isDefEq e.letValue! h) then
-      return { expr := e.letBody!.instantiate1 h }
-  trace[Meta.FunInd] "rwLetWith failed:{inlineExpr e}not a let expression or `{h}` is not definitionally equal to `{e.letValue!}`"
-  return { expr := e }
+  match e with
+  | .letE _ t v b nondep =>
+    unless (← isDefEq t (← inferType h)) do
+      trace[Meta.FunInd] "rwLetWith failed:The type of{inlineExpr h}is not definitionally equal to `{t}`"
+    unless nondep do
+      unless (← isDefEq v h) do
+        trace[Meta.FunInd] "rwLetWith failed:{inlineExpr h}is not definitionally equal to{inlineExpr v}"
+    return { expr := b.instantiate1 h }
+  | _ =>
+    trace[Meta.FunInd] "rwLetWith failed:{inlineExpr e}not a let expression"
+    return { expr := e }
 
 def rwMData (e : Expr) : MetaM Simp.Result := do
   return { expr := e.consumeMData }
@@ -735,7 +742,7 @@ as `MVars` as it goes.
 partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
   withTraceNode `Meta.FunInd
-    (pure m!"{exceptEmoji ·} buildInductionBody: {oldIH.name} → {newIH.name}\ngoal: {goal}:{indentExpr e}") do
+    (pure m!"{exceptEmoji ·} buildInductionBody: {oldIH.name} → {newIH.name}\ngoal:{indentExpr goal}\nexpr:{indentExpr e}") do
 
   -- if-then-else cause case split:
   match_expr e with
@@ -863,13 +870,14 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
       buildInductionBody toErase toClear goal' oldIH newIH isRecCall e.mdataExpr!
     return e.updateMData! b
 
-  if let .letE n t v b _ := e then
+  if let .letE n t v b nondep := e then
+    trace[Meta.FunInd] "Let-binding {n} with (nondep := {nondep})"
     let t' ← foldAndCollect oldIH newIH isRecCall t
     let v' ← foldAndCollect oldIH newIH isRecCall v
-    return ← withLetDecl n t' v' fun x => M2.branch do
+    return ← withLetDecl n t' v' (nondep := nondep) fun x => M2.branch do
       let b' ← withRewrittenMotiveArg goal (rwLetWith x) fun goal' =>
         buildInductionBody toErase toClear goal' oldIH newIH isRecCall (b.instantiate1 x)
-      mkLetFVars #[x] b'
+      mkLetFVars (generalizeNondepLet := false) #[x] b'
 
   -- Special case for traversing the PProd’ed bodies in our encoding of structural mutual recursion
   if let .lam n t b bi := e then
@@ -903,19 +911,25 @@ do not handle delayed assignments correctly.
 -/
 def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : MetaM Expr := do
   trace[Meta.FunInd] "abstractIndependentMVars, to revert after {index}, original mvars: {mvars}"
-  let mvars ← mvars.mapM fun mvar => do
-    let mvar ← cleanupAfter mvar index
-    mvar.withContext do
-      let fvarIds := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl => fvarIds.push decl.fvarId
-      let (_, mvar) ← mvar.revert fvarIds
-      pure mvar
-  trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
+  let mvars ← mvars.mapM (cleanupAfter · index)
   let names := Array.ofFn (n := mvars.size) fun ⟨i,_⟩ => .mkSimple s!"case{i+1}"
-  let types ← mvars.mapM MVarId.getType
+  let types ← mvars.mapM fun mvar => do
+    mvar.withContext do
+      let goal ← mvar.getType
+      let xs := (← getLCtx).foldl (init := #[]) (start := index+1) fun fvarIds decl =>
+        fvarIds.push (mkFVar decl.fvarId)
+      mkForallFVars (generalizeNondepLet := true) xs goal
+  trace[Meta.FunInd] "abstractIndependentMVars, reverted types: {types}"
   Meta.withLocalDeclsDND (names.zip types) fun xs => do
-      for mvar in mvars, x in xs do
-        mvar.assign x
-      mkLambdaFVars xs (← instantiateMVars e)
+    for mvar in mvars, x in xs do
+      mvar.withContext do
+        let e := (← getLCtx).foldl (init := x) (start := index+1) fun e decl =>
+          if decl.isLet (allowNondep := false) then
+            e
+          else
+            .app e (mkFVar decl.fvarId)
+        mvar.assign e
+    mkLambdaFVars xs (← instantiateMVars e)
 
 /--
 Given a unary definition `foo` defined via `WellFounded.fixF`, derive a suitable induction principle

tests/lean/run/doLogicTests.lean

@@ -241,8 +241,8 @@ theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n
 
 theorem fib_triple_cases : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   apply fib_impl.fun_cases n _ ?case1 ?case2
-  case case1 => rintro rfl; mintro -; simp only [fib_impl, ↓reduceIte]; mspec
-  intro h
+  case case1 => rintro _ rfl; mintro -; simp only [fib_impl, ↓reduceIte]; mspec
+  intro _ h
   mintro -
   simp only [fib_impl, h, reduceIte]
   mspec
@@ -261,8 +261,8 @@ theorem fib_impl_vcs
                   (I n hn).1 ⟨⟨pref, cur::suff, by simp[h]⟩, r⟩ ⊢ₛ (I n hn).1 ⟨⟨pref ++ [cur], suff, by simp[h]⟩, r.2, r.1+r.2⟩)
     : ⊢ₛ wp⟦fib_impl n⟧ (Q n) := by
   apply fib_impl.fun_cases n _ ?case1 ?case2
-  case case1 => intro h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec
-  intro hn
+  case case1 => intro _ h; simp only [fib_impl, h, ↓reduceIte]; mstart; mspec
+  intro _ hn
   simp only [fib_impl, hn, ↓reduceIte]
   mstart
   mspec

tests/lean/run/funind_tests.lean

@@ -81,7 +81,7 @@ termination_by n => n
 info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
   (a✝ : Nat) : motive a✝
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 #check have_tailrec.induct
 
 set_option linter.unusedVariables false in

tests/lean/run/funind_unfolding.lean

@@ -54,20 +54,31 @@ def fib'' (n : Nat) : Nat :=
       0
 
 /--
-info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n)
+info: fib''.induct_unfolding (motive : Nat → Nat → Prop) (case1 : ∀ (x : Nat), x < 2 → motive x x)
   (case2 :
-    ¬n < 2 →
-      have foo := n - 2;
-      foo < 100 → motive (fib'' (n - 1) + fib'' foo))
+    ∀ (x : Nat),
+      ¬x < 2 →
+        have foo := x - 2;
+        foo < 100 → motive (x - 1) (fib'' (x - 1)) → motive foo (fib'' foo) → motive x (fib'' (x - 1) + fib'' foo))
   (case3 :
-    ¬n < 2 →
-      have foo := n - 2;
-      ¬foo < 100 → motive 0) :
-  motive (fib'' n)
+    ∀ (x : Nat),
+      ¬x < 2 →
+        have foo := x - 2;
+        ¬foo < 100 → motive x 0)
+  (n : Nat) : motive n (fib'' n)
+-/
+#guard_msgs(pass trace, all) in
+#check fib''.induct_unfolding
+
+/--
+info: fib''.fun_cases_unfolding (n : Nat) (motive : Nat → Prop) (case1 : n < 2 → motive n)
+  (case2 : ¬n < 2 → ∀ (foo : Nat), foo < 100 → motive (fib'' (n - 1) + fib'' foo))
+  (case3 : ¬n < 2 → ∀ (foo : Nat), ¬foo < 100 → motive 0) : motive (fib'' n)
 -/
 #guard_msgs(pass trace, all) in
 #check fib''.fun_cases_unfolding
 
+
 -- set_option trace.Meta.FunInd true in
 def filter (p : Nat → Bool) : List Nat → List Nat
   | [] => []

tests/lean/run/issue10516.lean

@@ -0,0 +1,27 @@
+-- set_option trace.Meta.FunInd true
+
+def bla (a : Nat) (h : 0 < a) : Nat :=
+  if h : a ≤ 1 then
+    0
+  else
+    have : 0 ≠ a := by omega
+    match a with
+    | 0 => False.elim (by contradiction)
+    | a + 1 => bla a (by omega)
+termination_by structural a
+
+/--
+info: theorem bla.induct_unfolding : ∀ (motive : (a : Nat) → 0 < a → Nat → Prop),
+  (∀ (t : Nat) (h : 0 < t), t ≤ 1 → motive t h 0) →
+    (∀ (a : Nat) (h : 0 < a + 1) (h_1 : ¬a + 1 ≤ 1), 0 ≠ a + 1 → motive a ⋯ (bla a ⋯) → motive a.succ h (bla a ⋯)) →
+      ∀ (a : Nat) (h : 0 < a), motive a h (bla a h)
+-/
+#guard_msgs(pass trace, all) in #print sig bla.induct_unfolding
+
+/--
+info: theorem bla.induct : ∀ (motive : (a : Nat) → 0 < a → Prop),
+  (∀ (t : Nat) (h : 0 < t), t ≤ 1 → motive t h) →
+    (∀ (a : Nat) (h : 0 < a + 1) (h_1 : ¬a + 1 ≤ 1), 0 ≠ a + 1 → motive a ⋯ → motive a.succ h) →
+      ∀ (a : Nat) (h : 0 < a), motive a h
+-/
+#guard_msgs(pass trace, all) in #print sig bla.induct