fix: remove unused hypotheses from conditional equation theorems

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -200,6 +200,24 @@ where
     else
       saveEqn mvarId
 
+/--
+  Some of the hypotheses added by `mkEqnTypes` may not be used by the actual proof (i.e., `value` argument).
+  This method eliminates them.
+
+  Alternative solution: improve `saveEqn` and make sure it never includes unnecessary hypotheses.
+  These hypotheses are leftovers from tactics such as `splitMatch?` used in `mkEqnTypes`.
+-/
+partial def removeUnusedEqnHypotheses (type value : Expr) : MetaM (Expr × Expr) := do
+  match value with
+  | .lam n d b i =>
+    withLocalDecl n i.binderInfo d fun x => do
+      let (type, value) ← removeUnusedEqnHypotheses (type.bindingBody!.instantiate1 x) (b.instantiate1 x)
+      if value.containsFVar x.fvarId! || type.containsFVar x.fvarId! then
+        return (← mkForallFVars #[x] type, ← mkLambdaFVars #[x] value)
+      else
+        return (type, value)
+  | _ => return (type, value)
+
 structure EqnsExtState where
   map : Std.PHashMap Name (Array Name) := {}
   deriving Inhabited

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -70,6 +70,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
+    let (type, value) ← removeUnusedEqnHypotheses type value
     addDecl <| Declaration.thmDecl {
       name, type, value
       levelParams := info.levelParams

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -80,6 +80,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
+    let (type, value) ← removeUnusedEqnHypotheses type value
     addDecl <| Declaration.thmDecl {
       name, type, value
       levelParams := info.levelParams

tests/lean/run/lazyListRotateUnfoldProof.lean

@@ -0,0 +1,31 @@
+inductive LazyList (α : Type u)
+| nil : LazyList α
+| cons (hd : α) (tl : LazyList α) : LazyList α
+| delayed (t : Thunk (LazyList α)) : LazyList α
+
+namespace LazyList
+def length : LazyList α → Nat
+| nil        => 0
+| cons _ as  => length as + 1
+| delayed as => length as.get
+
+def force : LazyList α → Option (α × LazyList α)
+| delayed as => force as.get
+| nil        => none
+| cons a as  => some (a,as)
+end LazyList
+
+def rotate (f : LazyList τ) (r : List τ) (a : LazyList τ)
+  (h : f.length + 1 = r.length) : LazyList τ :=
+  match r with
+  | List.nil => False.elim (by simp_arith [LazyList.length] at h)
+  | y::r' =>
+  match f.force with
+  | none =>  LazyList.cons y a
+  | some (x, f') => LazyList.cons x (rotate f' r' (LazyList.cons y a) (sorry))
+
+theorem rotate_inv {F : LazyList τ} {R : List τ} : (h : F.length + 1 = R.length) → (rotate F R nil h).length = F.length + R.length := by
+  match F with
+  | LazyList.nil => intro h; unfold rotate; sorry
+  | LazyList.cons Fh Ft => sorry
+  | LazyList.delayed Ft => sorry