feat(library/algebra): add lattice instances for Prop, fun, and set

Adds weak_order, lattice and complete_lattice instances for Prop, fun, and set. Adds supporting
theorems to various other places.

library/algebra/complete_lattice.lean

@@ -270,3 +270,92 @@ have le₂ : ⨅ univ ≤ ⨆ (∅ : set A), from
 le.antisymm le₁ le₂
 
 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,
+  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_fun_Inf {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_fun_Sup {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_fun_Inf, apply (@le_Inf (A → Prop) _), exact H end,
+  Inf_le := begin intros X S H, rewrite sInter_eq_fun_Inf, apply (@Inf_le (A → Prop) _), exact H end,
+  le_Sup := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@le_Sup (A → Prop) _), exact H end,
+  Sup_le := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@Sup_le (A → Prop) _), exact H end
+⦄
+
+end
+
+end

library/algebra/lattice.lean

@@ -106,3 +106,35 @@ section
   theorem sup_eq_right {a b : A} (H : a ≤ b) : a ⊔ b = b :=
   eq.subst !sup.comm (sup_eq_left H)
 end
+
+/- lattice instances  -/
+
+definition lattice_Prop [instance] : lattice Prop :=
+⦃ lattice, weak_order_Prop,
+  inf          := and,
+  le_inf       := take a b c Ha Hb Hc, and.intro (Ha Hc) (Hb Hc),
+  inf_le_left  := @and.elim_left,
+  inf_le_right := @and.elim_right,
+  sup          := or,
+  sup_le       := @or.rec,
+  le_sup_left  := @or.intro_left,
+  le_sup_right := @or.intro_right
+⦄
+
+definition lattice_fun [instance] {A B : Type} [lattice B] : lattice (A → B) :=
+⦃ lattice, weak_order_fun,
+  inf          := λf g x, inf (f x) (g x),
+  le_inf       := take f g h Hf Hg x, le_inf (Hf x) (Hg x),
+  inf_le_left  := take f g x, !inf_le_left,
+  inf_le_right := take f g x, !inf_le_right,
+  sup          := λf g x, sup (f x) (g x),
+  sup_le       := take f g h Hf Hg x, sup_le (Hf x) (Hg x),
+  le_sup_left  := take f g x, !le_sup_left,
+  le_sup_right := take t g x, !le_sup_right
+⦄
+
+/-
+  Should we add a trans-instance from total orders to lattices?
+  If we added we should add it with lower priority:
+    Prop is added as a lattice, but in the classical case it is a total order!
+-/

library/algebra/order.lean

@@ -434,3 +434,35 @@ section
     (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
     (assume H : a > b, by rewrite (max_eq_left_of_lt H); apply H₁)
 end
+
+/- order instances -/
+
+definition weak_order_Prop [instance] : weak_order Prop :=
+⦃ weak_order,
+  le           := λx y, x → y,
+  le_refl      := λx, id,
+  le_trans     := λa b c H1 H2 x, H2 (H1 x),
+  le_antisymm  := λf g H1 H2, propext (and.intro H1 H2)
+⦄
+
+definition weak_order_fun [instance] {A B : Type} [weak_order B] : weak_order (A → B) :=
+⦃ weak_order,
+  le := λx y, ∀b, x b ≤ y b,
+  le_refl := λf b, !le.refl,
+  le_trans := λf g h H1 H2 b, !le.trans (H1 b) (H2 b),
+  le_antisymm := λf g H1 H2, funext (λb, !le.antisymm (H1 b) (H2 b))
+⦄
+
+definition weak_order_dual {A : Type} (wo : weak_order A) : weak_order A :=
+⦃ weak_order,
+  le := λx y, y ≤ x,
+  le_refl := le.refl,
+  le_trans := take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`,
+  le_antisymm := take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄
+
+lemma dual {A : Type} (wo : weak_order A) (a b : A) :
+  @le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b =
+  @le _ (@weak_order.to_has_le _ wo) b a :=
+rfl
+
+-- what to do with the strict variants?

library/data/set/basic.lean

@@ -64,6 +64,54 @@ theorem bounded_exists.intro {P : X → Prop} {s : set X} {x : X} (xs : x ∈ s)
   ∃₀ x ∈ s, P x :=
 exists.intro x (and.intro xs Px)
 
+lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
+  (∀₀ x ∈ S, P x) = (∀₀ x ∈ S, Q x) :=
+begin
+  apply propext,
+  apply forall_congr,
+  intros x,
+  apply imp_congr_right,
+  apply H
+end
+
+lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) :
+  (∃₀ x ∈ S, P x) = (∃₀ x ∈ S, Q x) :=
+begin
+  apply propext,
+  apply exists_congr,
+  intros x,
+  apply and_congr_right,
+  apply H
+end
+
+section
+  open classical
+
+  lemma not_bounded_exists {A : Type} {S : set A} {P : A → Prop} :
+    (¬ (∃₀ x ∈ S, P x)) = (∀₀ x ∈ S, ¬ P x) :=
+  begin
+    rewrite forall_iff_not_exists,
+    apply propext,
+    apply forall_congr,
+    intro x,
+    rewrite not_and_iff_not_or_not,
+    rewrite imp_iff_not_or
+  end
+
+  lemma not_bounded_forall {A : Type} {S : set A} {P : A → Prop} :
+    (¬ (∀₀ x ∈ S, P x)) = (∃₀ x ∈ S, ¬ P x) :=
+  calc (¬ (∀₀ x ∈ S, P x)) = ¬ ¬ (∃₀ x ∈ S, ¬ P x) :
+    begin
+      rewrite not_bounded_exists,
+      apply (congr_arg not),
+      apply bounded_forall_congr,
+      intros x H,
+      rewrite not_not_iff
+    end
+    ... = (∃₀ x ∈ S, ¬ P x) : by (rewrite not_not_iff)
+
+end
+
 /- empty set -/
 
 definition empty : set X := λx, false
@@ -95,6 +143,10 @@ subset.antisymm H (empty_subset s)
 theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ :=
 iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
 
+lemma bounded_forall_empty_iff {P : X → Prop} :
+  (∀₀x∈∅, P x) ↔ true :=
+iff.intro (take H, true.intro) (take H, by contradiction)
+
 /- universal set -/
 
 definition univ : set X := λx, true
@@ -287,6 +339,18 @@ theorem forall_of_forall_insert {P : X → Prop} {a : X} {s : set X}
   ∀ x, x ∈ s → P x :=
 λ x xs, H x (!mem_insert_of_mem xs)
 
+lemma forall_insert_iff {P : X → Prop} {a : X} {s : set X} :
+  (∀₀x ∈ insert a s, P x) ↔ P a ∧ (∀₀x ∈ s, P x) :=
+begin
+  apply iff.intro, all_goals (intro H),
+  { apply and.intro,
+    { apply H, apply mem_insert },
+    { intro x Hx, apply H, apply mem_insert_of_mem, assumption } },
+  { intro x Hx, cases Hx with eq Hx,
+    { cases eq, apply (and.elim_left H) },
+    { apply (and.elim_right H), assumption } }
+end
+
 /- singleton -/
 
 theorem mem_singleton_iff (a b : X) : a ∈ '{b} ↔ a = b :=
@@ -521,8 +585,45 @@ theorem complement_complement_image (S : set (set X)) :
   complement ' (complement ' S) = S :=
 by rewrite [-image_compose, complement_compose_complement, image_id]
 
+lemma forall_image_implies_forall {f : X → Y} {S : set X} {P : Y → Prop} (H : ∀₀ x ∈ S, P (f x)) :
+  ∀₀ y ∈ f ' S, P y :=
+begin
+  intro x' Hx;
+  cases Hx with x Hx;
+  cases Hx with Hx eq;
+  rewrite (eq⁻¹);
+  apply H;
+  assumption
+end
+
+lemma forall_image_iff {f : X → Y} {S : set X} {P : Y → Prop} :
+  (∀₀ y ∈ f ' S, P y) ↔ (∀₀ x ∈ S, P (f x)) :=
+iff.intro (take H x Hx, H _ (!mem_image_of_mem `x ∈ S`)) forall_image_implies_forall
+
+lemma image_insert_eq {f : X → Y} {a : X} {S : set X} :
+  f ' insert a S = insert (f a) (f ' S) :=
+begin
+  apply set.ext,
+  intro x, apply iff.intro, all_goals (intros H),
+  { cases H with y Hy, cases Hy with Hy eq, rewrite (eq⁻¹), cases Hy with y_eq,
+    { rewrite y_eq, apply mem_insert },
+    { apply mem_insert_of_mem, apply mem_image_of_mem, assumption } },
+  { cases H with eq Hx,
+    { rewrite eq, apply mem_image_of_mem, apply mem_insert },
+    { cases Hx with y Hy, cases Hy with Hy eq,
+      rewrite (eq⁻¹), apply mem_image_of_mem, apply mem_insert_of_mem, assumption } }
+end
+
 end image
 
+/- function pre image  -/
+
+definition preimage {A B:Type} (f : A → B) (Y : set B) : set A := { x | f x ∈ Y }
+
+lemma image_subset_iff {A B : Type} {f : A → B} {X : set A} {Y : set B} :
+  f ' X ⊆ Y ↔ X ⊆ preimage f Y :=
+@forall_image_iff A B f X Y
+
 /- collections of disjoint sets -/
 
 definition disjoint_sets (S : set (set X)) : Prop := ∀ a b, a ∈ S → b ∈ S → a ≠ b → a ∩ b = ∅

library/init/classical.lean

@@ -159,6 +159,18 @@ propext (iff.intro
   (assume H, eq.of_iff H)
   (assume H, iff.of_eq H))
 
+lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
+begin
+  rewrite ((@iff_eq_eq a false)⁻¹),
+  rewrite iff_false
+end
+
+lemma eq_true {a : Prop} : (a = true) = a :=
+begin
+  rewrite ((@iff_eq_eq a true)⁻¹),
+  rewrite iff_true
+end
+
 end aux
 
 /- All propositions are decidable -/

library/init/logic.lean

@@ -342,6 +342,11 @@ iff.intro
   (λHab Hc, iff.mp H2 (Hab (iff.mpr H1 Hc)))
   (λHcd Ha, iff.mpr H2 (Hcd (iff.mp H1 Ha)))
 
+theorem imp_congr_right (H : a → (b ↔ c)) : (a → b) ↔ (a → c) :=
+iff.intro
+  (take Hab Ha, iff.elim_left (H Ha) (Hab Ha))
+  (take Hab Ha, iff.elim_right (H Ha) (Hab Ha))
+
 theorem not_not_intro (Ha : a) : ¬¬a :=
 assume Hna : ¬a, Hna Ha
 
@@ -392,6 +397,11 @@ and.rec (λHa Hb, and.intro (H₂ Ha) (H₃ Hb))
 theorem and_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) :=
 iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2))
 
+theorem and_congr_right (H : a → (b ↔ c)) : (a ∧ b) ↔ (a ∧ c) :=
+iff.intro
+  (take Hab, obtain `a` `b`, from Hab, and.intro `a` (iff.elim_left (H `a`) `b`))
+  (take Hac, obtain `a` `c`, from Hac, and.intro `a` (iff.elim_right (H `a`) `c`))
+
 theorem and.comm [simp] : a ∧ b ↔ b ∧ a :=
 iff.intro and.swap and.swap