From 6ffd719c1a4ed10d7d65446c90f47b5c49f64409 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Fri, 29 Aug 2014 23:45:57 -0400 Subject: [PATCH] refactor(library/logic): move identities from classical to identities --- library/logic/axioms/classical.lean | 143 ++--------------------- library/logic/axioms/prop_decidable.lean | 5 +- library/logic/core/cast.lean | 2 +- library/logic/core/connectives.lean | 6 + library/logic/core/eq.lean | 4 +- library/logic/core/identities.lean | 119 ++++++++++++++++++- library/struc/wf.lean | 11 +- tests/lean/run/class4.lean | 4 +- tests/lean/run/is_nil.lean | 2 +- 9 files changed, 150 insertions(+), 146 deletions(-) diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 04b1787f9..b982c5665 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -2,61 +2,42 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura +-- logic.axioms.classical +-- ====================== + import logic.core.quantifiers logic.core.cast struc.relation using eq_ops axiom prop_complete (a : Prop) : a = true ∨ a = false -theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := +theorem cases (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := or_elim (prop_complete a) (assume Ht : a = true, Ht⁻¹ ▸ H1) (assume Hf : a = false, Hf⁻¹ ▸ H2) -theorem case_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a := -case P H1 H2 a +theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a := +cases P H1 H2 a +-- this supercedes the em in decidable theorem em (a : Prop) : a ∨ ¬a := or_elim (prop_complete a) - (assume Ht : a = true, or_inl (eqt_elim Ht)) - (assume Hf : a = false, or_inr (eqf_elim Hf)) + (assume Ht : a = true, or_inl (eq_true_elim Ht)) + (assume Hf : a = false, or_inr (eq_false_elim Hf)) theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true := -case (λ x, x = false ∨ x = true) +cases (λ x, x = false ∨ x = true) (or_inr (refl true)) (or_inl (refl false)) a -theorem not_true : (¬true) = false := -have aux : (¬true) ≠ true, from - assume H : (¬true) = true, - absurd trivial (H⁻¹ ▸ trivial), -resolve_right (prop_complete (¬true)) aux - -theorem not_false : (¬false) = true := -have aux : (¬false) ≠ false, from - assume H : (¬false) = false, - H ▸ not_false_trivial, -resolve_right (prop_complete_swapped (¬false)) aux - -theorem not_not_eq (a : Prop) : (¬¬a) = a := -case (λ x, (¬¬x) = x) - (calc (¬¬true) = (¬false) : {not_true} - ... = true : not_false) - (calc (¬¬false) = (¬true) : {not_false} - ... = false : not_true) - a - -theorem not_not_elim {a : Prop} (H : ¬¬a) : a := -(not_not_eq a) ▸ H - theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b := or_elim (prop_complete a) (assume Hat, or_elim (prop_complete b) (assume Hbt, Hat ⬝ Hbt⁻¹) - (assume Hbf, false_elim (a = b) (Hbf ▸ (Hab (eqt_elim Hat))))) + (assume Hbf, false_elim (a = b) (Hbf ▸ (Hab (eq_true_elim Hat))))) (assume Haf, or_elim (prop_complete b) - (assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eqt_elim Hbt)))) + (assume Hbt, false_elim (a = b) (Haf ▸ (Hba (eq_true_elim Hbt)))) (assume Hbf, Haf ⬝ Hbf⁻¹)) theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b := @@ -67,106 +48,6 @@ propext (assume H, iff_to_eq H) (assume H, eq_to_iff H) -theorem eqt_intro {a : Prop} (H : a) : a = true := -propext - (assume H1 : a, trivial) - (assume H2 : true, H) - -theorem eqf_intro {a : Prop} (H : ¬a) : a = false := -propext - (assume H1 : a, absurd H1 H) - (assume H2 : false, false_elim a H2) - -theorem by_contradiction {a : Prop} (H : ¬a → false) : a := -or_elim (em a) - (assume H1 : a, H1) - (assume H1 : ¬a, false_elim a (H H1)) - -theorem a_neq_a {A : Type} (a : A) : (a ≠ a) = false := -propext - (assume H, a_neq_a_elim H) - (assume H, false_elim (a ≠ a) H) - -theorem eq_id {A : Type} (a : A) : (a = a) = true := -eqt_intro (refl a) - -theorem heq_id {A : Type} (a : A) : (a == a) = true := -eqt_intro (hrefl a) - -theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) := -propext - (assume H, or_elim (em a) - (assume Ha, absurd (or_inl Ha) H) - (assume Hna, or_elim (em b) - (assume Hb, absurd (or_inr Hb) H) - (assume Hnb, and_intro Hna Hnb))) - (assume (H : ¬a ∧ ¬b) (N : a ∨ b), - or_elim N - (assume Ha, absurd Ha (and_elim_left H)) - (assume Hb, absurd Hb (and_elim_right H))) - -theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b) := -propext - (assume H, or_elim (em a) - (assume Ha, or_elim (em b) - (assume Hb, absurd (and_intro Ha Hb) H) - (assume Hnb, or_inr Hnb)) - (assume Hna, or_inl Hna)) - (assume (H : ¬a ∨ ¬b) (N : a ∧ b), - or_elim H - (assume Hna, absurd (and_elim_left N) Hna) - (assume Hnb, absurd (and_elim_right N) Hnb)) - -theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b) := -propext - (assume H : a → b, (or_elim (em a) - (assume Ha : a, or_inr (H Ha)) - (assume Hna : ¬a, or_inl Hna))) - (assume (H : ¬a ∨ b) (Ha : a), - resolve_right H ((not_not_eq a)⁻¹ ▸ Ha)) - -theorem not_implies (a b : Prop) : (¬(a → b)) = (a ∧ ¬b) := -calc (¬(a → b)) = (¬(¬a ∨ b)) : {imp_or a b} - ... = (¬¬a ∧ ¬b) : not_or (¬a) b - ... = (a ∧ ¬b) : {not_not_eq a} - -theorem a_eq_not_a (a : Prop) : (a = ¬a) = false := -propext - (assume H, or_elim (em a) - (assume Ha, absurd Ha (H ▸ Ha)) - (assume Hna, absurd (H⁻¹ ▸ Hna) Hna)) - (assume H, false_elim (a = ¬a) H) - -theorem true_eq_false : (true = false) = false := -not_true ▸ (a_eq_not_a true) - -theorem false_eq_true : (false = true) = false := -not_false ▸ (a_eq_not_a false) - -theorem a_eq_true (a : Prop) : (a = true) = a := -propext (assume H, eqt_elim H) (assume H, eqt_intro H) - -theorem a_eq_false (a : Prop) : (a = false) = ¬a := -propext (assume H, eqf_elim H) (assume H, eqf_intro H) - -theorem not_exists_forall {A : Type} {P : A → Prop} (H : ¬∃x, P x) : ∀x, ¬P x := -take x, or_elim (em (P x)) - (assume Hp : P x, absurd (exists_intro x Hp) H) - (assume Hn : ¬P x, Hn) - -theorem not_forall_exists {A : Type} {P : A → Prop} (H : ¬∀x, P x) : ∃x, ¬P x := -by_contradiction (assume H1 : ¬∃ x, ¬P x, - have H2 : ∀x, ¬¬P x, from not_exists_forall H1, - have H3 : ∀x, P x, from take x, not_not_elim (H2 x), - absurd H3 H) - -theorem peirce (a b : Prop) : ((a → b) → a) → a := -assume H, by_contradiction (assume Hna : ¬a, - have Hnna : ¬¬a, from not_implies_left (mt H Hna), - absurd (not_not_elim Hnna) Hna) - --- with classical logic, every predicate respects iff - using relation theorem iff_congr [instance] (P : Prop → Prop) : congr iff iff P := congr_mk diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index 98ce31a1f..d575875bc 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -1,8 +1,9 @@ ----------------------------------------------------------------------------------------------------- -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ----------------------------------------------------------------------------------------------------- + +-- logic.axioms.prop_decidable +-- =========================== import logic.axioms.classical logic.axioms.hilbert logic.classes.decidable using decidable inhabited nonempty diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean index a5c3aac52..748e05b10 100644 --- a/library/logic/core/cast.lean +++ b/library/logic/core/cast.lean @@ -45,7 +45,7 @@ theorem hrefl {A : Type} (a : A) : a == a := eq_to_heq (refl a) theorem heqt_elim {a : Prop} (H : a == true) : a := -eqt_elim (heq_to_eq H) +eq_true_elim (heq_to_eq H) opaque_hint (hiding cast) diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index 780005225..7b669fbd1 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -137,6 +137,12 @@ iff_intro calc_refl iff_refl calc_trans iff_trans +theorem iff_true_elim {a : Prop} (H : a ↔ true) : a := +iff_mp (iff_symm H) trivial + +theorem iff_false_elim {a : Prop} (H : a ↔ false) : ¬a := +assume Ha : a, iff_mp H Ha + theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb) diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean index 4b12924fa..235e86746 100644 --- a/library/logic/core/eq.lean +++ b/library/logic/core/eq.lean @@ -85,10 +85,10 @@ H1 ▸ H2 theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a := H1⁻¹ ▸ H2 -theorem eqt_elim {a : Prop} (H : a = true) : a := +theorem eq_true_elim {a : Prop} (H : a = true) : a := H⁻¹ ▸ trivial -theorem eqf_elim {a : Prop} (H : a = false) : ¬a := +theorem eq_false_elim {a : Prop} (H : a = false) : ¬a := assume Ha : a, H ▸ Ha theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c := diff --git a/library/logic/core/identities.lean b/library/logic/core/identities.lean index 2a8029e4d..31529ddab 100644 --- a/library/logic/core/identities.lean +++ b/library/logic/core/identities.lean @@ -1,6 +1,6 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Jeremy Avigad +-- Authors: Jeremy Avigad, Leonardo de Moura -- logic.connectives.identities -- ============================ @@ -8,9 +8,9 @@ -- Useful logical identities. In the absence of propositional extensionality, some of the -- calculations use the type class support provided by logic.connectives.instances -import logic.core.instances +import logic.core.instances logic.classes.decidable logic.core.quantifiers logic.core.cast -using relation +using relation decidable relation.iff_ops theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := calc @@ -35,3 +35,116 @@ calc a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm and_assoc ... ↔ (b ∧ a) ∧ c : {and_comm} ... ↔ b ∧ (a ∧ c) : and_assoc + + +theorem not_not_iff {a : Prop} {D : decidable a} : (¬¬a) ↔ a := +iff_intro + (assume H : ¬¬a, + by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H)) + (assume H : a, assume H', H' H) + +theorem not_not_elim {a : Prop} {D : decidable a} (H : ¬¬a) : a := +iff_mp not_not_iff H + +theorem not_true : (¬true) ↔ false := +iff_intro (assume H, H trivial) (false_elim _) + +theorem not_false : (¬false) ↔ true := +iff_intro (assume H, trivial) (assume H H', H') + +theorem not_or {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) := +iff_intro + (assume H, or_elim (em a) + (assume Ha, absurd (or_inl Ha) H) + (assume Hna, or_elim (em b) + (assume Hb, absurd (or_inr Hb) H) + (assume Hnb, and_intro Hna Hnb))) + (assume (H : ¬a ∧ ¬b) (N : a ∨ b), + or_elim N + (assume Ha, absurd Ha (and_elim_left H)) + (assume Hb, absurd Hb (and_elim_right H))) + +theorem not_and {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) := +iff_intro + (assume H, or_elim (em a) + (assume Ha, or_elim (em b) + (assume Hb, absurd (and_intro Ha Hb) H) + (assume Hnb, or_inr Hnb)) + (assume Hna, or_inl Hna)) + (assume (H : ¬a ∨ ¬b) (N : a ∧ b), + or_elim H + (assume Hna, absurd (and_elim_left N) Hna) + (assume Hnb, absurd (and_elim_right N) Hnb)) + +theorem imp_or {a b : Prop} {Da : decidable a} : (a → b) ↔ (¬a ∨ b) := +iff_intro + (assume H : a → b, (or_elim (em a) + (assume Ha : a, or_inr (H Ha)) + (assume Hna : ¬a, or_inl Hna))) + (assume (H : ¬a ∨ b) (Ha : a), + resolve_right H (not_not_iff⁻¹ ▸ Ha)) + +theorem not_implies {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a → b)) ↔ (a ∧ ¬b) := +calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or} + ... ↔ (¬¬a ∧ ¬b) : not_or + ... ↔ (a ∧ ¬b) : {not_not_iff} + +theorem peirce {a b : Prop} {D : decidable a} : ((a → b) → a) → a := +assume H, by_contradiction (assume Hna : ¬a, + have Hnna : ¬¬a, from not_implies_left (mt H Hna), + absurd (not_not_elim Hnna) Hna) + +theorem not_exists_forall {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)} + (H : ¬∃x, P x) : ∀x, ¬P x := +-- TODO: when type class instances can use quantifiers, we can use write em +take x, or_elim (@em _ (D x)) + (assume Hp : P x, absurd (exists_intro x Hp) H) + (assume Hn : ¬P x, Hn) + +theorem not_forall_exists {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)} + {D' : decidable (∃x, ¬P x)} (H : ¬∀x, P x) : + ∃x, ¬P x := +@by_contradiction _ D' (assume H1 : ¬∃x, ¬P x, + have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not_decidable (D x)) H1, + have H3 : ∀x, P x, from take x, @not_not_elim _ (D x) (H2 x), + absurd H3 H) + +theorem iff_true_intro {a : Prop} (H : a) : a ↔ true := +iff_intro + (assume H1 : a, trivial) + (assume H2 : true, H) + +theorem iff_false_intro {a : Prop} (H : ¬a) : a ↔ false := +iff_intro + (assume H1 : a, absurd H1 H) + (assume H2 : false, false_elim a H2) + +theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false := +iff_intro + (assume H, a_neq_a_elim H) + (assume H, false_elim (a ≠ a) H) + +theorem eq_id {A : Type} (a : A) : (a = a) ↔ true := +iff_true_intro (refl a) + +theorem heq_id {A : Type} (a : A) : (a == a) ↔ true := +iff_true_intro (hrefl a) + +theorem a_iff_not_a (a : Prop) : (a ↔ ¬a) ↔ false := +iff_intro + (assume H, + have H' : ¬a, from assume Ha, (H ▸ Ha) Ha, + H' (H⁻¹ ▸ H')) + (assume H, false_elim (a ↔ ¬a) H) + +theorem true_eq_false : (true ↔ false) ↔ false := +not_true ▸ (a_iff_not_a true) + +theorem false_eq_true : (false ↔ true) ↔ false := +not_false ▸ (a_iff_not_a false) + +theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a := +iff_intro (assume H, iff_true_elim H) (assume H, iff_true_intro H) + +theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a := +iff_intro (assume H, iff_false_elim H) (assume H, iff_false_intro H) diff --git a/library/struc/wf.lean b/library/struc/wf.lean index 162175d73..17e2254e8 100644 --- a/library/struc/wf.lean +++ b/library/struc/wf.lean @@ -1,10 +1,11 @@ ----------------------------------------------------------------------------------------------------- -- 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.axioms.classical +import logic.axioms.classical logic.axioms.prop_decidable logic.classes.decidable +import logic.core.identities + +using decidable -- Well-founded relation definition -- We are essentially saying that a relation R is well-founded @@ -16,7 +17,9 @@ definition wf {A : Type} (R : A → A → Prop) : Prop := theorem wf_induction {A : Type} {R : A → A → Prop} {P : A → Prop} (Hwf : wf R) (iH : ∀x, (∀y, R y x → P y) → P x) : ∀x, P x := by_contradiction (assume N : ¬∀x, P x, - obtain (w : A) (Hw : ¬P w), from not_forall_exists N, + -- TODO: when type classes can handle quantifiers, we will not need to give the implicit + -- arguments to not_forall_exists + obtain (w : A) (Hw : ¬P w), from @not_forall_exists _ _ (take x, _) _ N, -- The main "trick" is to define Q x as ¬P x. -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬P r) let Q x := ¬P x in diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index 3a9110d35..39f59eacb 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -19,10 +19,10 @@ definition is_zero (x : nat) := nat_rec true (λ n r, false) x theorem is_zero_zero : is_zero zero -:= eqt_elim (refl _) +:= eq_true_elim (refl _) theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x) -:= eqf_elim (refl _) +:= eq_false_elim (refl _) theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n) := nat_rec diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index 70cad2a88..dfa0355e7 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -9,7 +9,7 @@ definition is_nil {A : Type} (l : list A) : Prop := list_rec true (fun h t r, false) l theorem is_nil_nil (A : Type) : is_nil (@nil A) -:= eqt_elim (refl true) +:= eq_true_elim (refl true) theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil := not_intro (assume H : cons a l = nil,