partition basics

Stream: new members

[Iocta]

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]

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

[Iocta]

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]

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

[Iocta]

Yeah fair enough

[Iocta]

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]

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

[Iocta]

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]

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]

ha

[Iocta]

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]

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]

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]

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]

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]

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]

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]

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

[Reid Barton]

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

[Iocta]

Sounds plausible, what do you have in mind?

[Reid Barton]

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

[Iocta]

you're right :-/

[Iocta]

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]

You can use partial_order.lift

[Kenny Lau]

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]

What does // do vs |?

[Kevin Buzzard]

Makes a type not a term

[Iocta]

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

doesn't make a type?

[Iocta]

well, function for generating types

[Kenny Lau]

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

[Kenny Lau]

the results are defeq

[Kenny Lau]

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

[Iocta]

but we pick // for clarity I guess

[Iocta]

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

[Kenny Lau]

yes

[Kevin Buzzard]

Except you'd get little arrows everywhere

[Iocta]

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

[Kenny Lau]

there's the have := @h trick

[Kenny Lau]

to make its arguments explicit

[Iocta]

doesn't help

[Kenny Lau]

begin
  have := @h,
end

[Kenny Lau]

?

[Iocta]

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

[Kenny Lau]

oh well

[Iocta]

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

[Kenny Lau]

how about have := @h _

[Kenny Lau]

oh I think that's a bug

[Iocta]

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

[Iocta]

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]

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]

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

?

[Iocta]

that does something, I'll fiddle with it

[Kenny Lau]

as I said, the API for partition is really lacking

[Kyle Miller]

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

[Arthur Paulino]

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

[Arthur Paulino]

(when mapping colorings to partitions and vice-versa)

[Yaël Dillies]

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

[Kevin Buzzard]

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

[Kyle Miller]

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