has_mem (DCPOs)

Stream: new members

[Aram Bingham]

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!

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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⟩

[Bryan Gin-ge Chen]

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)⟩

[Aram Bingham]

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?

[Bryan Gin-ge Chen]

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.

[Aram Bingham]

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

[Aram Bingham]

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 \to \alpha$ of a chain $c$. 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?

[Aram Bingham]

nvm, I think I got around it by defining

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

[Aram Bingham]

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...

[Mario Carneiro]

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

[Mario Carneiro]

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

[Aram Bingham]

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