Boolean equality vs Prop equality

Stream: lean4

[Jesse Slater]

What is the difference between single = and double ==? I understand that = has type prop, and == has type bool, but I don't really understand what the consequences of that are. Also, is there a boolean equivalent of >= and <=?

[Henrik Böving]

Really you are asking for the difference between Bool and Prop here. The difference is the following: Bool is the computer science true or false value, Prop is the mathematical idea of a property, while a property can also be both false or true there is a third way, we simply don't know what is the case (for example with open mathematical problems). If we have a certain property hyp : Prop Lean denotes the idea that we have a proof that hyp is either false or true by: proof : hyp or proof : ¬ hyp, the idea here being that hyp is a type and proofs of hyp are values of that type.

So if we write a = b this denotes the property that a is equal to b, this can be true, false or we don't know whether it is true or false. Now if we have a procedure to decide whether a = b such as for example with a b : Nat we can of course always know whether a is equal to b for any concrete values of a and b. This is where Lean's docs4#Decidable typeclass kicks in. If we have a function to decide a property, that is given hyp : Prop can return true iff we know there is an element proof : hyp or false iff we know there is an element proof : ¬ hyp we can declare an instance of Decidable that then allows us to write code such as if a = b then sorry else sorry(the if then else notation is mostly a wrapper around the Decidable typeclass that is looking for some way to decide the value after if based on a Decidable instance) because the program now has a function to determine whether that property holds or does not.

Now in the special case of the Decidable instance for n = m where n m : Nat something interesting is done. The instance is docs4#instDecidableEqNat docs4#DecidableEq is just an alias for a certain kind of Decidable things (namely equality on values) the function it uses is: docs4#Nat.decEq now as you can see this actually uses the docs4#Nat.beq function (docs4#BEq being the typeclass for the == notation).

So in the special case of Nat and many other types there is actually no difference between = and == at all since their docs4#DecidableEq instance is merely a verified version of their docs4#BEq instance, thus usually you can convert back and forth between h : (a == b) = true and h : a = b. There are however exceptions to this and by defining your own weird BEq instance it is of course easy to come up with them yourself.

To wrap it up, generally speaking a = b means "mathematically equal" and a == b means "computer science equal" with both meaning the same in the vast majority of cases.

Regarding the LE and LT operations what you want to do in this case is also to just use the decidable instances, for example docs4#Nat.decLe. Since if then else is just a wrapper around these we end up being able to just write if a <= b then sorry else sorry in most cases. If you are writing a generic function over some general implementation of docs4#LE you will have to accompany it with the appropriate instance parameter that your LE instance is decidable

[Kevin Buzzard]

Bool is a type but Prop is a universe, so they can do different things.

[Jesse Slater]

Thanks for the thorough response!

[Andrés Goens]

Henrik Böving said:

Prop is the mathematical idea of a property, while a property can also be both false or true there is a third way, we simply don't know what is the case (for example with open mathematical problems). If we have a certain property hyp : Prop Lean denotes the idea that we have a proof that hyp is either false or true by: proof : hyp or proof : ¬ hyp, the idea here being that hyp is a type and proofs of hyp are values of that type.

oh, curious, I always thought Prop stood for "proposition" :sweat_smile:

[Yaël Dillies]

It does. A "property"/"predicate" would rather be p : α → Prop for some α : Type _