Proof of non-instance

Stream: new members

[Julian Berman]

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]

You could prove inhabited empty → false

[Kevin Buzzard]

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

[Julian Berman]

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]

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

[Martin Dvořák]

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

[Mario Carneiro]

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

[Mario Carneiro]

src#not

[Mario Carneiro]

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]

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]

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]

Or simply is_empty A.

[Kevin Buzzard]

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