Zulip Chat Archive

Stream: new members

Topic: Composition with metavariable


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

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 02:22):

#mwe ?

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

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

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

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:32):

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

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

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:34):

partitions were in data.setoid.

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 02:36):

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

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:36):

As {s // is_partition s}.

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:39):

There were a few minor changes, see #2853

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