What do propositional types do for us?

Stream: new members

[Nick Attkiss]

Consider the following definition for a monoid homomorphism:

structure isMonoidHom [Monoid G] [Monoid H] (f : G → H) : Prop where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

I understand that the tag : Prop marks the definition as a proposition rather than a general type, which is apparently useful. What's an example of work I can do with isMonoidHom that wouldn't be possible if I removed : Prop from the structure definition?

Additional question: Why does this definition work even without {G H : Type*} as a first argument?

[Edward van de Meent]

1: make DecidablePred isMonoidHom typecheck.
2: because of an option called autoImplicit, which automatically adds such assumptions for symbols that arent in scope yet. this is disabled by default in mathlib, however.

[Ruben Van de Velde]

(deleted)

[Nick Attkiss]

@Edward van de Meent Can you elaborate more on your answer to (1)? I was imagining something like a proof example that uses isMonoidHom and fails if isMonoidHom is not a propositional type.

[Edward van de Meent]

i have to admit, my answer was a bit of a cop-out. i think in most cases the proofs should be managable. i do think that it should make equality proofs and the like rather easier. if you didn't know, in lean types which themselves have type Prop have at most 1 element. because of this, lean can do some optimisation in what to store for elements of such types.

[Edward van de Meent]

i think you could prove that isMonoidHom f is a so-called subsingleton type, and all relevant theorems should probably still work, however it's a lot easier to just let lean figure that out, and still reap the profits.

[Edward van de Meent]

i seem to recall that for other statements (such as a = b), them being Prop is crucial, as there are models (e.g. HOTT) where two proofs of such a statement (or elements of such types) are not definitionally equal.

[Nick Attkiss]

Makes a bit of sense; I'm vaguely familiar with propositions being singleton types. My issue is that I don't yet see what profits are to be reaped. Consider the following, for example:

structure isMonoidHom₁ {G H : Type*} [Monoid G] [Monoid H] (f : G → H) : Prop where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

structure isMonoidHom₂ {G H : Type*} [Monoid G] [Monoid H] (f : G → H) where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

example {G : Type*} [Monoid G] : isMonoidHom₁ (id : G → G) :=
  ⟨rfl, by simp⟩

example {G : Type*} [Monoid G] : isMonoidHom₂ (id : G → G) :=
  ⟨rfl, by simp⟩

Here only isMonoidHom₁ is marked as a propositional type, but the proof at the bottom works equally well for both definitions. I expected the second example to fail since isMonoidHom₂ (id : G → G) is not a proposition. So I haven't yet witnessed a situation where it actually helps to specify the structure as a propositional type. Can I appreciate any of the benefits of propositional types as a Lean beginner, or are they more subtle?

[Edward van de Meent]

i'd say the benefits are mostly things you don't think about, or things which you expect to be the case without thinking.

[Edward van de Meent]

someone else might be able to give a convincing example though?

[Nick Attkiss]

I'm satisfied with that, thanks!

[Edward van de Meent]

for what it's worth, there are proof assistants which manage without. (for example i believe Agda is one of those)

[Eric Wieser]

As another datapoint, mathlib frequently accidentally made such structures : Type rather than : Prop, and usually this went un-noticed for a long time. Probably the most obvious way to notice is IsMonoidHom f ↔ _ doesn't typecheck if IsMonoidHom _ : Type

[Robert Maxton]

The big difference between Prop and Type u is that Prop has propext, and so Lean can treat all instances of that type the same. This mostly comes up when dealing with dependent types. As an example of the opposite behavior making trouble for you, consider Fin n, where n is a Nat and thus data. Lean is significantly more limited in how much simplification it can do with data at the type level; if I have a Fin n and a Fin n - 1 + 1, these are definitionally different types to the compiler, and a "proof" that they are the same actually resolves into a type cast between the two, plus an assurance that this will always work out. Sometimes, this isn't enough to prove the thing you want; always, it tends to make life (and automation) difficult.

[Robert Maxton]

(This specific example came up recently for me, as a side note)

[Robert Maxton]

Putting a Prop into that sort of position can make things easier -- I believe Foo h1 and Foo h2 for h1 h2 : p, p : Prop are still different types, but it's now an extremely standardized and simple case where you can make a bunch of API for the exact same specific use case and your life is much easier doing it.

[Daniel Weber]

No, they aren't, as proof irrelevance is definitional:

import Mathlib.Tactic

irreducible_def P : Prop := True
opaque h₁ : P := (Iff.of_eq P_def).mpr True.intro
opaque h₂ : P := cast P_def.symm True.intro

opaque f : P → Type

example : f h₁ = f h₂ := rfl

[Nicolas Rolland]

Nick Attkiss said:

So I haven't yet witnessed a situation where it actually helps to specify the structure as a propositional type. Can I appreciate any of the benefits of propositional types as a Lean beginner, or are they more subtle?

I think it's linked to the difference between a property and type of its proofs.
If you trust the system, it might tell you that some property holds, without telling you how.
You can imagine I have a proof, and I dont want to show it to you, but I show it to Lean, who can thus broker that information (I would actually love that ability). Of course this proof that is being handed to you has no "computational content" to begin with.

To give an example I just saw in Small Scale Reflection for the Working Lean User where they use the property Even on Nat , which gets translated to the type "even : Nat -> Prop"

If we had a "categorical" type system, with a category of proposition E on top of B, a category of types, we would have Even \in E sitting on top of Nat \in B. And we could reflect a property of E into B in a precise way (this is called a comprehension), just like we transport a presheaf to its category of elements

in E             Even
                  -- 
                 |  |
in B             Nat -------> Bool 
               /              / true
             \int Even -----> 1

In their example the "category of elements" of Even, \int Even, is an inductive type even : Nat -> Prop with the obvious two constructors. They focus on the unique morphism Nat -> Bool, to show that its' useful to go back and forth, but that's beside the point.

The bottom line is that intuitively, if it has Prop in it, it comes from the logical system above, you can't inspect it, and can't use it except to produce other prop, and ultimately give them back to the logical system. I see the presence of Prop as being really about this 2 level system, one of which, E, we can't manipulate through terms.

Concretely, it means we get propext {a b : Prop} : (a ↔ b) → a = b.
We get the strongest thing in the book, defeq, because a and b are Prop.

[Robert Maxton]

Daniel Weber said:

No, they aren't, as proof irrelevance is definitional:

import Mathlib.Tactic

irreducible_def P : Prop := True
opaque h₁ : P := (Iff.of_eq P_def).mpr True.intro
opaque h₂ : P := cast P_def.symm True.intro

opaque f : P → Type

example : f h₁ = f h₂ := rfl

Huh. Okay, good to know. And yeah, in that case all the more so, using Props when possible will greatly simplify your life working with dependent types.