feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions

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

library/standard/logic/axioms/examples/diaconescu.lean

@@ -47,7 +47,7 @@ assume Hp : p,
     Hpred ▸ (refl (epsilon (λ x, x = true ∨ p)))
 
 theorem em : p ∨ ¬p :=
-have H : ¬(u = v) → ¬p, from contrapos p_implies_uv,
+have H : ¬(u = v) → ¬p, from mt p_implies_uv,
   or_elim uv_implies_p
     (assume Hne : ¬(u = v), or_inr (H Hne))
     (assume Hp : p, or_inl Hp)

library/standard/logic/classes/decidable.lean

@@ -12,12 +12,15 @@ inductive decidable (p : Prop) : Type :=
 | inl : p  → decidable p
 | inr : ¬p → decidable p
 
+theorem decidable_true [instance] : decidable true :=
+inl trivial
+
+theorem decidable_false [instance] : decidable false :=
+inr not_false_trivial
+
 theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
 decidable_rec H1 H2 H
 
-theorem em {p : Prop} (H : decidable p) : p ∨ ¬p :=
-induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
-
 definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
 decidable_rec H1 H2 H
 
@@ -33,11 +36,13 @@ decidable_rec
     d2)
   d1
 
-theorem decidable_true [instance] : decidable true :=
-inl trivial
+theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
+induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
 
-theorem decidable_false [instance] : decidable false :=
-inr not_false_trivial
+theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
+or_elim (em p)
+  (assume H1 : p, H1)
+  (assume H1 : ¬p, false_elim p (H H1))
 
 theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) :=
 rec_on Ha

library/standard/logic/connectives/basic.lean

@@ -45,9 +45,6 @@ assume Hna : ¬a, absurd Ha Hna
 theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
 assume Ha : a, absurd (H1 Ha) H2
 
-theorem contrapos {a b : Prop} (H : a → b) : ¬b → ¬a :=
-assume Hnb : ¬b, mt H Hnb
-
 theorem absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬a) : b :=
 false_elim b (absurd H1 H2)
 

library/standard/logic/connectives/eq.lean

@@ -98,9 +98,17 @@ theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a)
 theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a :=
 assume H1 : b = a, H (H1⁻¹)
 
-theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := H1⁻¹ ▸ H2
+theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c :=
+H1⁻¹ ▸ H2
 
-theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := H2 ▸ H1
+theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c :=
+H2 ▸ H1
 
 calc_trans eq_ne_trans
 calc_trans ne_eq_trans
+
+theorem p_ne_false {p : Prop} (Hp : p) : p ≠ false :=
+assume Heq : p = false, Heq ▸ Hp
+
+theorem p_ne_true {p : Prop} (Hnp : ¬p) : p ≠ true :=
+assume Heq : p = true, absurd_not_true (Heq ▸ Hnp)

library/standard/logic/connectives/if.lean

@@ -51,3 +51,23 @@ theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t
                  (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
+
+exit
+theorem app_if_distribute {A B : Type} (c : Prop) {H : decidable c} (f : A → B) (a b : A) : f (if c then a else b) = if c then f a else f b :=
+or_elim (decidable.em H)
+  (assume Hc  :  c, calc
+    f (if c then a else b) = f (if true then a else b)    : { eqt_intro Hc }
+  (assume Hnc : ¬c, sorry)
+
+exit
+:= or_elim (em c)
+     (λ Hc : c , calc
+          f (if c then a else b) = f (if true then a else b)    : { eqt_intro Hc }
+                            ...  = f a                          : { if_true a b }
+                            ...  = if true then f a else f b    : symm (if_true (f a) (f b))
+                            ...  = if c then f a else f b       : { symm (eqt_intro Hc) })
+     (λ Hnc : ¬ c, calc
+          f (if c then a else b) = f (if false then a else b)   : { eqf_intro Hnc }
+                            ...  = f b                          : { if_false a b }
+                            ...  = if false then f a else f b   : symm (if_false (f a) (f b))
+                            ...  = if c then f a else f b       : { symm (eqf_intro Hnc) })