Stream: new members

Topic: def vs structure

Nicolò Cavalleri (Jul 08 2020 at 14:20):

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 (Jul 08 2020 at 14:22):

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

Nicolò Cavalleri (Jul 08 2020 at 14:23):

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 (Jul 08 2020 at 14:24):

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

Kevin Buzzard (Jul 08 2020 at 14:24):

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

Kevin Buzzard (Jul 08 2020 at 14:25):

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 (Jul 08 2020 at 14:26):

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 (Jul 08 2020 at 14:31):

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

Nicolò Cavalleri (Jul 08 2020 at 14:31):

Coercions work in both cases right?

Patrick Massot (Jul 08 2020 at 14:32):

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

Kevin Buzzard (Jul 08 2020 at 14:32):

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

Nicolò Cavalleri (Jul 08 2020 at 14:34):

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 (Jul 08 2020 at 14:36):

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 (Jul 08 2020 at 14:49):

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 (Jul 08 2020 at 15:11):

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

Last updated: May 14 2021 at 23:14 UTC