fix: cases to fail gracefully when motive has complex argument of dependent type

This PR lets `cases` fail gracefully when the motive has an complex
argument whose type is dependent type on the targets. While the
`induction` tactic can handle this well, `cases` does not. This change
at least gracefully degrades to not instantiating that motive parameter.
See issue #8296 for more details on this issue.

src/Lean/Elab/Tactic/Induction.lean

@@ -135,10 +135,11 @@ structure Result where
   complexArgs : Array Expr
 
 /--
-  Construct the an eliminator/recursor application. `targets` contains the explicit and implicit targets for
-  the eliminator. For example, the indices of builtin recursors are considered implicit targets.
-  Remark: the method `addImplicitTargets` may be used to compute the sequence of implicit and explicit targets
-  from the explicit ones.
+  Construct the an eliminator/recursor application. `targets` contains the explicit and implicit
+  targets for the eliminator, not yet generalized.
+  For example, the indices of builtin recursors are considered implicit targets.
+  Remark: the method `addImplicitTargets` may be used to compute the sequence of implicit and
+  explicit targets from the explicit ones.
 -/
 partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
   let rec loop : M Unit := do
@@ -213,24 +214,37 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
 /--
 Given a goal `... targets ... |- C[targets, complexArgs]` associated with `mvarId`,
 where `complexArgs` are the the complex (i.e. non-target) arguments to the motive in the conclusion
-of the eliminator, construct `motiveArg := fun targets xs => C[targets, xs]`
+of the eliminator, construct `motiveArg := fun targets rs => C[targets, rs]`
+
+This checks if the type of the complex arguments match what's expected by the motive, and
+ignores them otherwise. This limits the ability of `cases` to use unfolding function
+principles with dependent types, because after generalization of the targets, the types do
+no longer match. This can likely be improved.
 -/
 def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) (complexArgs : Array Expr := #[]) : MetaM Unit := do
   let type ← inferType (mkMVar mvarId)
+
+  let motiveType ← inferType (mkMVar motiveArg)
+  let exptComplexArgTypes ← arrowDomainsN complexArgs.size (← instantiateForall motiveType (targets.map mkFVar))
+
   let mut absType := type
-  for complexArg in complexArgs.reverse do
-    let complexTypeArg ← inferType complexArg
-    let absType' ← kabstract absType complexArg
-    let absType' := .lam (← mkFreshUserName `x) complexTypeArg absType' .default
-    if (← isTypeCorrect absType') then
-      absType := absType'
+  for complexArg in complexArgs.reverse, exptComplexArgType in exptComplexArgTypes.reverse do
+    trace[Elab.induction] "setMotiveArg: trying to abstract over {complexArg}, expected type {exptComplexArgType}"
+    let complexArgType ← inferType complexArg
+    if (← isDefEq complexArgType exptComplexArgType) then
+      let absType' ← kabstract absType complexArg
+      let absType' := .lam (← mkFreshUserName `x) complexArgType absType' .default
+      if (← isTypeCorrect absType') then
+        absType := absType'
+      else
+        trace[Elab.induction] "Not abstracing goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
+        absType := .lam (← mkFreshUserName `x) complexArgType absType .default
     else
-      trace[Elab.induction] "Not abstracing goal over {complexArg}, resulting term is not type correct:{indentExpr absType'} }"
-      absType := .lam (← mkFreshUserName `x) complexTypeArg absType .default
+      trace[Elab.induction] "Not abstracing goal over {complexArg}, its type {complexArgType} does not match the expected {exptComplexArgType}"
+      absType := .lam (← mkFreshUserName `x) exptComplexArgType absType .default
 
   let motive ← mkLambdaFVars (targets.map mkFVar) absType
   let motiverInferredType ← inferType motive
-  let motiveType ← inferType (mkMVar motiveArg)
   unless (← isDefEqGuarded motiverInferredType motiveType) do
     throwError "type mismatch when assigning motive{indentExpr motive}\n{← mkHasTypeButIsExpectedMsg motiverInferredType motiveType}"
   motiveArg.assign motive

tests/lean/run/inductionComplexMotive.lean

@@ -71,7 +71,7 @@ case case3
 n✝ m✝ : Nat
 ⊢ ackermann n✝ (ackermann (n✝ + 1) m✝) ≤ ackermann (n✝.succ + 1) m✝.succ
 -/
-#guard_msgs in
+#guard_msgs(pass trace, all) in
 example : ackermann n m ≤ ackermann (n+1) m := by
   cases n, m using ackermann_cases_unfolding
   fail
@@ -138,3 +138,50 @@ P : (n : Nat) → n > 0 → Prop
 example (P : (n : Nat) → (h : n > 0) → Prop) : P (n + 1) (Nat.zero_lt_succ n) := by
   cases n using strange_induction
   fail
+
+-- One where the type of the complex argument depends on the other targets
+
+axiom dep_induction
+  {motive : (n : Nat) → Fin (n+1) → Prop}
+  (case1 : motive 0 0) :
+  ∀ n, motive n (Fin.last n)
+
+/--
+error: tactic 'fail' failed
+case case1
+P : (n : Nat) → Fin (n + 1) → Prop
+⊢ P 0 0
+-/
+#guard_msgs in
+example (P : (n : Nat) → Fin (n+1) → Prop) : P n (Fin.last n) := by
+  induction n using dep_induction
+  fail
+
+
+-- Using cases does not unfold as expected, due to the dependent motive.
+-- This can be improved, but at least it does not error
+
+/--
+error: tactic 'fail' failed
+case case1
+P : (n : Nat) → Fin (n + 1) → Prop
+⊢ P 0 (Fin.last 0)
+-/
+#guard_msgs in
+example (P : (n : Nat) → Fin (n+1) → Prop) : P n (Fin.last n) := by
+  cases n using dep_induction
+  fail
+
+-- Using cases does not unfold as expected, due to the dependent motive.
+-- This can be improved, but at least it does not error
+
+/--
+error: tactic 'fail' failed
+case case1
+P : (n : Nat) → Fin (n + 1) → Prop
+⊢ P 0 (Fin.last 0)
+-/
+#guard_msgs(pass trace, all) in
+example (P : (n : Nat) → Fin (n+1) → Prop) : P 10 (Fin.last 10) := by
+  cases 10 using dep_induction
+  fail