feat(library/standard/logic/connectives/quantifiers): add some theorems for simplifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/data/pair.lean

@@ -1,9 +1,10 @@
------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+------------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.classes.inhabited
+import logic.classes.inhabited logic.connectives.eq
 
 namespace pair
 inductive pair (A : Type) (B : Type) : Type :=

library/standard/logic/axioms/hilbert.lean

@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.classes.inhabited
+import logic.classes.inhabited logic.connectives.eq logic.connectives.quantifiers
 
 variable epsilon {A : Type} {H : inhabited A} (P : A → Prop) : A
 axiom epsilon_ax {A : Type} {P : A → Prop} (Hex : ∃ a, P a) : P (@epsilon A (inhabited_exists Hex) P)

library/standard/logic/classes/inhabited.lean

@@ -4,7 +4,7 @@
 -- Authors: Leonardo de Moura, Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import logic.connectives.quantifiers
+import logic.connectives.basic
 
 inductive inhabited (A : Type) : Prop :=
 | inhabited_intro : A → inhabited A
@@ -17,6 +17,3 @@ inhabited_intro true
 
 theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
 inhabited_elim H (take b, inhabited_intro (λa, b))
-
-theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
-obtain w Hw, from H, inhabited_intro w

library/standard/logic/connectives/quantifiers.lean

@@ -4,7 +4,7 @@
 -- Authors: Leonardo de Moura, Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import .basic .eq
+import .basic .eq ..classes.inhabited
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 | exists_intro : ∀ (a : A), P a → Exists P
@@ -37,3 +37,51 @@ theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
                            (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬p y) → b) : b :=
 obtain w Hw, from H2,
 H1 w (and_elim_left Hw) (and_elim_right Hw)
+
+theorem inhabited_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : inhabited A :=
+obtain w Hw, from H, inhabited_intro w
+
+theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) :=
+iff_intro
+  (assume Hl, take x, iff_elim_left (H x) (Hl x))
+  (assume Hr, take x, iff_elim_right (H x) (Hr x))
+
+theorem exists_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∃x, φ x) ↔ (∃x, ψ x) :=
+iff_intro
+  (assume Hex, obtain w Pw, from Hex,
+    exists_intro w (iff_elim_left (H w) Pw))
+  (assume Hex, obtain w Qw, from Hex,
+    exists_intro w (iff_elim_right (H w) Qw))
+
+theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
+iff_intro (assume H, trivial) (assume H, take x, trivial)
+
+theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p :=
+iff_intro (assume Hl, inhabited_elim H (take x, Hl x)) (assume Hr, take x, Hr)
+
+theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p :=
+iff_intro
+  (assume Hl, obtain a Hp, from Hl, Hp)
+  (assume Hr, inhabited_elim H (take a, exists_intro a Hr))
+
+theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
+iff_intro
+  (assume H, and_intro (take x, and_elim_left (H x)) (take x, and_elim_right (H x)))
+  (assume H, take x, and_intro (and_elim_left H x) (and_elim_right H x))
+
+theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
+iff_intro
+  (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H,
+    or_elim Hw
+      (assume Hw1 : φ w, or_inl (exists_intro w Hw1))
+      (assume Hw2 : ψ w, or_inr (exists_intro w Hw2)))
+  (assume H, or_elim H
+    (assume H1, obtain (w : A) (Hw : φ w), from H1,
+      exists_intro w (or_inl Hw))
+    (assume H2, obtain (w : A) (Hw : ψ w), from H2,
+      exists_intro w (or_inr Hw)))
+
+theorem forall_not_inhabited {A : Type} {B : A → Prop} (H : ¬ inhabited A) : ∀x, B x :=
+take x,
+  have Hi : inhabited A, from inhabited_intro x,
+  absurd_elim (B x) Hi H