When to use structure/inductive v. And/Or/Prod/Sum

Stream: general

[Ricardo Prado Cunha]

When defining a relatively simple type that is just the product or sum of other types, when should I use structure or inductive as opposed to just using And/Prod or Or/Sum? For more complicated types, it makes sense to use the former, but I see some inconsistency on simpler things like Iff (which uses structure) and Function.Bijective (which uses And).
Side note: would it be accurate to call types defined like Function.Bijective as "anonymous types"?

[Patrick Massot]

The nice thing with structure compared to And in this case is that you get to name the components.

[Ricardo Prado Cunha]

Yeah, that's another advantage. I'm asking this since I'm going to be teaching Lean to some students, and I want to get ahead of any "when should we use And v. defining our own structure" questions. I guess I'll just say that they should use non-anonymous types for things that show up often and anonymous types for quick things like Exists predicates.

[Ricardo Prado Cunha]

Also, Or for things that return a disjunction, though I'll make sure to tell them that in the case of arguments they should just stick to have them being separate arguments (for And) or separate theorems (for Or, unless the combinatorics start getting out of hand).

[Ricardo Prado Cunha]

Please let me know if anyone has different opinions on this. I'm also just debating letting them try them out and figure out what they like on their own.

[Kyle Miller]

I think it's usually better to use a structure for the reason Patrick mentions. Plus, if you use @[mk_iff] you get a rw lemma to transform between the two for free:

@[mk_iff]
structure MyProperty (n : ℕ) : Prop where
  a : n > 5
  b : ∃ k ≤ n, n ∣ 2 * k

#check myProperty_iff
/-
myProperty_iff (n : ℕ) : MyProperty n ↔ n > 5 ∧ ∃ k ≤ n, n ∣ 2 * k
-/

[Kyle Miller]

@[mk_iff] works for inductive too

[Eric Wieser]

As soon as you have three fields, using And twice and ending up with .1, .2.1, and .2.2 is much less appealing than defining your own thing and ending up with .p, .q, and .r

[Eric Wieser]

You can of course define theorem MyType.r (h : MyType) := p.2.2 etc though, so this isn't a major reason

[Kyle Miller]

In programming, there's a similar tension between setting up the boilerplate to make things nice with a structure/inductive, and just using Prod and Sum (which are direct analogues of And and Or).