From 8f83c78bc9e97fc99b1930532202a0a79801053d Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Tue, 16 Feb 2016 11:54:26 -0500 Subject: [PATCH] fix(library/logic/identities,library/*): fix implicit arguments, add implications. Closes #1002. --- library/data/list/basic.lean | 2 +- library/data/real/complete.lean | 8 ++-- library/logic/identities.lean | 42 +++++++++++++-------- library/theories/analysis/metric_space.lean | 14 +++---- library/theories/group_theory/cyclic.lean | 2 +- 5 files changed, 40 insertions(+), 28 deletions(-) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index a8a8867ee6..2d7bd1c37b 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -401,7 +401,7 @@ list.rec_on l assume iH : ¬x ∈ l → find x l = length l, suppose ¬x ∈ y::l, have ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem_cons_iff) this, - have ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not this), + have ¬x = y ∧ ¬x ∈ l, from (iff.elim_left !not_or_iff_not_and_not this), calc find x (y::l) = if x = y then 0 else succ (find x l) : !find_cons ... = succ (find x l) : if_neg (and.elim_left this) diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 094e556c99..4f92638252 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -621,7 +621,7 @@ private theorem under_spec : ¬ ub under := rewrite ↑ub, apply not_forall_of_exists_not, existsi elt, - apply iff.mpr not_implies_iff_and_not, + apply iff.mpr !not_implies_iff_and_not, apply and.intro, apply inh, apply not_le_of_gt under_spec1 @@ -780,7 +780,7 @@ private theorem PB (n : ℕ) : ub (over_seq n) := private theorem under_lt_over : under < over := begin cases exists_not_of_not_forall under_spec with [x, Hx], - cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu], + cases and_not_of_not_implies Hx with [HXx, Hxu], apply lt_of_of_rat_lt_of_rat, apply lt_of_lt_of_le, apply lt_of_not_ge Hxu, @@ -791,7 +791,7 @@ private theorem under_seq_lt_over_seq : ∀ m n : ℕ, under_seq m < over_seq n begin intros, cases exists_not_of_not_forall (PA m) with [x, Hx], - cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu], + cases iff.mp !not_implies_iff_and_not Hx with [HXx, Hxu], apply lt_of_of_rat_lt_of_rat, apply lt_of_lt_of_le, apply lt_of_not_ge Hxu, @@ -947,7 +947,7 @@ private theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y := apply le_of_reprs_le, intro n, cases exists_not_of_not_forall (PA _) with [x, Hx], - cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxn], + cases and_not_of_not_implies Hx with [HXx, Hxn], apply le.trans, apply le_of_lt, apply lt_of_not_ge Hxn, diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 81473cd8dc..9c418a47db 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -21,54 +21,66 @@ calc ... ↔ a ∧ (c ∧ b) : {and.comm} ... ↔ (a ∧ c) ∧ b : iff.symm and.assoc -theorem or_not_self_iff {a : Prop} [D : decidable a] : a ∨ ¬ a ↔ true := +theorem or_not_self_iff (a : Prop) [D : decidable a] : a ∨ ¬ a ↔ true := iff.intro (assume H, trivial) (assume H, em a) -theorem not_or_self_iff {a : Prop} [D : decidable a] : ¬ a ∨ a ↔ true := +theorem not_or_self_iff (a : Prop) [D : decidable a] : ¬ a ∨ a ↔ true := iff.intro (λ H, trivial) (λ H, or.swap (em a)) -theorem and_not_self_iff {a : Prop} : a ∧ ¬ a ↔ false := +theorem and_not_self_iff (a : Prop) : a ∧ ¬ a ↔ false := iff.intro (assume H, (and.right H) (and.left H)) (assume H, false.elim H) -theorem not_and_self_iff {a : Prop} : ¬ a ∧ a ↔ false := +theorem not_and_self_iff (a : Prop) : ¬ a ∧ a ↔ false := iff.intro (λ H, and.elim H (by contradiction)) (λ H, false.elim H) -theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a := +theorem not_not_iff (a : Prop) [D : decidable a] : ¬¬a ↔ a := iff.intro by_contradiction not_not_intro theorem not_not_elim {a : Prop} [D : decidable a] : ¬¬a → a := by_contradiction -theorem not_or_iff_not_and_not {a b : Prop} : ¬(a ∨ b) ↔ ¬a ∧ ¬b := +theorem not_or_iff_not_and_not (a b : Prop) : ¬(a ∨ b) ↔ ¬a ∧ ¬b := or.imp_distrib -theorem not_and_iff_not_or_not {a b : Prop} [Da : decidable a] : +theorem not_or_not_of_not_and {a b : Prop} [Da : decidable a] (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b := +by_cases (λHa, or.inr (not.mto (and.intro Ha) H)) or.inl + +theorem not_or_not_of_not_and' {a b : Prop} [Db : decidable b] (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b := +by_cases (λHb, or.inl (λHa, H (and.intro Ha Hb))) or.inr + +theorem not_and_iff_not_or_not (a b : Prop) [Da : decidable a] : ¬(a ∧ b) ↔ ¬a ∨ ¬b := iff.intro - (λH, by_cases (λa, or.inr (not.mto (and.intro a) H)) or.inl) + not_or_not_of_not_and (or.rec (not.mto and.left) (not.mto and.right)) -theorem or_iff_not_and_not {a b : Prop} [Da : decidable a] [Db : decidable b] : +theorem or_iff_not_and_not (a b : Prop) [Da : decidable a] [Db : decidable b] : a ∨ b ↔ ¬ (¬a ∧ ¬b) := by rewrite [-not_or_iff_not_and_not, not_not_iff] -theorem and_iff_not_or_not {a b : Prop} [Da : decidable a] [Db : decidable b] : +theorem and_iff_not_or_not (a b : Prop) [Da : decidable a] [Db : decidable b] : a ∧ b ↔ ¬ (¬ a ∨ ¬ b) := by rewrite [-not_and_iff_not_or_not, not_not_iff] -theorem imp_iff_not_or {a b : Prop} [Da : decidable a] : (a → b) ↔ ¬a ∨ b := +theorem imp_iff_not_or (a b : Prop) [Da : decidable a] : (a → b) ↔ ¬a ∨ b := iff.intro (by_cases (λHa H, or.inr (H Ha)) (λHa H, or.inl Ha)) (or.rec not.elim imp.intro) -theorem not_implies_iff_and_not {a b : Prop} [Da : decidable a] : +theorem not_implies_iff_and_not (a b : Prop) [Da : decidable a] : ¬(a → b) ↔ a ∧ ¬b := calc - ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or} + ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or a b} ... ↔ ¬¬a ∧ ¬b : not_or_iff_not_and_not - ... ↔ a ∧ ¬b : {not_not_iff} + ... ↔ a ∧ ¬b : {not_not_iff a} -theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a := +theorem and_not_of_not_implies {a b : Prop} [Da : decidable a] (H : ¬ (a → b)) : a ∧ ¬ b := +iff.mp !not_implies_iff_and_not H + +theorem not_implies_of_and_not {a b : Prop} [Da : decidable a] (H : a ∧ ¬ b) : ¬ (a → b) := +iff.mpr !not_implies_iff_and_not H + +theorem peirce (a b : Prop) [D : decidable a] : ((a → b) → a) → a := by_cases imp.intro (imp.syl imp.mp not.elim) theorem forall_not_of_not_exists {A : Type} {p : A → Prop} [D : ∀x, decidable (p x)] diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index b3f0372fae..7c42303b83 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -349,7 +349,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) by_contradiction (assume Hnot : ¬ (f ⟶ l at c), obtain ε Hε, from exists_not_of_not_forall Hnot, - let Hε' := iff.mp not_implies_iff_and_not Hε in + let Hε' := and_not_of_not_implies Hε in obtain (H1 : ε > 0) H2, from Hε', have H3 [visible] : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!! intros δ Hδ, @@ -359,7 +359,7 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) note H5 := exists_not_of_not_forall this, cases H5 with x' Hx', existsi x', - note H6 := iff.mp not_implies_iff_and_not Hx', + note H6 := and_not_of_not_implies Hx', rewrite and.assoc at H6, cases H6, split, @@ -560,8 +560,8 @@ private theorem not_mem_intersect_of_boundary_pt {s t : set V} (a : Open s) (a_1 note Htih := exists_not_of_not_forall (v_1 Hxt), cases Hsih with ε1 Hε1, cases Htih with ε2 Hε2, - note Hε1' := iff.mp not_implies_iff_and_not Hε1, - note Hε2' := iff.mp not_implies_iff_and_not Hε2, + note Hε1' := and_not_of_not_implies Hε1, + note Hε2' := and_not_of_not_implies Hε2, cases Hε1' with Hε1p Hε1', cases Hε2' with Hε2p Hε2', note Hε1'' := forall_not_of_not_exists Hε1', @@ -596,7 +596,7 @@ private theorem not_mem_sUnion_of_boundary_pt {S : set (set V)} (a : ∀₀ s cases Hex with s Hs, cases Hs with Hs Hxs, cases exists_not_of_not_forall (v_0 Hs Hxs) with ε Hε, - cases iff.mp not_implies_iff_and_not Hε with Hεp Hv, + cases and_not_of_not_implies Hε with Hεp Hv, cases Hbd _ Hεp with v Hv', cases Hv' with Hvnm Hdist, apply Hv, @@ -633,13 +633,13 @@ theorem ex_Open_ball_subset_of_Open_of_nonempty {U : set V} (HU : Open U) {x : V cases em (balloon = ∅), have H : ∀ r : ℝ, r > 0 → ∃ v : V, v ∉ U ∧ dist x v < r, begin intro r Hr, - note Hor := iff.mp not_and_iff_not_or_not (forall_not_of_sep_empty a (mem_univ r)), + note Hor := not_or_not_of_not_and (forall_not_of_sep_empty a (mem_univ r)), note Hor' := or.neg_resolve_left Hor Hr, apply exists_of_not_forall_not, intro Hall, apply Hor', intro y Hy, - cases iff.mp not_and_iff_not_or_not (Hall y) with Hmem Hge, + cases not_or_not_of_not_and (Hall y) with Hmem Hge, apply not_not_elim Hmem, apply absurd (and.right Hy) Hge end, diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index 4a1130fd95..3f861bafb1 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/library/theories/group_theory/cyclic.lean @@ -69,7 +69,7 @@ assert Pninj : ¬(injective f), from assume Pinj, (begin rewrite [card_fin], apply not_succ_le_self end), obtain i₁ P₁, from exists_not_of_not_forall Pninj, obtain i₂ P₂, from exists_not_of_not_forall P₁, -obtain Pfe Pne, from iff.elim_left not_implies_iff_and_not P₂, +obtain Pfe Pne, from and_not_of_not_implies P₂, assert Pvne : val i₁ ≠ val i₂, from assume Pveq, absurd (eq_of_veq Pveq) Pne, exists.intro (pred (dist i₁ i₂)) (begin rewrite [succ_pred_of_pos (dist_pos_of_ne Pvne)], apply and.intro,