Zulip Chat Archive

Stream: new members

Topic: partition basics


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

view this post on Zulip Iocta (Aug 04 2020 at 21:12):

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

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:37):

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

view this post on Zulip Iocta (Aug 04 2020 at 21:38):

Yeah fair enough

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:45):

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

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

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

view this post on Zulip Iocta (Aug 04 2020 at 22:11):

ha

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

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

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

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

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

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

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

view this post on Zulip Iocta (Aug 05 2020 at 01:51):

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

view this post on Zulip Reid Barton (Aug 05 2020 at 02:02):

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

view this post on Zulip Iocta (Aug 05 2020 at 02:04):

Sounds plausible, what do you have in mind?

view this post on Zulip Reid Barton (Aug 05 2020 at 02:04):

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

view this post on Zulip Iocta (Aug 05 2020 at 02:07):

you're right :-/

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 08:05):

You can use partial_order.lift

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

view this post on Zulip Iocta (Aug 05 2020 at 08:35):

What does // do vs |?

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 08:37):

Makes a type not a term

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

view this post on Zulip Iocta (Aug 05 2020 at 08:38):

well, function for generating types

view this post on Zulip Kenny Lau (Aug 05 2020 at 08:38):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 08:38):

the results are defeq

view this post on Zulip Kenny Lau (Aug 05 2020 at 08:40):

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

view this post on Zulip Iocta (Aug 05 2020 at 08:40):

but we pick // for clarity I guess

view this post on Zulip Iocta (Aug 05 2020 at 08:41):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 08:49):

yes

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 08:57):

Except you'd get little arrows everywhere

view this post on Zulip Iocta (Aug 05 2020 at 09:18):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:18):

there's the have := @h trick

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:19):

to make its arguments explicit

view this post on Zulip Iocta (Aug 05 2020 at 09:19):

doesn't help

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:25):

begin
  have := @h,
end

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:25):

?

view this post on Zulip Iocta (Aug 05 2020 at 09:26):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:28):

oh well

view this post on Zulip Iocta (Aug 05 2020 at 09:28):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:28):

how about have := @h _

view this post on Zulip Kenny Lau (Aug 05 2020 at 09:28):

oh I think that's a bug

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

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

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

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 22:36):

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

?

view this post on Zulip Iocta (Aug 05 2020 at 22:37):

that does something, I'll fiddle with it

view this post on Zulip Kenny Lau (Aug 06 2020 at 08:43):

as I said, the API for partition is really lacking


Last updated: May 11 2021 at 13:22 UTC