prop false and type false

Stream: new members

[Huỳnh Trần Khanh]

it seems that the two are different right? this is making me really confused can anyone explain this stuff

[Huỳnh Trần Khanh]

from what i understand type false is a type that has no inhabitants and there is a function that maps an instance of an uninhabited type to any type on earth called false.elim

[Huỳnh Trần Khanh]

and the false prop is like a boolean value and that's it

[Huỳnh Trần Khanh]

but under that mental model there are things that feel incongruent

[Huỳnh Trần Khanh]

so I'm pretty sure my understanding is wrong somehow

[Kevin Buzzard]

Can you link to the terms you're talking about e.g. docs#false ? I only know of false : Prop, which is the false proposition. Sure you can call it a type, if you're happy to call Propositions types. If you're confused about the whole "propositions as types" thing then maybe you want to look at #tpil chapter 3 or my blog post about it.

[Adam Topaz]

By type false do you mean docs#pempty ?

[Huỳnh Trần Khanh]

I think now I know where my confusion stems from. The false type that I talk about is actually the proof of false type. There is the proof type and there is the prop type. And the two types are conflated to simplify the syntax. When I write def something : Prop := false, I'm telling Lean that there is something that is false. It doesn't constitute a proof of false, the word false here is only a truth value. However when I use exfalso for example and the goal turns into false, the word false here indicates that I have to show a term that has type Proof false, and the word Proof is elided because proof and prop are conflated.

From #tpil chapter 3:

This approach would provide us with a reasonable way of building assertions and proofs. Determining that an expression t is a correct proof of assertion p would then simply be a matter of checking that t has type Proof p.

Some simplifications are possible, however. To start with, we can avoid writing the term Proof repeatedly by conflating Proof p with p itself. In other words, whenever we have p : Prop, we can interpret p as a type, namely, the type of its proofs. We can then read t : p as the assertion that t is a proof of p.

[Eric Wieser]

I think your "there is the proof for and there is the prop type" model is not a good one. Try replacing false with nat in your above code snippets; the nat in 37 : nat and nat : Type are the same.

[Eric Wieser]

Just as the false in (sorry : false) and (false : Prop) are the same

[Mario Carneiro]

There are type theories that would require some transformation or coercion in order to treat a term as a type, so that the latter example would be sorry : T(false) and false : Prop where T is a constructor that makes types from terms representing types. This T, renamed to Proof, is what TPIL is talking about, but in lean there is no such coercion, the set of types is a literal subset of the set of terms so T is an identity