Zulip Chat Archive

Stream: new members

Topic: sets with two elements


view this post on Zulip Damiano Testa (Sep 01 2020 at 14:53):

Dear All,

I have managed to find a very convoluted proof of what I think of as a very simple fact. Can anyone suggest a proof of the lemma below?

I am happy to be embarrassed by showing my proof, although I am not doing it right away, in order not to lead anyone astray... I will post it, if you ask, though!

Thank you very much!

import tactic

lemma card_two {sup : finset } {H : 2  sup.card} : finset.min' sup  finset.max' sup :=
begin
    sorry,
end

view this post on Zulip Damiano Testa (Sep 01 2020 at 14:54):

(The reason that I would like a shorter proof is that at the moment, Lean times out every time I try to continue with my proofs...)

view this post on Zulip Reid Barton (Sep 01 2020 at 14:59):

I was going to say your lemma doesn't look like it would type check but I guess it actually does.

view this post on Zulip Reid Barton (Sep 01 2020 at 14:59):

Did you really prove it as a top-level lemma in this form?

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:00):

Reid Barton said:

Did you really prove it as a top-level lemma in this form?

I did prove it, but I am not really proud of my proof:

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:00):

lemma card_two {sup : finset } {H : 2  sup.card} : finset.min' sup  finset.max' sup :=
begin
    intro,
    have sne : sup.nonempty,
        {
            refine finset.card_pos.mp _,
            refine lt_of_lt_of_le _ H,
            exact two_pos,
        },
    have ineq : {c :  |  d  sup , d = c}  {c :  | (finset.min' sup sne)  c  c  (finset.max' sup sne)},
        {
            intros c chip,
            have cinsup : c  sup,
                simp only [*, exists_prop, exists_eq_right, finset.set_of_mem, finset.mem_coe] at *,
            have clemax : c  finset.max' sup sne,
                exact finset.le_max' sup sne c cinsup,
            have minlec : finset.min' sup sne  c,
                exact finset.min'_le sup sne c cinsup,
            simp only [*, and_self, set.mem_set_of_eq] at *,
        },
    rw a at ineq,
    have : {c :  | (finset.max' sup sne)  c  c  (finset.max' sup sne)} = {c :  | c = (finset.max' sup sne)},
        {
            simp only [exists_prop, set.set_of_eq_eq_singleton, exists_eq_right, finset.set_of_mem] at *,
            ext,
            split;{simp only [and_imp, set.mem_singleton_iff, set.mem_set_of_eq] at *,omega},
        },
    rw this at ineq,
    simp only [*, exists_prop, set.set_of_eq_eq_singleton, exists_eq_right, finset.set_of_mem] at *,
    have consingle : {c :  |  d  sup , d = c}  {finset.max' sup sne},
        simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
    have supfintype : fintype {c :  |  d  sup , d = c},
        {
            refine set.finite.fintype _,
            refine set.finite.subset _ _,
            exact {dd :  |  d  sup , d = dd},
            simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
            exact finset.finite_to_set sup,
            simp only [exists_prop] at *,
        },
    have supfinite : {c :  |  d  sup , d = c}.finite,
        refine set.finite.subset _ _,
        exact {dd :  |  d  sup , d = dd},
        simp only [*, exists_prop, exists_eq_right, finset.set_of_mem] at *,
        exact finset.finite_to_set sup,
        simp only [exists_prop] at *,
    have supins : sup = supfinite.to_finset,
        simp only [exists_prop, finset.finite_to_set_to_finset, exists_eq_right, finset.set_of_mem] at *,
    have singlefinite: {d :  | d = sup.max' sne}.finite,
        exact set.finite_pure (finset.max' sup sne),
    have le : supfinite.to_finset.card  singlefinite.to_finset.card,
        {
            apply finset.card_le_of_subset,
            intros a ah,
            refine set.mem_def.mpr _,
            refine multiset.mem_map.mpr _,
            tidy,
        },
    let singsing : set  := {finset.max' sup sne},
    have singsingfinite : singsing.finite,
        exact set.finite_singleton (finset.max' sup sne),
    have eq1 : singlefinite.to_finset.card = 1,
        {
            apply finset.card_eq_one.mpr,
            use (finset.max' sup sne),
            ext1,
            split;
                {intros xx,finish,},
        },
    rw eq1 at le,
    have careq : sup.card = supfinite.to_finset.card,
        exact congr_arg finset.card supins,
    rw  careq at le,
    linarith,
end

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:01):

(I am not sure whether I need more imports for the proof to go through: I produced the mwe with only the statement)
I just checked that there is the need for no other imports.

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:03):

Reid Barton said:

Did you really prove it as a top-level lemma in this form?

Btw, what does "top-level lemma" means?

view this post on Zulip Reid Barton (Sep 01 2020 at 15:04):

Not part of another proof

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:04):

well, this lemma is supposed to be part of another proof... ahahah! so I guess that it is a "bottom-level lemma"!

view this post on Zulip Reid Barton (Sep 01 2020 at 15:11):

Here's a more efficient proof

lemma card_two {α : Type*} {s : finset α} [decidable_linear_order α] {H : 2  s.card} : finset.min' s  finset.max' s :=
begin
  intro h,
  have sne : s.nonempty,
  { rw finset.card_pos, linarith },
  let min := finset.min' s sne,
  let max := finset.max' s sne,
  have : min = max,
  { dsimp only [min, max], rw h },
  have :  x  s, x = min,
  { intros x hx,
    apply le_antisymm,
    { rw this,
      exact finset.le_max' s sne x hx },
    { exact finset.min'_le s sne x hx } },
  have : s.card  1,
  { rw finset.card_le_one_iff,
    intros x y hx hy,
    rw [this x hx, this y hy] },
  linarith
end

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:12):

finset.le_max' seems to have spurious assumptions.

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:12):

Reid Barton said:

Here's a more efficient proof

Thank you so much!!!

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:12):

I will try to understand why your proof works, but for the moment, I will continue with what I was doing!

view this post on Zulip Reid Barton (Sep 01 2020 at 15:13):

The main step is to guess that something like docs#finset.card_le_one_iff already exists

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:14):

Here is my proof, without looking at the one by Reid. I haven't made golfing attempts yet.

open_locale classical

lemma card_two (sup : finset ) (H : 2  sup.card) :
  finset.min' sup  finset.max' sup :=
begin
  contrapose! H,
  suffices : sup.card = 0  sup.card = 1,
  { cases this with h h; rw h; linarith, },
  rw or_iff_not_imp_left,
  intro h0,
  rw finset.card_eq_one,
  rw [ ne.def,  nat.pos_iff_ne_zero, finset.card_pos] at h0,
  obtain x, hx := h0,
  use x,
  rw finset.eq_singleton_iff_unique_mem,
  refine hx, _⟩,
  rintro i hi,
  suffices :  a b, a  sup  b  sup  a  b,
  { apply le_antisymm; solve_by_elim },
  rintro a b ha hb,
  apply le_trans (sup.le_max' x, hx a ha),
  rw  H,
  apply sup.min'_le x, hx b hb,
end

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:15):

Reid Barton said:

The main step is to guess that something like docs#finset.card_le_one_iff already exists

It always seems to simple, when someone else points it out to me...

view this post on Zulip Sebastien Gouezel (Sep 01 2020 at 15:15):

The assumption is calling to be formulated in terms of nontrivial (which is equivalent to your assumption thanks to docs#fintype.one_lt_card_iff_nontrivial )

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:15):

Reid Barton said:

The main step is to guess that something like docs#finset.card_le_one_iff already exists

What does Type* mean?

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:15):

Golfed

open_locale classical

lemma card_two (sup : finset ) (H : 2  sup.card) :
  finset.min' sup  finset.max' sup :=
begin
  contrapose! H,
  suffices : sup.card  1, by linarith,
  rw finset.card_le_one_iff,
  suffices :  a b, a  sup  b  sup  a  b,
  { intros, apply le_antisymm; solve_by_elim },
  rintro a b ha hb,
  apply le_trans (sup.le_max' a, ha a ha),
  rw  H,
  apply sup.min'_le a, ha b hb,
end

view this post on Zulip Reid Barton (Sep 01 2020 at 15:16):

Oh, now I understand what you mean about extraneous assumptions

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:16):

Damiano Testa said:

What does Type* mean?

Type _, in other words: "Hey lean, figure out the universe yourself"

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:16):

Johan Commelin said:

Golfed

Wow! This proof is also very short!

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:17):

Johan Commelin said:

Damiano Testa said:

What does Type* mean?

Type _, in other words: "Hey lean, figure out the universe yourself"

Ah, so I can skip introducing universes and go directly to never think about them anymore!

view this post on Zulip Sebastien Gouezel (Sep 01 2020 at 15:17):

No, sorry, nontrivial is for (fin)types, but you're working with a finset.

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:18):

Yup... until you start doing fpqc cohomology (-;

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:19):

@Reid Barton Are you PRing a fix? Otherwise I will do it

view this post on Zulip Reid Barton (Sep 01 2020 at 15:21):

Go ahead

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:24):

#4020

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:26):

@Reid Barton I also finally understand why you were so surprised that this lemma typechecked :face_palm:

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:27):

Reid Barton said:

Here's a more efficient proof

I really like your proof! I see that you went for the minimum, rather than the maximum! Anyway, it was very instructive for me, thanks!

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:31):

@Damiano Testa Here is an evil proof that might satisfy Reid:

lemma card_two (sup : finset ) (H : 2  sup.card) :
  finset.min' sup  finset.max' sup :=
begin
  have h0 : 0 < sup.card, by linarith,
  rw finset.card_pos at h0,
  rw [ne.def, function.funext_iff, not_forall],
  use h0,
  apply ne_of_lt,
  apply finset.min'_lt_max'_of_card,
  linarith,
end

view this post on Zulip Damiano Testa (Sep 01 2020 at 15:32):

Johan Commelin said:

Damiano Testa Here is an evil proof that might satisfy Reid:

Ahaha an evil proof!

I was going over your previous one and I find it very clean!

view this post on Zulip Johan Commelin (Sep 01 2020 at 15:33):

lemma card_two (sup : finset ) (H : 2  sup.card) :
  finset.min' sup  finset.max' sup :=
begin
  have h0 : sup.nonempty, by { rw  finset.card_pos, linarith },
  rw [ne.def, function.funext_iff, not_forall],
  use h0,
  apply ne_of_lt,
  apply finset.min'_lt_max'_of_card _ _ H,
end

view this post on Zulip Reid Barton (Sep 01 2020 at 15:34):

Johan Commelin said:

Damiano Testa Here is an evil proof that might satisfy Reid:

  apply finset.min'_lt_max'_of_card,

Oh nice

view this post on Zulip Reid Barton (Sep 01 2020 at 15:34):

Presumably this is the statement one actually wants anyways (the inequality of functions is not very convenient)

view this post on Zulip Yakov Pechersky (Sep 01 2020 at 15:58):

If you look at the definition of finset.min'_lt_max'_of_card, you'll see the closely related finset.min'_lt_max', which might be more convenient. Not sure how you showed that the cardinality is 2 or more. Could be that if you're still proving things about disjoint elements, the card-free lemma is simpler to utilize, instead of generating a hypothesis about card that is just for this lemma.

view this post on Zulip Damiano Testa (Sep 01 2020 at 16:19):

Thank you all for the useful lemmas that you found!

view this post on Zulip Bhavik Mehta (Sep 21 2020 at 00:08):

Perhaps I'm missing something, but to me the obvious thing to do here would be:

lemma card_two {sup : finset } {H : 2  sup.card} : finset.min' sup  finset.max' sup :=
mt (λ h, congr_fun h _) (ne_of_lt (finset.min'_lt_max'_of_card sup H))

view this post on Zulip Damiano Testa (Sep 21 2020 at 07:49):

@Bhavik Mehta I would like this to be easy, but using your approach, I get the following error:

expected type:
sup: finset 
H: 2  sup.card
 sup.min'  sup.max'
Messages (2)
mwe.lean:4:21
don't know how to synthesize placeholder
context:
sup : finset ,
H : 2  sup.card
 sup.nonempty
mwe.lean:4:35
type mismatch at application
  sup.min'_lt_max'_of_card H
term
  H
has type
  2  sup.card
but is expected to have type
  sup.nonempty
Additional information:
/home/damiano/Matematica/Lean/Chevalley01/mwe.lean:4:35: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    ?m_3.min'_lt_max'_of_card ?m_4
  has type
    1 < ?m_2.card  ?m_2.min' ?m_4 < ?m_2.max' ?m_4
  but is expected to have type
    sup.min' ?m_1 < sup.max' ?m_1

(the underlined bits are the underscore in congr_fun h _and finset)

view this post on Zulip Kyle Miller (Sep 21 2020 at 07:56):

(deleted)

view this post on Zulip Kyle Miller (Sep 21 2020 at 07:57):

(deleted)

view this post on Zulip Shing Tak Lam (Sep 21 2020 at 08:00):

@Damiano Testa What Bhavik posted works for me. finset.min'_lt_max'_of_card was changed 15 days ago (#4020), so maybe you need to update mathlib?

view this post on Zulip Kyle Miller (Sep 21 2020 at 08:03):

(Scratch what I said. I wasn't paying attention to what was going on.)

view this post on Zulip Damiano Testa (Sep 21 2020 at 10:09):

Shing Tak Lam said:

Damiano Testa What Bhavik posted works for me. finset.min'_lt_max'_of_card was changed 15 days ago (#4020), so maybe you need to update mathlib?

Thanks: after downloading the new version of mathlib, it works!


Last updated: May 10 2021 at 00:31 UTC