refactor(library): add 'and' namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
364bba2129
commit
2bc6f92d33
18 changed files with 95 additions and 94 deletions
|
|
@ -454,16 +454,16 @@ In the following example we use =and.intro= for creating a proof for
|
|||
check fun (Hp : p) (Hq : q), and.intro Hp Hq
|
||||
#+END_SRC
|
||||
|
||||
The expression =and_elim_left H= creates a proof =a= from a proof =H : a ∧ b=.
|
||||
Similarly =and_elim_right H= is a proof for =b=. We say they are the _left/right and-eliminators_.
|
||||
The expression =and.elim_left H= creates a proof =a= from a proof =H : a ∧ b=.
|
||||
Similarly =and.elim_right H= is a proof for =b=. We say they are the _left/right and-eliminators_.
|
||||
|
||||
#+BEGIN_SRC lean
|
||||
import logic
|
||||
variables p q : Prop
|
||||
-- Proof for p ∧ q → p
|
||||
check fun H : p ∧ q, and_elim_left H
|
||||
check fun H : p ∧ q, and.elim_left H
|
||||
-- Proof for p ∧ q → q
|
||||
check fun H : p ∧ q, and_elim_right H
|
||||
check fun H : p ∧ q, and.elim_right H
|
||||
#+END_SRC
|
||||
|
||||
Now, we prove =p ∧ q → q ∧ p= with the following simple proof term.
|
||||
|
|
@ -471,7 +471,7 @@ Now, we prove =p ∧ q → q ∧ p= with the following simple proof term.
|
|||
#+BEGIN_SRC lean
|
||||
import logic
|
||||
variables p q : Prop
|
||||
check fun H : p ∧ q, and.intro (and_elim_right H) (and_elim_left H)
|
||||
check fun H : p ∧ q, and.intro (and.elim_right H) (and.elim_left H)
|
||||
#+END_SRC
|
||||
|
||||
Note that the proof term is very similar to a function that just swaps the
|
||||
|
|
@ -573,8 +573,8 @@ Here is the proof term for =a ∧ b ↔ b ∧ a=
|
|||
import logic
|
||||
variables a b : Prop
|
||||
check iff_intro
|
||||
(fun H : a ∧ b, and.intro (and_elim_right H) (and_elim_left H))
|
||||
(fun H : b ∧ a, and.intro (and_elim_right H) (and_elim_left H))
|
||||
(fun H : a ∧ b, and.intro (and.elim_right H) (and.elim_left H))
|
||||
(fun H : b ∧ a, and.intro (and.elim_right H) (and.elim_left H))
|
||||
#+END_SRC
|
||||
|
||||
In Lean, we can use =assume= instead of =fun= to make proof terms look
|
||||
|
|
@ -584,8 +584,8 @@ more like proofs found in text books.
|
|||
import logic
|
||||
variables a b : Prop
|
||||
check iff_intro
|
||||
(assume H : a ∧ b, and.intro (and_elim_right H) (and_elim_left H))
|
||||
(assume H : b ∧ a, and.intro (and_elim_right H) (and_elim_left H))
|
||||
(assume H : a ∧ b, and.intro (and.elim_right H) (and.elim_left H))
|
||||
(assume H : b ∧ a, and.intro (and.elim_right H) (and.elim_left H))
|
||||
#+END_SRC
|
||||
|
||||
*** True and False
|
||||
|
|
|
|||
|
|
@ -260,11 +260,11 @@ induction_on l
|
|||
-- assume P1 : ¬ (mem x (cons y l)),
|
||||
-- have P2 : ¬ (mem x l ∨ (y = x)), from subst P1 (mem_cons _ _ _),
|
||||
-- have P3 : ¬ (mem x l) ∧ (y ≠ x),from subst P2 (not_or _ _),
|
||||
-- have P4 : x ≠ y, from ne_symm (and_elim_right P3),
|
||||
-- have P4 : x ≠ y, from ne_symm (and.elim_right P3),
|
||||
-- calc
|
||||
-- find x (cons y l) = succ (find x l) :
|
||||
-- trans (find_cons _ _ _) (not_imp_if_eq P4 _ _)
|
||||
-- ... = succ (length l) : {IH (and_elim_left P3)}
|
||||
-- ... = succ (length l) : {IH (and.elim_left P3)}
|
||||
-- ... = length (cons y l) : symm (length_cons _ _))
|
||||
|
||||
-- nth element
|
||||
|
|
|
|||
|
|
@ -128,10 +128,10 @@ have stronger : P a ∧ P (succ a), from
|
|||
induction_on a
|
||||
(and.intro H1 H2)
|
||||
(take k IH,
|
||||
have IH1 : P k, from and_elim_left IH,
|
||||
have IH2 : P (succ k), from and_elim_right IH,
|
||||
have IH1 : P k, from and.elim_left IH,
|
||||
have IH2 : P (succ k), from and.elim_right IH,
|
||||
and.intro IH2 (H3 k IH1 IH2)),
|
||||
and_elim_left stronger
|
||||
and.elim_left stronger
|
||||
|
||||
theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
|
||||
(H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m :=
|
||||
|
|
|
|||
|
|
@ -673,14 +673,14 @@ gcd_induct m n
|
|||
assume npos : 0 < n,
|
||||
assume IH : (gcd n (m mod n) | n) ∧ (gcd n (m mod n) | (m mod n)),
|
||||
have H : gcd n (m mod n) | (m div n * n + m mod n), from
|
||||
dvd_add (dvd_trans (and_elim_left IH) dvd_mul_self_right) (and_elim_right IH),
|
||||
dvd_add (dvd_trans (and.elim_left IH) dvd_mul_self_right) (and.elim_right IH),
|
||||
have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H,
|
||||
have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos),
|
||||
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and_elim_left IH)))
|
||||
show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and.elim_left IH)))
|
||||
|
||||
theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and_elim_left (gcd_dvd _ _)
|
||||
theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and.elim_left (gcd_dvd _ _)
|
||||
|
||||
theorem gcd_dvd_right (m n : ℕ) : (gcd m n | n) := and_elim_right (gcd_dvd _ _)
|
||||
theorem gcd_dvd_right (m n : ℕ) : (gcd m n | n) := and.elim_right (gcd_dvd _ _)
|
||||
|
||||
-- add_rewrite gcd_dvd_left gcd_dvd_right
|
||||
|
||||
|
|
|
|||
|
|
@ -282,7 +282,7 @@ lt_intro add_move_succ
|
|||
-- ### basic facts
|
||||
|
||||
theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
|
||||
and_elim_right (succ_le_imp_le_and_ne H)
|
||||
and.elim_right (succ_le_imp_le_and_ne H)
|
||||
|
||||
theorem lt_irrefl {n : ℕ} : ¬ n < n :=
|
||||
not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
|
||||
|
|
@ -310,7 +310,7 @@ theorem self_lt_succ {n : ℕ} : n < succ n :=
|
|||
le_refl
|
||||
|
||||
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m :=
|
||||
and_elim_left (succ_le_imp_le_and_ne H)
|
||||
and.elim_left (succ_le_imp_le_and_ne H)
|
||||
|
||||
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m :=
|
||||
le_imp_succ_le_or_eq H
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ section
|
|||
have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
|
||||
iff_intro
|
||||
(assume H, subst H (and.intro rfl rfl))
|
||||
(assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
|
||||
(assume H, and.elim H (assume H4 H5, prod_eq H4 H5)),
|
||||
decidable_iff_equiv _ (iff_symm H3)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ theorem intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A
|
|||
and.intro H1 (and.intro H2 H3)
|
||||
|
||||
theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
|
||||
iff_intro (assume Hab, and_elim_right Hab) (assume Hb, and.intro Ha Hb)
|
||||
iff_intro (assume Hab, and.elim_right Hab) (assume Hb, and.intro Ha Hb)
|
||||
|
||||
theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(H1 : reflexive R) (H2 : ∀b, abs (rep b) = b)
|
||||
|
|
@ -46,27 +46,27 @@ intro
|
|||
|
||||
theorem abs_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) (b : B) : abs (rep b) = b :=
|
||||
and_elim_left Q b
|
||||
and.elim_left Q b
|
||||
|
||||
theorem refl_rep {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) (b : B) : R (rep b) (rep b) :=
|
||||
and_elim_left (and_elim_right Q) b
|
||||
and.elim_left (and.elim_right Q) b
|
||||
|
||||
theorem R_iff {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) (r s : A) : R r s ↔ (R r r ∧ R s s ∧ abs r = abs s) :=
|
||||
and_elim_right (and_elim_right Q) r s
|
||||
and.elim_right (and.elim_right Q) r s
|
||||
|
||||
theorem refl_left {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) {r s : A} (H : R r s) : R r r :=
|
||||
and_elim_left (iff_elim_left (R_iff Q r s) H)
|
||||
and.elim_left (iff_elim_left (R_iff Q r s) H)
|
||||
|
||||
theorem refl_right {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) {r s : A} (H : R r s) : R s s :=
|
||||
and_elim_left (and_elim_right (iff_elim_left (R_iff Q r s) H))
|
||||
and.elim_left (and.elim_right (iff_elim_left (R_iff Q r s) H))
|
||||
|
||||
theorem eq_abs {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) {r s : A} (H : R r s) : abs r = abs s :=
|
||||
and_elim_right (and_elim_right (iff_elim_left (R_iff Q r s) H))
|
||||
and.elim_right (and.elim_right (iff_elim_left (R_iff Q r s) H))
|
||||
|
||||
theorem R_intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) {r s : A} (H1 : R r r) (H2 : R s s) (H3 : abs r = abs s) : R r s :=
|
||||
|
|
@ -262,7 +262,7 @@ calc
|
|||
theorem representative_map_idempotent {A : Type} {R : A → A → Prop} {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b ↔ R a a ∧ R b b ∧ f a = f b) (a : A) :
|
||||
f (f a) = f a :=
|
||||
symm (and_elim_right (and_elim_right (iff_elim_left (H2 a (f a)) (H1 a))))
|
||||
symm (and.elim_right (and.elim_right (iff_elim_left (H2 a (f a)) (H1 a))))
|
||||
|
||||
theorem representative_map_idempotent_equiv {A : Type} {R : A → A → Prop} {f : A → A}
|
||||
(H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) (a : A) :
|
||||
|
|
|
|||
|
|
@ -47,8 +47,8 @@ theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A
|
|||
iff_intro
|
||||
(assume H, and.intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H))
|
||||
(assume H,
|
||||
have e1 : A x = tt, from and_elim_left H,
|
||||
have e2 : B x = tt, from and_elim_right H,
|
||||
have e1 : A x = tt, from and.elim_left H,
|
||||
have e2 : B x = tt, from and.elim_right H,
|
||||
show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band_tt_left tt)
|
||||
|
||||
theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A :=
|
||||
|
|
|
|||
|
|
@ -51,8 +51,8 @@ theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable
|
|||
rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (and.intro Ha Hb))
|
||||
(assume Hnb : ¬b, inr (and_not_right a Hnb)))
|
||||
(assume Hna : ¬a, inr (and_not_left b Hna))
|
||||
(assume Hnb : ¬b, inr (and.not_right a Hnb)))
|
||||
(assume Hna : ¬a, inr (and.not_left b Hna))
|
||||
|
||||
theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
|
||||
decidable (a ∨ b) :=
|
||||
|
|
|
|||
|
|
@ -13,33 +13,34 @@ intro : a → b → and a b
|
|||
infixr `/\` := and
|
||||
infixr `∧` := and
|
||||
|
||||
theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c :=
|
||||
and.rec H2 H1
|
||||
namespace and
|
||||
theorem elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c :=
|
||||
rec H2 H1
|
||||
|
||||
theorem and_elim_left {a b : Prop} (H : a ∧ b) : a :=
|
||||
and.rec (λa b, a) H
|
||||
theorem elim_left {a b : Prop} (H : a ∧ b) : a :=
|
||||
rec (λa b, a) H
|
||||
|
||||
theorem and_elim_right {a b : Prop} (H : a ∧ b) : b :=
|
||||
and.rec (λa b, b) H
|
||||
theorem elim_right {a b : Prop} (H : a ∧ b) : b :=
|
||||
rec (λa b, b) H
|
||||
|
||||
theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a :=
|
||||
and.intro (and_elim_right H) (and_elim_left H)
|
||||
theorem swap {a b : Prop} (H : a ∧ b) : b ∧ a :=
|
||||
intro (elim_right H) (elim_left H)
|
||||
|
||||
theorem and_not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (and_elim_left H) Hna
|
||||
theorem not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_left H) Hna
|
||||
|
||||
theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (and_elim_right H) Hnb
|
||||
theorem not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
|
||||
assume H : a ∧ b, absurd (elim_right H) Hnb
|
||||
|
||||
theorem and_imp_and {a b c d : Prop} (H1 : a ∧ b) (H2 : a → c) (H3 : b → d) : c ∧ d :=
|
||||
and_elim H1 (assume Ha : a, assume Hb : b, and.intro (H2 Ha) (H3 Hb))
|
||||
theorem imp_and {a b c d : Prop} (H1 : a ∧ b) (H2 : a → c) (H3 : b → d) : c ∧ d :=
|
||||
elim H1 (assume Ha : a, assume Hb : b, intro (H2 Ha) (H3 Hb))
|
||||
|
||||
theorem imp_and_left {a b c : Prop} (H1 : a ∧ c) (H : a → b) : b ∧ c :=
|
||||
and_elim H1 (assume Ha : a, assume Hc : c, and.intro (H Ha) Hc)
|
||||
|
||||
theorem imp_and_right {a b c : Prop} (H1 : c ∧ a) (H : a → b) : c ∧ b :=
|
||||
and_elim H1 (assume Hc : c, assume Ha : a, and.intro Hc (H Ha))
|
||||
theorem imp_left {a b c : Prop} (H1 : a ∧ c) (H : a → b) : b ∧ c :=
|
||||
elim H1 (assume Ha : a, assume Hc : c, intro (H Ha) Hc)
|
||||
|
||||
theorem imp_right {a b c : Prop} (H1 : c ∧ a) (H : a → b) : c ∧ b :=
|
||||
elim H1 (assume Hc : c, assume Ha : a, intro Hc (H Ha))
|
||||
end and
|
||||
|
||||
-- or
|
||||
-- --
|
||||
|
|
@ -151,16 +152,16 @@ iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb)
|
|||
-- ---------------------------
|
||||
|
||||
theorem and_comm {a b : Prop} : a ∧ b ↔ b ∧ a :=
|
||||
iff_intro (λH, and_swap H) (λH, and_swap H)
|
||||
iff_intro (λH, and.swap H) (λH, and.swap H)
|
||||
|
||||
theorem and_assoc {a b c : Prop} : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
|
||||
iff_intro
|
||||
(assume H, and.intro
|
||||
(and_elim_left (and_elim_left H))
|
||||
(and.intro (and_elim_right (and_elim_left H)) (and_elim_right H)))
|
||||
(and.elim_left (and.elim_left H))
|
||||
(and.intro (and.elim_right (and.elim_left H)) (and.elim_right H)))
|
||||
(assume H, and.intro
|
||||
(and.intro (and_elim_left H) (and_elim_left (and_elim_right H)))
|
||||
(and_elim_right (and_elim_right H)))
|
||||
(and.intro (and.elim_left H) (and.elim_left (and.elim_right H)))
|
||||
(and.elim_right (and.elim_right H)))
|
||||
|
||||
theorem or_comm {a b : Prop} : a ∨ b ↔ b ∨ a :=
|
||||
iff_intro (λH, or_swap H) (λH, or_swap H)
|
||||
|
|
|
|||
|
|
@ -61,8 +61,8 @@ iff_intro
|
|||
(assume Hnb, and.intro Hna Hnb)))
|
||||
(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)))
|
||||
(assume Ha, absurd Ha (and.elim_left H))
|
||||
(assume Hb, absurd Hb (and.elim_right H)))
|
||||
|
||||
theorem not_and {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) :=
|
||||
iff_intro
|
||||
|
|
@ -73,8 +73,8 @@ iff_intro
|
|||
(assume Hna, or_inl 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))
|
||||
(assume Hna, absurd (and.elim_left N) Hna)
|
||||
(assume Hnb, absurd (and.elim_right N) Hnb))
|
||||
|
||||
theorem imp_or {a b : Prop} {Da : decidable a} : (a → b) ↔ (¬a ∨ b) :=
|
||||
iff_intro
|
||||
|
|
|
|||
|
|
@ -26,8 +26,8 @@ congruence2.mk
|
|||
(take a1 b1 a2 b2,
|
||||
assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
|
||||
iff_intro
|
||||
(assume H3 : a1 ∧ a2, and_imp_and H3 (iff_elim_left H1) (iff_elim_left H2))
|
||||
(assume H3 : b1 ∧ b2, and_imp_and H3 (iff_elim_right H1) (iff_elim_right H2)))
|
||||
(assume H3 : a1 ∧ a2, and.imp_and H3 (iff_elim_left H1) (iff_elim_left H2))
|
||||
(assume H3 : b1 ∧ b2, and.imp_and H3 (iff_elim_right H1) (iff_elim_right H2)))
|
||||
|
||||
theorem congruence_or : congruence2 iff iff iff or :=
|
||||
congruence2.mk
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ 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 :=
|
||||
obtain w Hw, from H2,
|
||||
H1 w (and_elim_left Hw) (and_elim_right Hw)
|
||||
H1 w (and.elim_left Hw) (and.elim_right Hw)
|
||||
|
||||
theorem forall_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∀x, φ x) ↔ (∀x, ψ x) :=
|
||||
iff_intro
|
||||
|
|
@ -65,8 +65,8 @@ iff_intro
|
|||
|
||||
theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
|
||||
iff_intro
|
||||
(assume H, and.intro (take x, and_elim_left (H x)) (take x, and_elim_right (H x)))
|
||||
(assume H, take x, and.intro (and_elim_left H x) (and_elim_right H x))
|
||||
(assume H, and.intro (take x, and.elim_left (H x)) (take x, and.elim_right (H x)))
|
||||
(assume H, take x, and.intro (and.elim_left H x) (and.elim_right H x))
|
||||
|
||||
theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
|
||||
iff_intro
|
||||
|
|
|
|||
|
|
@ -58,8 +58,8 @@ assume Hnem : ¬(P ∨ ¬P),
|
|||
theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q) :=
|
||||
assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q),
|
||||
or_elim H
|
||||
(assume Hnp : ¬P, absurd (and_elim_left Hn) Hnp)
|
||||
(assume Hnq : ¬Q, absurd (and_elim_right Hn) Hnq)
|
||||
(assume Hnp : ¬P, absurd (and.elim_left Hn) Hnp)
|
||||
(assume Hnq : ¬Q, absurd (and.elim_right Hn) Hnq)
|
||||
|
||||
theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q :=
|
||||
assume H : ¬(P ∨ Q),
|
||||
|
|
@ -70,8 +70,8 @@ assume H : ¬(P ∨ Q),
|
|||
theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) :=
|
||||
assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
|
||||
or_elim Hn
|
||||
(assume Hp : P, absurd Hp (and_elim_left H))
|
||||
(assume Hq : Q, absurd Hq (and_elim_right H))
|
||||
(assume Hp : P, absurd Hp (and.elim_left H))
|
||||
(assume Hq : Q, absurd Hq (and.elim_right H))
|
||||
|
||||
theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q :=
|
||||
assume (Hor : ¬P ∨ Q) (Hp : P),
|
||||
|
|
@ -82,13 +82,13 @@ assume (Hor : ¬P ∨ Q) (Hp : P),
|
|||
theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) :=
|
||||
assume (Hpq : P → Q) (Hn : ¬(¬P ∨ Q)),
|
||||
have H1 : ¬¬P ∧ ¬Q, from thm12 Hn,
|
||||
have Hnp : ¬P, from mt Hpq (and_elim_right H1),
|
||||
absurd Hnp (and_elim_left H1)
|
||||
have Hnp : ¬P, from mt Hpq (and.elim_right H1),
|
||||
absurd Hnp (and.elim_left H1)
|
||||
|
||||
theorem thm16 {P Q : Prop} : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)) → ¬P ∨ Q :=
|
||||
assume H : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)),
|
||||
have Hpq : P → Q, from and_elim_left H,
|
||||
or_elim (and_elim_right H)
|
||||
have Hpq : P → Q, from and.elim_left H,
|
||||
or_elim (and.elim_right H)
|
||||
(assume Hem1 : P ∨ ¬P, or_elim Hem1
|
||||
(assume Hp : P, or_inr (Hpq Hp))
|
||||
(assume Hnp : ¬P, or_inl Hnp))
|
||||
|
|
@ -190,26 +190,26 @@ assume Hem H1,
|
|||
|
||||
theorem thm23a : (∃x, P x) ∧ C → (∃x, P x ∧ C) :=
|
||||
assume H,
|
||||
have Hex : ∃x, P x, from and_elim_left H,
|
||||
have Hc : C, from and_elim_right H,
|
||||
have Hex : ∃x, P x, from and.elim_left H,
|
||||
have Hc : C, from and.elim_right H,
|
||||
obtain (w : T) (Hw : P w), from Hex,
|
||||
exists_intro w (and.intro Hw Hc)
|
||||
|
||||
theorem thm23b : (∃x, P x ∧ C) → (∃x, P x) ∧ C :=
|
||||
assume H,
|
||||
obtain (w : T) (Hw : P w ∧ C), from H,
|
||||
have Hex : ∃x, P x, from exists_intro w (and_elim_left Hw),
|
||||
and.intro Hex (and_elim_right Hw)
|
||||
have Hex : ∃x, P x, from exists_intro w (and.elim_left Hw),
|
||||
and.intro Hex (and.elim_right Hw)
|
||||
|
||||
theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C) :=
|
||||
assume H, take x,
|
||||
and.intro (and_elim_left H x) (and_elim_right H)
|
||||
and.intro (and.elim_left H x) (and.elim_right H)
|
||||
|
||||
theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C :=
|
||||
assume Hin H,
|
||||
obtain (w : T) (Hw : true), from Hin,
|
||||
have Hc : C, from and_elim_right (H w),
|
||||
have Hx : ∀x, P x, from take x, and_elim_left (H x),
|
||||
have Hc : C, from and.elim_right (H w),
|
||||
have Hx : ∀x, P x, from take x, and.elim_left (H x),
|
||||
and.intro Hx Hc
|
||||
|
||||
end -- of section
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ by_contradiction (assume N : ¬∀x, P x,
|
|||
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
|
||||
not_not_elim (and_elim_right Hr b H),
|
||||
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,
|
||||
have s3 : ¬P r, from and.elim_left Hr,
|
||||
absurd s2 s3)
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ instance is_equivalence.is_symmetric
|
|||
instance is_equivalence.is_transitive
|
||||
|
||||
theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b :=
|
||||
iff_intro (take Hab, and_elim_right Hab) (take Hb, and.intro Ha Hb)
|
||||
iff_intro (take Hab, and.elim_right Hab) (take Hb, and.intro Ha Hb)
|
||||
|
||||
theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b :=
|
||||
subst_iff H1 H2
|
||||
|
|
|
|||
|
|
@ -115,10 +115,10 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
|
|||
induction_on a
|
||||
(and_intro H1 H2)
|
||||
(take k IH,
|
||||
have IH1 : P k, from and_elim_left IH,
|
||||
have IH2 : P (succ k), from and_elim_right IH,
|
||||
have IH1 : P k, from and.elim_left IH,
|
||||
have IH2 : P (succ k), from and.elim_right IH,
|
||||
and_intro IH2 (H3 k IH1 IH2)),
|
||||
and_elim_left stronger
|
||||
and.elim_left stronger
|
||||
|
||||
theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
|
||||
(H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m
|
||||
|
|
@ -681,7 +681,7 @@ infix `>`:50 := gt
|
|||
---------- basic facts
|
||||
|
||||
theorem lt_ne {n m : ℕ} (H : n < m) : n ≠ m
|
||||
:= and_elim_right (succ_le_left_inv H)
|
||||
:= and.elim_right (succ_le_left_inv H)
|
||||
|
||||
theorem lt_irrefl (n : ℕ) : ¬ n < n
|
||||
:= assume H : n < n, absurd (refl n) (lt_ne H)
|
||||
|
|
@ -711,7 +711,7 @@ theorem self_lt_succ (n : ℕ) : n < succ n
|
|||
:= le_refl (succ n)
|
||||
|
||||
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m
|
||||
:= and_elim_left (succ_le_imp_le_and_ne H)
|
||||
:= and.elim_left (succ_le_imp_le_and_ne H)
|
||||
|
||||
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m
|
||||
:= le_imp_succ_le_or_eq H
|
||||
|
|
|
|||
|
|
@ -110,10 +110,10 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1)
|
|||
induction_on a
|
||||
(and.intro H1 H2)
|
||||
(take k IH,
|
||||
have IH1 : P k, from and_elim_left IH,
|
||||
have IH2 : P (succ k), from and_elim_right IH,
|
||||
have IH1 : P k, from and.elim_left IH,
|
||||
have IH2 : P (succ k), from and.elim_right IH,
|
||||
and.intro IH2 (H3 k IH1 IH2)),
|
||||
and_elim_left stronger
|
||||
and.elim_left stronger
|
||||
|
||||
theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m)
|
||||
(H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m
|
||||
|
|
@ -680,7 +680,7 @@ infix `>`:50 := gt
|
|||
---------- basic facts
|
||||
|
||||
theorem lt_ne {n m : ℕ} (H : n < m) : n ≠ m
|
||||
:= and_elim_right (succ_le_left_inv H)
|
||||
:= and.elim_right (succ_le_left_inv H)
|
||||
|
||||
theorem lt_irrefl (n : ℕ) : ¬ n < n
|
||||
:= assume H : n < n, absurd (eq.refl n) (lt_ne H)
|
||||
|
|
@ -710,7 +710,7 @@ theorem self_lt_succ (n : ℕ) : n < succ n
|
|||
:= le_refl (succ n)
|
||||
|
||||
theorem lt_imp_le {n m : ℕ} (H : n < m) : n ≤ m
|
||||
:= and_elim_left (succ_le_imp_le_and_ne H)
|
||||
:= and.elim_left (succ_le_imp_le_and_ne H)
|
||||
|
||||
theorem le_imp_lt_or_eq {n m : ℕ} (H : n ≤ m) : n < m ∨ n = m
|
||||
:= le_imp_succ_le_or_eq H
|
||||
|
|
|
|||
Loading…
Reference in a new issue