## Stream: new members

### Topic: Composition with metavariable

#### Brandon Brown (Jun 01 2020 at 02:20):

I have two functions F : setoid ?M_1 → partition ?M_1 and G : partition ?M_1 → setoid ?M_1 and I want to prove function.left_inverse G F or that (G ∘ F) = id . If I do #check function.left_inverse G F I get Prop which is what I expect, but if I try to prove this e.g. example : function.left_inverse G F I get an error don't know how to synthesize placeholder. Which I think is due to the metavariables since setoid and partition are not referring to particular types yet. What is the proper way to do this with these kind of functions?

#mwe ?

#### Brandon Brown (Jun 01 2020 at 02:24):

import data.setoid
import data.equiv.basic
open set
open setoid

structure partition (X : Type*) :=
(F : set (set X))
(disjoint : ∀ A B ∈ F, A ≠ B → A ∩ B = ∅)
(cover : ∀ x : X, ∃ A ∈ F, x ∈ A)
(nonempty : ∀ A ∈ F, A ≠ ∅)

def F {X : Type*} (S : setoid X) : partition X :=
partition.mk
(
classes S
)
( -- ⊢ (disjoint : ∀ A B ∈ ℱ, A ≠ B → A ∩ B = ∅)
begin
intros,
apply eq_of_subset_of_subset,
{
intro x,
intros,
rw mem_empty_eq,
apply a,
cases a_1,
--have F : set (set X), from classes S,
apply eq_of_mem_classes,
repeat {assumption},
},
{
apply set.empty_subset,
}
end
)
( -- ⊢ (cover : ∀ x : X, ∃ A ∈ ℱ, x ∈ A)
begin
intros,
split,
use x,
simp,
end
)
( -- ⊢ (nonempty : ∀ A ∈ ℱ, A ≠ ∅)
begin
intros,
intro aqn,
apply empty_not_mem_classes,
rwa ← aqn,
end
)
#check F

/-
Q3 : now define a map the other way
-/

def G {X : Type*} (P : partition X) : setoid X :=
begin
intros,
apply setoid.setoid_of_disjoint_union,
swap 3,
exact P.F,
apply eq_of_subset_of_subset,
intro p1,
intros,
trivial,
intro p1,
intros,
dsimp at *,
apply P.cover,
unfold set.pairwise_disjoint,
unfold set.pairwise_on,
intros,
unfold disjoint,
have z : x ∩ y = ∅, apply P.disjoint,
repeat {assumption},
finish,
end

#check function.left_inverse G F -- Prop
example : function.left_inverse G F := sorry --error


#### Yury G. Kudryashov (Jun 01 2020 at 02:31):

You need to explicitly provide one of the types: function.left_inverse (G : partition X → setoid X) F.

#### Yury G. Kudryashov (Jun 01 2020 at 02:32):

Otherwise Lean doesn't know that G takes partition X and not partition Y or partition nat.

#### Yury G. Kudryashov (Jun 01 2020 at 02:32):

BTW, we have this equivalence in mathlib, see data/setoid/partition.

#### Bryan Gin-ge Chen (Jun 01 2020 at 02:33):

You may have to update mathlib first, since I see from the code you posted that you're importing data.setoid which was split up a few days ago.

#### Yury G. Kudryashov (Jun 01 2020 at 02:34):

partitions were in data.setoid.

#### Bryan Gin-ge Chen (Jun 01 2020 at 02:36):

Yeah, I guess the code was just moved, not changed.

#### Yury G. Kudryashov (Jun 01 2020 at 02:36):

As {s // is_partition s}.

#### Yury G. Kudryashov (Jun 01 2020 at 02:39):

There were a few minor changes, see #2853

#### Brandon Brown (Jun 01 2020 at 11:03):

I see, thanks! And I'm just doing this for practice which is why I'm not just using the mathlib version.

Last updated: May 12 2021 at 04:19 UTC