Zulip Chat Archive

Stream: maths

Topic: I still don't understand how to use extends


view this post on Zulip Bhavik Mehta (Sep 30 2020 at 21:02):

import order.preorder_hom

structure subset_system :=
(to_fun : Π (α : Type*) [partial_order α], set (set α))
(sings :  (α : Type*) [partial_order α] (a : α), {a}  to_fun α)
(mono :  {α β : Type*} [partial_order α] [partial_order β] (f : α →ₘ β) {S : set α}, S  to_fun α  f '' S  to_fun β)

instance : has_coe_to_fun subset_system :=
{ F := _, coe := subset_system.to_fun }

variable (Z : subset_system)

set_option old_structure_cmd true

class complete (α : Type*) extends partial_order α :=
(sup : Π (S : set α), S  Z α  α)
(is_sup :  (S : set α), (S  Z α)  is_lub S (sup S _›))

variables {α : Type*} [partial_order α]

def ideal (α : Type*) [partial_order α] : Type* := {S : set α //  (x  S) (y  x), y  S}.

-- TODO: make this a complete lattice
instance : partial_order (ideal α) := subtype.partial_order _

structure union_complete (Z : subset_system) extends complete Z (ideal α) :=
(h :  (S : set (ideal α)) (H : S  Z (ideal α)), complete.sup S H = _)

Here's the error:

type mismatch at application
  complete.sup S H
term
  H
has type
  S  Z (@ideal α _inst_1) (@ideal.partial_order α _inst_1)
but is expected to have type
  S  Z (@ideal α _inst_1) (@complete.to_partial_order Z (@ideal α _inst_1) zcomp)

I'm getting errors like this, and they're happening because Lean can't match up the two partial order instances in the last argument of Z.
The only thing I can think of is to change complete to not use extends, but then I can't use bundled to make the category of complete things. I think what I want is for the partial_order instance inside of zcomp to be the one inferred rather than a new one, is there a nice way to fix this?

view this post on Zulip Kyle Miller (Sep 30 2020 at 21:20):

Does subset_system need all those partial_order arguments? If you do

structure subset_system :=
(to_fun : Π (α : Type*), set (set α))
(sings :  (α : Type*) (a : α), {a}  to_fun α)
(mono :  {α β : Type*} [partial_order α] [partial_order β] (f : α →ₘ β) {S : set α}, S  to_fun α  f '' S  to_fun β)

the errors go away.

(Should union_complete be a class?)

view this post on Zulip Bhavik Mehta (Sep 30 2020 at 21:22):

One of my cases is

open omega_complete_partial_order
def omega_chain : subset_system :=
{ to_fun := λ α I S, by exactI ( (c : chain α), set.range c = S),
  sings := λ α I a, by exactI preorder_hom.const _ a, by { ext, simp [eq_comm] }⟩,
  mono := λ α β   f S hS,
  begin
    rcases hS with S, rfl⟩,
    exactI chain.map S f, by { ext, simp }⟩,
  end }
end

where there does need to be the partial_order instance, unless I change it so that to_fun gives junk values if there's no partial order available

view this post on Zulip Bhavik Mehta (Sep 30 2020 at 21:22):

As for making union_complete a class; possibly but that doesn't fix any of the problems

view this post on Zulip Kyle Miller (Sep 30 2020 at 21:25):

I noticed that removing set_option old_structure_cmd true makes the error go away, too.

view this post on Zulip Bhavik Mehta (Sep 30 2020 at 21:26):

Agh that was my first guess of how to fix it but I thought I'd already got rid of them all! Thanks


Last updated: May 06 2021 at 18:20 UTC