From 1c93c5bbb21710fb03cc1935cbb76ed66fb2d02b Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 8 Jun 2015 16:58:08 +1000
Subject: [PATCH] feat(library/logic/{connectives.lean,quantiers.lean}): add
 iff congruence rules

---
 library/data/set/function.lean |  1 -
 library/logic/connectives.lean | 32 ++++++++++++++++++++++++++++++++
 library/logic/quantifiers.lean | 29 ++++++++++++++++++++++++++++-
 3 files changed, 60 insertions(+), 2 deletions(-)

diff --git a/library/data/set/function.lean b/library/data/set/function.lean
index e5d59969f..24f5e7f0a 100644
--- a/library/data/set/function.lean
+++ b/library/data/set/function.lean
@@ -180,7 +180,6 @@ match Hg with and.intro Hgmap (and.intro Hginj Hgsurj) :=
   end
 end
 
--- TODO: simplify when we have a better way of handling congruences wrt iff
 lemma bijective_iff_bij_on_univ {f : X → Y} : bijective f ↔ bij_on f univ univ :=
 iff.intro
   (assume H,
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
index 5462e541b..2aeea79fe 100644
--- a/library/logic/connectives.lean
+++ b/library/logic/connectives.lean
@@ -297,3 +297,35 @@ section
   definition if_false (t e : A) : (if false then t else e) = e :=
   if_neg not_false
 end
+
+/- congruences -/
+
+theorem congr_not {a b :  Prop} (H : a ↔ b) : ¬a ↔ ¬b :=
+iff.intro
+  (assume H₁ : ¬a, assume H₂ : b, H₁ (iff.elim_right H H₂))
+  (assume H₁ : ¬b, assume H₂ : a, H₁ (iff.elim_left H H₂))
+
+section
+  variables {a₁ b₁ a₂ b₂ : Prop}
+  variables (H₁ : a₁ ↔ b₁) (H₂ : a₂ ↔ b₂)
+
+  theorem congr_and : a₁ ∧ a₂ ↔ b₁ ∧ b₂ :=
+  iff.intro
+    (assume H₃ : a₁ ∧ a₂, and_of_and_of_imp_of_imp H₃ (iff.elim_left H₁) (iff.elim_left H₂))
+    (assume H₃ : b₁ ∧ b₂, and_of_and_of_imp_of_imp H₃ (iff.elim_right H₁) (iff.elim_right H₂))
+
+  theorem congr_or : a₁ ∨ a₂ ↔ b₁ ∨ b₂ :=
+  iff.intro
+    (assume H₃ : a₁ ∨ a₂, or_of_or_of_imp_of_imp H₃ (iff.elim_left H₁) (iff.elim_left H₂))
+    (assume H₃ : b₁ ∨ b₂, or_of_or_of_imp_of_imp H₃ (iff.elim_right H₁) (iff.elim_right H₂))
+
+  theorem congr_imp : (a₁ → a₂) ↔ (b₁ → b₂) :=
+  iff.intro
+    (assume H₃ : a₁ → a₂, assume Hb₁ : b₁, iff.elim_left H₂ (H₃ ((iff.elim_right H₁) Hb₁)))
+    (assume H₃ : b₁ → b₂, assume Ha₁ : a₁, iff.elim_right H₂ (H₃ ((iff.elim_left H₁) Ha₁)))
+
+  theorem congr_iff : (a₁ ↔ a₂) ↔ (b₁ ↔ b₂) :=
+  iff.intro
+    (assume H₃ : a₁ ↔ a₂, iff.trans (iff.symm H₁) (iff.trans H₃ H₂))
+    (assume H₃ : b₁ ↔ b₂, iff.trans H₁ (iff.trans H₃ (iff.symm H₂)))
+end
diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index 357528cfc..a1a83be0b 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 Universal and existential quantifiers. See also init.logic.
 -/
-
+import .connectives
 open inhabited nonempty
 
 theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
@@ -97,3 +97,30 @@ theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop}
     (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
 obtain w Hw, from H2,
 H1 w (and.elim_left Hw) (and.elim_right Hw)
+
+/- congruences -/
+
+section
+  variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀x, p₁ x ↔ p₂ x)
+
+  theorem congr_forall : (∀x, p₁ x) ↔ (∀x, p₂ x) :=
+  iff.intro
+    (assume H', take x, iff.mp (H x) (H' x))
+    (assume H', take x, iff.mp' (H x) (H' x))
+
+  theorem congr_exists : (∃x, p₁ x) ↔ (∃x, p₂ x) :=
+  iff.intro
+    (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp (H x) H₁)))
+    (assume H', exists.elim H' (λ x H₁, exists.intro x (iff.mp' (H x) H₁)))
+
+  include H
+  theorem congr_exists_unique : (∃!x, p₁ x) ↔ (∃!x, p₂ x) :=
+  begin
+    apply congr_exists,
+    intro x,
+    apply congr_and (H x),
+    apply congr_forall,
+    intro y,
+    apply congr_imp (H y) !iff.rfl
+  end
+end