set is a complete lattice

Stream: general

[Kenny Lau]

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

[Kenny Lau]

I win

[Gabriel Ebner]

I guess Sup and Inf are defined differently now?

[Kenny Lau]

really?

[Gabriel Ebner]

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

[Kenny Lau]

well one could prove that they are equal

[Kenny Lau]

simp lemma

[Gabriel Ebner]

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.

[Kenny Lau]

I see

[Kevin Buzzard]

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

[Kenny Lau]

such as?

[Kevin Buzzard]

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

[Chris Hughes]

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

[Johannes Hölzl]

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.