lean2/library/algebra/complete_lattice.lean
Floris van Doorn e5d5ef9d55 feat(hott/library): various changes and additions.
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
2016-03-03 10:13:20 -08:00

430 lines
14 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Complete lattices
TODO: define dual complete lattice and simplify proof of dual theorems.
-/
import algebra.lattice data.set.basic algebra.monotone
open set
variable {A : Type}
structure complete_lattice [class] (A : Type) extends lattice A :=
(Inf : set A → A)
(Sup : set A → A)
(Inf_le : ∀ {a : A} {s : set A}, a ∈ s → le (Inf s) a)
(le_Inf : ∀ {b : A} {s : set A}, (∀ (a : A), a ∈ s → le b a) → le b (Inf s))
(le_Sup : ∀ {a : A} {s : set A}, a ∈ s → le a (Sup s))
(Sup_le : ∀ {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → le a b), le (Sup s) b)
section
variable [complete_lattice A]
definition Inf (S : set A) : A := complete_lattice.Inf S
prefix `⨅ `:70 := Inf
definition Sup (S : set A) : A := complete_lattice.Sup S
prefix `⨆ `:65 := Sup
theorem Inf_le {a : A} {s : set A} (H : a ∈ s) : (Inf s) ≤ a := complete_lattice.Inf_le H
theorem le_Inf {b : A} {s : set A} (H : ∀ (a : A), a ∈ s → b ≤ a) : b ≤ Inf s :=
complete_lattice.le_Inf H
theorem le_Sup {a : A} {s : set A} (H : a ∈ s) : a ≤ Sup s := complete_lattice.le_Sup H
theorem Sup_le {b : A} {s : set A} (H : ∀ (a : A), a ∈ s → a ≤ b) : Sup s ≤ b :=
complete_lattice.Sup_le H
end
-- Minimal complete_lattice definition based just on Inf.
-- We later show that complete_lattice_Inf is a complete_lattice.
structure complete_lattice_Inf [class] (A : Type) extends weak_order A :=
(Inf : set A → A)
(Inf_le : ∀ {a : A} {s : set A}, a ∈ s → le (Inf s) a)
(le_Inf : ∀ {b : A} {s : set A}, (∀ (a : A), a ∈ s → le b a) → le b (Inf s))
-- Minimal complete_lattice definition based just on Sup.
-- We later show that complete_lattice_Sup is a complete_lattice.
structure complete_lattice_Sup [class] (A : Type) extends weak_order A :=
(Sup : set A → A)
(le_Sup : ∀ {a : A} {s : set A}, a ∈ s → le a (Sup s))
(Sup_le : ∀ {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → le a b), le (Sup s) b)
namespace complete_lattice_Inf
variable [C : complete_lattice_Inf A]
include C
definition Sup (s : set A) : A :=
Inf {b | ∀ a, a ∈ s → a ≤ b}
local prefix `⨅`:70 := Inf
local prefix `⨆`:65 := Sup
lemma le_Sup {a : A} {s : set A} : a ∈ s → a ≤ ⨆ s :=
suppose a ∈ s, le_Inf
(show ∀ (b : A), (∀ (a : A), a ∈ s → a ≤ b) → a ≤ b, from
take b, assume h, h a `a ∈ s`)
lemma Sup_le {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → a ≤ b) : ⨆ s ≤ b :=
Inf_le h
definition inf (a b : A) := ⨅ '{a, b}
definition sup (a b : A) := ⨆ '{a, b}
local infix `⊓` := inf
local infix `⊔` := sup
lemma inf_le_left (a b : A) : a ⊓ b ≤ a :=
Inf_le !mem_insert
lemma inf_le_right (a b : A) : a ⊓ b ≤ b :=
Inf_le (!mem_insert_of_mem !mem_insert)
lemma le_inf {a b c : A} : c ≤ a → c ≤ b → c ≤ a ⊓ b :=
assume h₁ h₂,
le_Inf (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, begin subst x, exact h₁ end)
(suppose x ∈ '{b},
have x = b, from !eq_of_mem_singleton this,
begin subst x, exact h₂ end))
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
le_Sup !mem_insert
lemma le_sup_right (a b : A) : b ≤ a ⊔ b :=
le_Sup (!mem_insert_of_mem !mem_insert)
lemma sup_le {a b c : A} : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
assume h₁ h₂,
Sup_le (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, by subst x; assumption)
(suppose x ∈ '{b},
have x = b, from !eq_of_mem_singleton this,
by subst x; assumption))
end complete_lattice_Inf
-- Every complete_lattice_Inf is a complete_lattice_Sup
definition complete_lattice_Inf_to_complete_lattice_Sup [C : complete_lattice_Inf A] :
complete_lattice_Sup A :=
⦃ complete_lattice_Sup, C ⦄
-- Every complete_lattice_Inf is a complete_lattice
definition complete_lattice_Inf_to_complete_lattice [trans_instance] [C : complete_lattice_Inf A] :
complete_lattice A :=
⦃ complete_lattice, C ⦄
namespace complete_lattice_Sup
variable [C : complete_lattice_Sup A]
include C
definition Inf (s : set A) : A :=
Sup {b | ∀ a, a ∈ s → b ≤ a}
lemma Inf_le {a : A} {s : set A} : a ∈ s → Inf s ≤ a :=
suppose a ∈ s, Sup_le
(show ∀ (b : A), (∀ (a : A), a ∈ s → b ≤ a) → b ≤ a, from
take b, assume h, h a `a ∈ s`)
lemma le_Inf {b : A} {s : set A} (h : ∀ (a : A), a ∈ s → b ≤ a) : b ≤ Inf s :=
le_Sup h
local prefix `⨅`:70 := Inf
local prefix `⨆`:65 := Sup
definition inf (a b : A) := ⨅ '{a, b}
definition sup (a b : A) := ⨆ '{a, b}
local infix `⊓` := inf
local infix `⊔` := sup
lemma inf_le_left (a b : A) : a ⊓ b ≤ a :=
Inf_le !mem_insert
lemma inf_le_right (a b : A) : a ⊓ b ≤ b :=
Inf_le (!mem_insert_of_mem !mem_insert)
lemma le_inf {a b c : A} : c ≤ a → c ≤ b → c ≤ a ⊓ b :=
assume h₁ h₂,
le_Inf (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(suppose x = a, begin subst x, exact h₁ end)
(suppose x ∈ '{b},
have x = b, from !eq_of_mem_singleton this,
begin subst x, exact h₂ end))
lemma le_sup_left (a b : A) : a ≤ a ⊔ b :=
le_Sup !mem_insert
lemma le_sup_right (a b : A) : b ≤ a ⊔ b :=
le_Sup (!mem_insert_of_mem !mem_insert)
lemma sup_le {a b c : A} : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
assume h₁ h₂,
Sup_le (take x, suppose x ∈ '{a, b},
or.elim (eq_or_mem_of_mem_insert this)
(assume H : x = a, by subst x; exact h₁)
(suppose x ∈ '{b},
have x = b, from !eq_of_mem_singleton this,
by subst x; exact h₂))
end complete_lattice_Sup
-- Every complete_lattice_Sup is a complete_lattice_Inf
definition complete_lattice_Sup_to_complete_lattice_Inf [C : complete_lattice_Sup A] :
complete_lattice_Inf A :=
⦃ complete_lattice_Inf, C ⦄
-- Every complete_lattice_Sup is a complete_lattice
section
definition complete_lattice_Sup_to_complete_lattice [trans_instance] [C : complete_lattice_Sup A] :
complete_lattice A :=
⦃ complete_lattice, C ⦄
end
section complete_lattice
variable [C : complete_lattice A]
include C
variable {f : A → A}
premise (mono : nondecreasing f)
theorem knaster_tarski : ∃ a, f a = a ∧ ∀ b, f b = b → a ≤ b :=
let a := ⨅ {u | f u ≤ u} in
have h₁ : f a = a, from
have ge : f a ≤ a, from
have ∀ b, b ∈ {u | f u ≤ u} → f a ≤ b, from
take b, suppose f b ≤ b,
have a ≤ b, from Inf_le this,
have f a ≤ f b, from mono this,
le.trans `f a ≤ f b` `f b ≤ b`,
le_Inf this,
have le : a ≤ f a, from
have f (f a) ≤ f a, from !mono ge,
have f a ∈ {u | f u ≤ u}, from this,
Inf_le this,
le.antisymm ge le,
have h₂ : ∀ b, f b = b → a ≤ b, from
take b,
suppose f b = b,
have b ∈ {u | f u ≤ u}, from
show f b ≤ b, by rewrite this,
Inf_le this,
exists.intro a (and.intro h₁ h₂)
theorem knaster_tarski_dual : ∃ a, f a = a ∧ ∀ b, f b = b → b ≤ a :=
let a := ⨆ {u | u ≤ f u} in
have h₁ : f a = a, from
have le : a ≤ f a, from
have ∀ b, b ∈ {u | u ≤ f u} → b ≤ f a, from
take b, suppose b ≤ f b,
have b ≤ a, from le_Sup this,
have f b ≤ f a, from mono this,
le.trans `b ≤ f b` `f b ≤ f a`,
Sup_le this,
have ge : f a ≤ a, from
have f a ≤ f (f a), from !mono le,
have f a ∈ {u | u ≤ f u}, from this,
le_Sup this,
le.antisymm ge le,
have h₂ : ∀ b, f b = b → b ≤ a, from
take b,
suppose f b = b,
have b ≤ f b, by rewrite this,
le_Sup this,
exists.intro a (and.intro h₁ h₂)
/- top and bot -/
definition bot : A := ⨅ univ
definition top : A := ⨆ univ
notation `⊥` := bot
notation `` := top
lemma bot_le (a : A) : ⊥ ≤ a :=
Inf_le !mem_univ
lemma eq_bot {a : A} : (∀ b, a ≤ b) → a = ⊥ :=
assume h,
have a ≤ ⊥, from le_Inf (take b bin, h b),
le.antisymm this !bot_le
lemma le_top (a : A) : a ≤ :=
le_Sup !mem_univ
lemma eq_top {a : A} : (∀ b, b ≤ a) → a = :=
assume h,
have ≤ a, from Sup_le (take b bin, h b),
le.antisymm !le_top this
/- general facts about complete lattices -/
lemma Inf_singleton {a : A} : ⨅'{a} = a :=
have ⨅'{a} ≤ a, from
Inf_le !mem_insert,
have a ≤ ⨅'{a}, from
le_Inf (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this),
le.antisymm `⨅'{a} ≤ a` `a ≤ ⨅'{a}`
lemma Sup_singleton {a : A} : ⨆'{a} = a :=
have ⨆'{a} ≤ a, from
Sup_le (take b, suppose b ∈ '{a}, have b = a, from eq_of_mem_singleton this, by rewrite this),
have a ≤ ⨆'{a}, from
le_Sup !mem_insert,
le.antisymm `⨆'{a} ≤ a` `a ≤ ⨆'{a}`
lemma Inf_antimono {s₁ s₂ : set A} : s₁ ⊆ s₂ → ⨅ s₂ ≤ ⨅ s₁ :=
suppose s₁ ⊆ s₂, le_Inf (take a : A, suppose a ∈ s₁, Inf_le (mem_of_subset_of_mem `s₁ ⊆ s₂` `a ∈ s₁`))
lemma Sup_mono {s₁ s₂ : set A} : s₁ ⊆ s₂ → ⨆ s₁ ≤ ⨆ s₂ :=
suppose s₁ ⊆ s₂, Sup_le (take a : A, suppose a ∈ s₁, le_Sup (mem_of_subset_of_mem `s₁ ⊆ s₂` `a ∈ s₁`))
lemma Inf_union (s₁ s₂ : set A) : ⨅ (s₁ s₂) = (⨅s₁) ⊓ (⨅s₂) :=
have le₁ : ⨅ (s₁ s₂) ≤ (⨅s₁) ⊓ (⨅s₂), from
!le_inf
(le_Inf (take a : A, suppose a ∈ s₁, Inf_le (mem_unionl `a ∈ s₁`)))
(le_Inf (take a : A, suppose a ∈ s₂, Inf_le (mem_unionr `a ∈ s₂`))),
have le₂ : (⨅s₁) ⊓ (⨅s₂) ≤ ⨅ (s₁ s₂), from
le_Inf (take a : A, suppose a ∈ s₁ s₂,
or.elim this
(suppose a ∈ s₁,
have (⨅s₁) ⊓ (⨅s₂) ≤ ⨅s₁, from !inf_le_left,
have ⨅s₁ ≤ a, from Inf_le `a ∈ s₁`,
le.trans `(⨅s₁) ⊓ (⨅s₂) ≤ ⨅s₁` `⨅s₁ ≤ a`)
(suppose a ∈ s₂,
have (⨅s₁) ⊓ (⨅s₂) ≤ ⨅s₂, from !inf_le_right,
have ⨅s₂ ≤ a, from Inf_le `a ∈ s₂`,
le.trans `(⨅s₁) ⊓ (⨅s₂) ≤ ⨅s₂` `⨅s₂ ≤ a`)),
le.antisymm le₁ le₂
lemma Sup_union (s₁ s₂ : set A) : ⨆ (s₁ s₂) = (⨆s₁) ⊔ (⨆s₂) :=
have le₁ : ⨆ (s₁ s₂) ≤ (⨆s₁) ⊔ (⨆s₂), from
Sup_le (take a : A, suppose a ∈ s₁ s₂,
or.elim this
(suppose a ∈ s₁,
have a ≤ ⨆s₁, from le_Sup `a ∈ s₁`,
have ⨆s₁ ≤ (⨆s₁) ⊔ (⨆s₂), from !le_sup_left,
le.trans `a ≤ ⨆s₁` `⨆s₁ ≤ (⨆s₁) ⊔ (⨆s₂)`)
(suppose a ∈ s₂,
have a ≤ ⨆s₂, from le_Sup `a ∈ s₂`,
have ⨆s₂ ≤ (⨆s₁) ⊔ (⨆s₂), from !le_sup_right,
le.trans `a ≤ ⨆s₂` `⨆s₂ ≤ (⨆s₁) ⊔ (⨆s₂)`)),
have le₂ : (⨆s₁) ⊔ (⨆s₂) ≤ ⨆ (s₁ s₂), from
!sup_le
(Sup_le (take a : A, suppose a ∈ s₁, le_Sup (mem_unionl `a ∈ s₁`)))
(Sup_le (take a : A, suppose a ∈ s₂, le_Sup (mem_unionr `a ∈ s₂`))),
le.antisymm le₁ le₂
lemma Inf_empty_eq_Sup_univ : ⨅ (∅ : set A) = ⨆ univ :=
have le₁ : ⨅ (∅ : set A) ≤ ⨆ univ, from
le_Sup !mem_univ,
have le₂ : ⨆ univ ≤ ⨅ ∅, from
le_Inf (take a : A, suppose a ∈ ∅, absurd this !not_mem_empty),
le.antisymm le₁ le₂
lemma Sup_empty_eq_Inf_univ : ⨆ (∅ : set A) = ⨅ univ :=
have le₁ : ⨆ (∅ : set A) ≤ ⨅ univ, from
Sup_le (take a, suppose a ∈ ∅, absurd this !not_mem_empty),
have le₂ : ⨅ univ ≤ ⨆ (∅ : set A), from
Inf_le !mem_univ,
le.antisymm le₁ le₂
lemma Sup_pair (a b : A) : Sup '{a, b} = sup a b :=
by rewrite [insert_eq, Sup_union, *Sup_singleton]
lemma Inf_pair (a b : A) : Inf '{a, b} = inf a b :=
by rewrite [insert_eq, Inf_union, *Inf_singleton]
end complete_lattice
/- complete lattice instances -/
section
open eq.ops complete_lattice
definition complete_lattice_fun [instance] (A B : Type) [complete_lattice B] :
complete_lattice (A → B) :=
⦃ complete_lattice, lattice_fun A B,
Inf := λS x, Inf ((λf, f x) ' S),
le_Inf := take f S H x,
le_Inf (take y Hy, obtain g `g ∈ S` `g x = y`, from Hy, `g x = y` ▸ H g `g ∈ S` x),
Inf_le := take f S `f ∈ S` x,
Inf_le (exists.intro f (and.intro `f ∈ S` rfl)),
Sup := λS x, Sup ((λf, f x) ' S),
le_Sup := take f S `f ∈ S` x,
le_Sup (exists.intro f (and.intro `f ∈ S` rfl)),
Sup_le := take f S H x,
Sup_le (take y Hy, obtain g `g ∈ S` `g x = y`, from Hy, `g x = y` ▸ H g `g ∈ S` x)
section
open classical -- Prop and set are only in the classical setting a complete lattice
definition complete_lattice_Prop [instance] : complete_lattice Prop :=
⦃ complete_lattice, lattice_Prop,
Inf := λS, false ∉ S,
le_Inf := take x S H Hx Hf,
H _ Hf Hx,
Inf_le := take x S Hx Hf,
(classical.cases_on x (take x, true.intro) Hf) Hx,
Sup := λS, true ∈ S,
le_Sup := take x S Hx H,
iff_subst (iff.intro (take H, true.intro) (take H', H)) Hx,
Sup_le := take x S H Ht,
H _ Ht true.intro
lemma sInter_eq_Inf_fun {A : Type} (S : set (set A)) : ⋂₀ S = @Inf (A → Prop) _ S :=
funext (take x,
calc
(⋂₀ S) x = ∀₀ P ∈ S, P x : rfl
... = ¬ (∃₀ P ∈ S, P x = false) :
begin
rewrite not_bounded_exists,
apply bounded_forall_congr,
intros,
rewrite eq_false,
rewrite not_not_iff
end
... = @Inf (A → Prop) _ S x : rfl)
lemma sUnion_eq_Sup_fun {A : Type} (S : set (set A)) : ⋃₀ S = @Sup (A → Prop) _ S :=
funext (take x,
calc
(⋃₀ S) x = ∃₀ P ∈ S, P x : rfl
... = (∃₀ P ∈ S, P x = true) :
begin
apply bounded_exists_congr,
intros,
rewrite eq_true
end
... = @Sup (A → Prop) _ S x : rfl)
definition complete_lattice_set [instance] (A : Type) : complete_lattice (set A) :=
⦃ complete_lattice,
le := subset,
le_refl := @le_refl (A → Prop) _,
le_trans := @le_trans (A → Prop) _,
le_antisymm := @le_antisymm (A → Prop) _,
inf := inter,
sup := union,
inf_le_left := @inf_le_left (A → Prop) _,
inf_le_right := @inf_le_right (A → Prop) _,
le_inf := @le_inf (A → Prop) _,
le_sup_left := @le_sup_left (A → Prop) _,
le_sup_right := @le_sup_right (A → Prop) _,
sup_le := @sup_le (A → Prop) _,
Inf := sInter,
Sup := sUnion,
le_Inf := begin intros X S H, rewrite sInter_eq_Inf_fun, apply (@le_Inf (A → Prop) _), exact H end,
Inf_le := begin intros X S H, rewrite sInter_eq_Inf_fun, apply (@Inf_le (A → Prop) _), exact H end,
le_Sup := begin intros X S H, rewrite sUnion_eq_Sup_fun, apply (@le_Sup (A → Prop) _), exact H end,
Sup_le := begin intros X S H, rewrite sUnion_eq_Sup_fun, apply (@Sup_le (A → Prop) _), exact H end
end
end