bounded quantifiers

Stream: general

[Sean Leather]

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]

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]

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

[Sean Leather]

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]

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]

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

[Sean Leather]

A b(ounded for)all. :soccer:

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

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]

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

[Sean Leather]

I actually like forall_mem for the reason you said.

[Sean Leather]

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]

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]

And a punched card computer that supports UTF-8?

[Mario Carneiro]

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

[Sean Leather]

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]

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

[Mario Carneiro]

If you kick vscode enough times it shows prefixes only

[Johan Commelin]

Fair enough, we can grep with word boundaries

[Sean Leather]

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]

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]

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

[Sean Leather]

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]

So you'd have all_iff_forall_mem and all_iff_forall_mem'.

[Sean Leather]

Or even all_iff_forall_bool and all_iff_forall_mem?

[Mario Carneiro]

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]

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]

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]

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]

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

[Sean Leather]

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]

That would be epic.

[Moses Schönfinkel]

Oh using the joy_cat is super clever.

[Johan Commelin]

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