From 3ef3e88f375bda3e10e1633bcd67d10c79bd8800 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jul 2024 10:01:14 +0200 Subject: [PATCH 1/2] refactor: deriving DecidableEq to use `termination_by structural` now that we support structural mutual recursion, I expect that every `DecidableEq` instance be implemented using structural recursion, so let's be explicit about it. --- src/Lean/Elab/Deriving/DecEq.lean | 7 +++++-- tests/lean/decEqMutualInductives.lean.expected.out | 5 +++++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 33b6fedb909d..1a86a97aa745 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -91,8 +91,11 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T let header ← mkDecEqHeader indVal let body ← mkMatch ctx header indVal let binders := header.binders - let type ← `(Decidable ($(mkIdent header.targetNames[0]!) = $(mkIdent header.targetNames[1]!))) - `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term) + let target₁ := mkIdent header.targetNames[0]! + let target₂ := mkIdent header.targetNames[1]! + let type ← `(Decidable ($target₁ = $target₂)) + `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term + termination_by structural $target₁) def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do let mut res : Array (TSyntax `command) := #[] diff --git a/tests/lean/decEqMutualInductives.lean.expected.out b/tests/lean/decEqMutualInductives.lean.expected.out index a64cfd97338f..bc22d84274e3 100644 --- a/tests/lean/decEqMutualInductives.lean.expected.out +++ b/tests/lean/decEqMutualInductives.lean.expected.out @@ -6,6 +6,7 @@ let inst✝ := decEqListTree✝ @a✝ @b✝; if h✝ : @a✝ = @b✝ then by subst h✝; exact isTrue✝ rfl✝ else isFalse✝ (by intro n✝; injection n✝; apply h✝ _; assumption) + termination_by structural x✝ private def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @ListTree.nil, @ListTree.nil => isTrue✝¹ rfl✝¹ @@ -19,6 +20,7 @@ if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝² rfl✝² else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝³ _; assumption) else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption) + termination_by structural x✝² end, instance : DecidableEq✝ (@ListTree✝) := decEqListTree✝] @@ -33,18 +35,21 @@ let inst✝ := decEqFoo₂✝ @a✝ @b✝; if h✝¹ : @a✝ = @b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹ else isFalse✝¹ (by intro n✝; injection n✝; apply h✝¹ _; assumption) + termination_by structural x✝ private def decEqFoo₂✝ (x✝² : @Foo₂✝) (x✝³ : @Foo₂✝) : Decidable✝ (x✝² = x✝³) := match x✝², x✝³ with | @Foo₂.foo₂ a✝¹, @Foo₂.foo₂ b✝¹ => let inst✝¹ := decEqFoo₃✝ @a✝¹ @b✝¹; if h✝² : @a✝¹ = @b✝¹ then by subst h✝²; exact isTrue✝² rfl✝² else isFalse✝² (by intro n✝¹; injection n✝¹; apply h✝² _; assumption) + termination_by structural x✝² private def decEqFoo₃✝ (x✝⁴ : @Foo₃✝) (x✝⁵ : @Foo₃✝) : Decidable✝ (x✝⁴ = x✝⁵) := match x✝⁴, x✝⁵ with | @Foo₃.foo₃ a✝², @Foo₃.foo₃ b✝² => let inst✝² := decEqFoo₁✝ @a✝² @b✝²; if h✝³ : @a✝² = @b✝² then by subst h✝³; exact isTrue✝³ rfl✝³ else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝³ _; assumption) + termination_by structural x✝⁴ end, instance : DecidableEq✝ (@Foo₁✝) := decEqFoo₁✝] From 1f3061a92ea401f809be335cb4ba23e82788ff9e Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 25 Jul 2024 12:01:51 +0200 Subject: [PATCH 2/2] Only for recursive data types --- src/Lean/Elab/Deriving/DecEq.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 1a86a97aa745..a3b6fbf5e0b5 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -93,9 +93,12 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T let binders := header.binders let target₁ := mkIdent header.targetNames[0]! let target₂ := mkIdent header.targetNames[1]! + let termSuffix ← if indVal.isRec + then `(Parser.Termination.suffix|termination_by structural $target₁) + else `(Parser.Termination.suffix|) let type ← `(Decidable ($target₁ = $target₂)) `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : $type:term := $body:term - termination_by structural $target₁) + $termSuffix:suffix) def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do let mut res : Array (TSyntax `command) := #[]