From ae2e0fd3dcdcbe29e0d2b2101a27f0b740ed7a89 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 3 Aug 2014 21:41:01 -0700
Subject: [PATCH] feat(library/standard/logic/connectives/if): add
 'if-then-else' congruence theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/logic/classes/decidable.lean |  8 ++++++++
 library/standard/logic/connectives/if.lean    | 19 +++++++++++++++++--
 2 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean
index 071734005..cdb378446 100644
--- a/library/standard/logic/classes/decidable.lean
+++ b/library/standard/logic/classes/decidable.lean
@@ -74,4 +74,12 @@ rec_on Ha
     (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
   (assume Hna : ¬a, inl (assume Ha, absurd_elim b Ha Hna))
 
+theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
+rec_on Ha
+  (assume Ha : a,   inl (iff_elim_left H Ha))
+  (assume Hna : ¬a, inr (iff_elim_left (iff_flip_sign H) Hna))
+
+theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
+decidable_iff_equiv Ha (eq_to_iff H)
+
 end
\ No newline at end of file
diff --git a/library/standard/logic/connectives/if.lean b/library/standard/logic/connectives/if.lean
index 44bb046ee..2783def6c 100644
--- a/library/standard/logic/connectives/if.lean
+++ b/library/standard/logic/connectives/if.lean
@@ -5,8 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.classes.decidable tools.tactic
-
-using decidable tactic
+using decidable tactic eq_proofs
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
 rec_on H (assume Hc,  t) (assume Hnc, e)
@@ -36,3 +35,19 @@ if_pos trivial t e
 
 theorem if_false {A : Type} (t e : A) : (if false then t else e) = e :=
 if_neg not_false_trivial t e
+
+theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A}
+                     (Hc : c₁ = c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
+                 (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) :=
+have H1 : ∀ (H : decidable c₁), (@ite c₁ H₁ A t₁ e₁) = (@ite c₁ H A t₁ e₁), from
+  take H : decidable c₁,
+    have Hd : H₁ = H, from irrelevant H₁ H,
+    Hd ▸ refl (@ite c₁ H₁ A t₁ e₁),
+have H2 : (@ite c₁ H₁ A t₁ e₁) = (@ite c₂ H₂ A t₁ e₁), from
+  (Hc ▸ H1) H₂,
+Ht ▸ He ▸ H2
+
+theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ = c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) :
+                 (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_eq_equiv H₁ Hc) A t₂ e₂) :=
+have H2 [fact] : decidable c₂, from (decidable_eq_equiv H₁ Hc),
+if_congr_aux Hc Ht He