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

fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument (#2918)

Browse source 
Fixes #2914
This commit is contained in:
Kyle Miller 2023-11-20 01:51:47 -08:00 • committed by GitHub
parent 9bf0f5116b
commit 4d39a0b0e3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 23 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -24,15 +24,15 @@ where
| [] => ``(isTrue rfl)
| (a, b, recField, isProof) :: todo => withFreshMacroScope do
let rhs ← if isProof then
`(have h : $a = $b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
`(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
else
`(if h : $a = $b then
`(if h : @$a = @$b then
by subst h; exact $(← mkSameCtorRhs todo):term
else
isFalse (by intro n; injection n; apply h _; assumption))
if let some auxFunName := recField then
-- add local instance for `a = b` using the function being defined `auxFunName`
`(let inst := $(mkIdent auxFunName) $a $b; $rhs)
`(let inst := $(mkIdent auxFunName) @$a @$b; $rhs)
else
return rhs

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

@ -3,8 +3,8 @@
private def decEqTree✝ (x✝ : @Tree✝) (x✝¹ : @Tree✝) : Decidable✝ (x✝ = x✝¹) :=
match x✝, x✝¹ with
| @Tree.node a✝, @Tree.node b✝ =>
let inst✝ := decEqListTree✝ a✝ b✝;
if h✝ : a✝ = b✝ then by subst h✝; exact isTrue✝ rfl✝
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)
private def decEqListTree✝ (x✝² : @ListTree✝) (x✝³ : @ListTree✝) : Decidable✝ (x✝² = x✝³) :=
match x✝², x✝³ with
@ -12,11 +12,11 @@
| ListTree.nil .., ListTree.cons .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
| ListTree.cons .., ListTree.nil .. => isFalse✝¹ (by intro h✝¹; injection h✝¹)
| @ListTree.cons a✝¹ a✝², @ListTree.cons b✝¹ b✝² =>
let inst✝¹ := decEqTree✝ a✝¹ b✝¹;
if h✝² : a✝¹ = b✝¹ then by subst h✝²;
let inst✝¹ := decEqTree✝ @a✝¹ @b✝¹;
if h✝² : @a✝¹ = @b✝¹ then by subst h✝²;
exact
let inst✝² := decEqListTree✝ a✝² b✝²;
if h✝³ : a✝² = b✝² then by subst h✝³; exact isTrue✝² rfl✝²
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)
else isFalse✝³ (by intro n✝²; injection n✝²; apply h✝² _; assumption)
end,
@ -30,20 +30,20 @@
| Foo₁.foo₁₁ .., Foo₁.foo₁₂ .. => isFalse✝ (by intro h✝; injection h✝)
| Foo₁.foo₁₂ .., Foo₁.foo₁₁ .. => isFalse✝ (by intro h✝; injection h✝)
| @Foo₁.foo₁₂ a✝, @Foo₁.foo₁₂ b✝ =>
let inst✝ := decEqFoo₂✝ a✝ b✝;
if h✝¹ : a✝ = b✝ then by subst h✝¹; exact isTrue✝¹ rfl✝¹
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)
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✝²
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)
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✝³
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)
end,
instance : DecidableEq✝ (@Foo₁✝) :=

8
tests/lean/run/2914.lean Normal file
View file

@ -0,0 +1,8 @@
/-
The DecidableEq deriving handler should succeed even if fields have types starting with implicit arguments.
-/
structure Foo where
a : List Nat
ha : ∀ {i}, i ∈ a → 0 < i
deriving DecidableEq