Zulip Chat Archive

Stream: new members

Topic: has_mem (DCPOs)


view this post on Zulip Aram Bingham (Nov 22 2020 at 07:39):

I'm trying to define DCPOs and I'm sure I'm doing a zillion things wrong but mostly I don't understand the behavior of has_mem, which seems to be needed somehow in part of my code. I see has_mem is in a lot of other mathlib files used for defining things like subgroups, subrings with lines like instance : has_mem G (subgroup G) := ⟨λ m K, m ∈ (K : set G)⟩ which I have tried to mimic but I can't get this message to go away:

failed to synthesize type class instance for
α : Type u,
β : Type v,
P : Type u_1,
K : Type u_2,
P : Type,
to_partial_order : partial_order P,
to_has_sup : has_sup P,
le : (λ {α : Type} (c : partial_order α), α  α  Prop) to_partial_order := partial_order.le,
lt : (λ {α : Type} (c : partial_order α), α  α  Prop) to_partial_order := partial_order.lt,
le_refl : (λ {α : Type} (c : partial_order α),  (a : α), a  a) to_partial_order := partial_order.le_refl,
le_trans : (λ {α : Type} (c : partial_order α),  (a b c_1 : α), a  b  b  c_1  a  c_1)
  to_partial_order :=
  partial_order.le_trans,
lt_iff_le_not_le : (λ {α : Type} (c : partial_order α),
   auto_param ( (a b : α), a < b  a  b  ¬b  a) (name.mk_string "order_laws_tac" name.anonymous))
  to_partial_order :=
  partial_order.lt_iff_le_not_le,
le_antisymm : (λ {α : Type} (c : partial_order α),  (a b : α), a  b  b  a  a = b) to_partial_order :=
  partial_order.le_antisymm,
sup : (λ {P : Type} {_inst_1 : partial_order P} (c : has_sup P), dset P  P) to_has_sup := has_sup.sup,
D : dset P,
x : P
 has_mem P (dset P)

I guess I don't really know why all those other mathlib files need this has_mem instance, or why it's showing up in my infoview. Here's roughly what I have so far.

structure dset (P:Type) [partial_order P]:=
    (D: set P )
    (is_directed {x y : P}: ((x  D)  (y  D))  (z  D, x  z  y  z))
class has_sup (P : Type) [partial_order P] := (sup: dset P  P )

class dcpo (P : Type) extends partial_order P, has_sup P:=
    (le_sup  :  D : dset P,  x  D, x  sup D)

Any help would be appreciated!

view this post on Zulip Bryan Gin-ge Chen (Nov 22 2020 at 07:48):

has_mem is a notation type class associated to the symbol . To provide a has_mem P (dset P) instance, you need to supply a function of type P → dset P → Prop.

view this post on Zulip Bryan Gin-ge Chen (Nov 22 2020 at 07:51):

I'm guessing something like the following is what you want:

instance (P : Type) [partial_order P] : has_mem P (dset P) := λ x dP, x  dP.D

view this post on Zulip Bryan Gin-ge Chen (Nov 22 2020 at 07:55):

It might end up being more convenient to first provide a coercion from dset P to set P, like so:

instance (P : Type) [partial_order P] : has_coe (dset P) (set P) := dset.D
instance (P : Type) [partial_order P] : has_mem P (dset P) := λ x dP, x  (dP : set P)⟩

view this post on Zulip Aram Bingham (Nov 22 2020 at 08:02):

ahhh ok thank you this works! so is the idea that i have to tell lean what it means for terms of type P to be in a directed set by coercing dsets to be sets
and then the symbol \in makes sense?

view this post on Zulip Bryan Gin-ge Chen (Nov 22 2020 at 08:05):

An instance of has_mem tells Lean what should mean, and the instance of has_coe (dset P) (set P) tells Lean how to coerce something of type dset P to type set P. That's used in the expression (dP : set P) in the second has_mem instance I defined above.

view this post on Zulip Aram Bingham (Nov 22 2020 at 08:07):

Gotcha this is making much more sense now, thank you!

view this post on Zulip Aram Bingham (Nov 22 2020 at 19:53):

OK so now I'm trying to show that DCPOs are also ω\omega-CPOs. To do this, I want to be able to coerce chains into directed sets and I'm trying to do this in stages by first defining the set that is the image of the underlying function Nα \N \to \alpha of a chain cc. Something is not type-checking with the first part already

instance : has_coe_to_fun (chain P) :=
@infer_instance (has_coe_to_fun $  →ₘ P) _

def has_coe_to_dset (c: chain P) : dset P :=
    {D:= set.image has_coe_to_fun c,
     is_directed:= sorry}

where I get the error

type mismatch at application
  has_coe_to_fun c
term
  c
has type
  chain P : Type u_1
but is expected to have type
  Sort ? : Type ?

I don't have a great grasp of what this means, but when I go to the mathlib file omega_complete_partial_order and try to check the same thing with #check has_coe_to_fun c I get a very similar error. What's going wrong?

view this post on Zulip Aram Bingham (Nov 22 2020 at 20:23):

nvm, I think I got around it by defining

def chain_image (c: chain P) : set P :=
    {p |  n, c n = p}

view this post on Zulip Aram Bingham (Nov 22 2020 at 23:26):

OK, i've been able to show that chains give directed sets, now I think it makes sense to create an ω\omega-CPO as an instance of a DCPO but having a new trouble

instance (P:Type*) [dcpo P] : ωcpo P:=
    { ωsup:= sorry,
      le_ωsup:= sorry,
      ωsup_le:= sorry,
}

gives the error
invalid definition, a declaration named 'ωcpo' has already been declared
I assume I have bad syntax somewhere but I was just trying to copy examples from lftcm2020 so I'm not sure where...

view this post on Zulip Mario Carneiro (Nov 22 2020 at 23:28):

You should name the instance if it doesn't get a good name

view this post on Zulip Mario Carneiro (Nov 22 2020 at 23:29):

instance dcpo.to_ωcpo (P : Type*) [dcpo P] : ωcpo P :=

view this post on Zulip Aram Bingham (Nov 22 2020 at 23:33):

aha! thank you, so it was that the instance was trying to take on the name ωcpo by default ?


Last updated: May 06 2021 at 21:09 UTC