## Stream: general

### Topic: bounded quantifiers

#### 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?

#### 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

#### 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?"

#### 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:

#### 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

#### Patrick Massot (Apr 26 2018 at 14:34):

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

#### Sean Leather (Apr 26 2018 at 14:50):

A b(ounded for)all. :soccer:

#### 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 (-;

#### 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.

#### 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.

#### 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

#### 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

#### Sean Leather (Apr 30 2018 at 08:36):

I actually like forall_mem for the reason you said.

#### 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:

#### 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

#### Sean Leather (Apr 30 2018 at 08:43):

And a punched card computer that supports UTF-8?

#### Mario Carneiro (Apr 30 2018 at 08:45):

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

#### 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.

#### Mario Carneiro (Apr 30 2018 at 08:50):

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

#### Mario Carneiro (Apr 30 2018 at 08:50):

If you kick vscode enough times it shows prefixes only

#### Johan Commelin (Apr 30 2018 at 08:51):

Fair enough, we can grep with word boundaries

#### 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')


#### 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

#### 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

#### 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.

#### Sean Leather (Apr 30 2018 at 09:18):

So you'd have all_iff_forall_mem and all_iff_forall_mem'.

#### Sean Leather (Apr 30 2018 at 09:19):

Or even all_iff_forall_bool and all_iff_forall_mem?

#### 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

#### 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.

#### 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.

#### 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.

#### Kevin Buzzard (Apr 30 2018 at 10:23):

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

#### 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.

#### Moses Schönfinkel (Apr 30 2018 at 11:08):

That would be epic.

#### Moses Schönfinkel (Apr 30 2018 at 11:11):

Oh using the joy_cat is super clever.

#### 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