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

feat(library/algebra): add one directional versions of iff theorems

Browse source
This commit is contained in:
Rob Lewis 2015-08-03 17:16:18 -04:00
parent 78942a0689
commit e004ed8cba
3 changed files with 146 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
library/algebra/group.lean
View file

@ -197,9 +197,12 @@ section group
theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
iff.intro (assume H, inv.inj H) (assume H, congr_arg _ H)
theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
theorem inv_eq_one_iff_eq_one (a : A) : a⁻¹ = 1 ↔ a = 1 :=
one_inv ▸ inv_eq_inv_iff_eq a 1
theorem eq_one_of_inv_eq_one (a : A) : a⁻¹ = 1 → a = 1 :=
iff.mp !inv_eq_one_iff_eq_one
theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
by rewrite [H, inv_inv]
@ -379,9 +382,15 @@ section add_group
theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
iff.intro (assume H, neg.inj H) (assume H, congr_arg _ H)
theorem eq_of_neg_eq_neg {a b : A} : -a = -b → a = b :=
iff.mp !neg_eq_neg_iff_eq
theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 :=
neg_zero ▸ !neg_eq_neg_iff_eq
theorem eq_zero_of_neg_eq_zero {a : A} : -a = 0 → a = 0 :=
iff.mp !neg_eq_zero_iff_eq_zero
theorem eq_neg_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
H⁻¹ ▸ (neg_neg b)⁻¹

134
library/algebra/ordered_group.lean
View file

@ -278,87 +278,219 @@ section
theorem le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff_le
theorem le_neg_of_le_neg : a ≤ -b → b ≤ -a := iff.mp !le_neg_iff_le_neg
theorem neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff_le
theorem neg_le_of_neg_le : -a ≤ b → -b ≤ a := iff.mp !neg_le_iff_neg_le
theorem lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff_lt
theorem lt_neg_of_lt_neg : a < -b → b < -a := iff.mp !lt_neg_iff_lt_neg
theorem neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff_lt
theorem neg_lt_of_neg_lt : -a < b → -b < a := iff.mp !neg_lt_iff_neg_lt
theorem sub_nonneg_iff_le : 0 ≤ a - b ↔ b ≤ a := !sub_self ▸ !add_le_add_right_iff
theorem sub_nonneg_of_le : b ≤ a → 0 ≤ a - b := iff.mpr !sub_nonneg_iff_le
theorem le_of_sub_nonneg : 0 ≤ a - b → b ≤ a := iff.mp !sub_nonneg_iff_le
theorem sub_nonpos_iff_le : a - b ≤ 0 ↔ a ≤ b := !sub_self ▸ !add_le_add_right_iff
theorem sub_nonpos_of_le : a ≤ b → a - b ≤ 0 := iff.mpr !sub_nonpos_iff_le
theorem le_of_sub_nonpos : a - b ≤ 0 → a ≤ b := iff.mp !sub_nonpos_iff_le
theorem sub_pos_iff_lt : 0 < a - b ↔ b < a := !sub_self ▸ !add_lt_add_right_iff
theorem sub_pos_of_lt : b < a → 0 < a - b := iff.mpr !sub_pos_iff_lt
theorem lt_of_sub_pos : 0 < a - b → b < a := iff.mp !sub_pos_iff_lt
theorem sub_neg_iff_lt : a - b < 0 ↔ a < b := !sub_self ▸ !add_lt_add_right_iff
theorem sub_neg_of_lt : a < b → a - b < 0 := iff.mpr !sub_neg_iff_lt
theorem lt_of_sub_neg : a - b < 0 → a < b := iff.mp !sub_neg_iff_lt
theorem add_le_iff_le_neg_add : a + b ≤ c ↔ b ≤ -a + c :=
have H: a + b ≤ c ↔ -a + (a + b) ≤ -a + c, from iff.symm (!add_le_add_left_iff),
!neg_add_cancel_left ▸ H
theorem add_le_of_le_neg_add : b ≤ -a + c → a + b ≤ c :=
iff.mpr !add_le_iff_le_neg_add
theorem le_neg_add_of_add_le : a + b ≤ c → b ≤ -a + c :=
iff.mp !add_le_iff_le_neg_add
theorem add_le_iff_le_sub_left : a + b ≤ c ↔ b ≤ c - a :=
by rewrite [sub_eq_add_neg, {c+_}add.comm]; apply add_le_iff_le_neg_add
theorem add_le_of_le_sub_left : b ≤ c - a → a + b ≤ c :=
iff.mpr !add_le_iff_le_sub_left
theorem le_sub_left_of_add_le : a + b ≤ c → b ≤ c - a :=
iff.mp !add_le_iff_le_sub_left
theorem add_le_iff_le_sub_right : a + b ≤ c ↔ a ≤ c - b :=
have H: a + b ≤ c ↔ a + b - b ≤ c - b, from iff.symm (!add_le_add_right_iff),
!add_neg_cancel_right ▸ H
theorem add_le_of_le_sub_right : a ≤ c - b → a + b ≤ c :=
iff.mpr !add_le_iff_le_sub_right
theorem le_sub_right_of_add_le : a + b ≤ c → a ≤ c - b :=
iff.mp !add_le_iff_le_sub_right
theorem le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c :=
assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem le_add_of_neg_add_le : -b + a ≤ c → a ≤ b + c :=
iff.mpr !le_add_iff_neg_add_le
theorem neg_add_le_of_le_add : a ≤ b + c → -b + a ≤ c :=
iff.mp !le_add_iff_neg_add_le
theorem le_add_iff_sub_left_le : a ≤ b + c ↔ a - b ≤ c :=
by rewrite [sub_eq_add_neg, {a+_}add.comm]; apply le_add_iff_neg_add_le
theorem le_add_of_sub_left_le : a - b ≤ c → a ≤ b + c :=
iff.mpr !le_add_iff_sub_left_le
theorem sub_left_le_of_le_add : a ≤ b + c → a - b ≤ c :=
iff.mp !le_add_iff_sub_left_le
theorem le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b :=
assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
by rewrite add_neg_cancel_right at H; exact H
theorem le_add_of_sub_right_le : a - c ≤ b → a ≤ b + c :=
iff.mpr !le_add_iff_sub_right_le
theorem sub_right_le_of_le_add : a ≤ b + c → a - c ≤ b :=
iff.mp !le_add_iff_sub_right_le
theorem le_add_iff_neg_add_le_left : a ≤ b + c ↔ -b + a ≤ c :=
assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem le_add_of_neg_add_le_left : -b + a ≤ c → a ≤ b + c :=
iff.mpr !le_add_iff_neg_add_le_left
theorem neg_add_le_left_of_le_add : a ≤ b + c → -b + a ≤ c :=
iff.mp !le_add_iff_neg_add_le_left
theorem le_add_iff_neg_add_le_right : a ≤ b + c ↔ -c + a ≤ b :=
by rewrite add.comm; apply le_add_iff_neg_add_le_left
theorem le_add_of_neg_add_le_right : -c + a ≤ b → a ≤ b + c :=
iff.mpr !le_add_iff_neg_add_le_right
theorem neg_add_le_right_of_le_add : a ≤ b + c → -c + a ≤ b :=
iff.mp !le_add_iff_neg_add_le_right
theorem le_add_iff_neg_le_sub_left : c ≤ a + b ↔ -a ≤ b - c :=
assert H : c ≤ a + b ↔ -a + c ≤ b, from !le_add_iff_neg_add_le,
assert H' : -a + c ≤ b ↔ -a ≤ b - c, from !add_le_iff_le_sub_right,
iff.trans H H'
theorem le_add_of_neg_le_sub_left : -a ≤ b - c → c ≤ a + b :=
iff.mpr !le_add_iff_neg_le_sub_left
theorem neg_le_sub_left_of_le_add : c ≤ a + b → -a ≤ b - c :=
iff.mp !le_add_iff_neg_le_sub_left
theorem le_add_iff_neg_le_sub_right : c ≤ a + b ↔ -b ≤ a - c :=
by rewrite add.comm; apply le_add_iff_neg_le_sub_left
theorem le_add_of_neg_le_sub_right : -b ≤ a - c → c ≤ a + b :=
iff.mpr !le_add_iff_neg_le_sub_right
theorem neg_le_sub_right_of_le_add : c ≤ a + b → -b ≤ a - c :=
iff.mp !le_add_iff_neg_le_sub_right
theorem add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c :=
assert H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
begin rewrite neg_add_cancel_left at H, exact H end
theorem add_lt_of_lt_neg_add_left : b < -a + c → a + b < c :=
iff.mpr !add_lt_iff_lt_neg_add_left
theorem lt_neg_add_left_of_add_lt : a + b < c → b < -a + c :=
iff.mp !add_lt_iff_lt_neg_add_left
theorem add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c :=
by rewrite add.comm; apply add_lt_iff_lt_neg_add_left
theorem add_lt_of_lt_neg_add_right : a < -b + c → a + b < c :=
iff.mpr !add_lt_iff_lt_neg_add_right
theorem lt_neg_add_right_of_add_lt : a + b < c → a < -b + c :=
iff.mp !add_lt_iff_lt_neg_add_right
theorem add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a :=
begin
rewrite [sub_eq_add_neg, {c+_}add.comm],
apply add_lt_iff_lt_neg_add_left
end
theorem add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b :=
theorem add_lt_of_lt_sub_left : b < c - a → a + b < c :=
iff.mpr !add_lt_iff_lt_sub_left
theorem lt_sub_left_of_add_lt : a + b < c → b < c - a :=
iff.mp !add_lt_iff_lt_sub_left
theorem add_lt_iff_lt_sub_right : a + b < c ↔ a < c - b :=
assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
by rewrite add_neg_cancel_right at H; exact H
theorem add_lt_of_lt_sub_right : a < c - b → a + b < c :=
iff.mpr !add_lt_iff_lt_sub_right
theorem lt_sub_right_of_add_lt : a + b < c → a < c - b :=
iff.mp !add_lt_iff_lt_sub_right
theorem lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c :=
assert H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
theorem lt_add_of_neg_add_lt_left : -b + a < c → a < b + c :=
iff.mpr !lt_add_iff_neg_add_lt_left
theorem neg_add_lt_left_of_lt_add : a < b + c → -b + a < c :=
iff.mp !lt_add_iff_neg_add_lt_left
theorem lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b :=
by rewrite add.comm; apply lt_add_iff_neg_add_lt_left
theorem lt_add_of_neg_add_lt_right : -c + a < b → a < b + c :=
iff.mpr !lt_add_iff_neg_add_lt_right
theorem neg_add_lt_right_of_lt_add : a < b + c → -c + a < b :=
iff.mp !lt_add_iff_neg_add_lt_right
theorem lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c :=
by rewrite [sub_eq_add_neg, {a + _}add.comm]; apply lt_add_iff_neg_add_lt_left
theorem lt_add_of_sub_lt_left : a - b < c → a < b + c :=
iff.mpr !lt_add_iff_sub_lt_left
theorem sub_lt_left_of_lt_add : a < b + c → a - b < c :=
iff.mp !lt_add_iff_sub_lt_left
theorem lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b :=
by rewrite add.comm; apply lt_add_iff_sub_lt_left
theorem lt_add_of_sub_lt_right : a - c < b → a < b + c :=
iff.mpr !lt_add_iff_sub_lt_right
theorem sub_lt_right_of_lt_add : a < b + c → a - c < b :=
iff.mp !lt_add_iff_sub_lt_right
-- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
theorem le_iff_le_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d :=
calc

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

@ -570,12 +570,12 @@ theorem floor_succ (x : ℝ) : (floor x) + 1 = floor (x + 1) :=
apply by_contradiction,
intro H,
cases int.lt_or_gt_of_ne H with [Hlt, Hgt],
let Hl := floor_largest (iff.mp !int.add_lt_add_iff_lt_sub_right Hlt),
let Hl := floor_largest (iff.mp !int.add_lt_iff_lt_sub_right Hlt),
rewrite [of_int_sub at Hl, -of_rat_sub at Hl],
apply (not_le_of_gt (iff.mpr !add_lt_add_iff_lt_sub_right Hl)) !floor_spec,
apply not_le_of_gt (iff.mpr !add_lt_iff_lt_sub_right Hl) !floor_spec,
let Hl := floor_largest Hgt,
rewrite [of_int_add at Hl, -of_rat_add at Hl],
apply (not_le_of_gt (lt_of_add_lt_add_right Hl)) !floor_spec
apply not_le_of_gt (lt_of_add_lt_add_right Hl) !floor_spec
end
theorem floor_succ_lt (x : ℝ) : floor (x - 1) < floor x :=