What does it mean for a structure/class to be of type Prop?

Stream: new members

[Kevin Cheung]

The definition for LawfulFunctor is class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop. In both Theorem Proving in Lean 4 and Functional Programming in Lean, I haven't seen a class declaration with a : Prop. Trying to understand what this could mean, I cooked up the following:

structure Stuff : Prop where
  addProp : 1 + 1 = 2
  mulProp : 2 * 3 = 6

#check Stuff -- Stuff : Prop

structure Stuff' where
  addProp : 1 + 1 = 2
  mulProp : 2 * 3 = 6

#check Stuff' -- Stuff' : Type

def someStuff : Stuff := Stuff.mk rfl rfl
def someStuff' : Stuff' := Stuff'.mk rfl rfl

#check someStuff -- someStuff : Stuff
#check someStuff' -- someStuff' : Stuff'

From the info I gathered, I couldn't really figure out when one would want to define a structure or a class to be a Prop. Insights or pointers greatly appreciated.

[Kyle Miller]

If each field is a proof, then the structure is essentially a conjunction, and generally you want it to be a Prop. In the next release of Lean, this will be the default.

[Kevin Cheung]

So in the next release, Stuff' will be automatically a Prop?

[Kyle Miller]

Yes

[Kyle Miller]

Here's what it means that it's a Prop:

theorem Stuff_iff : Stuff ↔ 1 + 1 = 2 ∧ 2 * 3 = 6 := by
  constructor <;>
  · rintro ⟨ha, hm⟩
    exact ⟨ha, hm⟩

[Kyle Miller]

It "is" a conjunction, and you can use it wherever the conjunction would appear. It's nicer than a conjunction since each field has a nice name.

[Kyle Miller]

With Stuff', you can only use it as a proposition if you write something like Nonempty Stuff'

[Kevin Cheung]

Now I am a bit confused. What is someStuff then?

[Kevin Cheung]

someStuff is of type Stuff, but it itself is not a Prop.

[Kyle Miller]

someStuff is a proof of Stuff

[Kevin Cheung]

Does that mean someStuff is a proof of Stuff?

[Kevin Cheung]

Ok. Thanks.

[Kyle Miller]

By the way, since it's useful to be able to break up these named conjunctions inside proofs, mathlib has a @[mk_iff] attribute to automatically generate the iff theorem:

@[mk_iff]
structure Stuff : Prop where
  addProp : 1 + 1 = 2
  mulProp : 2 * 3 = 6

#check stuff_iff
/-
stuff_iff : Stuff ↔ 1 + 1 = 2 ∧ 2 * 3 = 6
-/

[Kevin Cheung]

Wow. This looks like something that needs to be added to the books.

[Kyle Miller]

I sort of wonder if Lean should automatically generate this theorem without being asked to

[Kevin Cheung]

I should write a blog article about this so I don't forget. Thank you very much for the help.

[Alex Mobius]

What's the benefit of generating the And theorem? Things like simp won't attempt to destructure it otherwise?

[Kyle Miller]

Yes, exactly. In particular, simp has no way of destructuring structures without such a theorem. If simp had this feature, it would need to contain an implementation of @[mk_iff].