def vs structure

Stream: new members

[Nicolò Cavalleri]

Is there a general rule of thumb to decide whether a property should be defined with def : Prop or as a structure/class : Prop?

[Kevin Buzzard]

Do you want the type class inference system to handle it or not?

[Nicolò Cavalleri]

Kevin Buzzard said:

Do you want the type class inference system to handle it or not?

Actually I imagined it for class but what about a structure : Prop? It is not handled by class inference (or is it)?

[Kevin Buzzard]

No, structures aren't handled by the type class inference system.

[Kevin Buzzard]

The difference between a structure and a def is just different syntax for the default constructor, basically

[Kevin Buzzard]

equivalence r is defined to be reflexive r \and symmetric r \and transitive r so you build an instance with \<refl_proof, symm_proof, trans_proof\>.

[Kevin Buzzard]

If they'd made it a structure then this would work, but so would {reflexive := refl_proof, symmetric := symm_proof, transitive := trans_proof}

[Nicolò Cavalleri]

And is there a particular reason why they did not want the second syntax to be possible?

[Nicolò Cavalleri]

Coercions work in both cases right?

[Patrick Massot]

There is a function emulating the structure behavior here. I guess it's a historical accident.

[Kevin Buzzard]

Coercions don't care if the things you're going from and to are structures or just defs.

[Nicolò Cavalleri]

Patrick Massot said:

There is a function emulating the structure behavior here. I guess it's a historical accident.

So if I like better the structure syntax because I like the clarity of the second constructor, I can choose to always use structure I guess

[Kevin Buzzard]

Of course you can define functions and pi types more generally with def; structures are limited to being inductive types with one constructor.

[Rob Lewis]

One (minor) reason to prefer the definition using and is uniformity for automation. Things may know how to deal with conjunctions but not with your custom structure. Here's a contrived example:

constants A B C : Prop
def f : Prop := A ∧ B ∧ C

structure g : Prop :=
(one : A) (two : B) (three : C)

example (h : f) : B := by simp [f, *] at * -- works
example (h : g) : B := by simp [g, *] at * -- fails

[Nicolò Cavalleri]

Ok cool these look to be good reasons, thanks to all!