Zulip Chat Archive

Stream: new members

Topic: Need help on proving {1,2,3} and P{1,2,3} are nontrivial


view this post on Zulip Lars Ericson (Dec 13 2020 at 01:08):

Proving that fin 3 is nontrivial works out of the box:

import data.finset.basic
example : nontrivial (fin 3) := fin.nontrivial

However, taking the powerset doesn't work: 𝒫 (fin 3)

So I need to change representations to

def X : set  := ({1, 2, 3} : finset )

But then I'm not sure of a couple of things:

  • How do I construct emptyset and top
  • How do I use those constructed objects in a proof

I am stuck on that and sorry here:

import data.finset.basic
def X : set  := ({1, 2, 3} : finset )
lemma is_nontrivial_X :  (x y : X), x  y := sorry

I have looked at library_search! which has no suggestions and output of suggest and hint which put out some ideas but haven't worked for me so far.

I'm also stuck for powerset. Here I've got 3 ideas and I don't know how to make them work:

import data.finset.basic
def X : set  := ({1, 2, 3} : finset )
lemma empty_in_PX : (  (𝒫 X)) := sorry
lemma top_in_PX : (  (𝒫 X)) := sorry
lemma is_nontrivial_PX :  (x y : 𝒫 X), x  y := sorry
instance : nontrivial (𝒫 X) := { exists_pair_ne := is_nontrivial_PX }

Any help greatly appreciated.

view this post on Zulip Yakov Pechersky (Dec 13 2020 at 01:17):

Why do you need that powerset?

view this post on Zulip Yakov Pechersky (Dec 13 2020 at 01:18):

The number of unique terms of "set (fin 3)" is the cardinality of that powerset

view this post on Zulip Alex J. Best (Dec 13 2020 at 02:29):

Nontrivial takes a type as input, not a set so it inserts a coercion which you may not want.
If all the elements you ever want to consider are 1,2,3 I'd recommend starting with fin 3 rather than making subsets of sets, you can just work with set (fin 3) more naturally in lean

def X : set  := ({1, 2, 3} : finset )

lemma empty_mem_powerset :   𝒫 X := by simp
lemma top_in_PX : (  (𝒫 X)) := sorry -- this is false ⊤ is the set of all naturals which is not a subset of X
lemma is_nontrivial_PX :  (x  𝒫 X) (y   𝒫 X), x  y :=  {1}, by simp [X], , empty_mem_powerset, begin intros h, exact set.eq_empty_iff_forall_not_mem.mp h 1 rfl, end 
instance : nontrivial (𝒫 X) := { exists_pair_ne := begin simp,rcases is_nontrivial_PX with x , hx, y, hy, h⟩, use [x, hx, y, hy],  end }

view this post on Zulip Lars Ericson (Dec 13 2020 at 02:32):

Thanks I will try set X . I got it in my head I needed 𝒫 X but that's incorrect.

view this post on Zulip Lars Ericson (Dec 13 2020 at 02:45):

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
  refine nontrivial_of_ne _ _ _,
  exact set.univ,
  exact  ,
  exact set.empty_ne_univ.symm,
end

view this post on Zulip Eric Wieser (Dec 13 2020 at 08:21):

Does unfold X, apply_instance work for the second?

view this post on Zulip Lars Ericson (Dec 13 2020 at 14:36):

Yes

import data.finset.basic
def X := fin 3

instance : nontrivial (set X) :=
begin
  unfold X,
  apply_instance
end

view this post on Zulip Damiano Testa (Dec 14 2020 at 06:37):

Lars Ericson said:

DONE (most of the work done by library_search!)

import data.finset.basic
def X := fin 3

instance : nontrivial X := fin.nontrivial

instance : nontrivial (set X) :=
begin
  refine nontrivial_of_ne _ _ _,
  exact set.univ,
  exact  ,
  exact set.empty_ne_univ.symm,
end

As far as I understand, the three exact after the refine fill in the underscores. Thus, also refine nontrivial_of_ne set.univ ∅ set.empty_ne_univ.symm, finishes the goal. At this point, you can notice that the last underscore is filled in with a proof that ∅ ≠ set.univ, so just this is enough for Lean to figure out what the two sets in question were. Hence, refine nontrivial_of_ne _ _ set.empty_ne_univ.symm,is sufficient information to create a proof. Once you are here, you no longer need tactic mode:

instance : nontrivial (set X) := nontrivial_of_ne _ _ set.empty_ne_univ.symm

Last updated: May 10 2021 at 00:31 UTC