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

feat(library/init/logic): add transitivity theorems for = + <->

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-01 10:09:46 -08:00
parent e8ef1f97b6
commit 9c0375b6e2
2 changed files with 14 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
library/algebra/ordered_group.lean
View file

@ -336,18 +336,17 @@ section
!add.comm ▸ !lt_add_iff_sub_lt_left
-- 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
a ≤ b ↔ a - b ≤ 0 : iff.symm (sub_nonpos_iff_le a b)
... ↔ c - d ≤ 0 : H ▸ !iff.refl
... ↔ c ≤ d : sub_nonpos_iff_le c d
a ≤ b ↔ a - b ≤ 0 : iff.symm (sub_nonpos_iff_le a b)
... = (c - d ≤ 0) : H
... ↔ c ≤ d : sub_nonpos_iff_le c d
theorem lt_iff_lt_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a < b ↔ c < d :=
calc
a < b ↔ a - b < 0 : iff.symm (sub_neg_iff_lt a b)
... ↔ c - d < 0 : H ▸ !iff.refl
... ↔ c < d : sub_neg_iff_lt c d
a < b ↔ a - b < 0 : iff.symm (sub_neg_iff_lt a b)
... = (c - d < 0) : H
... ↔ c < d : sub_neg_iff_lt c d
theorem sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
add_le_add_left (neg_le_neg H) c

8
library/init/logic.lean
View file

@ -226,8 +226,16 @@ iff.mp (iff.symm H) trivial
theorem not_of_iff_false (H : a ↔ false) : ¬a :=
assume Ha : a, iff.mp H Ha
theorem iff_of_eq_of_iff (H₁ : a = b) (H₂ : b ↔ c) : a ↔ c :=
H₁⁻¹ ▸ H₂
theorem iff_of_iff_of_eq (H₁ : a ↔ b) (H₂ : b = c) : a ↔ c :=
H₂ ▸ H₁
calc_refl iff.refl
calc_trans iff.trans
calc_trans iff_of_eq_of_iff
calc_trans iff_of_iff_of_eq
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P