feat: mutual recursion: allow common prefix up to alpha-equivalence (#…

…5041)

@arthur-adjedj was very confused when a mutually recursive definition
didn't work as expected, and the reason was that he used different names
for the fixed parameters.

It seems plausible to simply allow that and calculate the fixed-prefix
up to alpha renaming.

It does mean, though, that, for example, termination proof goals will
mention the names as used by the first function. But probably better
than simply failing. And we could even fix that later (by passing down
the
actual names, and renmaing the variables in the context of the mvar,
depending on the “current function”) should it bother our users.

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

@@ -65,7 +65,7 @@ where
   go (fvars : Array Expr) (vals : Array Expr) : M α := do
     if !(vals.all fun val => val.isLambda) then
       k fvars vals
-    else if !(← vals.allM fun val => return val.bindingName! == vals[0]!.bindingName! && val.binderInfo == vals[0]!.binderInfo && (← isDefEq val.bindingDomain! vals[0]!.bindingDomain!)) then
+    else if !(← vals.allM fun val=> isDefEq val.bindingDomain! vals[0]!.bindingDomain!) then
       k fvars vals
     else
       withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>

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

@@ -36,7 +36,7 @@ where
   go (fvars : Array Expr) (vals : Array Expr) : TermElabM α := do
     if !(vals.all fun val => val.isLambda) then
       k fvars vals
-    else if !(← vals.allM fun val => return val.bindingName! == vals[0]!.bindingName! && val.binderInfo == vals[0]!.binderInfo && (← isDefEq val.bindingDomain! vals[0]!.bindingDomain!)) then
+    else if !(← vals.allM fun val => isDefEq val.bindingDomain! vals[0]!.bindingDomain!) then
       k fvars vals
     else
       withLocalDecl vals[0]!.bindingName! vals[0]!.binderInfo vals[0]!.bindingDomain! fun x =>

tests/lean/run/recCommonPrefixAlpha.lean

@@ -0,0 +1,34 @@
+namespace Structural
+mutual
+def f1 (α : Type) : List α → Nat
+| [] => 0
+| _ :: xs => f2 α xs + 1
+termination_by structural n => n
+
+-- NB β, not α. Used to prevent this from working (with an unhelpful error message)
+def f2 (β : Type) : List β → Nat
+| [] => 0
+| _ :: xs => f1 β xs + 1
+termination_by structural n => n
+end
+end Structural
+
+namespace WF
+
+mutual
+def f1 (α : Type) : List α → Nat
+| [] => 0
+| _ :: xs => f2 α xs + 1
+termination_by n => n
+
+-- NB β, not α. Used to prevent this from working (with an unhelpful error message)
+def f2 (β : Type) : List β → Nat
+| [] => 0
+| _ :: xs => f1 β xs + 1
+termination_by n => n
+decreasing_by
+  -- NB: The proof goal for `f2` mentions `α`, not `β`. Could be fixed in theory if we really care
+  guard_hyp α : Type
+  decreasing_tactic
+end
+end WF