fun with syntax ambiguity

Stream: lean4

[Mario Carneiro]

I don't know if we can/should do anything about this, but it's amusing to me to see how type ascription, implication and the new "dependent implication" syntax interact:

#check Nat → Prop -- Nat → Prop : Type
#check (Nat : Type) → Prop -- Type → Prop : Type 1
#check (Int : Type) → Prop -- Type → Prop : Type 1
#check (Prop : Type) → Prop -- Prop → Prop : Type
#check ((Nat : Type)) → Prop -- Nat → Prop : Type

[Sebastian Ullrich]

Looks perfectly reasonable to me :big_smile:

[Mario Carneiro]

also:

#check (id Nat : Type) → Prop -- Type → Type → Prop : Type 1
#check ((id Nat) : Type) → Prop -- id Nat → Prop : Type

[Leonardo de Moura]

@Mario Carneiro I don't see any surprises above. Note that Prop is not an identifier, but a keyword.

Disclaimer: the "dependent implication" notation is off-limits, I love it and we use it all the time :)

We could try to change the type ascription notation. David Christiansen told me they use the <type> <expr> in Idris, where the is just our id where the type is an explicit argument. I think Agda uses <type> ∋ <expr>, but this is probably not a good match for mathlib :)

[Mario Carneiro]

I think I'll get along just fine with the new notation; with the lack of initial symbol it's a little bit of a garden path notation but I don't think it's too big of a deal. I don't know whether we should learn to love this notation or find a way to change it to ∀ for actual for-all statements in mathematics like ∀ x : Nat, ∃ p : Prime, p > x though.

[Mario Carneiro]

currently that pretty prints as (x : Nat) → Exists fun (p : Prime) => p > x : Prop btw, so I'm sure we'll be adding delaborator extensions in the mathlib prelude for this

[Leonardo de Moura]

We can add a flag for pretty-printing "dependent implication" using ∀.
The delaborator for Exists and Subtype are missing right now, but they will be added soon.

[Mario Carneiro]

In lean 3, there was an automatic switch between \forall and \Pi depending on the universe. Would something like that be acceptable here, where the prop version is \forall (x : A), B x and the type version is (x : A) -> B x?

[Leonardo de Moura]

Mario Carneiro: In lean 3, there was an automatic switch between \forall and \Pi depending on the universe. Would something like that be acceptable here, where the prop version is \forall (x : A), B x and the type version is (x : A) -> B x?

Yes, this is reasonable.

[Eric Wieser]

The docs claim the old sigma notation is still legal

[Mario Carneiro]

the example ∀ x : Nat, ∃ p : Prime, p > x parses in lean 4 today, so it looks like that has not changed

[Mario Carneiro]

it's just the pretty printing that is not supported yet

[Mario Carneiro]

However Sigma's notation has also changed, to (x : A) × B x (which makes good sense to me)

[Mario Carneiro]

PSigma, Subtype and Exists all have no pretty printing notation, but {x // p x} and ∃ x, p x work as parser input. (PSigma doesn't have any parser notation, although I'm not particularly fussed about losing Σ'. We could do (x : A) ×' B x if we want something similar)

[Nasos Evangelou-Oost]

is mathlib compatible with lean4?

[Huỳnh Trần Khanh]

Not yet but it will eventually. Also this is offtopic for this thread. Create a new one.

[Huỳnh Trần Khanh]

@Nasos Evangelou-Oost tag to get your attention

[Eric Wieser]

Eric Wieser said:

Only tangentially related to this thread, but if commas are no longer used to introduce binders in functions, is the intent to also avoid them in unions/sums/existential notation, all of which are syntactic sugar for a function?

Taking docs#tsum as an example, it seems odd to require => in tsum $ λ i => f i yet use a comma in ∑' i, f i (c.f. lean 3's tsum $ λ i, f i, where ∑' can be read as a shorthand for tsum $ λ). We could make these consistent by making the lean4 notation for tsum ∑' i => f i, but I suspect that would be unpopular.