michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/logic/identities,library/*): fix implicit arguments, add implications. Closes #1002.

Browse source
This commit is contained in:
Jeremy Avigad 2016-02-16 11:54:26 -05:00 committed by Leonardo de Moura
parent 769ae6830d
commit 8f83c78bc9
5 changed files with 40 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/list/basic.lean
View file

@ -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)

8
library/data/real/complete.lean
View file

@ -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,

42
library/logic/identities.lean
View file

@ -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)]

14
library/theories/analysis/metric_space.lean
View file

@ -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,

2
library/theories/group_theory/cyclic.lean
View file

@ -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,