Composition with metavariable

Stream: new members

[Brandon Brown]

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?

[Bryan Gin-ge Chen]

#mwe ?

[Brandon Brown]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Bryan Gin-ge Chen]

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]

partitions were in data.setoid.

[Bryan Gin-ge Chen]

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

[Yury G. Kudryashov]

As {s // is_partition s}.

[Yury G. Kudryashov]

There were a few minor changes, see #2853

[Brandon Brown]

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