Zulip Chat Archive

Stream: general

Topic: set is a complete lattice


view this post on Zulip Kenny Lau (Apr 13 2018 at 14:57):

mathlib proof:

instance lattice_set : complete_lattice (set α) :=
{ lattice.complete_lattice .
  le           := (⊆),
  le_refl      := subset.refl,
  le_trans     := assume a b c, subset.trans,
  le_antisymm  := assume a b, subset.antisymm,

  lt           := λ x y, x ⊆ y ∧ ¬ y ⊆ x,
  lt_iff_le_not_le := λ x y, iff.refl _,

  sup          := (∪),
  le_sup_left  := subset_union_left,
  le_sup_right := subset_union_right,
  sup_le       := assume a b c, union_subset,

  inf          := (∩),
  inf_le_left  := inter_subset_left,
  inf_le_right := inter_subset_right,
  le_inf       := assume a b c, subset_inter,

  top          := {a | true },
  le_top       := assume s a h, trivial,

  bot          := ∅,
  bot_le       := assume s a, false.elim,

  Sup          := λs, {a | ∃ t ∈ s, a ∈ t },
  le_Sup       := assume s t t_in a a_in, ⟨t, ⟨t_in, a_in⟩⟩,
  Sup_le       := assume s t h a ⟨t', ⟨t'_in, a_in⟩⟩, h t' t'_in a_in,

  Inf          := λs, {a | ∀ t ∈ s, a ∈ t },
  le_Inf       := assume s t h a a_in t' t'_in, h t' t'_in a_in,
  Inf_le       := assume s t t_in a h, h _ t_in }

my proof:

instance lattice_set : complete_lattice (set α) :=
lattice.complete_lattice_fun

view this post on Zulip Kenny Lau (Apr 13 2018 at 14:57):

I win

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 15:03):

I guess Sup and Inf are defined differently now?

view this post on Zulip Kenny Lau (Apr 13 2018 at 15:04):

really?

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 15:12):

They should be equal. However I don't think they are definitionally equal. Sup s a = (∃ b ∈ set.image (λ f, f a) s, b) = (∃ b, (∃ c, s c ∧ s c a = b) → b) which is different

view this post on Zulip Kenny Lau (Apr 13 2018 at 15:13):

well one could prove that they are equal

view this post on Zulip Kenny Lau (Apr 13 2018 at 15:13):

simp lemma

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 15:15):

This still doesn't give you definitional reduction. If you want to prove a ∈ Sup s, you'll now always need to simp first. There are quite a few places where we accept some additional complexity in order to guarantee good definitional reduction, the lt in preorder is another place. We can define lt in terms of le, but we want it to reduce differently for natural numbers.

view this post on Zulip Kenny Lau (Apr 13 2018 at 15:15):

I see

view this post on Zulip Kevin Buzzard (Apr 13 2018 at 15:29):

Yes, for nat, a<b is _defined_ to be succ a <= b and if you know this you can write some neat obfuscated code :-)

view this post on Zulip Kenny Lau (Apr 13 2018 at 15:29):

such as?

view this post on Zulip Kevin Buzzard (Apr 13 2018 at 15:30):

I believe I used this to do some golf question here a week or two ago. Either a question of Chris or of Nima.

view this post on Zulip Chris Hughes (Apr 13 2018 at 15:37):

It just means that you never have to use the lemma succ_le_of_lt

view this post on Zulip Johannes Hölzl (Apr 13 2018 at 15:44):

you can match or use the equation compiler to do case analysis and inductionon <, with the definition following the default setup this would be not possible.


Last updated: May 14 2021 at 03:27 UTC