From e817260c6d7ac2c38fbbf4f0485d1335bfbdc057 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Jul 2014 09:29:04 +0100 Subject: [PATCH] feat(library/standard): add or_comm, and_comm, ... theorems, cleanup notation Signed-off-by: Leonardo de Moura --- library/standard/cast.lean | 2 +- library/standard/classical.lean | 98 ++++++++++++++---------------- library/standard/logic.lean | 103 +++++++++++++++++++++----------- library/standard/wf.lean | 26 ++++---- 4 files changed, 127 insertions(+), 102 deletions(-) diff --git a/library/standard/cast.lean b/library/standard/cast.lean index 46f9b9418..849a8e7f3 100644 --- a/library/standard/cast.lean +++ b/library/standard/cast.lean @@ -16,7 +16,7 @@ theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a := calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a ... = a : cast_refl a -definition heq {A B : Type} (a : A) (b : B) := ∃ H, cast H a = b +definition heq {A B : Type} (a : A) (b : B) := ∃H, cast H a = b infixl `==`:50 := heq diff --git a/library/standard/classical.lean b/library/standard/classical.lean index 17b95fc5c..f9bbdf9bf 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -10,7 +10,7 @@ theorem case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a (assume Ht : a = true, subst (symm Ht) H1) (assume Hf : a = false, subst (symm Hf) H2) -theorem em (a : Bool) : a ∨ ¬ a +theorem em (a : Bool) : a ∨ ¬a := or_elim (boolcomplete a) (assume Ht : a = true, or_intro_left (¬ a) (eqt_elim Ht)) (assume Hf : a = false, or_intro_right a (eqf_elim Hf)) @@ -21,37 +21,37 @@ theorem boolcomplete_swapped (a : Bool) : a = false ∨ a = true (or_intro_left (false = true) (refl false)) a -theorem not_true : (¬ true) = false -:= have aux : ¬ (¬ true) = true, from - not_intro (assume H : (¬ true) = true, +theorem not_true : (¬true) = false +:= have aux : ¬ (¬true) = true, from + not_intro (assume H : (¬true) = true, absurd_not_true (subst (symm H) trivial)), - resolve_right (boolcomplete (¬ true)) aux + resolve_right (boolcomplete (¬true)) aux -theorem not_false : (¬ false) = true -:= have aux : ¬ (¬ false) = false, from - not_intro (assume H : (¬ false) = false, +theorem not_false : (¬false) = true +:= have aux : ¬ (¬false) = false, from + not_intro (assume H : (¬false) = false, subst H not_false_trivial), resolve_right (boolcomplete_swapped (¬ false)) aux -theorem not_not_eq (a : Bool) : (¬ ¬ a) = a -:= case (λ x, (¬ ¬ x) = x) - (calc (¬ ¬ true) = (¬ false) : { not_true } - ... = true : not_false) - (calc (¬ ¬ false) = (¬ true) : { not_false } - ... = false : not_true) +theorem not_not_eq (a : Bool) : (¬¬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 : Bool} (H : ¬ ¬ a) : a +theorem not_not_elim {a : Bool} (H : ¬¬a) : a := (not_not_eq a) ◂ H theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b := or_elim (boolcomplete a) - (λ Hat : a = true, or_elim (boolcomplete b) - (λ Hbt : b = true, trans Hat (symm Hbt)) - (λ Hbf : b = false, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat))))) - (λ Haf : a = false, or_elim (boolcomplete b) - (λ Hbt : b = true, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt)))) - (λ Hbf : b = false, trans Haf (symm Hbf))) + (assume Hat, or_elim (boolcomplete b) + (assume Hbt, trans Hat (symm Hbt)) + (assume Hbf, false_elim (a = b) (subst Hbf (Hab (eqt_elim Hat))))) + (assume Haf, or_elim (boolcomplete b) + (assume Hbt, false_elim (a = b) (subst Haf (Hba (eqt_elim Hbt)))) + (assume Hbf, trans Haf (symm Hbf))) theorem iff_to_eq {a b : Bool} (H : a ↔ b) : a = b := iff_elim (assume H1 H2, boolext H1 H2) H @@ -65,12 +65,12 @@ theorem eqt_intro {a : Bool} (H : a) : a = true := boolext (assume H1 : a, trivial) (assume H2 : true, H) -theorem eqf_intro {a : Bool} (H : ¬ a) : a = false +theorem eqf_intro {a : Bool} (H : ¬a) : a = false := boolext (assume H1 : a, absurd H1 H) (assume H2 : false, false_elim a H2) -theorem by_contradiction {a : Bool} (H : ¬ a → false) : a -:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) +theorem by_contradiction {a : Bool} (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 := boolext (assume H, a_neq_a_elim H) @@ -108,20 +108,18 @@ theorem not_and (a b : Bool) : (¬ (a ∧ b)) = (¬ a ∨ ¬ b) theorem imp_or (a b : Bool) : (a → b) = (¬ a ∨ b) := boolext - (assume H : a → b, - (or_elim (em a) - (λ Ha : a, or_intro_right (¬ a) (H Ha)) - (λ Hna : ¬ a, or_intro_left b Hna))) - (assume H : ¬ a ∨ b, - assume Ha : a, - resolve_right H ((symm (not_not_eq a)) ◂ Ha)) + (assume H : a → b, (or_elim (em a) + (assume Ha : a, or_intro_right (¬ a) (H Ha)) + (assume Hna : ¬ a, or_intro_left b Hna))) + (assume (H : ¬ a ∨ b) (Ha : a), + resolve_right H ((symm (not_not_eq a)) ◂ Ha)) -theorem not_implies (a b : Bool) : (¬ (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 not_implies (a b : Bool) : (¬ (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 : Bool) : (a = ¬ a) = false +theorem a_eq_not_a (a : Bool) : (a = ¬a) = false := boolext (assume H, or_elim (em a) (assume Ha, absurd Ha (subst H Ha)) @@ -135,27 +133,23 @@ theorem false_eq_true : (false = true) = false := subst not_false (a_eq_not_a false) theorem a_eq_true (a : Bool) : (a = true) = a -:= boolext - (assume H, eqt_elim H) - (assume H, eqt_intro H) +:= boolext (assume H, eqt_elim H) (assume H, eqt_intro H) -theorem a_eq_false (a : Bool) : (a = false) = (¬ a) -:= boolext - (assume H, eqf_elim H) - (assume H, eqf_intro H) +theorem a_eq_false (a : Bool) : (a = false) = ¬a +:= boolext (assume H, eqf_elim H) (assume H, eqf_intro H) -theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬ ∃ x, P x) : ∀ x, ¬ P x +theorem not_exists_forall {A : Type} {P : A → Bool} (H : ¬∃x, P x) : ∀x, ¬P x := take x, or_elim (em (P x)) - (assume Hp : P x, absurd_elim (¬ P x) (exists_intro x Hp) H) - (assume Hn : ¬ P x, Hn) + (assume Hp : P x, absurd_elim (¬P x) (exists_intro x Hp) H) + (assume Hn : ¬P x, Hn) -theorem not_forall_exists {A : Type} {P : A → Bool} (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), +theorem not_forall_exists {A : Type} {P : A → Bool} (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 : Bool) : ((a → b) → a) → a -:= assume H, by_contradiction (λ Hna : ¬ a, - have Hnna : ¬ ¬ a, from not_implies_left (mt H Hna), +:= assume H, by_contradiction (assume Hna : ¬a, + have Hnna : ¬¬a, from not_implies_left (mt H Hna), absurd (not_not_elim Hnna) Hna) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index bbc8cadd0..c12b52636 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.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. --- Author: Leonardo de Moura +-- Authors: Leonardo de Moura, Jeremy Avigad definition Bool [inline] := Type.{0} inductive false : Bool := @@ -18,34 +18,34 @@ prefix `¬`:40 := not notation `assume` binders `,` r:(scoped f, f) := r notation `take` binders `,` r:(scoped f, f) := r -theorem not_intro {a : Bool} (H : a → false) : ¬ a +theorem not_intro {a : Bool} (H : a → false) : ¬a := H -theorem not_elim {a : Bool} (H1 : ¬ a) (H2 : a) : false +theorem not_elim {a : Bool} (H1 : ¬a) (H2 : a) : false := H1 H2 -theorem absurd {a : Bool} (H1 : a) (H2 : ¬ a) : false +theorem absurd {a : Bool} (H1 : a) (H2 : ¬a) : false := H2 H1 -theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a +theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬b) : ¬a := assume Ha : a, absurd (H1 Ha) H2 theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a -:= assume Hnb : ¬ b, mt H Hnb +:= assume Hnb : ¬b, mt H Hnb -theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b +theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬a) : b := false_elim b (absurd H1 H2) -theorem absurd_not_true (H : ¬ true) : false +theorem absurd_not_true (H : ¬true) : false := absurd trivial H -theorem not_false_trivial : ¬ false +theorem not_false_trivial : ¬false := assume H : false, H -theorem not_implies_left {a b : Bool} (H : ¬ (a → b)) : ¬ ¬ a -:= assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna) H +theorem not_implies_left {a b : Bool} (H : ¬(a → b)) : ¬¬a +:= assume Hna : ¬a, absurd (assume Ha : a, absurd_elim b Ha Hna) H -theorem not_implies_right {a b : Bool} (H : ¬ (a → b)) : ¬ b +theorem not_implies_right {a b : Bool} (H : ¬(a → b)) : ¬b := assume Hb : b, absurd (assume Ha : a, Hb) H inductive and (a b : Bool) : Bool := @@ -58,10 +58,13 @@ theorem and_elim {a b c : Bool} (H1 : a → b → c) (H2 : a ∧ b) : c := and_rec H1 H2 theorem and_elim_left {a b : Bool} (H : a ∧ b) : a -:= and_rec (λ a b, a) H +:= and_rec (λa b, a) H theorem and_elim_right {a b : Bool} (H : a ∧ b) : b -:= and_rec (λ a b, b) H +:= and_rec (λa b, b) H + +theorem and_swap {a b : Bool} (H : a ∧ b) : b ∧ a +:= and_intro (and_elim_right H) (and_elim_left H) inductive or (a b : Bool) : Bool := | or_intro_left : a → or a b @@ -73,13 +76,13 @@ infixr `∨`:30 := or theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := or_rec H2 H3 H1 -theorem resolve_right {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b +theorem resolve_right {a b : Bool} (H1 : a ∨ b) (H2 : ¬a) : b := or_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb) -theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬ b) : a +theorem resolve_left {a b : Bool} (H1 : a ∨ b) (H2 : ¬b) : a := or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2) -theorem or_flip {a b : Bool} (H : a ∨ b) : b ∨ a +theorem or_swap {a b : Bool} (H : a ∨ b) : b ∨ a := or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb) inductive eq {A : Type} (a : A) : A → Bool := @@ -97,7 +100,7 @@ calc_subst subst calc_refl refl calc_trans trans -theorem true_ne_false : ¬ true = false +theorem true_ne_false : ¬true = false := assume H : true = false, subst H trivial @@ -113,10 +116,10 @@ theorem congr2 {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b := subst H1 (subst H2 (refl (f a))) -theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀ x, f x = g x +theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := take x, congr1 H x -theorem not_congr {a b : Bool} (H : a = b) : (¬ a) = (¬ b) +theorem not_congr {a b : Bool} (H : a = b) : (¬a) = (¬b) := congr2 not H theorem eqmp {a b : Bool} (H1 : a = b) (H2 : a) : b @@ -131,7 +134,7 @@ theorem eqmpr {a b : Bool} (H1 : a = b) (H2 : b) : a theorem eqt_elim {a : Bool} (H : a = true) : a := (symm H) ◂ trivial -theorem eqf_elim {a : Bool} (H : a = false) : ¬ a +theorem eqf_elim {a : Bool} (H : a = false) : ¬a := not_intro (assume Ha : a, H ◂ Ha) theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c @@ -143,7 +146,7 @@ theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b = c) : a → c theorem eq_imp_trans {a b c : Bool} (H1 : a = b) (H2 : b → c) : a → c := assume Ha, H2 (H1 ◂ Ha) -definition ne {A : Type} (a b : A) := ¬ (a = b) +definition ne {A : Type} (a b : A) := ¬(a = b) infix `≠`:50 := ne theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b @@ -171,7 +174,7 @@ calc_trans eq_ne_trans calc_trans ne_eq_trans definition iff (a b : Bool) := (a → b) ∧ (b → a) -infix `↔`:50 := iff +infix `↔`:25 := iff theorem iff_intro {a b : Bool} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2 @@ -194,34 +197,62 @@ theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a theorem eq_to_iff {a b : Bool} (H : a = b) : a ↔ b := iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb) +theorem and_comm (a b : Bool) : a ∧ b ↔ b ∧ a +:= iff_intro (λH, and_swap H) (λH, and_swap H) + +theorem and_assoc (a b c : Bool) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) +:= iff_intro + (assume H, and_intro + (and_elim_left (and_elim_left H)) + (and_intro (and_elim_right (and_elim_left H)) (and_elim_right H))) + (assume H, and_intro + (and_intro (and_elim_left H) (and_elim_left (and_elim_right H))) + (and_elim_right (and_elim_right H))) + +theorem or_comm (a b : Bool) : a ∨ b ↔ b ∨ a +:= iff_intro (λH, or_swap H) (λH, or_swap H) + +theorem or_assoc (a b c : Bool) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) +:= iff_intro + (assume H, or_elim H + (assume H1, or_elim H1 + (assume Ha, or_intro_left _ Ha) + (assume Hb, or_intro_right a (or_intro_left c Hb))) + (assume Hc, or_intro_right a (or_intro_right b Hc))) + (assume H, or_elim H + (assume Ha, (or_intro_left c (or_intro_left b Ha))) + (assume H1, or_elim H1 + (assume Hb, or_intro_left c (or_intro_right a Hb)) + (assume Hc, or_intro_right _ Hc))) + inductive Exists {A : Type} (P : A → Bool) : Bool := | exists_intro : ∀ (a : A), P a → Exists P notation `∃` binders `,` r:(scoped P, Exists P) := r -theorem exists_elim {A : Type} {P : A → Bool} {B : Bool} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) : B +theorem exists_elim {A : Type} {p : A → Bool} {B : Bool} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B := Exists_rec H2 H1 -theorem exists_not_forall {A : Type} {P : A → Bool} (H : ∃ x, P x) : ¬ ∀ x, ¬ P x -:= assume H1 : ∀ x, ¬ P x, - obtain (w : A) (Hw : P w), from H, +theorem exists_not_forall {A : Type} {p : A → Bool} (H : ∃x, p x) : ¬∀x, ¬p x +:= assume H1 : ∀x, ¬p x, + obtain (w : A) (Hw : p w), from H, absurd Hw (H1 w) -theorem forall_not_exists {A : Type} {P : A → Bool} (H2 : ∀ x, P x) : ¬ ∃ x, ¬ P x -:= assume H1 : ∃ x, ¬ P x, - obtain (w : A) (Hw : ¬ P w), from H1, +theorem forall_not_exists {A : Type} {p : A → Bool} (H2 : ∀x, p x) : ¬∃x, ¬p x +:= assume H1 : ∃x, ¬p x, + obtain (w : A) (Hw : ¬p w), from H1, absurd (H2 w) Hw -definition exists_unique {A : Type} (p : A → Bool) := ∃ x, p x ∧ ∀ y, y ≠ x → ¬ p y +definition exists_unique {A : Type} (p : A → Bool) := ∃x, p x ∧ ∀y, y ≠ x → ¬ p y notation `∃!` binders `,` r:(scoped P, exists_unique P) := r -theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : ∀ y, y ≠ w → ¬ p y) : ∃! x, p x +theorem exists_unique_intro {A : Type} {p : A → Bool} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬ p y) : ∃!x, p x := exists_intro w (and_intro H1 H2) -theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃! x, p x) (H1 : ∀ x, p x → (∀ y, y ≠ x → ¬ p y) → b) : b +theorem exists_unique_elim {A : Type} {p : A → Bool} {b : Bool} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬ p y) → b) : b := obtain w Hw, from H2, - H1 w (and_elim_left Hw) (and_elim_right Hw) + H1 w (and_elim_left Hw) (and_elim_right Hw) inductive inhabited (A : Type) : Bool := | inhabited_intro : A → inhabited A @@ -233,7 +264,7 @@ theorem inhabited_Bool [instance] : inhabited Bool := inhabited_intro true theorem inhabited_fun [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) -:= inhabited_elim H (take (b : B), inhabited_intro (λ a : A, b)) +:= inhabited_elim H (take b, inhabited_intro (λa, b)) -theorem inhabited_exists {A : Type} {P : A → Bool} (H : ∃ x, P x) : inhabited A +theorem inhabited_exists {A : Type} {p : A → Bool} (H : ∃x, p x) : inhabited A := obtain w Hw, from H, inhabited_intro w diff --git a/library/standard/wf.lean b/library/standard/wf.lean index 02051eaab..fd5a7ccb1 100644 --- a/library/standard/wf.lean +++ b/library/standard/wf.lean @@ -7,24 +7,24 @@ import logic classical -- We are essentially saying that a relation R is well-founded -- if every non-empty "set" P, has a R-minimal element definition wf {A : Type} (R : A → A → Bool) : Bool -:= ∀ P, (∃ w, P w) → ∃ min, P min ∧ ∀ b, R b min → ¬ P b +:= ∀P, (∃w, P w) → ∃min, P min ∧ ∀b, R b min → ¬P b -- Well-founded induction theorem -theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (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, +theorem wf_induction {A : Type} {R : A → A → Bool} {P : A → Bool} (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, -- 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 [inline] := λ x, ¬ P x in - have Qw : ∃ w, Q w, from exists_intro w Hw, - have Qwf : ∃ min, Q min ∧ ∀ b, R b min → ¬ Q b, from Hwf Q Qw, - obtain (r : A) (Hr : Q r ∧ ∀ b, R b r → ¬ Q b), from Qwf, + let Q [inline] x := ¬P x in + have Qw : ∃w, Q w, from exists_intro w Hw, + have Qwf : ∃min, Q min ∧ ∀b, R b min → ¬Q b, from Hwf Q Qw, + obtain (r : A) (Hr : Q r ∧ ∀b, R b r → ¬Q b), from Qwf, -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction. - have s1 : ∀ b, R b r → P b, from + have s1 : ∀b, R b r → P b, from take b : A, assume H : R b r, -- We are using Hr to derive ¬ ¬ P b not_not_elim (and_elim_right Hr b H), - have s2 : P r, from iH r s1, - have s3 : ¬ P r, from and_elim_left Hr, - show false, from absurd s2 s3) + have s2 : P r, from iH r s1, + have s3 : ¬P r, from and_elim_left Hr, + absurd s2 s3)