From abe1dbd7e0c66f71d92cae110474f2e8bc5b2297 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 11:36:28 -0700 Subject: [PATCH] refactor(library/standard): cleanup notation Signed-off-by: Leonardo de Moura --- library/standard/bool.lean | 2 +- library/standard/classical.lean | 42 ++++++++++++++++---------------- library/standard/diaconescu.lean | 4 +-- library/standard/logic.lean | 13 ++++------ library/standard/wf.lean | 6 ++--- 5 files changed, 32 insertions(+), 35 deletions(-) diff --git a/library/standard/bool.lean b/library/standard/bool.lean index ddd203f68..aa44614da 100644 --- a/library/standard/bool.lean +++ b/library/standard/bool.lean @@ -116,6 +116,6 @@ using decidable theorem decidable_eq [instance] (a b : bool) : decidable (a = b) := bool_rec (bool_rec (inl (refl '0)) (inr b0_ne_b1) b) - (bool_rec (inr (not_eq_symm b0_ne_b1)) (inl (refl '1)) b) + (bool_rec (inr (ne_symm b0_ne_b1)) (inl (refl '1)) b) a end diff --git a/library/standard/classical.lean b/library/standard/classical.lean index ae4df841e..271fa6bb4 100644 --- a/library/standard/classical.lean +++ b/library/standard/classical.lean @@ -13,7 +13,7 @@ theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a theorem em (a : Prop) : a ∨ ¬a := or_elim (prop_complete a) - (assume Ht : a = true, or_intro_left (¬ a) (eqt_elim Ht)) + (assume Ht : a = true, or_intro_left (¬a) (eqt_elim Ht)) (assume Hf : a = false, or_intro_right a (eqf_elim Hf)) theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true @@ -23,16 +23,16 @@ theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true a theorem not_true : (¬true) = false -:= have aux : ¬ (¬true) = true, from +:= have aux : (¬true) ≠ true, from assume H : (¬true) = true, absurd_not_true (H⁻¹ ▸ trivial), resolve_right (prop_complete (¬true)) aux theorem not_false : (¬false) = true -:= have aux : ¬ (¬false) = false, from +:= have aux : (¬false) ≠ false, from assume H : (¬false) = false, H ▸ not_false_trivial, - resolve_right (prop_complete_swapped (¬ false)) aux + resolve_right (prop_complete_swapped (¬false)) aux theorem not_not_eq (a : Prop) : (¬¬a) = a := case (λ x, (¬¬x) = x) @@ -83,41 +83,41 @@ theorem eq_id {A : Type} (a : A) : (a = a) = true theorem heq_id {A : Type} (a : A) : (a == a) = true := eqt_intro (hrefl a) -theorem not_or (a b : Prop) : (¬ (a ∨ b)) = (¬ a ∧ ¬ b) +theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b) := propext (assume H, or_elim (em a) - (assume Ha, absurd_elim (¬ a ∧ ¬ b) (or_intro_left b Ha) H) + (assume Ha, absurd_elim (¬a ∧ ¬b) (or_intro_left b Ha) H) (assume Hna, or_elim (em b) - (assume Hb, absurd_elim (¬ a ∧ ¬ b) (or_intro_right a Hb) H) + (assume Hb, absurd_elim (¬a ∧ ¬b) (or_intro_right a Hb) H) (assume Hnb, and_intro Hna Hnb))) - (assume (H : ¬ a ∧ ¬ b) (N : a ∨ b), + (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) +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_elim (¬ a ∨ ¬ b) (and_intro Ha Hb) H) - (assume Hnb, or_intro_right (¬ a) Hnb)) - (assume Hna, or_intro_left (¬ b) Hna)) - (assume (H : ¬ a ∨ ¬ b) (N : a ∧ b), + (assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H) + (assume Hnb, or_intro_right (¬a) Hnb)) + (assume Hna, or_intro_left (¬b) 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) +theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b) := propext (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), + (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 ((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 +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 @@ -125,7 +125,7 @@ theorem a_eq_not_a (a : Prop) : (a = ¬a) = false (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) + (assume H, false_elim (a = ¬a) H) theorem true_eq_false : (true = false) = false := not_true ▸ (a_eq_not_a true) diff --git a/library/standard/diaconescu.lean b/library/standard/diaconescu.lean index 730693fb6..5d338a18f 100644 --- a/library/standard/diaconescu.lean +++ b/library/standard/diaconescu.lean @@ -44,8 +44,8 @@ lemma p_implies_uv [private] : p → u = v show u = v, from Hpred ▸ (refl (epsilon (λ x, x = true ∨ p))) -theorem em : p ∨ ¬ p -:= have H : ¬(u = v) → ¬ p, from contrapos p_implies_uv, +theorem em : p ∨ ¬p +:= have H : ¬(u = v) → ¬p, from contrapos p_implies_uv, or_elim uv_implies_p (assume Hne : ¬(u = v), or_intro_right p (H Hne)) (assume Hp : p, or_intro_left (¬p) Hp) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index f15aa99d9..0bcd5c090 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -32,7 +32,7 @@ theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a 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 +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 @@ -196,11 +196,8 @@ theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a) -theorem not_eq_symm {A : Type} {a b : A} (H : ¬ a = b) : ¬ b = a -:= assume H1 : b = a, H (H1⁻¹) - theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a -:= not_eq_symm H +:= 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 @@ -301,14 +298,14 @@ theorem forall_not_exists {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, obtain (w : A) (Hw : ¬p w), from H1, absurd (H2 w) Hw -definition exists_unique {A : Type} (p : A → Prop) := ∃x, p x ∧ ∀y, y ≠ x → ¬ p y +definition exists_unique {A : Type} (p : A → Prop) := ∃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 → Prop} (w : A) (H1 : p w) (H2 : ∀y, y ≠ w → ¬ p y) : ∃!x, p x +theorem exists_unique_intro {A : Type} {p : A → Prop} (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 → Prop} {b : Prop} (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, y ≠ x → ¬ p y) → b) : b +theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop} (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) diff --git a/library/standard/wf.lean b/library/standard/wf.lean index df0e4bc55..f56d3d30f 100644 --- a/library/standard/wf.lean +++ b/library/standard/wf.lean @@ -14,8 +14,8 @@ theorem wf_induction {A : Type} {R : A → A → Prop} {P : A → Prop} (Hwf : w : ∀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) + -- 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, @@ -23,7 +23,7 @@ theorem wf_induction {A : Type} {R : A → A → Prop} {P : A → Prop} (Hwf : w -- Using the inductive hypothesis iH and Hr, we show P r, and derive the contradiction. 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 + -- 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,