max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: deriving DecidableEq to use termination_by structural (#4826)

Browse source 
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.
This commit is contained in:
Joachim Breitner 2024-07-29 18:24:05 -03:00 • committed by GitHub
parent 69c71f6476
commit 4ea55687a5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Elab/Deriving/DecEq.lean
View file

@ -91,8 +91,14 @@ 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 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
$termSuffix:suffix)
def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do
let mut res : Array (TSyntax `command) := #[]

5
tests/lean/decEqMutualInductives.lean.expected.out
View file

@ -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₁✝]