subtype.eq has wrong signature

fgdorais commented 6 years ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
  - Specifically, check out the wishlist, open RFCs, or feature requests.
- Reduced the issue to a self-contained, reproducible test case.

Description

The signature of subtype.eq is incompatible with that of subtype. (Specifically, the former doesn't accept Sort 0 while the latter does.)

Steps to Reproduce

set_option pp.notation false
#check @subtype
#check @subtype.eq

Expected behavior: [What you expect to happen]

subtype : Π {α : Sort u_1}, (α → Prop) → Sort (max 1 u_1)
subtype.eq : ∀ {α : Sort u_1} {p : α → Prop} {a1 a2 : subtype (λ (x : α), p x)}, eq (a1.val) (a2.val) → eq a1 a2

Actual behavior: [What actually happens]

subtype : Π {α : Sort u_1}, (α → Prop) → Sort (max 1 u_1)
subtype.eq : ∀ {α : Type u_1} {p : α → Prop} {a1 a2 : subtype (λ (x : α), p x)}, eq (a1.val) (a2.val) → eq a1 a2

Reproduces how often: Always

Versions

Lean (version 3.4.1, Release)
Darwin Kernel Version 17.6.0: Tue May  8 15:22:16 PDT 2018; root:xnu-4570.61.1~1/RELEASE_X86_64

Additional information

From library/init/core.lean:

/- Remark: subtype must take a Sort instead of Type because of the axiom strong_indefinite_description. -/
structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

spl commented 6 years ago

FYI, for Lean 3.4.1, “[o]nly major bugs (e.g., soundness) will be fixed for this code base from now on” (e181232c8ffd2bc2ba1b2f9799f8ac0ea0e4e505), so I don't know if this change will be made. Given that, you may want to consider using mathlib, which has subtype.eq' with the better signature:

import data.sigma.basic
#check @subtype.eq'

subtype.eq' : ∀ {α : Sort u_1} {β : α → Prop} {a1 a2 : {x // β x}}, a1.val = a2.val → a1 = a2

fgdorais commented 6 years ago

@spl Thanks for the reminder. This bug gave me some really unexpected errors so at least it's here for documentation purposes.

I didn't want to add mathlib as a dependency in my situation. An easy workaround is:

lemma subtype_eq {α : Sort*} {p : α → Prop} :
∀ {a1 a2 : subtype p}, a1.val = a2.val → a1 = a2
| ⟨x,h1⟩ ⟨.(x),h2⟩ rfl := rfl

The mathlib implementation is probably the same, but it comes with a lot of unnecessary baggage...

digama0 commented 6 years ago

If you have "baggage restrictions", another viable approach is to pluck individual theorems from mathlib and add them to your project. At least in this early section there will be very few dependencies.

leanprover / lean3