question about bool vs Prop

Stream: new members

[Eric Taucher]

Doing Theorem Proving in Lean section 2.1 Simple Type Theory
For
#check b1 || b2 result: b1 || b2 : bool

Then using Mathlib naming conventions
saw that \or could be used

However for
#check b1 ∨ b2 result: ↥b1 ∨ ↥b2 : Prop

Can someone explain the difference? Thanks.

[Johan Commelin]

@Eric Taucher Do you understand the difference between bool and Prop?

[Eric Taucher]

Johan Commelin said:

Eric Taucher Do you understand the difference between bool and Prop?

Thanks.
If you mean do I understand they are different types then yes.

My path to Lean is via years of programming and not as a mathematician, so my thinking is that I have two bool types and that the only operators for bool types are the standard ones like and, or, etc. But here the \or is not like those operators so my guess is, a function, that takes in two bool types and returns a prop type. Also, what does the upward pointing errors before b1 and b2 mean?

[Yaël Dillies]

A bool is either tt or ff. A Prop can be many things, but classically it is either equivalent to true or equivalent to false.

[Patrick Johnson]

bool is an inductive datatype. bool.rec is computable. Prop is equivalent to Sort 0. Prop is not an inductive datatype. Classical Prop has exactly two distinct members: true and false. Decidable Prop is equivalent to bool (there is a bijection between bool and Prop). Doing cases on a Prop is noncomputable.

Logical connectives ∧ ∨ ¬ are all inductive datatypes.

[Yaël Dillies]

The names of the bool operations are band, bor, bnot, list.all, list.any as opposed to and, or, not, forall, exists.

[Yaël Dillies]

You can think of bool as a very computable Prop.

[Eric Taucher]

Thanks for the replies. I don't fully understand them but do have an idea of where they are leading, so will take some time by reading further keeping what has been noted and see if it comes out making sense. Also thanks for the key words to keep in mind. :smile:

[Yaël Dillies]

The upward pointing arrow is a coercion, and in that case it's a coercion to Sort, where the said Sort is Sort 0, aka Prop.

[Marcus Rossel]

@Eric Taucher It should all make sense once you've read chapter 3.

[Huỳnh Trần Khanh]

Eric Taucher said:

Thanks for the replies. I don't fully understand them but do have an idea of where they are leading, so will take some time by reading further keeping what has been noted and see if it comes out making sense. Also thanks for the key words to keep in mind. :smile:

you need a (vague) understanding of universes. #new members > prop false and type false is a thread I made a while ago on this topic, I hope you can learn something from the replies there

[Yaël Dillies]

I don't think this is very related. You would better look at docs#decidable, although I must say it's quite opaque to an untrained eye.

[Huỳnh Trần Khanh]

sure, the question is different but I asked the question precisely because I wanted to know why on earth there is a bool type and a prop type, and the answers to that question led me to understand why

[Yaël Dillies]

Ah sure

[Kevin Buzzard]

@Eric Taucher Every expression in Lean lives in one of three "levels" -- it's either a universe, a type-which-is-not-a-universe, or a term-which-is-not-a-type. For simplicity, let me just call them universes, types and terms. Examples: Type is a universe, bool is a type (in universe Type), tt is a term (of type bool). Prop is a universe, 2+2=4 is a type (in universe Prop), and a proof of 2+2=4 is a term (of type 2+2=4). Both bool and Prop express the "same kind of idea", however they are at different levels in this hierarchy. There are types true and false(in universe Prop), but these are types, not terms. || is a function which takes two terms, ∨ is a function which takes two types. The weird up-arrow you're seeing is a coercion which lifts terms of type bool to types in universe Prop, it sends tt to true and ff to false. The two concepts have to be distinguished in Lean because they are different levels in the universe/type/term hierarchy.

[Kevin Buzzard]

The reason we have Prop as well as bool is that Prop is crucial to mathematics, or more generally crucial for reasoning. I write more about this point of view here but you might not find this helpful because it might be too math-focused. Hopefully I cover the main points above though.

[Eric Taucher]

@Kevin Buzzard Your blog Mathematics in type theory Is really useful for a programmer with a Computer Science BS degree and knowledge of functional programming coming to Lean. It connects more dots than I knew needed connecting. :smile:

[Kyle Miller]

De Bruijn used the word "degrees" for the three "levels" that Kevin is talking about. I'm not sure anyone still uses that terminology, but I think it's nice because Lean also has a system of universe levels, which is orthogonal to the universe/type/term system.

image.png

A somewhat confusing (but useful) thing that Lean does is to declare that each universe is also a type of the universe the next level up, which is why Kevin had to say the contortions "type-which-is-not-a-universe" and "term-which-is-not-a-type".

[Eric Taucher]

Thanks. Now trivial enters the picture so more to think about. :smile:

[Eric Taucher]

@Kyle Miller Can you give a reference paper for degrees. In searching I am not finding anything right away. Thanks. :smile:

[Kyle Miller]

I saw it in some of the papers from this book https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/133/suppl/C (De Bruijn used the word "degree" for the Automath system)

[Eric Taucher]

@Kyle Miller This looks like the paper or at least notes degree in the same manner. could you confirm. :smile:
Some Extensions of Automath : The Aut-4 Family
The usage of the word degree is right in the first paragraph.

[Eric Taucher]

Is there anyone here who uses "Types and Programming Languages" by Benjamin C. Pierce (WorldCat) as a reference. If so then in the book, Chapter 29 Type Operators and Kinding on page 442 it notes

The expressions of our language are now dividend into three separate classes: terms, types and kinds.
Is this the same as Lean but just using Kind for Universe?

[Kyle Miller]

Yes, in all the papers I looked at they seemed to use degree in the same way (automath to lean translation: 1=universe, 2=type, 3=term).

That paper, however, seems to have an exception to this in its description of AUT-4. To preserve a property called "type reduction" when there are universal quantifications, they make Prop be degree 2, individual propositions be degree 3, and proofs be a new degree 4. They justify this, saying that it's a natural way to incorporate "irrelevance of proofs" by having it occur only for things of degree 4. With this system, Prop and bool would be of the same degree.

[Kyle Miller]

As far as I understand, universes and kinds are basically the same thing, but experts probably see some sort of distinction (type universes might be more restrictive than the concept of kinds, I'm not sure).

[Horatiu Cheval]

I don't know if this is right, but after skimming through that chapter it may be worth noting that Lean's universes are somewhat more stratified than what you find in Benjamin Pierce's book, in that universes form a hierarchy. So that we don't just have one atomic kind called * from which you can build other "higher-kinded types" (if that's the right name) like * -> *, but we have an infinite hierarchy Type 0 : Type 1 : Type 2 : ... and so on. So things like Type 0 -> Type 1 or Type 2 -> Type 0 are different types, instead of just being * -> *.

[Horatiu Cheval]

And in Lean it's not really the case that the expressions are divided into those classes. Rather, everything is one class, everything is a term. It's just that some terms are allowed to appear on the right of the : in a typing judgement, and those terms are said to be types (or at least that's my mental picture of it).

[Eric Taucher]

Thanks for the replies.
Does Lean have formal type rules?
My curiosity is up and want to compare them to the books.

[Horatiu Cheval]

You can find them in Mario's thesis: https://github.com/digama0/lean-type-theory/releases