## 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}?

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


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)

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

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

doesn't help

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

begin
have := @h,
end


?

#### Iocta (Aug 05 2020 at 09:26):

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


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

Last updated: May 11 2021 at 13:22 UTC