Zulip Chat Archive

Stream: general

Topic: finite stuff


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:23):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 11:24):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 11:25):

is finite even a typeclass?

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:25):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 11:25):

yeah, it's defined as nonempty (fintype t) so just pop it open and use resetI

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:26):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:29):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:30):

How come mem_Union is an iff and mem_bUnion isn't?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 11:33):

probably because mem_bUnion is too old

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:33):

That bit at the end could use some tidying

view this post on Zulip Mario Carneiro (Apr 08 2020 at 11:34):

it looks like a term mode proof written vertically

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:34):

that's how I roll

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:34):

you should see my codewars solutions

view this post on Zulip 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 :-)

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:45):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:48):

There should be a mem_fUnion

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:48):

or possibly a mem_fUnion_iff...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 11:52):

The proof of mem_Union doesn't seem to be rfl

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:36):

Than you very much Kevin and Mario!

view this post on Zulip 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.

view this post on Zulip 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⟩⟩

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 12:45):

Nice :-)

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:46):

although I did swap in the use of mem_bUnion_iff

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:48):

I ctrl-clicked on mem_bUnion and looked for neighbors

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:48):

it was two lemmas previous

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:50):

Do you think we should keep both version finite_stuff and finite_stuff'?

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:50):

(with better names of course)

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:51):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:53):

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

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:53):

I want to use only the second one.

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:54):

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

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:54):

(in order to avoid unpacking the existential)

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:55):

I feel like there is a simpler core underlying principle here

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:55):

That was my question about missing lemmas.

view this post on Zulip Mario Carneiro (Apr 08 2020 at 12:56):

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

view this post on Zulip Sebastien Gouezel (Apr 08 2020 at 12:58):

In the conclusion of finite_stuff', it would be better to replace t ⊆ ⋃ i, σ iwith t = ⋃ i, σ i.

view this post on Zulip Patrick Massot (Apr 08 2020 at 12:59):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:04):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:08):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:10):

Like most principles

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:11):

Replacement says the image of a set is a set

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:11):

right

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:11):

here it's the image under a relation

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:11):

A relation on X

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:11):

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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:11):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:15):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:15):

I mentioned fUnion earlier (which doesn't exist)

view this post on Zulip Patrick Massot (Apr 08 2020 at 13:15):

I know I can write ⋂₀ s.to_set but it looks silly.

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:16):

you can use the coercion as I did above

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:18):

ok hey look what I found

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:18):

finset isn't a class

view this post on Zulip Johan Commelin (Apr 08 2020 at 13:18):

It should be just a structure, right?

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:18):

Fixed

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:18):

It's the wrong way around

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:20):

arguably, finite s should be called is_finite s. Is that your point?

view this post on Zulip 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

view this post on Zulip 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 concepts

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:22):

I think I have this straight now

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:23):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:23):

Reasoning purely by analogy

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:23):

finset is a structure

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:23):

subgroup is also a structure

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:24):

I see so I still have one error

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:24):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:24):

Is finite a class?

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:25):

I'm on mobile right now

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:25):

Because is_subgroup is a class

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:26):

finite is not a class, is_subgroup is a class, and yes this is inconsistent

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:27):

my proposed solution is to delete is_subgroup and call it a day

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:27):

Is finite deprecated? Because is_subgroup is, kinda

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2020 at 13:28):

for example you can meaningfully negate it

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:30):

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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:30):

Bundled ftw

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 13:30):

We should have infinset

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 08 2020 at 13:58):

Brilliant hack!

view this post on Zulip Patrick Massot (Apr 08 2020 at 13:58):

Too bad this topology stuff come too late.

view this post on Zulip Patrick Massot (Apr 08 2020 at 13:59):

You still get the jury special honorary mention.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 (?) ?

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 08 2020 at 14:10):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 08 2020 at 14:16):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 09 2020 at 09:45):

view this post on Zulip Johan Commelin (Apr 09 2020 at 09:50):

So... why did library_search not find this?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 09 2020 at 09:54):

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

view this post on Zulip Patrick Massot (Apr 09 2020 at 09:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 03 2021 at 20:29):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Apr 03 2021 at 21:36):

noncomputable lemma strikes me as nonsense

view this post on Zulip Eric Wieser (Apr 03 2021 at 21:38):

Probably the conclusion should be nonempty (s \equiv fin _), which also eliminates the classical

view this post on Zulip 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⟩⟩⟩

view this post on Zulip Eric Wieser (Apr 04 2021 at 08:44):

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

view this post on Zulip Eric Wieser (Apr 04 2021 at 08:45):

Or better, docs#nonempty_of_trunc

view this post on Zulip Patrick Massot (Apr 04 2021 at 16:35):

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

view this post on Zulip Eric Wieser (Apr 04 2021 at 17:09):

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

view this post on Zulip Patrick Massot (Apr 04 2021 at 17:10):

Indeed, it's in prop

view this post on Zulip Eric Wieser (Apr 04 2021 at 17:22):

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

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip Eric Wieser (Apr 04 2021 at 17:24):

The docs specifically list that lemma as being computable

view this post on Zulip Eric Wieser (Apr 04 2021 at 17:24):

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

view this post on Zulip 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

view this post on Zulip 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