# Zulip Chat Archive

## Stream: general

### Topic: finite stuff

#### Patrick Massot (Apr 08 2020 at 10:58):

I'm really bad at manipulating finite sets in Lean. This is frustrating because everything about finite sets seem obvious. I'd be very grateful if someone could prove the following lemmas (the second one has the same assumption but a more precise conclusion):

import data.set.finite open set variables {ι : Type*} {α : Type*} {s : ι → set α} {t : set α} lemma finite_stuff (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i := sorry lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, ∃ σ : {i | i ∈ I} → set α, (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i := sorry

Of course I'm also interested if someone explains those lemmas should be stated like this and will be a pain to use.

#### Johan Commelin (Apr 08 2020 at 11:09):

This reminds me of https://github.com/leanprover-community/mathlib/blob/51553e36ff9ae93ee4fbfb05a39e5d04c71be565/src/linear_algebra/finsupp.lean#L434

#### Johan Commelin (Apr 08 2020 at 11:13):

@Patrick Massot I think the statements are fine. (Maybe I would use `t : finset _`

... To prove this, I would do something like

have : \forall x : (t : Type*), \ex i, x \in s i, choose this using f hf, let I := finset.image f t,

modulo minor tweaks

#### Kevin Buzzard (Apr 08 2020 at 11:20):

apparently Lean can't synthesize decidable equality on iota. I am assuming that this isn't an issue for Patrick...

#### Kevin Buzzard (Apr 08 2020 at 11:23):

`example (α : Type*) (t : set α) [finite t] : fintype t := by apply_instance -- fails`

#### Mario Carneiro (Apr 08 2020 at 11:24):

I think you can do cases on the proof of `finite t`

#### Mario Carneiro (Apr 08 2020 at 11:25):

is `finite`

even a typeclass?

#### Kevin Buzzard (Apr 08 2020 at 11:25):

no it isn't -- sorry. But still...

#### Mario Carneiro (Apr 08 2020 at 11:25):

yeah, it's defined as `nonempty (fintype t)`

so just pop it open and use `resetI`

#### Kevin Buzzard (Apr 08 2020 at 11:26):

It's great that to prove this triviality I need to unfreeze local instances :-)

#### Mario Carneiro (Apr 08 2020 at 11:27):

hey, you're the one that wants to use instances that aren't present in the statement

#### Mario Carneiro (Apr 08 2020 at 11:27):

it's not needed for the statement and I'm not sure how it's being used in the proof

#### Kevin Buzzard (Apr 08 2020 at 11:29):

stupid mum_bUnion_iff wants the term to be in a set, not a finset :-)

#### Kevin Buzzard (Apr 08 2020 at 11:30):

How come `mem_Union`

is an iff and `mem_bUnion`

isn't?

#### Mario Carneiro (Apr 08 2020 at 11:33):

probably because `mem_bUnion`

is too old

#### Kevin Buzzard (Apr 08 2020 at 11:33):

lemma finite_stuff (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i := begin have : ∀ x : t, ∃ i, x.1 ∈ s i, rintros ⟨x, hx⟩, rcases h hx with ⟨_, ⟨i, rfl⟩, hi⟩, exact ⟨i, hi⟩, choose f hf using this, tactic.unfreeze_local_instances, cases tfin, use finset.image f finset.univ, intros x hx, rw mem_Union, use f ⟨x, hx⟩, rw mem_Union, existsi _, apply hf, rw finset.mem_image, use ⟨x, hx⟩, simp, end

#### Kevin Buzzard (Apr 08 2020 at 11:33):

That bit at the end could use some tidying

#### Mario Carneiro (Apr 08 2020 at 11:34):

it looks like a term mode proof written vertically

#### Kevin Buzzard (Apr 08 2020 at 11:34):

that's how I roll

#### Kevin Buzzard (Apr 08 2020 at 11:34):

you should see my codewars solutions

#### Kevin Buzzard (Apr 08 2020 at 11:39):

@Patrick Massot in the second one, why not have sigma mapping to finset alpha? it's `finset.unbind`

then :-)

#### Kevin Buzzard (Apr 08 2020 at 11:45):

Did someone find a proof of `finite t -> finite s \cap t`

?

#### Kevin Buzzard (Apr 08 2020 at 11:48):

There should be a `mem_fUnion`

#### Kevin Buzzard (Apr 08 2020 at 11:48):

or possibly a mem_fUnion_iff...

#### Kevin Buzzard (Apr 08 2020 at 11:50):

lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, ∃ σ : {i | i ∈ I} → set α, (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i := begin cases finite_stuff tfin h with I hI, use I, use (λ x, s x.1 ∩ t), split, { intro i, sorry}, -- finite t → finite s ∩ t split, { intro i, apply inter_subset_left}, { intros x hx, rw mem_Union, replace hI := hI hx, rw mem_Union at hI, cases hI with i hi, rw mem_Union at hi, cases hi with hi hsi, use ⟨i, hi⟩, split, exact hsi, exact hx} end

I'm not sure this is mathlib-ready </sarcasm>, and I assumed finite t -> finite s \cap t, but if it's just something you need now then there it is

#### Kevin Buzzard (Apr 08 2020 at 11:51):

I'm not sure these are term mode proofs really, because of the occasional rw mem_Union.

#### Kevin Buzzard (Apr 08 2020 at 11:52):

The proof of `mem_Union`

doesn't seem to be rfl

#### Mario Carneiro (Apr 08 2020 at 12:33):

lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, ∃ σ : (↑I:set ι) → set α, (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i := begin cases finite_stuff tfin h with I hI, use I, use (λ x, s x.1 ∩ t), split, { intro i, apply finite_subset tfin, apply inter_subset_right }, split, { intro i, apply inter_subset_left }, { intros x hx, rw mem_Union, replace hI := hI hx, rw mem_Union at hI, cases hI with i hi, rw mem_Union at hi, cases hi with hi hsi, use ⟨i, hi⟩, split, { exact hsi }, { exact hx } } end

#### Patrick Massot (Apr 08 2020 at 12:36):

Than you very much Kevin and Mario!

#### Patrick Massot (Apr 08 2020 at 12:36):

Mario, do you think we are missing intermediate lemmas here? It looks like a very long proof for such an obvious fact.

#### Mario Carneiro (Apr 08 2020 at 12:45):

here's kevin's proof in term mode:

```lean lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, ∃ σ : (↑I:set ι) → set α, (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i := let ⟨I, hI⟩ := finite_stuff tfin h in ⟨I, λ x, s x.1 ∩ t, λ i, finite_subset tfin (inter_subset_right _ _), λ i, inter_subset_left _ _, λ x hx, mem_Union.2 $ let ⟨i, hi, hsi⟩ := mem_bUnion_iff.1 (hI hx) in ⟨⟨i, hi⟩, hsi, hx⟩⟩

#### Kevin Buzzard (Apr 08 2020 at 12:45):

Nice :-)

#### Mario Carneiro (Apr 08 2020 at 12:46):

although I did swap in the use of `mem_bUnion_iff`

#### Kevin Buzzard (Apr 08 2020 at 12:47):

To do that I would have had to understand how supr was implemented and I couldn't be bothered to dig

#### Mario Carneiro (Apr 08 2020 at 12:47):

I don't think this is an unreasonably long proof, given the complexity of the statement itself. Once you set the logical manipulation aside the only actually interesting part is the last 3 lines of my version of the proof

#### Mario Carneiro (Apr 08 2020 at 12:48):

I ctrl-clicked on `mem_bUnion`

and looked for neighbors

#### Mario Carneiro (Apr 08 2020 at 12:48):

it was two lemmas previous

#### Patrick Massot (Apr 08 2020 at 12:50):

Do you think we should keep both version `finite_stuff`

and `finite_stuff'`

?

#### Patrick Massot (Apr 08 2020 at 12:50):

(with better names of course)

#### Mario Carneiro (Apr 08 2020 at 12:51):

If you find it useful, I don't see why not

#### Mario Carneiro (Apr 08 2020 at 12:52):

I usually try to find an appropriate constructive analogue for these sorts of things, that is, a function with the stated properties, since existentials have to be unpacked and lack global coherence of choices

#### Patrick Massot (Apr 08 2020 at 12:53):

In my question the first lemma was really meant as training for the second one.

#### Patrick Massot (Apr 08 2020 at 12:53):

I want to use only the second one.

#### Patrick Massot (Apr 08 2020 at 12:54):

If you can turn this lemma into a function that would be even better of course.

#### Patrick Massot (Apr 08 2020 at 12:54):

(in order to avoid unpacking the existential)

#### Mario Carneiro (Apr 08 2020 at 12:55):

I feel like there is a simpler core underlying principle here

#### Patrick Massot (Apr 08 2020 at 12:55):

That was my question about missing lemmas.

#### Mario Carneiro (Apr 08 2020 at 12:56):

like, you can swap forall and exists a la skolemization for finite sets

#### Sebastien Gouezel (Apr 08 2020 at 12:58):

In the conclusion of `finite_stuff'`

, it would be better to replace `t ⊆ ⋃ i, σ i`

with `t = ⋃ i, σ i`

.

#### Patrick Massot (Apr 08 2020 at 12:59):

I didn't need this, but feel free to prove that stronger version!

#### Mario Carneiro (Apr 08 2020 at 12:59):

what do you think of this formulation:

lemma finite_stuff'' (s : finset α) (P : α → ι → Prop) (h : ∀ x ∈ s, ∃ i, P x i) : ∃ t : finset ι, ∀ x ∈ s, ∃ i ∈ t, P x i := sorry

#### Patrick Massot (Apr 08 2020 at 13:03):

That certainly looks cleaner. Can you prove it and deduce Sébastien's version of the original question?

#### Mario Carneiro (Apr 08 2020 at 13:04):

I think it's not quite enough to get the second version of the statement

#### Kevin Buzzard (Apr 08 2020 at 13:08):

Do we have an equiv e between finset X and Pi (s : set X), finite s, and the lemma that for x : X, x \in s iff x \in e s?

#### Mario Carneiro (Apr 08 2020 at 13:08):

Hey, isn't this just the collection principle from zfc?

#### Kevin Buzzard (Apr 08 2020 at 13:09):

All I know is that it's a mathematical triviality so it wouldn't surprise me if the logicians called it a principle

#### Mario Carneiro (Apr 08 2020 at 13:10):

I'm thinking of the version where you replace "finite" with "is a set" and depending on how you set things up it might be a theorem or an axiom

#### Kevin Buzzard (Apr 08 2020 at 13:10):

Like most principles

#### Mario Carneiro (Apr 08 2020 at 13:10):

it's essentially a souped up version of replacement without the assumption that the relation is a function

#### Kevin Buzzard (Apr 08 2020 at 13:11):

Replacement says the image of a set is a set

#### Mario Carneiro (Apr 08 2020 at 13:11):

right

#### Mario Carneiro (Apr 08 2020 at 13:11):

here it's the image under a relation

#### Kevin Buzzard (Apr 08 2020 at 13:11):

A relation on X

#### Mario Carneiro (Apr 08 2020 at 13:11):

and it's not really an image because you can take a subset

#### Mario Carneiro (Apr 08 2020 at 13:11):

but you have to preserve "enough" of the original relation

#### Kevin Buzzard (Apr 08 2020 at 13:14):

is_monoid_hom f is unbundled monoid homs and it's a class. monoid_hom is bundled and it's a structure

#### Kevin Buzzard (Apr 08 2020 at 13:15):

finite s is unbundled finiteness and it's a structure. finset is bundled and a structure

#### Patrick Massot (Apr 08 2020 at 13:15):

Do we have a version `sInter s`

when `s : finset (set X)`

? This is why I used `finite`

everywhere instead of `finset`

.

#### Kevin Buzzard (Apr 08 2020 at 13:15):

I mentioned fUnion earlier (which doesn't exist)

#### Patrick Massot (Apr 08 2020 at 13:15):

I know I can write `⋂₀ s.to_set`

but it looks silly.

#### Mario Carneiro (Apr 08 2020 at 13:16):

you can use the coercion as I did above

#### Mario Carneiro (Apr 08 2020 at 13:17):

If we did have something like that, I would prefer it generalize to lattices. I would call it `finset.inf`

#### Mario Carneiro (Apr 08 2020 at 13:18):

ok hey look what I found

#### Johan Commelin (Apr 08 2020 at 13:18):

Kevin Buzzard said:

finite s is unbundled finiteness and it's a structure. finset is bundled and a class

Whut?? Is `finset`

a class?

#### Mario Carneiro (Apr 08 2020 at 13:18):

finset isn't a class

#### Johan Commelin (Apr 08 2020 at 13:18):

It should be just a `structure`

, right?

#### Kevin Buzzard (Apr 08 2020 at 13:18):

Fixed

#### Kevin Buzzard (Apr 08 2020 at 13:18):

It's the wrong way around

#### Mario Carneiro (Apr 08 2020 at 13:20):

arguably, `finite s`

should be called `is_finite s`

. Is that your point?

#### Mario Carneiro (Apr 08 2020 at 13:21):

I think the problem, grammatically, is that `finite`

is an adjective and `monoid_hom`

is a noun

#### Kevin Buzzard (Apr 08 2020 at 13:22):

I am saying that the class/structure choice is different in the two situations for ~~both~~ the unbundled ~~and the bundled~~ concept~~s~~

#### Kevin Buzzard (Apr 08 2020 at 13:22):

I think I have this straight now

#### Mario Carneiro (Apr 08 2020 at 13:22):

Oh I see. Well, using typeclasses for these things has always been dubious, that's why we're moving away from them

#### Kevin Buzzard (Apr 08 2020 at 13:23):

~~I'm saying that either finset should be a structure or subgroup should be a class~~

#### Kevin Buzzard (Apr 08 2020 at 13:23):

Reasoning purely by analogy

#### Mario Carneiro (Apr 08 2020 at 13:23):

finset is a structure

#### Mario Carneiro (Apr 08 2020 at 13:23):

subgroup is also a structure

#### Kevin Buzzard (Apr 08 2020 at 13:24):

I see so I still have one error

#### Mario Carneiro (Apr 08 2020 at 13:24):

I'm failing to see past the typo to the point

#### Kevin Buzzard (Apr 08 2020 at 13:24):

Is finite a class?

#### Kevin Buzzard (Apr 08 2020 at 13:25):

I'm on mobile right now

#### Kevin Buzzard (Apr 08 2020 at 13:25):

Because is_subgroup is a class

#### Mario Carneiro (Apr 08 2020 at 13:26):

`finite`

is not a class, `is_subgroup`

is a class, and yes this is inconsistent

#### Mario Carneiro (Apr 08 2020 at 13:27):

my proposed solution is to delete `is_subgroup`

and call it a day

#### Kevin Buzzard (Apr 08 2020 at 13:27):

Is `finite`

deprecated? Because `is_subgroup`

is, kinda

#### Mario Carneiro (Apr 08 2020 at 13:27):

finite is not deprecated, it is meant to be a proposition to talk about finiteness in other positions

#### Mario Carneiro (Apr 08 2020 at 13:28):

for example you can meaningfully negate it

#### Kevin Buzzard (Apr 08 2020 at 13:30):

This is some sort of indication that one should stick to finsets where one can though

#### Kevin Buzzard (Apr 08 2020 at 13:30):

Bundled ftw

#### Kevin Buzzard (Apr 08 2020 at 13:30):

We should have infinset

#### Reid Barton (Apr 08 2020 at 13:54):

import topology.subset_properties import data.set.finite open set variables {ι : Type*} {α : Type*} {s : ι → set α} {t : set α} lemma finite_stuff (tfin : finite t) (h : t ⊆ ⋃ i, s i) : ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i := begin letI : topological_space α := ⊥, haveI : discrete_topology α := ⟨rfl⟩, exact tfin.compact.elim_finite_subcover _ (λ i, is_open_discrete _) h end

#### Johan Commelin (Apr 08 2020 at 13:58):

Brilliant hack!

#### Patrick Massot (Apr 08 2020 at 13:58):

Too bad this topology stuff come too late.

#### Patrick Massot (Apr 08 2020 at 13:59):

You still get the jury special honorary mention.

#### Patrick Massot (Apr 08 2020 at 14:00):

It's too late because I want to put this below `order.filter.basic`

. But it's also good to see that the form of the statement is used elsewhere in mathlib.

#### Reid Barton (Apr 08 2020 at 14:05):

Yes, I expected it to be easy but I didn't realize it would be quite this easy.

#### Ryan Lahfa (Apr 08 2020 at 14:09):

Mario Carneiro said:

for example you can meaningfully negate it

BTW, is it normal that `push_neg`

on `not set.finite`

cannot rename it as `set.infinite`

, I guess it has to do with `simp`

(?) ?

#### Ryan Lahfa (Apr 08 2020 at 14:09):

(I had to do a `rw set.infinite`

in order to get the nice `infinite S`

rather than `not set.finite S`

)

#### Mario Carneiro (Apr 08 2020 at 14:10):

`push_neg`

needs explicit support for each of these things. Seems like a good PR

#### Ryan Lahfa (Apr 08 2020 at 14:11):

Mario Carneiro said:

`push_neg`

needs explicit support for each of these things. Seems like a good PR

Sounds good, thanks

#### Patrick Massot (Apr 08 2020 at 14:16):

Yes, every end-game negation in push_neg is hardcoded.

#### Patrick Massot (Apr 09 2020 at 09:42):

Damn, I was trying to put this finite stuff in the proper place before PRing, and guess what? https://leanprover-community.github.io/mathlib_docs/data/set/finite.html#set.finite_subset_Union

#### Kenny Lau (Apr 09 2020 at 09:45):

#### Johan Commelin (Apr 09 2020 at 09:50):

So... why did `library_search`

not find this?

#### Mario Carneiro (Apr 09 2020 at 09:52):

It's very unlikely that library_search will find longer statements, because the probability that you spell the theorem the same way as the library decreases exponentially with the length of the theorem

#### Mario Carneiro (Apr 09 2020 at 09:53):

Because of our rigid naming convention and fairly deterministic file organization it's much likely to notice a collision the way Patrick did, by putting it in its proper place and seeing something already there, or getting a name conflict with a duplicate of your theorem

#### Patrick Massot (Apr 09 2020 at 09:54):

Yes, I'm trying to fit in the more precise version, and it's a pain.

#### Patrick Massot (Apr 09 2020 at 09:54):

Because of mathematically empty differences between my statement and the one already in mathlib.

#### Mario Carneiro (Apr 09 2020 at 09:55):

this is also why I highly recommend looking at sources for relevant files as a theorem discovery strategy

#### Patrick Massot (Apr 03 2021 at 18:42):

Let's try that Zulip tactic. For our experts in finiteness:

```
lemma set.finite.fin_param {α : Type*} {s : set α} (h : finite s) :
∃ f : fin (h.to_finset.card) → α, injective f ∧ range f = s :=
sorry
```

#### Johan Commelin (Apr 03 2021 at 18:59):

@Patrick Massot voila

```
open function
lemma set.finite.fin_param {α : Type*} {s : set α} (h : s.finite) :
∃ f : fin (h.to_finset.card) → α, injective f ∧ set.range f = s :=
begin
classical,
unfreezingI { cases h },
obtain ⟨e⟩ := fintype.equiv_fin s,
have : fintype.card s = (finset.card $ set.finite.to_finset ⟨h⟩),
{ symmetry,
refine finset.card_congr (λ a ha, ⟨a, _⟩) _ _ _,
{ simpa only [set.finite.mem_to_finset] using ha },
{ intros, exact finset.mem_univ _ },
{ intros a b ha hb H, simpa only [subtype.mk_eq_mk] using H },
{ rintro ⟨a, ha⟩ -, refine ⟨a, _, rfl⟩, simpa only [set.finite.mem_to_finset] using ha } },
rw ← this,
refine ⟨λ x, e.symm x, subtype.coe_injective.comp e.symm.injective, _⟩,
ext x,
simp only [set.mem_range],
split,
{ rintro ⟨i, rfl⟩, exact (e.symm i).2 },
{ intro h, refine ⟨e ⟨x, h⟩, _⟩, rw e.symm_apply_apply, refl }
end
```

#### Patrick Massot (Apr 03 2021 at 20:29):

Thanks Johan! This is much more complicated than what I hoped for :sad:

#### Patrick Massot (Apr 03 2021 at 21:00):

I massaged a bit into:

```
lemma set.finite.finset_card_eq_fintype_card {α : Type*} {s : set α} (h : finite s) :
h.to_finset.card = @fintype.card ↥s h.fintype:=
begin
letI := h.fintype,
refine finset.card_congr (λ a ha, ⟨a, _⟩) _ _ _,
{ simpa only [set.finite.mem_to_finset] using ha },
{ intros, exact finset.mem_univ _ },
{ intros a b ha hb H, simpa only [subtype.mk_eq_mk] using H },
{ rintro ⟨a, ha⟩ -, refine ⟨a, _, rfl⟩, simpa only [set.finite.mem_to_finset] using ha }
end
noncomputable
lemma set.finite.equiv_fin {α : Type*} {s : set α} (h : finite s) : s ≃ fin h.to_finset.card :=
begin
classical,
rw h.finset_card_eq_fintype_card,
letI := h.fintype,
exact classical.some (fintype.equiv_fin s).exists_rep
end
lemma set.finite.fin_param {α : Type*} {s : set α} (h : finite s) :
∃ f : fin (h.to_finset.card) → α, injective f ∧ range f = s :=
let e := h.equiv_fin in
⟨λ x, e.symm x, subtype.coe_injective.comp e.symm.injective, by simp [e.symm.surjective.range_comp]⟩
lemma set.finite.fin_param' {α : Type*} {s : set α} (h : finite s) :
∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
⟨_, h.fin_param⟩
```

Now I'm sure @Mario Carneiro will explain why we are writing nonsense.

#### Eric Wieser (Apr 03 2021 at 21:36):

`noncomputable lemma`

strikes me as nonsense

#### Eric Wieser (Apr 03 2021 at 21:38):

Probably the conclusion should be `nonempty (s \equiv fin _)`

, which also eliminates the `classical`

#### Bhavik Mehta (Apr 03 2021 at 22:05):

Patrick Massot said:

Thanks Johan! This is much more complicated than what I hoped for :sad:

```
open_locale classical
lemma set.finite.fin_param' {α : Type*} {s : set α} (h : finite s) :
∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
let f := (fintype.equiv_fin (h.to_finset : set α)).out in
⟨_, coe ∘ f.symm, subtype.coe_injective.comp (equiv.injective _),
set.ext $ λ x, ⟨λ ⟨y, h⟩, by simpa [←h] using (f.symm y).2, λ hs, ⟨f ⟨x, by simpa⟩, by simp⟩⟩⟩
```

#### Eric Wieser (Apr 04 2021 at 08:44):

Presumably you can avoid choice there by using docs#trunc.rec instead of trunc.out?

#### Eric Wieser (Apr 04 2021 at 08:45):

Or better, docs#nonempty_of_trunc

#### Patrick Massot (Apr 04 2021 at 16:35):

I don't see how any of this could avoid choice here.

#### Eric Wieser (Apr 04 2021 at 17:09):

Your conclusion is in prop, so you don't need to ever construct anything

#### Patrick Massot (Apr 04 2021 at 17:10):

Indeed, it's in prop

#### Eric Wieser (Apr 04 2021 at 17:22):

You're correct though, docs#fintype.equiv_fin already uses classical logic

#### Eric Wieser (Apr 04 2021 at 17:23):

Which seems ridiculous, because isn't the whole point of `trunc`

to be a computable version of `nonempty`

?

#### Patrick Massot (Apr 04 2021 at 17:23):

Yes, that's the issue. Maybe a proof exists in classical logic without going through that lemma, but I'm not very interested in avoiding classical logic anyway...

#### Eric Wieser (Apr 04 2021 at 17:24):

The docs specifically list that lemma as being computable

#### Eric Wieser (Apr 04 2021 at 17:24):

Oh, I guess functions can still be computable but use classical logic in internal proofs

#### Mario Carneiro (Apr 05 2021 at 05:03):

@Eric Wieser There is a difference between being computable and avoiding choice entirely. The former means that any uses of AC are confined to proof arguments where they don't hamper code generation. Large parts of mathlib are computable, but only a small fraction is AC-free

#### Mario Carneiro (Apr 05 2021 at 05:08):

In principle most of the things that are computable are also AC-free, but there aren't too many people besides me making any attempt to actually make it happen, and there are several foundational bits that need adjustment before there is any hope of making, say, finsets AC-free. I made another push toward AC-freedom in lean core recently, so we should see some improvement in mathlib when the next minor version is released.

Last updated: May 12 2021 at 23:13 UTC