sup and inf over sets

Stream: mathlib4

[David Loeffler]

Why are the notations ⨅ x ∈ s, f x and ⨆ x ∈ s, f x, for s a subset of the domain of f, defined the way they are?

I was expecting that ⨅ x ∈ s, f x was just a more compact way of writing ⨅ x : ↑s, f ↑x, i.e. the iInf over s coerced to a type. But it's really not the same!

Mathlib's definition seems to be that ⨅ x ∈ s, f s expands to a nested infimum, ⨅ x, ⨅ (_ : x ∈ s), f s, with the inner infimum over the type of proofs of x ∈ s. But if x isn't in s, then ⨅ (_ : x ∈ s), f s is the infimum of the empty set. If the target of f doesn't have a top element, then this is a meaningless question and so the return value is junk. But then the outer infimum is ⨅ x, if x ∈ s then f s else JUNK, and if s isn't the whole domain and the junk value happens to be strictly smaller than anything in f '' s, then we get nonsense.

For example, one can prove that ⨅ x ∈ ({1} : Set ℝ), x = 0. I find this rather disturbing!

What is the reasoning behind this decision about how to interpret ⨅ x ∈ s, f x? Why is it not defined to be inf / sup over the subtype defined by s?

[Violeta Hernández]

Perhaps the idea is you should be using sInf instead? Either way, this feels like a clear oversight, or at least a weird design decision without proper documentation.

[Violeta Hernández]

@Yaël Dillies

[Yaël Dillies]

That's a design decision predating me

[Yaël Dillies]

but the rationale is that you can actually put any predicate in that notation, and it does the same as what a forall would do

[Yaël Dillies]

David Loeffler said:

What is the reasoning behind this decision about how to interpret ⨅ x ∈ s, f x? Why is it not defined to be inf / sup over the subtype defined by s?

Also note that you then need to precompose f with Subtype.val

[Yaël Dillies]

Anyway, it's not impossible to change the notation but it would need to be clearly motivated and it will have fallout: eg lemmas about nested suprema/infima currently apply to \Sup x \in s, f x. With your proposal, they wouldn't anymore

[David Loeffler]

Yaël Dillies said:

but the rationale is that you can actually put any predicate in that notation, and it does the same as what a forall would do

I don't think so; it seems to be specific to predicates of the form x ∈ s, if I understand the code for iSup_delab in Mathlib.Order.SetNotation correctly.

[Yury G. Kudryashov]

You should read the notation to see how Lean elaborates the notation. Delaborator may be a partial inverse.

[Eric Wieser]

A more general situation is

variable (s : Set ℕ)
#check ⨆ (i : ℕ) (h : i ∈ s), {Subtype.mk i h}
#check ⨆ (i : ℕ) (j : ℕ) (hij : i < j), {(i, j)}

[Eric Wieser]

⨆ i ∈ s, is just a shorthand for ⨆ (i : ℕ) (_ : i ∈ s),

[David Loeffler]

@Eric Wieser I am not sure what point you are making with that comment. In what sense is that a more general situation? (Note that your code produces an unevaluated metavariable and a linter warning.)

[Johan Commelin]

@David Loeffler Thanks for flagging this. I agree that this is a footgun. If we can remove it that would be great. Atm I can't see through the ramifications of switching to quantifying over the subtype. Would that break a lot of mathlib? Would working with it become awkward? Or can we get a smooth API for it?

[Eric Wieser]

A downside of working with subtypes is that it becomes much more complex to exchange two binders; instead of rewriting by iSup_comm, you have to build the equiv

[David Loeffler]

@Eric Wieser Can you be more specific about the kind of "exchanging two binders" you have in mind? The cases I'm asking about are where the "inner" iInf / iSup is over proofs of a proposition which depends on the index variable of the "outer" iInf / iSup, so clearly it's not meaningful to exchange them anyway. Are you thinking of cases where we have multiple index variables (or multiple predicates), so we really have 3 or more binders?

[Eric Wieser]

Yes, precisely

[David Loeffler]

If you have two predicates involved, we'd just be rewriting {x // p x \and q x} to {x // q x \and p x} using Or.comm`, wouldn't we?

[Johan Commelin]

I think we'd get a nested subtype if we aren't careful

[Eric Wieser]

The rewrite won't work if anything inside the binder uses x.prop.1 and x.prop.2, which need to be exchanged

[Eric Wieser]

Note that even

example : {n : ℕ // 0 < n ∧ n < 10} := by
  simp_rw [and_comm] -- fails

does not work

[David Loeffler]

@Eric Wieser yet again I am unsure what you expect your example to demonstrate. Note that

example : {n : ℕ // 0 < n ∧ n < 10} = {n : ℕ // n < 10 ∧ 0 < n} := by
  simp_rw [and_comm] -- works

works fine.

[Eric Wieser]

That's not a particularly good example, since it involves equality of types. Here's a more realistic one:

import Mathlib

example :
    ⨆ i : {n : ℕ // 0 < n ∧ n < 10}, (i : ℕ) =
      ⨆ i : {n : ℕ // n < 10 ∧ 0 < n}, (i : ℕ) := by
  simp_rw [and_comm] -- fails

example :
    ⨆ (n : ℕ) (h : 0 < n ∧ n < 10), n =
      ⨆ (n : ℕ) (h : n < 10 ∧ 0 < n), n := by
  simp_rw [and_comm] -- works

[David Loeffler]

Yes, your last example works; but it is proving 0 = 0, when I am pretty sure that most mathematicians would agree that the infimum of the set {x : ℕ | 0 < x < 10} should be 1:

example : (⨅ (n : ℕ) (_ : 0 < n ∧ n < 10), n) = 0 := by
  rw [← Nat.le_zero_eq]
  apply ciInf_le_of_le' 0
  simp only [lt_self_iff_false, Nat.ofNat_pos, and_true, Nat.iInf_of_empty, le_refl]

I am not sure that it is a strong argument for the status quo that we can easily prove that one highly misleading junk answer is equal to another equally bad one.

[Eric Wieser]

Edited, I meant to use iSup

[Eric Wieser]

I don't disagree that there is a footgun here

[Johan Commelin]

Basically the current elaborator for \inf x, x \in s never gives a useful answer, unless \bot \in s, right?

[Eric Wieser]

I don't think s is relevant to whether it's useful

[Johan Commelin]

It's better to have a correct definition that is hard to work with than a bad definition that is easy to manipulate

[Eric Wieser]

That argument would lead to defining a / b : Option K instead of a / b : K in fields

[Eric Wieser]

Which is to say, there's a gray area of compromises

[David Loeffler]

Johan Commelin said:

Basically the current elaborator for \inf x, x \in s never gives a useful answer, unless \bot \in s, right?

The issue isn't about the set s, it's about the type in which the function takes values. For f : X → Y, our def of ⨅ x ∈ s, f x is almost always the wrong answer unless Y has a bottom element (and dually for ⨆ and top elements).

[David Loeffler]

(I suspect that the authors of the code mostly had in mind the cases of Y being either Set α for some α, or ENNReal.)

[Floris van Doorn]

To be more concrete:

⨅ x ∈ Icc (2 : ℝ) (3 : ℝ), x = 0 -- because of junk values for `x` outside the interval
⨅ x : Icc (2 : ℝ) (3 : ℝ), (x : ℝ) = 2

I agree this is a footfun, and I would be happy to change the way that ⨅ x ∈ s elaborates. This notation is from Lean 3, where "duplicate the binder" was basically the only thing we can do.
Though Eric raises a good point, it would be sad if that makes it harder to reason about infima (especially in complete lattices, where the two definitions coincide).

[Jireh Loreaux]

Floris van Doorn said:

Though Eric raises a good point, it would be sad if that makes it harder to reason about infima (especially in complete lattices, where the two definitions coincide).

Yeah, this would be very sad.

[Notification Bot]

A message was moved here from #mathlib4 > triangle ineq for finite sums/prods by David Loeffler.

[Violeta Hernández]

Even disregarding the foot gun argument, I think it's weird that we have these two distinct ways to write a supremum over a complete lattice.

[Violeta Hernández]

And that's disregarding Sup (f '' s)

[Violeta Hernández]

It's really jarring to see theorems being spelled out in these different alternatives with little consistency. A couple of the primes being tagged by the linter are the fault of this.

[Kyle Miller]

In mathlib4#7227 I was exploring a way to process binders that had an actual concept of bounded quantification, i.e. quantifiers that have a binder type and an object over which the binding is happening. This was to move away from Lean-3-style binder elaboration where it nests the expansions.

A motivation for this was that summation notation over finsets is special-cased (i.e., it doesn't use notation3's binder facilities) since it's not amenable to this Lean-3-style "use nested sums" elaboration, since Finset is restricted to Type _, so it's not possible to sum over proofs. The ∑ x ∈ s, f x syntax needs to expand to a Finset.sum s (fun x : X => f x) expression, with a binder type X, a binding object s, and the function to sum.

The binder elaborator in the PR is pretty flexible (and maybe too flexible). For example, it's easy to do cute things like define binders like ∑ x + y = 5, f x y. You don't even need to redefine the ∑ syntax — it's extensible. The following macro says "when expanding a a + b = n binder for some finset-focused notation, expand it as a (a, b) ∈ Finset.Nat.antidiagonal n binder.

macro_rules
  | `(binder%(finset%, $a + $b = $n)) => `(binder%(finset%, ($a, $b) ∈ Finset.Nat.antidiagonal $n))

The idea still needs refinement, but maybe it'll be useful at some point.