Zulip Chat Archive

Stream: new members

Topic: prop false and type false


view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 00:02):

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

view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

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

view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

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

view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

but under that mental model there are things that feel incongruent

view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 00:06):

so I'm pretty sure my understanding is wrong somehow

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 00:22):

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.

view this post on Zulip Adam Topaz (Mar 01 2021 at 00:53):

By type false do you mean docs#pempty ?

view this post on Zulip Huỳnh Trần Khanh (Mar 01 2021 at 05:52):

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.

view this post on Zulip Eric Wieser (Mar 01 2021 at 06:41):

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.

view this post on Zulip Eric Wieser (Mar 01 2021 at 06:42):

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

view this post on Zulip Mario Carneiro (Mar 01 2021 at 08:35):

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


Last updated: May 10 2021 at 00:31 UTC