## Stream: general

### Topic: set.image for Prop?

#### Kevin Buzzard (Apr 19 2021 at 10:17):

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 (Apr 19 2021 at 10:21):

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 (Apr 19 2021 at 10:22):

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

#### Kevin Buzzard (Apr 19 2021 at 10:23):

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

#### Damiano Testa (Apr 19 2021 at 10:24):

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 (Apr 19 2021 at 10:25):

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 (Apr 19 2021 at 10:26):

Thanks for sharing the trick!

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

#### Eric Wieser (Apr 19 2021 at 10:37):

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

#### Eric Wieser (Apr 19 2021 at 10:37):

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

#### Eric Wieser (Apr 19 2021 at 10:38):

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

#### Eric Wieser (Apr 19 2021 at 10:39):

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 (Apr 19 2021 at 10:57):

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 (Apr 19 2021 at 11:07):

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 (Apr 19 2021 at 11:10):

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

Yes

#### Gabriel Ebner (Apr 19 2021 at 11:15):

(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 (Apr 19 2021 at 11:18):

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

#### Gabriel Ebner (Apr 19 2021 at 11:18):

Yes, it is consistent. But also consistently problematic.

#### Gabriel Ebner (Apr 19 2021 at 11:19):

We have a different convention for finset.prod though.

#### Eric Wieser (Apr 19 2021 at 11:20):

As a reminder, what was the problematic simplification?

#### Gabriel Ebner (Apr 19 2021 at 11:24):

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 (Apr 19 2021 at 11:31):

I assume you mean set.range?

#### Sebastien Gouezel (Apr 19 2021 at 11:40):

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 (Apr 19 2021 at 11:43):

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

#### Gabriel Ebner (Apr 19 2021 at 11:46):

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 (Apr 19 2021 at 11:48):

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 (Apr 19 2021 at 11:56):

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 (Apr 19 2021 at 11:56):

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 (Apr 19 2021 at 12:03):

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

Last updated: Aug 03 2023 at 10:10 UTC