From 78146190e57e45e32fe4168f51afcb1228b60b10 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 19 Aug 2024 17:00:03 +0200
Subject: [PATCH] feat: mutual recursion: allow common prefix up to
 alpha-equivalence (#5041)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

@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.
---
 .../Elab/PreDefinition/Structural/Main.lean   |  2 +-
 src/Lean/Elab/PreDefinition/WF/Main.lean      |  2 +-
 tests/lean/run/recCommonPrefixAlpha.lean      | 34 +++++++++++++++++++
 3 files changed, 36 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/recCommonPrefixAlpha.lean

diff --git a/src/Lean/Elab/PreDefinition/Structural/Main.lean b/src/Lean/Elab/PreDefinition/Structural/Main.lean
index 73628cd472c2..e5f54bf6cc16 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Main.lean
+++ b/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 =>
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index bbe5b191da4f..85dbda6dc807 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/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 =>
diff --git a/tests/lean/run/recCommonPrefixAlpha.lean b/tests/lean/run/recCommonPrefixAlpha.lean
new file mode 100644
index 000000000000..e091fe432768
--- /dev/null
+++ b/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