set.image for `Prop`?

Stream: general

[Kevin Buzzard]

set.image : Π {α : Type u} {β : Type v}, (α → β) → set α → set β is in core. Is there any particular reason why we don't have this for Sort u and Sort v? I've just been working on #7199 , seeing if I can golf Eric's suggested proof of independent.disjoint_supr and I've run into the issue that I can use set.range if the source is a Sort u but I can't use set.image. I have it in my head that there's a good reason for this, but I can't remember it! Furthermore I'm not sure I can break down my proof into "if \iota is a Prop, then it's trivial, else do this..."

[Kevin Buzzard]

Aah, I've come up with a workaround -- instead of having a variable {ι : Sort*}, I just have this as a direct input to the function, and Lean will secretly turn it into Type* and nobody will ever notice!

[Damiano Testa]

Kevin, you have made me now so curious to look at this workaround... :upside_down:

[Kevin Buzzard]

Damiano I'm so obsessed with this stupid thing -- this is the reason I'm not helping with the condensed branch thing!

[Damiano Testa]

No worries: I was expecting that I should be maintaining the toric branch. I had been able to do so successfully, now with a unique exception!

[Kevin Buzzard]

You do this:

theorem independent_def' {ι : Sort*} {t : ι → α} :
  independent t ↔ ∀ i, disjoint (t i) (Sup (t '' {j | j ≠ i})) :=

and because Lean knows that t '' _ only makes sense for types, when the theorem is elaborated iota has magically changed to a Type but the maintainers don't notice so you don't get hassle about changing it back to a Sort.

[Damiano Testa]

Thanks for sharing the trick!

:smile: I am sure that now no one will notice that this is what is going on!

[Eric Wieser]

The problem is that set isn't even allowed for Prop

[Eric Wieser]

You're not allowed to have a set of proofs for some design reason

[Eric Wieser]

src#set defines set as def set (α : Type u) := α → Prop not def set (α : Sort u) := α → Prop

[Eric Wieser]

So obviously you can't take an image of a function from sort, because the set you'd be taking the image over isn't allowed to exist

[Gabriel Ebner]

Eric Wieser said:

You're not allowed to have a set of proofs for some design reason

There are roughly two reasons:

1. Sets (or lists) of proofs are not useful. (Since proofs are subsingletons.)
2. Using Sort instead of Type often makes inference of universe levels harder. This is because you then get expressions like max ?u 1 or imax ?u 1 which are hard to unify (but would be trivial if ?u = ?v+1). (Historical note: in early versions of Lean 3, Type u used to be defined as Sort (max u 1). This resulted in lots of problems with type inference. Switching to Sort (u+1) solved many of them.)

[Eric Wieser]

I think I'd dispute (1) - as a result of this choice, src#finprod has to use plift to lift its sets of proofs to Type, which definitely introduces some awkardness. Perhaps not as much as (2) resolves though.

[Gabriel Ebner]

Why do we want finprod to support Prop in the first place? Is this for ∏ᶠ n < 10, n^2?

[Eric Wieser]

Yes

[Gabriel Ebner]

(Side note: I'm not 100% sold on elaborating ∏ᶠ n < 10, p n as ∏ᶠ n, ∏ᶠ H : n < 10, p n. One issue is that simp can rewrite the second product on its own, breaking the "bound quantifier" syntax. We've had this recently with ∏ x ∈ set.image f, g x.)

[Eric Wieser]

(that's already how supr / Union is elaborated anyway though, right?)

[Gabriel Ebner]

Yes, it is consistent. But also consistently problematic.

[Gabriel Ebner]

We have a different convention for finset.prod though.

[Eric Wieser]

As a reminder, what was the problematic simplification?

[Gabriel Ebner]

AFAICR ⨅ x ∈ set.range f, g x would simplify to ⨅ x, ⨅ H : ∃ y, f y = x, g x, which you probably don't want. You can undo it with another simp lemma, but it would be better if the initial step didn't happen in the first place.

[Eric Wieser]

I assume you mean set.range?

[Sebastien Gouezel]

By the way, is this really a good simp lemma? It turns something into an existential, which is not very good as a normal form because it is hard to manipulate (Lean will almost never be able to guess the right y to discharge such a proof obligation).

[Gabriel Ebner]

I'd cautiously support removing it, for the reasons that you mention.

[Gabriel Ebner]

There are other ones as well though: ⊓ x ∈ A ∩ B, p x simplifies to ⊓ x, ⊓ H : x ∈ A ∧ x ∈ B, p x.

[David Wärn]

set for Props would be nice in docs#wide_subquiver. It would allow one to speak uniformly of subgraphs of multigraphs and of simple graphs. But it's not a big issue

[Eric Wieser]

Is ⨅ (x : T) (h : x ∈ A ∩ B), p x simplifying to ⨅ (x : T) (H : x ∈ A ∧ x ∈ B), p x such a bad thing?

[Eric Wieser]

The pretty printer already prints ⨅ x ∈ A ∩ B as ⨅ (x : T) (h : x ∈ A ∩ B), p x, which introduces most of the ugliness

[Gabriel Ebner]

The problem is that then lemmas like infi_union no longer apply. The pretty-printer issue will hopefully be fixed when the clover blooms.