feat(order): add order_dual (similar to with_top/with_bot) and dual o…

…rder instances

order/basic.lean

@@ -66,13 +66,25 @@ assume a b h, m_g (m_f h)
 
 end monotone
 
-/- order instances -/
+def order_dual (α : Type*) := α
 
-/-- Order dual of a preorder -/
-def preorder.dual (o : preorder α) : preorder α :=
-{ le       := λx y, y ≤ x,
-  le_refl  := le_refl,
-  le_trans := assume a b c h₁ h₂, le_trans h₂ h₁ }
+namespace order_dual
+instance (α : Type*) [has_le α] : has_le (order_dual α) := ⟨λx y:α, y ≤ x⟩
+
+instance (α : Type*) [preorder α] : preorder (order_dual α) :=
+{ le_refl  := le_refl,
+  le_trans := assume a b c hab hbc, le_trans hbc hab,
+  .. order_dual.has_le α }
+
+instance (α : Type*) [partial_order α] : partial_order (order_dual α) :=
+{ le_antisymm := assume a b hab hba, @le_antisymm α _ a b hba hab, .. order_dual.preorder α }
+
+instance (α : Type*) [linear_order α] : linear_order (order_dual α) :=
+{ le_total := assume a b:α, le_total b a, .. order_dual.partial_order α }
+
+end order_dual
+
+/- order instances on the function space -/
 
 instance pi.preorder {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)] : preorder (Πi, α i) :=
 { le       := λx y, ∀i, x i ≤ y i,
@@ -83,18 +95,6 @@ instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀i, partial_orde
 { le_antisymm := λf g h1 h2, funext (λb, le_antisymm (h1 b) (h2 b)),
   ..pi.preorder }
 
-/-- Order dual of a partial order -/
-def partial_order.dual (wo : partial_order α) : partial_order α :=
-{ le          := λx y, y ≤ x,
-  le_refl     := le_refl,
-  le_trans    := assume a b c h₁ h₂, le_trans h₂ h₁,
-  le_antisymm := assume a b h₁ h₂, le_antisymm h₂ h₁ }
-
-theorem le_dual_eq_le {α : Type} (wo : partial_order α) (a b : α) :
-  @has_le.le _ (@preorder.to_has_le _ (@partial_order.to_preorder _ wo.dual)) a b =
-  @has_le.le _ (@preorder.to_has_le _ (@partial_order.to_preorder _ wo)) b a :=
-rfl
-
 theorem comp_le_comp_left_of_monotone [preorder α] [preorder β] [preorder γ]
   {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g ≤ h) : has_le.le.{max w u} (f ∘ g) (f ∘ h) :=
 assume x, m_f (le_gh x)

order/bounded_lattice.lean

@@ -14,9 +14,9 @@ import order.lattice data.option
 set_option old_structure_cmd true
 
 universes u v
-variable {α : Type u}
 
 namespace lattice
+variable {α : Type u}
 
 /-- Typeclass for the `⊤` (`\top`) notation -/
 class has_top (α : Type u) := (top : α)
@@ -270,6 +270,7 @@ end lattice
 def with_bot (α : Type*) := option α
 
 namespace with_bot
+variable {α : Type u}
 open lattice
 
 instance : has_coe_t α (with_bot α) := ⟨some⟩
@@ -402,6 +403,7 @@ end with_bot
 def with_top (α : Type*) := option α
 
 namespace with_top
+variable {α : Type u}
 open lattice
 
 instance : has_coe_t α (with_top α) := ⟨some⟩
@@ -529,3 +531,35 @@ have acc_some : ∀ a : α, acc ((<) : with_top α → with_top α → Prop) (so
   (λ _ _, acc_some _))) acc_some⟩
 
 end with_top
+
+namespace order_dual
+open lattice
+variable (α : Type*)
+
+instance [has_bot α] : has_top (order_dual α) := ⟨(⊥ : α)⟩
+instance [has_top α] : has_bot (order_dual α) := ⟨(⊤ : α)⟩
+
+instance [order_bot α] : order_top (order_dual α) :=
+{ le_top := @bot_le α _,
+  .. order_dual.partial_order α, .. order_dual.lattice.has_top α }
+
+instance [order_top α] : order_bot (order_dual α) :=
+{ bot_le := @le_top α _,
+  .. order_dual.partial_order α, .. order_dual.lattice.has_bot α }
+
+instance [semilattice_inf_bot α] : semilattice_sup_top (order_dual α) :=
+{ .. order_dual.lattice.semilattice_sup α, .. order_dual.lattice.order_top α }
+
+instance [semilattice_inf_top α] : semilattice_sup_bot (order_dual α) :=
+{ .. order_dual.lattice.semilattice_sup α, .. order_dual.lattice.order_bot α }
+
+instance [semilattice_sup_bot α] : semilattice_inf_top (order_dual α) :=
+{ .. order_dual.lattice.semilattice_inf α, .. order_dual.lattice.order_top α }
+
+instance [semilattice_sup_top α] : semilattice_inf_bot (order_dual α) :=
+{ .. order_dual.lattice.semilattice_inf α, .. order_dual.lattice.order_bot α }
+
+instance [bounded_lattice α] : bounded_lattice (order_dual α) :=
+{ .. order_dual.lattice.lattice α, .. order_dual.lattice.order_top α, .. order_dual.lattice.order_bot α }
+
+end order_dual

order/complete_lattice.lean

@@ -9,10 +9,10 @@ import order.bounded_lattice data.set.basic tactic.pi_instances
 
 set_option old_structure_cmd true
 
-universes u v w w₂
-variables {α : Type u} {β : Type v} {ι : Sort w} {ι₂ : Sort w₂}
 
 namespace lattice
+universes u v w w₂
+variables {α : Type u} {β : Type v} {ι : Sort w} {ι₂ : Sort w₂}
 
 /-- class for the `Sup` operator -/
 class has_Sup (α : Type u) := (Sup : set α → α)
@@ -152,6 +152,16 @@ by finish [singleton_def]
 by finish [singleton_def]
 --eq.trans Inf_insert $ by simp
 
+@[simp] theorem Inf_eq_top : Inf s = ⊤ ↔ (∀a∈s, a = ⊤) :=
+iff.intro
+  (assume h a ha, top_unique $ h ▸ Inf_le ha)
+  (assume h, top_unique $ le_Inf $ assume a ha, top_le_iff.2 $ h a ha)
+
+@[simp] theorem Sup_eq_bot : Sup s = ⊥ ↔ (∀a∈s, a = ⊥) :=
+iff.intro
+  (assume h a ha, bot_unique $ h ▸ le_Sup ha)
+  (assume h, bot_unique $ Sup_le $ assume a ha, le_bot_iff.2 $ h a ha)
+
 end
 
 section complete_linear_order
@@ -276,18 +286,28 @@ le_antisymm
   (infi_le_infi2 $ assume j, ⟨pq.mpr j, le_of_eq $ f j⟩)
   (infi_le_infi2 $ assume j, ⟨pq.mp j, le_of_eq $ (f _).symm⟩)
 
-@[simp] theorem infi_const {a : α} [inhabited ι] : (⨅ b:ι, a) = a :=
-le_antisymm (Inf_le ⟨arbitrary ι, rfl⟩) (by finish)
+@[simp] theorem infi_const {a : α} : ∀[nonempty ι], (⨅ b:ι, a) = a
+| ⟨i⟩ := le_antisymm (Inf_le ⟨i, rfl⟩) (by finish)
 
-@[simp] theorem supr_const {a : α} [inhabited ι] : (⨆ b:ι, a) = a :=
-le_antisymm (by finish) (le_Sup ⟨arbitrary ι, rfl⟩)
+@[simp] theorem supr_const {a : α} : ∀[nonempty ι], (⨆ b:ι, a) = a
+| ⟨i⟩ := le_antisymm (by finish) (le_Sup ⟨i, rfl⟩)
 
-@[simp] lemma infi_top [complete_lattice α] : (⨅i:ι, ⊤ : α) = ⊤ :=
+@[simp] lemma infi_top : (⨅i:ι, ⊤ : α) = ⊤ :=
 top_unique $ le_infi $ assume i, le_refl _
 
-@[simp] lemma supr_bot [complete_lattice α] : (⨆i:ι, ⊥ : α) = ⊥ :=
+@[simp] lemma supr_bot : (⨆i:ι, ⊥ : α) = ⊥ :=
 bot_unique $ supr_le $ assume i, le_refl _
 
+@[simp] lemma infi_eq_top : infi s = ⊤ ↔ (∀i, s i = ⊤) :=
+iff.intro
+  (assume eq i, top_unique $ eq ▸ infi_le _ _)
+  (assume h, top_unique $ le_infi $ assume i, top_le_iff.2 $ h i)
+
+@[simp] lemma infi_eq_bot : supr s = ⊥ ↔ (∀i, s i = ⊥) :=
+iff.intro
+  (assume eq i, bot_unique $ eq ▸ le_supr _ _)
+  (assume h, bot_unique $ supr_le $ assume i, le_bot_iff.2 $ h i)
+
 @[simp] lemma infi_pos {p : Prop} {f : p → α} (hp : p) : (⨅ h : p, f h) = f hp :=
 le_antisymm (infi_le _ _) (le_infi $ assume h, le_refl _)
 
@@ -639,8 +659,6 @@ assume x y h, le_Inf $ assume x' ⟨f, f_in, fx_eq⟩, Inf_le_of_le ⟨f, f_in,
 
 end complete_lattice
 
-end lattice
-
 section ord_continuous
 open lattice
 variables [complete_lattice α] [complete_lattice β]
@@ -664,20 +682,20 @@ calc f a₁ ≤ f a₁ ⊔ f a₂ : le_sup_left
   ... = _ : by rw [sup_of_le_right h]
 
 end ord_continuous
+end lattice
 
-/- Classical statements:
-
-@[simp] theorem Inf_eq_top : Inf s = ⊤ ↔ (∀a∈s, a = ⊤) :=
-_
-
-@[simp] theorem infi_eq_top : infi s = ⊤ ↔ (∀i, s i = ⊤) :=
-_
-
-@[simp] theorem Sup_eq_bot : Sup s = ⊤ ↔ (∀a∈s, a = ⊥) :=
-_
+namespace order_dual
+open lattice
+variable (α : Type*)
 
-@[simp] theorem supr_eq_top : supr s = ⊤ ↔ (∀i, s i = ⊥) :=
-_
+instance [has_Inf α] : has_Sup (order_dual α) := ⟨(Inf : set α → α)⟩
+instance [has_Sup α] : has_Inf (order_dual α) := ⟨(Sup : set α → α)⟩
 
+instance [complete_lattice α] : complete_lattice (order_dual α) :=
+{ le_Sup := @complete_lattice.Inf_le α _,
+  Sup_le := @complete_lattice.le_Inf α _,
+  Inf_le := @complete_lattice.le_Sup α _,
+  le_Inf := @complete_lattice.Sup_le α _,
+  .. order_dual.lattice.bounded_lattice α, ..order_dual.lattice.has_Sup α, ..order_dual.lattice.has_Inf α }
 
--/
+end order_dual

order/galois_connection.lean

@@ -147,7 +147,7 @@ by intros a b; rw [gc2, gc1]
 
 protected lemma dual [pα : preorder α] [pβ : preorder β]
   (l : α → β) (u : β → α) (gc : galois_connection l u) :
-  @galois_connection β α pβ.dual pα.dual u l :=
+  @galois_connection (order_dual β) (order_dual α) _ _ u l :=
 assume a b, (gc _ _).symm
 
 protected lemma dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w}

order/lattice.lean

@@ -326,3 +326,27 @@ instance nat.distrib_lattice : distrib_lattice ℕ :=
 by apply_instance
 
 end lattice
+
+namespace order_dual
+open lattice
+variable (α : Type*)
+
+instance [has_inf α] : has_sup (order_dual α) := ⟨((⊓) : α → α → α)⟩
+instance [has_sup α] : has_inf (order_dual α) := ⟨((⊔) : α → α → α)⟩
+
+instance [semilattice_inf α] : semilattice_sup (order_dual α) :=
+{ le_sup_left  := @inf_le_left α _,
+  le_sup_right := @inf_le_right α _,
+  sup_le := assume a b c hca hcb, @le_inf α _ _ _ _ hca hcb,
+  .. order_dual.partial_order α, .. order_dual.lattice.has_sup α }
+
+instance [semilattice_sup α] : semilattice_inf (order_dual α) :=
+{ inf_le_left  := @le_sup_left α _,
+  inf_le_right := @le_sup_right α _,
+  le_inf := assume a b c hca hcb, @sup_le α _ _ _ _ hca hcb,
+  .. order_dual.partial_order α, .. order_dual.lattice.has_inf α }
+
+instance [lattice α] : lattice (order_dual α) :=
+{ .. order_dual.lattice.semilattice_sup α, .. order_dual.lattice.semilattice_inf α }
+
+end order_dual