Zulip Chat Archive

Stream: general

Topic: bounded quantifiers


view this post on Zulip Sean Leather (Apr 26 2018 at 13:34):

I've seen these referred to in different places. I've inferred that a bounded forall is {α : Sort*} {p : α → Prop} : ∀ x, p x and a bounded exists is {α : Sort*} {p : α → Prop} : ∃ x, p x. In some places, they're called ball and bex. In mathlib/docs/naming.md (only, it appears), they are called bforall and bexists.

There is also notation ∀ x ∈ s, t that refers to a bounded forall and produces ∀ (x : α), x ∈ s → t. It works similarly for exists. In lean/tests/lean/run/cute_binders.lean, there is even this rather interesting code:

definition range (lower : nat) (upper : nat) : set nat :=
λ a, lower  a  a  upper

local notation `[` L `, ` U `]` := range L U

variables s : set nat
variables p : nat  nat  Prop

-- #check a ∈ s
set_option pp.binder_types true
#check  b c a  s, a + b + c > 0
-- ∀ (b c a : ℕ), b ∈ s → c ∈ s → a ∈ s → a + b + c > 0 : Prop
#check  a < 5, p a (a+1)
-- ∀ (a : ℕ), a < 5 → p a (a + 1) : Prop
#check  a b  [2, 3], p a b
-- ∀ (a b : ℕ), a ∈ [2, 3] → b ∈ [2, 3] → p a b

So, to my questions: Where is this bounded quantifier notation defined? Does it work wherever binders is found in notation? What are its limitations, e.g. w.r.t. the p : α → Prop or notation (, <, etc.) used?

view this post on Zulip Simon Hudon (Apr 26 2018 at 13:44):

I think as you suggest, it's baked into the binder notation. I'm actually unclear on what is accepted. I think it might accept any infix operator: ∀ x ⊕ unit, list x

view this post on Zulip Patrick Massot (Apr 26 2018 at 13:47):

OMG, I never understood all these "ball". I always thought: "What ball? There is no distance here, why is this called ball?"

view this post on Zulip Sean Leather (Apr 26 2018 at 13:50):

OMG, I never understood all these "ball". I always thought: "What ball? There is no distance here, why is this called ball?"

Part of the motivation for writing this up was also to help others who were as confused as I was. :simple_smile:

view this post on Zulip Patrick Massot (Apr 26 2018 at 13:53):

My only excuse is I was seeing this in contexts not too far away from actual balls, like https://github.com/leanprover/mathlib/blob/14a19bf3d2589a9801ef281808d8e4faa90db2b1/data/analysis/topology.lean#L88 which is about topological space but not metric spaces, hence maximising the confusion probability

view this post on Zulip Patrick Massot (Apr 26 2018 at 14:34):

Sean, what's that orange thing next to the small mathematician in your reaction?

view this post on Zulip Sean Leather (Apr 26 2018 at 14:50):

A b(ounded for)all. :soccer:

view this post on Zulip Johan Commelin (Apr 26 2018 at 16:49):

Sean, what's that orange thing next to the small mathematician in your reaction?

If you hover over the emoji with your mouse, a popup will explain what the emoji tries to communicate (-;

view this post on Zulip Sean Leather (Apr 30 2018 at 08:29):

As Mario pointed out to me, there are yet more names for bounded quantifiers: forall_mem and exists_mem. These are used in (at least) data/list/basic.lean, data/finset.lean, and data/multiset.lean.

view this post on Zulip Sean Leather (Apr 30 2018 at 08:31):

Arguably, forall_mem is more accurate than ball because it explicitly describes the mem bound of the quantification.

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:35):

There is a reasonable argument for ball_mem instead of forall_mem since it is a mem bound on a bounded forall, but that's like half overlapping names and a direct reading looks more like forall_mem

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:36):

Currently, ball and bex are only used to describe "generic" bounded forall (some predicate) in logic.basic

view this post on Zulip Sean Leather (Apr 30 2018 at 08:36):

I actually like forall_mem for the reason you said.

view this post on Zulip Sean Leather (Apr 30 2018 at 08:40):

The lack of forall in ball and exists in bex means that they don't show up in grep, which is unfortunate for those of us who rely on old-school tools. :wink:

view this post on Zulip Johan Commelin (Apr 30 2018 at 08:41):

those of us who rely on old-school tools. :wink:

Yes, I'm still looking for a Lean plugin for good old ed

view this post on Zulip Sean Leather (Apr 30 2018 at 08:43):

And a punched card computer that supports UTF-8?

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:45):

The obvious solution is to shorten forall and exists to all and ex :)

view this post on Zulip Sean Leather (Apr 30 2018 at 08:47):

The obvious solution is to shorten forall and exists to all and ex :smiley:

That would be totally canonically exactin the next contextual parallel universe that extends this one.

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:50):

There's no way I'm going to try and avoid subsequences

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:50):

If you kick vscode enough times it shows prefixes only

view this post on Zulip Johan Commelin (Apr 30 2018 at 08:51):

Fair enough, we can grep with word boundaries

view this post on Zulip Sean Leather (Apr 30 2018 at 08:58):

Tee hee, yet more names. forall_prop and exists_prop in data/list.lean:

theorem all_iff_forall_prop {p : α  Prop} [decidable_pred p] {l} : all l (λ a, p a)   a  l, p a

theorem any_iff_exists_prop {p : α  Prop} [decidable_pred p] {l} : any l (λ a, p a)   a  l, p a

which are actually used differently in logic/basic.lean:

theorem forall_prop_of_true {p : Prop} {q : p  Prop} (h : p) : ( h' : p, q h')  q h
theorem forall_prop_of_false {p : Prop} {q : p  Prop} (hn : ¬ p) : ( h' : p, q h')  true

theorem exists_prop {p q : Prop} : ( h : p, q)  p  q
theorem exists_prop_of_true {p : Prop} {q : p  Prop} (h : p) : ( h' : p, q h')  q h
theorem exists_prop_of_false {p : Prop} {q : p  Prop} : ¬ p  ¬ ( h' : p, q h')

view this post on Zulip Mario Carneiro (Apr 30 2018 at 09:14):

the prop in all_iff_forall_prop is only there for disambiguation, it could just be all_iff_forall' which is marginally less descriptive

view this post on Zulip Mario Carneiro (Apr 30 2018 at 09:15):

Maybe it should be called all_to_bool instead, since there is a hidden to_bool coercion there

view this post on Zulip Sean Leather (Apr 30 2018 at 09:18):

But then it seems that all_iff_forall should be called all_iff_forall_mem to be consistent with the other forall_mems.

view this post on Zulip Sean Leather (Apr 30 2018 at 09:18):

So you'd have all_iff_forall_mem and all_iff_forall_mem'.

view this post on Zulip Sean Leather (Apr 30 2018 at 09:19):

Or even all_iff_forall_bool and all_iff_forall_mem?

view this post on Zulip Mario Carneiro (Apr 30 2018 at 09:19):

true, although I reserve the right to start lopping off the right hand side of a theorem name if we all know where it's going

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 10:21):

The obvious solution is to shorten forall and exists to all and ex :)

Let me just make the passing comment that there was a time a few months ago when Mario stopped what he was doing and wrote a bunch of one-line docstrings covering many of the important concepts in mathlib, and after that I found that old-skool grepping suddenly became a lot more effective.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 10:22):

For example, I once wanted to know whether surjections were covered in Lean, and I grepped the Lean source code for "surjection" and got nothing at all.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 10:22):

then after the docstrings, I grepped again and I found the word in a docstring and then I looked at the correponding theorem and found my mistake -- it's "surjective" I should be looking for.

view this post on Zulip Kevin Buzzard (Apr 30 2018 at 10:23):

so a better solution is to put the keywords in the docs :-)

view this post on Zulip Sean Leather (Apr 30 2018 at 10:59):

so a better solution is to put the keywords in the docs :-)

Yes, that is useful in general. But a consistent naming scheme that allows one to consistently associate names with concepts is useful as documentation of the theorem itself as well as documentation within a proof using the theorem.

Using the surjective example, I wouldn't like to see one theorem's name use surjective while another used onto, even though the theorems are referring to the same thing.

view this post on Zulip Moses Schönfinkel (Apr 30 2018 at 11:08):

That would be epic.

view this post on Zulip Moses Schönfinkel (Apr 30 2018 at 11:11):

Oh using the joy_cat is super clever.

view this post on Zulip Johan Commelin (Apr 30 2018 at 11:13):

Cool, didn't know that one existed. Will make use of it (-;


Last updated: May 06 2021 at 21:09 UTC