Zulip Chat Archive

Stream: new members

Topic: partition basics


Iocta (Aug 04 2020 at 20:52):

I want to do a few exercises with partitions, such as to show that {{a}, {b}, {c}} <= {{a, b}, {c}}. I think first step is to show that each of those are partitions, which means first showing they're setoids. I can do that manually but maybe there's another way?

import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import data.fintype.basic

inductive thing : Type
| a : thing
| b : thing
| c : thing


open thing


def s : setoid thing :=
setoid.mk_classes {{a}, {b}, {c}} _
/-
don't know how to synthesize placeholder
context:
⊢ ∀ (a : thing), ∃! (b : set thing) (H : b ∈ {{a}, {b}, {c}}), a ∈ b -/

Iocta (Aug 04 2020 at 21:12):

Actually I don't know how to do that manually.

Iocta (Aug 04 2020 at 21:33):

def s : setoid thing :=
setoid.mk_classes {{a}, {b}, {c}}
begin
intro x,
use {b},
-- x : thing
-- ⊢ (λ (b : set thing), ∃! (H : b ∈ {{a}, {b}, {c}}), x ∈ b) {b} ∧ ∀ (y : set thing), (λ (b : set thing), ∃! (H : b ∈ {{a}, {b}, {c}}), x ∈ b) y → y = {b}
end

That can't be right

Kevin Buzzard (Aug 04 2020 at 21:37):

Why would you expect {b} to work for any x? Why not use {x}?

Iocta (Aug 04 2020 at 21:38):

Yeah fair enough

Iocta (Aug 04 2020 at 21:38):

but the state after that is ⊢ (λ (b : set thing), ∃! (H : b ∈ {{a}, {b}, {c}}), x ∈ b) {x} ∧ ∀ (y : set thing), (λ (b : set thing), ∃! (H : b ∈ {{a}, {b}, {c}}), x ∈ b) y → y = {x} which I can barely even parse

Kevin Buzzard (Aug 04 2020 at 21:45):

Well it's what you've got to prove. Try simp.

Iocta (Aug 04 2020 at 22:04):

def s : setoid thing :=
setoid.mk_classes {{a}, {b}, {c}}
begin
intro x,
use {x},
simp,
split,
{
    cases x,
    { exact or.inl rfl },
    { exact or.inr (or.inl rfl) },
    { exact or.inr (or.inr rfl) },
},
intro s,
{
    intros h hx,
    cases h,
    {
        have hxa: x = a, { finish },
        exact eq.trans h (congr_arg singleton (eq.symm hxa)),
    },
    {
        cases h,
        {
            have hxb: x = b, { finish },
            exact eq.trans h (congr_arg singleton (eq.symm hxb)),
        },
        {
            have hxc: x = c, { finish },
            exact eq.trans h (congr_arg singleton (eq.symm hxc)),
        },
    },
},
end

Kevin Buzzard (Aug 04 2020 at 22:08):

import data.setoid.partition
import tactic

inductive thing : Type
| a : thing
| b : thing
| c : thing


open thing


def s : setoid thing :=
setoid.mk_classes {{a}, {b}, {c}}
begin
  intro x,
  use {x},
  cases x;
  finish,
end

Iocta (Aug 04 2020 at 22:11):

ha

Iocta (Aug 04 2020 at 22:38):

This works, what would make it more stylish?

def set_partition (t : Type) : Type :=
{s : set (set t) | setoid.is_partition s}


def ab_connected (p: set_partition thing) : Prop :=
 s  p.val, thing.a  s  thing.b  s

example :  p p' : set_partition thing,  setoid.is_partition p.val   setoid.is_partition p'.val  p.val  p'.val 
(ab_connected p  ab_connected p'):=
begin
intros p p',
intros h pab,
cases h with hp h,
cases h with hp' h,
simp at h,
unfold ab_connected at *,
cases pab with s pab,
cases pab with hs pab,
tauto,
end

Iocta (Aug 04 2020 at 22:43):

For example, I don't yet have a feel for when I want \forall vs left-of-colon, or when to use \and vs \to.

Iocta (Aug 04 2020 at 22:46):

example :  p p' : set_partition thing,  setoid.is_partition p.val   setoid.is_partition p'.val  p.val  p'.val 
(ab_connected p  ab_connected p'):=
begin
intros p p',
intros h pab,
rcases h with  hp , hp', h ,
unfold ab_connected at *,
tauto,
end

Kevin Buzzard (Aug 04 2020 at 22:46):

The argument for putting as much as you can left-of-colon is that it doesn't make theorem statements any longer, but it makes proofs shorter because you don't need to write intro as much. The \and v \to thing is not the same though -- they mean different things. It's a bit confusing because (P and Q) -> R is the same as P -> (Q -> R) so here they're playing a similar role (and in this situation you should use -> not and, because functional programming is easier that way). However in general and and to just mean different things so you should use the one which is logically correct

Iocta (Aug 04 2020 at 22:50):

example
(p p' : set_partition thing)
(hp: setoid.is_partition p.val)
(hp': setoid.is_partition p'.val)
(h: p.val  p'.val)
(pab: ab_connected p) :
ab_connected p':=
begin
unfold ab_connected at *,
tauto,
end

Iocta (Aug 05 2020 at 01:10):

Trying to do it more generically using is_monotone. How can I use h to fill the sorrys? I can't even figure out how to do the equivalent of unfold has_le at h.

import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import data.fintype.basic


variables {X Y: Type}

inductive thing : Type
| a : thing
| b : thing
| c : thing


open thing


def set_partition (t : Type) : Type :=
{s : set (set t) | setoid.is_partition s}


def ab_connected (p: set_partition thing) : Prop :=
 s  p.val, thing.a  s  thing.b  s


def is_monotone [preorder X] [preorder Y] (f : X  Y) : Prop :=
  x1 x2 : X, x1  x2  f x1  f x2


example [preorder (set_partition thing) ]: is_monotone ab_connected :=
begin
intros p p' h,
unfold ab_connected at *,
simp * at *,
intros h',
rcases h' with  s , hsp, ha, hb ,
have:  s'  p'.val, a  s',
{

-- _inst_1 : preorder (set_partition thing)
-- pp' : set_partition thing
-- h : p ≤ p'
-- s : set thing
-- hsp : s ∈ ↑p
-- ha : a ∈ s
-- hb : b ∈ s
-- ⊢ ∃ (s' : set thing) (H : s' ∈ p'.val), a ∈ s'
sorry,
},
cases this with s' hs',
use s',
split,
{ finish },
{
    split,
    {
        finish,
    },
    {
        cases hs' with hs' as',
--         _inst_1 : preorder (set_partition thing)
-- pp' : set_partition thing
-- h : p ≤ p'
-- s : set thing
-- hsp : s ∈ ↑p
-- ha : a ∈ s
-- hb : b ∈ s
-- s' : set thing
-- hs' : s' ∈ p'.val
-- as' : a ∈ s'
-- ⊢ b ∈ s'
        sorry,
    },
},
end

Bryan Gin-ge Chen (Aug 05 2020 at 01:20):

I don't think this is provable without adding some more assumptions on the preorder on set_partition thing. For example, just because p ≤ p' in your arbitrary preorder, that doesn't necessarily give you any way to prove s' ∈ p'.val from s ∈ ↑p.

Iocta (Aug 05 2020 at 01:51):

How do I express the same assumptions as in the prior version above?

Reid Barton (Aug 05 2020 at 02:02):

I'm guessing you didn't prove what you thought you were proving

Iocta (Aug 05 2020 at 02:04):

Sounds plausible, what do you have in mind?

Reid Barton (Aug 05 2020 at 02:04):

before, you wrote p.val ≤ p'.val where p.val : set (set thing)

Iocta (Aug 05 2020 at 02:07):

you're right :-/

Iocta (Aug 05 2020 at 07:50):

The order relation that I want is "finer is lesser". Is that the one that's built into partition? How do I get set_partition thing to inherit that ordering?

Kevin Buzzard (Aug 05 2020 at 08:05):

You can use partial_order.lift

Kenny Lau (Aug 05 2020 at 08:31):

import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import data.fintype.basic

variables (α β : Type*)

inductive thing : Type
| a : thing
| b : thing
| c : thing

open thing

def set_partition : Type* :=
{s : set (set α) // setoid.is_partition s}

namespace set_partition

instance : partial_order (set_partition α) :=
setoid.partition.partial_order

instance : complete_lattice (set_partition α) :=
setoid.partition.complete_lattice

def ab_connected (p : set_partition thing) : Prop :=
 s  p.val, thing.a  s  thing.b  s

lemma ab_connected_of_le (p p' : set_partition thing) (h : p  p')
  (hp : ab_connected p) : ab_connected p':=
begin
  sorry
end

end set_partition

Iocta (Aug 05 2020 at 08:35):

What does // do vs |?

Kevin Buzzard (Aug 05 2020 at 08:37):

Makes a type not a term

Iocta (Aug 05 2020 at 08:38):

def set_partition (t : Type) : Type :=
{s : set (set t) | setoid.is_partition s}

doesn't make a type?

Iocta (Aug 05 2020 at 08:38):

well, function for generating types

Kenny Lau (Aug 05 2020 at 08:38):

well it makes a set, which Lean knows how to coerce to type

Kenny Lau (Aug 05 2020 at 08:38):

the results are defeq

Kenny Lau (Aug 05 2020 at 08:40):

I have to say, the API of partition in the file is very incomplete

Iocta (Aug 05 2020 at 08:40):

but we pick // for clarity I guess

Iocta (Aug 05 2020 at 08:41):

if I understood you right, using | would have the same result in this case

Kenny Lau (Aug 05 2020 at 08:49):

yes

Kevin Buzzard (Aug 05 2020 at 08:57):

Except you'd get little arrows everywhere

Iocta (Aug 05 2020 at 09:18):

Can I unfold that h so I can see what I'm actually working with?

Kenny Lau (Aug 05 2020 at 09:18):

there's the have := @h trick

Kenny Lau (Aug 05 2020 at 09:19):

to make its arguments explicit

Iocta (Aug 05 2020 at 09:19):

doesn't help

Kenny Lau (Aug 05 2020 at 09:25):

begin
  have := @h,
end

Kenny Lau (Aug 05 2020 at 09:25):

?

Iocta (Aug 05 2020 at 09:26):

pp' : set_partition thing
h : p  p'
hp : p.ab_connected
this : p  p'
 p'.ab_connected

Kenny Lau (Aug 05 2020 at 09:28):

oh well

Iocta (Aug 05 2020 at 09:28):

also been wondering why is there no space between p and p'

Kenny Lau (Aug 05 2020 at 09:28):

how about have := @h _

Kenny Lau (Aug 05 2020 at 09:28):

oh I think that's a bug

Iocta (Aug 05 2020 at 09:28):

this :  y : thing⦄, (setoid.mk_classes p.val _).rel ?m_1 y  (setoid.mk_classes p'.val _).rel ?m_1 y

Iocta (Aug 05 2020 at 19:59):

I think I need to use h here but I can't figure out how to apply it.

import data.set.basic
import data.set.lattice
import data.setoid.partition
import order.filter.basic
import tactic.basic
import tactic
import data.fintype.basic

variables (α β : Type*)

inductive thing : Type
| a : thing
| b : thing
| c : thing

open thing

def set_partition : Type* :=
{s : set (set α) // setoid.is_partition s}

namespace set_partition

instance : partial_order (set_partition α) :=
setoid.partition.partial_order

instance : complete_lattice (set_partition α) :=
setoid.partition.complete_lattice

def ab_connected (p : set_partition thing) : Prop :=
 s  p.val, thing.a  s  thing.b  s

lemma ab_connected_of_le (p p' : set_partition thing) (h : p  p')
  (hp : ab_connected p) : ab_connected p':=
begin
rcases hp with  s, hs, ha, hb ,
unfold ab_connected,
have hs' :  s' : set thing, s'  p'.val  a  s',
{
    have := p'.2,
    unfold setoid.is_partition at this,
    cases this with hne hpart',
    specialize hpart' a,
    cases hpart' with s' hs',
    simp at hs',
    use s',
    apply hs'.1,
},
{
    cases hs' with s' hs',
    use s',
    split,
    {  apply hs'.1  },
    {
        split,
        {  apply hs'.2 },
        {
            show b  s',
            -- pp' : set_partition thing
            -- h : p ≤ p'
            -- s : set thing
            -- hs : s ∈ p.val
            -- ha : a ∈ s
            -- hb : b ∈ s
            -- s' : set thing
            -- hs' : s' ∈ p'.val ∧ a ∈ s'
            -- ⊢ b ∈ s'
            sorry,
        },
    },
},
end

end set_partition

Iocta (Aug 05 2020 at 22:25):

h means p <= p' which means p is finer than p', which means whenever a and b are in the same part of p, then a and b are in the same part of p'. That's exactly the thing I need, but I can' t see how to actually use h, aka this.

Kevin Buzzard (Aug 05 2020 at 22:36):

apply h _ _ hs'.1 hs'.2,

?

Iocta (Aug 05 2020 at 22:37):

that does something, I'll fiddle with it

Kenny Lau (Aug 06 2020 at 08:43):

as I said, the API for partition is really lacking

Kyle Miller (Nov 14 2021 at 00:39):

It only excludes S from containing the empty set -- it still allows S itself to be empty.

Arthur Paulino (Nov 14 2021 at 00:40):

Hmm, do you think it could have some issue with non-used colors?

Arthur Paulino (Nov 14 2021 at 00:42):

(when mapping colorings to partitions and vice-versa)

Yaël Dillies (Nov 14 2021 at 00:48):

My use case for is_antichain was branch#combinatorics, but yes I definitely had independent sets in mind.

Kevin Buzzard (Nov 14 2021 at 00:53):

The definition of partition is precisely to make "equivalence relations on X = partitions of X" true.

Kyle Miller (Nov 14 2021 at 00:57):

Arthur Paulino said:

Hmm, do you think it could have some issue with non-used colors?

This is ok if we use the coloring function to partition the vertices, since empty sets won't turn up. I think it's (setoid.ker C).classes. Then there's docs#setoid.is_partition_classes


Last updated: Dec 20 2023 at 11:08 UTC