## Stream: new members

### Topic: Proof of non-instance

#### Julian Berman (Dec 21 2021 at 02:00):

Can I state that no instance of a type class can exist for a certain type? Say that there is no inhabited instance for empty? (My real example is proving that an empty type is not an additive group but if the answer is yes it's possible to express this I don't want the answer spoiled for how to do that one :)

#### Kevin Buzzard (Dec 21 2021 at 02:02):

You could prove inhabited empty → false

#### Kevin Buzzard (Dec 21 2021 at 02:02):

Or define it if it's a type, I don't know the rules :-)

#### Julian Berman (Dec 21 2021 at 02:04):

Aha, I tried that, but then I tricked myself and rewrote it as \not inhabited empty thinking that was equivalent (and got an error) -- but that's only the case for prop-valued things of course then?

#### Julian Berman (Dec 21 2021 at 02:05):

OK indeed that works with the implication, that was silly of me. Thanks.

#### Martin Dvořák (Dec 21 2021 at 09:06):

What does \not do here if it doesn't translate to → false as we thought?

#### Mario Carneiro (Dec 21 2021 at 09:09):

\not p does translate to p -> false, but it is only defined for p : Prop

src#not

#### Mario Carneiro (Dec 21 2021 at 09:11):

on the other hand, A -> false, being notation for a function from the type A to the type false, works for any type A : Sort u

#### Mario Carneiro (Dec 21 2021 at 09:12):

If we wanted to, we could generalize not to accept arbitrary types, but this would make it different from the other logical connectives which only work on Prop

#### Mario Carneiro (Dec 21 2021 at 09:13):

I believe there used to be a definition for A -> false, written ~A, in lean 2, but it's not so useful since A -> false or not (nonempty A) are simple enough equivalent expressions

#### Yaël Dillies (Dec 21 2021 at 09:42):

Or simply is_empty A.

#### Kevin Buzzard (Dec 21 2021 at 10:19):

I just remember that about a year ago we had a discussion about the simp normal form way to say the Prop that a type was empty, and IIRC maps to false won

Last updated: Dec 20 2023 at 11:08 UTC