From c3f57cdb1cdade42893ddb752695a5156eab97af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 3 Aug 2014 22:58:12 -0700 Subject: [PATCH] feat(library/standard/logic/classes): add 'by_contradiction' theorem for decidable propositions Signed-off-by: Leonardo de Moura --- .../logic/axioms/examples/diaconescu.lean | 2 +- library/standard/logic/classes/decidable.lean | 19 +++++++++++------- library/standard/logic/connectives/basic.lean | 3 --- library/standard/logic/connectives/eq.lean | 14 ++++++++++--- library/standard/logic/connectives/if.lean | 20 +++++++++++++++++++ 5 files changed, 44 insertions(+), 14 deletions(-) diff --git a/library/standard/logic/axioms/examples/diaconescu.lean b/library/standard/logic/axioms/examples/diaconescu.lean index d48fb2cf8..00e33adb7 100644 --- a/library/standard/logic/axioms/examples/diaconescu.lean +++ b/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) diff --git a/library/standard/logic/classes/decidable.lean b/library/standard/logic/classes/decidable.lean index cdb378446..c916d2c0e 100644 --- a/library/standard/logic/classes/decidable.lean +++ b/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 diff --git a/library/standard/logic/connectives/basic.lean b/library/standard/logic/connectives/basic.lean index 5ac020c7a..2dacc6bbc 100644 --- a/library/standard/logic/connectives/basic.lean +++ b/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) diff --git a/library/standard/logic/connectives/eq.lean b/library/standard/logic/connectives/eq.lean index 56bd90c9b..e60df7082 100644 --- a/library/standard/logic/connectives/eq.lean +++ b/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 \ No newline at end of file +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) diff --git a/library/standard/logic/connectives/if.lean b/library/standard/logic/connectives/if.lean index 2783def6c..6d8256500 100644 --- a/library/standard/logic/connectives/if.lean +++ b/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) })