Convention for ∀ vs. Π

Stream: mathlib4

[Junyan Xu]

In mathlib3 I recall the convention was to use Π for data and ∀ for proofs (i.e. ∀ i, p i if p : ι → Prop and Π i, T i if T : ι → Type*. However, mathport has translated all Π to ∀ so we only saw the latter in mathlib4 for a while, and people probably followed this convention. But lately, new PRs by e.g. @Andrew Yang have been systematically using e.g. Π i, A i (for a product of algebra in this case) but still keep using ∀ in [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)] even though these are also data. Personally this also feels natural to me, and I think the rationale is that since typeclass arguments is meant to supply something unique, it's intuitive for people to speak that "for each i there exists a (canonical) CommRing/Algebra structure". Or in other words, Since there's only one canonical inhabitant of the type, it's natural to treat it as a subsingleton and use ∀ since Props are also subsingletons. If people agree with this convention (use ∀ for proofs and typeclass arguments and Π otherwise), we should probably codify it and prepare a PR to make mathlib4 compliant. Thoughts?

cc @Yaël Dillies since you once commented "the ship has sailed".

[Michał Staromiejski]

I definitely agree that Π i, A i is more natural than ∀ i, A i if we want to say "indexed product". And for me it reads more naturally [∀ i, CommRing (A i)] (each A i comes with CommRing structure) than [Π i, CommRing (A i)]. Analogously to [CommRing A] [CommRing B] having more in common with "and" and not ×.

It seems that Mathlib4 is quite consistent with typeclass arguments, but there are places with ∀ i, A i...

[Andrew Yang]

I think the convention I am following myself is not "∀ for proofs and typeclass arguments and Π otherwise".

For example I would write (A B : ι → Type) (e : ∀ i, A i ≃ B i) : (Π i, A i) ≃ (Π i, B i) despite e being data, because on paper we would say "If $A_i$ is isomorphic to $B_i$ for all $i$, then $\prod_i A_i$ is isomorphic to $\prod_i B_i$", and not "if we have a product of isomorphisms" or "'$A$ for all $i$' is isomorphic to '$B$ for all $i$'"

[Junyan Xu]

That would seem a bit arbitrary to me. Maybe we should fall back to using Π everywhere for data?
Worth noting in HoTT literature you'll see Π even for proofs (but their Props are not subsingletons).
image.png

[Edward van de Meent]

that's nice for HoTT, but as i understand it lean is not HoTT based?

[Edward van de Meent]

personally, i'd be fine with only using ∀, even for what may be clearly data

[Michał Staromiejski]

I don't think it's data/not-data, I agree with @Andrew Yang that if it should read "for all i we have ..." we use ∀ and if it should read "product of all X i for i : I" then use Π. In type theory I think it means the same and has even more basic syntax: (i : I) → X i. I'm guessing it was just readability (for mathematicians) to introduce both Π and ∀.

BTW, for terms we have to use "the basic syntax" fun i => x i anyway...

[Kyle Miller]

Yeah, I was going to write that my recommendation is:

• Use ∀ i, p i for propositions
• Use (x : X) → A x for dependent functions
• Use Π i, A i for indexed products (note that this is mathlib-only notation)

Sometimes it's more convenient writing [∀ i, Algebra R (A i)] since (1) you sort of think of "A i is an algebra" as a proposition and (2) the alternative using vanilla Lean is [(i : _) → Algebra R (A i)], which has some extra symbols that make it harder to read.

[Kyle Miller]

Edward van de Meent said:

that's nice for HoTT, but as i understand it lean is not HoTT based?

That page is about basic dependent type theory; it doesn't matter that it came from the HoTT book :-)

[Kyle Miller]

We added Π i, A i notation to mathlib because Algebra R (Π i, A i) is a lot more friendly to a mathematical reader than Algebra R ((i : I) → A i) (or worse, Algebra R (∀ i, A i) — try explaining that one to someone just getting into Lean!)

[Junyan Xu]

What exactly is the distinction between bullet points 2 and 3? Can we implement the rule to convert existing mathlib automatically?

[Eric Wieser]

I think we could at least implement the rule to distinguish 1, and leave 2 vs 3 as a subjective stylistic decision

[Kyle Miller]

The distinction is how you think about it — somehow we all know that the product of algebras looks better with pi notation, but somehow also we all know that functions on Fin for example look better with dependent function notation.

[Kyle Miller]

(I don't have any concrete idea how to codify that difference.)

[Michał Staromiejski]

@Kyle Miller can you point to an example when vanilla-Lean syntax is used and would be preferred?

Anyway, I have an impression that most of us agree that it is about how we want to read.

[Kyle Miller]

Random example: would you rather read

(n m : Nat) → n = m → Fin n → Fin m

or

Π n m : Nat, n = m → Fin n → Fin m

The point of the vanilla Lean syntax is that it fits in perfectly well with plain arrow notation. You can make any of the arrows dependent by just giving one of the types a binder.

[Kyle Miller]

(Similarly, would you rather read Σ i : I, X i or (i : I) × X i? There are some cases where sigma might be more agreeable, but if you already know about products, dependent products are a small increase in complexity rather than an entirely new syntax.)

[Yaël Dillies]

Kyle Miller said:

Random example: would you rather read

(n m : Nat) → n = m → Fin n → Fin m

or

Π n m : Nat, n = m → Fin n → Fin m

Hot take: Second one, because if I remove the type ascriptions I get n → m → n = m → Fin n → Fin m and it is nonsense to write a function from a natural number.

[Kevin Buzzard]

I think I'd rather read ∀ n m : Nat, n = m → Fin n → Fin m!

[Yaël Dillies]

More seriously, I dislike this new syntax for dependent functions because (e : type) stands for e everywhere else in Lean (meaning we can type-ascript any expression e) but here instead (e : type) stands for type!

[Kyle Miller]

if h : p then ... else ... and for h : x in lst do ... are some counterexamples to that

[Yaël Dillies]

I am claiming that no, they are not. if (h : p) then ... else ... would be but I've never seen anyone write this so I don't even know whether it's valid syntax

[Kyle Miller]

Editing-wise, in my experience sometimes you have a non-dependent function type and you realize you actually want to later use one of the parameters in the middle in a dependent way. With the new notation, it's so easy to modify the type, but with the forall/pi notation you have to do a larger-scale transformation.

[Yaël Dillies]

That I agree, but dually it has happened to me that α → β doesn't quite mean what I want, so I do (α : myType) → β and suddenly get an obscure error. After a minute of staring at it, I finally think "Oh" and must do the larger scale transformation of writing ∀ _ : (α : myType), β

[Edward van de Meent]

do we need (a <: b) and (a :> b) notations?

[Edward van de Meent]

(btw, i think this is a core lean question/issue, not a mathlib one)

[Edward van de Meent]

or maybe do we want (_ : α : myType) to be a sensible notion in that case?

[Kyle Miller]

I think I'm missing something @Yaël Dillies. Is this an example involving a coercion? You could write ((α : myType)) → β at least.

That's admittedly a wart, this lack of compositionality with type ascriptions for coercion.

[Thomas Murrills]

Friction with : aside, I love (a : X) → … conceptually. These things are functions, so I think it makes sense to write them as functions; having a unified syntax to reflect a unified concept is a really appealing to me. (I might go a step further and claim that being confronted with this fact is sometimes good for mathematicians, even if we’re used to thinking of these things exclusively as products! :) )

[Thomas Murrills]

Once you start to see → as something which can bind, I think it’s not so big a shift in the end, and at least usually unambiguous. The only case where it’s ambiguous is when a is a type or can be coerced to one, so maybe it makes sense to warn the user of this ambiguity in those cases (possibly behind an option, like autoimplicits).

[Kyle Miller]

It seems possible to improve the error message in this case too

[Yaël Dillies]

Kyle Miller said:

I think I'm missing something @Yaël Dillies. Is this an example involving a coercion?

Yes, that has come up in the form of me wanting to write a function (s : Set α) → β where s : Finset α

[Notification Bot]

4 messages were moved from this topic to #mathlib4 > CoeSort for Finset by Kyle Miller.

[Violeta Hernández]

I agree with ∀ for propositions and Π for non-unique data. I prefer Π for all data, even if unique, but I'm willing to settle.

[Johan Commelin]

I'm in strong support of ∀ for props, and Π for indexed products, and letting the context/author/conventions influence the middle ground.

[Michał Staromiejski]

Following the discussion, I created a PR #21213 with changes in Algebra.Algebra.Pi. I basically did the following:

• make consistent usage of Π and ∀
• rename variables
• use section variables
• use Type* instead of explicit universe variables.

If this is what we all like, I could refactor other Pi files.

[Jon Eugster]

I think the first move after agreement should be a PR to the style guide and only start refactor PRs based on decisions written down in the style guide

[Michał Staromiejski]

The file required cleanup anyway. I posted in this topic because it is connected. But I agree, if we want the clear rules, let's write them down.

[Michał Staromiejski]

Also, I think the PR could serve as a material for any further discussion. After all, I don't think we'd write down the rules and refactor all the mathlib. Algebra.Algebra.Pi was the starting point of the discussion so it feels natural to try to clean it up.