Basic notation question

Stream: general

[Gihan Marasingha]

The proof of docs#summable_zero is has_sum_zero.summable. I'm unfamiliar with this use of the . notation. What does it mean? Is it discussed in TPIL?

[Eric Wieser]

The simple version is that f.bar when f : foo means foo.bar f.

[Eric Wieser]

The slightly more complex version is that f doesn't even need to be the first argument.

[Eric Wieser]

I think the range of things it supports has increased since TPIL was written

[Bryan Gin-ge Chen]

Generally, we refer to this as "dot notation"; you might find some more discussions in Zulip using that term.

Here's a hopefully helpful repost:
Bryan Gin-ge Chen said:

For more on dot notation see the end of 3.3.1 and 9.1 in TPiL. I think it finally clicked for me though after I read this thread.

[Gihan Marasingha]

Thanks @Eric Wieser and @Bryan Gin-ge Chen !

[Heather Macbeth]

By the way, a lot of the library is written to exploit this notation. For example, we have docs#differentiable.continuous, so that if you ever know (hf : differentiable ℝ f), then you can write hf.continuous for the fact that f is continuous.

[Heather Macbeth]

And we have docs#is_compact.bounded, so that if you ever know (hs : is_compact s), then you can write hs.bounded for the fact that s is bounded.

[Heather Macbeth]

And many many more :)

[Yaël Dillies]

I even recently defined has_subset.subset.finpartition_on to be able to write h.finpartition_on when h : A ⊆ B.

[Gihan Marasingha]

Thanks @Heather Macbeth!

[Yaël Dillies]

Very useful examples that I wish I knew before are le.trans, le.trans_lt, lt.trans, lt.trans_le

[Heather Macbeth]

Yaël Dillies said:

Very useful examples that I wish I knew before are le.trans, le.trans_lt, lt.trans, lt.trans_le

Yes, and docs#has_lt.lt.ne, docs#has_lt.lt.ne'.

[Yaël Dillies]

So instead of le_of_le_lt hle hlt, you can seamlessly write hle.trans_lt hlt and get a < result in the end. You also have the handy lt.le instead of le_of_lt and .antisymm which works at least for ≤ and ⊆.

[Yaël Dillies]

The biggest drawback in my opinion is that typeclass inference basically stops at the dot notation so, because many projections are overloaded (.antisymm, .trans, ...), the type of what you dot notate on has to be pretty clear for the notation to work.

[Gihan Marasingha]

OK, I think I get it now. Thanks for the explanations! I see that

set_option pp.generalized_field_notation false

desugars (is that a word?) this notation. So in the example @Yaël Dillies mentioned, we can do

import algebra.algebra.ordered

set_option pp.generalized_field_notation false

lemma bar (a b c : ℤ) (hle : a ≤ b) (hlt : b < c) : a < c := hle.trans_lt hlt

#print bar

and find that the proof of bar is

λ (a b c : ℤ) (hle : a ≤ b) (hlt : b < c), has_le.le.trans_lt hle hlt

The reason the dot notation works here is that hle : has_le.le a b and, coincidentally (not), there's a function called has_le.le.trans_lt which takes, as its first parameter, a term of type has_le.le x y. So hle.trans_lt is just applying the has_le.le.trans_lt function, but with hle as the first argument.

Rephrasing, this works because:

1. The name of the type of hle matches the first part of the name of a dotted-function (here has_le.le.trans_lt) and
2. The type of the first parameter of the function has_le.le.trans_lt matches the type of hle.

I hope that's correct!

[Yaël Dillies]

It's correct except that it works even slightly more generally! hle doen't have to be the first explicit parameter of the function. It has to be the first explicit parameter of type has_le.le of the function. So for example this would work:

import analysis.convex.topology

variables {α : Type*} [normed_group α] [normed_space ℝ α] {A : set α}

-- mathematically stupid
def convex.foo (hAcomp : is_compact A) (hAconv : convex A) : is_closed A := hAcomp.is_closed

variables (hAconv : convex A) (hAcomp : is_compact A)
#check hAconv.foo hAcomp -- convex.foo hAcomp hAconv : is_closed A
#check hAconv.foo -- I would have expected this to work
/- type mismatch at application
  convex.foo hAconv
term
  hAconv
has type
  convex A
but is expected to have type
  is_compact ?m_3-/

but surprisingly (to me) it doesn't like partial application.

[Eric Wieser]

I think dot notation will also unfold definitions sometimes too; if you have def my_nat := nat, then dot notation on terms of type mynat will first try the mynat namespace then the nat namespace. I can't check that right now though.

[Eric Wieser]

Maybe it has to be reducible