From 6632a50015cee0bb8cfab09e62e57fd3db494344 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Sep 2014 21:25:21 -0700 Subject: [PATCH] refactor(library): add namespaces 'or', 'and' and 'iff' Signed-off-by: Leonardo de Moura --- doc/lean/tutorial.org | 28 +-- library/data/bool.lean | 8 +- library/data/int/basic.lean | 44 ++-- library/data/int/order.lean | 76 +++--- library/data/list/basic.lean | 28 +-- library/data/nat/basic.lean | 12 +- library/data/nat/div.lean | 22 +- library/data/nat/order.lean | 46 ++-- library/data/nat/sub.lean | 12 +- library/data/prod.lean | 4 +- library/data/quotient/basic.lean | 20 +- library/data/quotient/classical.lean | 2 +- library/data/set.lean | 32 +-- library/data/subtype.lean | 4 +- library/data/sum.lean | 8 +- library/general_notation.lean | 1 - library/logic/axioms/classical.lean | 20 +- library/logic/axioms/examples/diaconescu.lean | 24 +- library/logic/axioms/hilbert.lean | 2 +- library/logic/axioms/prop_decidable.lean | 2 +- library/logic/classes/decidable.lean | 24 +- library/logic/core/connectives.lean | 229 ++++++++++-------- library/logic/core/eq.lean | 2 +- library/logic/core/identities.lean | 80 +++--- library/logic/core/if.lean | 4 +- library/logic/core/instances.lean | 66 ++--- library/logic/core/quantifiers.lean | 34 +-- library/logic/examples/nuprl_examples.lean | 60 ++--- src/library/resolve_macro.cpp | 8 +- tests/lean/interactive/in4.input.expected.out | 8 +- tests/lean/run/class4.lean | 4 +- tests/lean/run/elab_bug1.lean | 4 +- tests/lean/run/rel.lean | 11 +- tests/lean/run/sum_bug.lean | 8 +- tests/lean/run/tactic10.lean | 6 +- tests/lean/run/tactic11.lean | 6 +- tests/lean/run/tactic12.lean | 2 +- tests/lean/run/tactic13.lean | 2 +- tests/lean/run/tactic14.lean | 2 +- tests/lean/slow/nat_bug2.lean | 40 +-- tests/lean/slow/nat_wo_hints.lean | 46 ++-- tests/lua/res1.lua | 8 +- 42 files changed, 528 insertions(+), 521 deletions(-) diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 629a7b880..c31aed13f 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -495,14 +495,14 @@ We say they are the _left/right or-introduction_. The or-elimination rule is slightly more complicated. The basic idea is the following, we can prove =c= from =a ∨ b=, by showing we can prove =c= by assuming =a= or by assuming =b=. It is essentially a proof by cases. -=or_elim Hab Hac Hbc= takes three arguments =Hab : a ∨ b=, =Hac : a → c= and =Hbc : b → c= and produces a proof for =c=. -In the following example, we use =or_elim= to prove that =p v q → q ∨ p=. +=or.elim Hab Hac Hbc= takes three arguments =Hab : a ∨ b=, =Hac : a → c= and =Hbc : b → c= and produces a proof for =c=. +In the following example, we use =or.elim= to prove that =p v q → q ∨ p=. #+BEGIN_SRC lean import logic variables p q : Prop check fun H : p ∨ q, - or_elim H + or.elim H (fun Hp : p, or.intro_right q Hp) (fun Hq : q, or.intro_left p Hq) @@ -510,7 +510,7 @@ In the following example, we use =or_elim= to prove that =p v q → q ∨ p=. In most cases, the first argument of =or.intro_right= and =or.intro_left= can be inferred automatically by Lean. Moreover, Lean -provides =or_inr= and =or_inl= as shorthands for =or.intro_right _= +provides =or.inr= and =or.inl= as shorthands for =or.intro_right _= and =or.intro_left _=. These two shorthands are extensively used in the Lean standard library. @@ -518,9 +518,9 @@ the Lean standard library. import logic variables p q : Prop check fun H : p ∨ q, - or_elim H - (fun Hp : p, or_inr Hp) - (fun Hq : q, or_inl Hq) + or.elim H + (fun Hp : p, or.inr Hp) + (fun Hq : q, or.inl Hq) #+END_SRC @@ -564,15 +564,15 @@ Now, here is the proof term for =¬a → b → (b → a) → c= *** Iff (if-and-only-if) -The expression =iff_intro H1 H2= produces a proof for =a ↔ b= from =H1 : a → b= and =H2 : b → a=. -=iff_elim_left H= produces a proof for =a → b= from =H : a ↔ b=. Similarly, -=iff_elim_right H= produces a proof for =b → a= from =H : a ↔ b=. +The expression =iff.intro H1 H2= produces a proof for =a ↔ b= from =H1 : a → b= and =H2 : b → a=. +=iff.elim_left H= produces a proof for =a → b= from =H : a ↔ b=. Similarly, +=iff.elim_right H= produces a proof for =b → a= from =H : a ↔ b=. Here is the proof term for =a ∧ b ↔ b ∧ a= #+BEGIN_SRC lean import logic variables a b : Prop - check iff_intro + 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)) #+END_SRC @@ -583,7 +583,7 @@ more like proofs found in text books. #+BEGIN_SRC lean import logic variables a b : Prop - check iff_intro + 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)) #+END_SRC @@ -610,7 +610,7 @@ and use it to prove a theorem that would be quite tedious to prove by hand. -- create a rewrite rule set with name 'simple' rewrite_set simple -- add some theorems to the rewrite rule set 'simple' - add_rewrite and_id and_truer and_truel and_comm and_assoc and_left_comm iff_id : simple + add_rewrite and_id and_truer and_truel and_comm and.assoc and_left_comm iff_id : simple theorem th1 (a b : Bool) : a ∧ b ∧ true ∧ b ∧ true ∧ b ↔ a ∧ b := (by simp simple) #+END_SRC @@ -621,7 +621,7 @@ tedious steps. Here is a very simple example. #+BEGIN_SRC theorem th2 (a b : Prop) : a ∧ b ↔ b ∧ a - := iff_intro + := iff.intro (fun H : a ∧ b, (by simp simple)) (fun H : b ∧ a, (by simp simple)) #+END_SRC diff --git a/library/data/bool.lean b/library/data/bool.lean index 26a90426a..c1110a47d 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -22,7 +22,7 @@ definition cond {A : Type} (b : bool) (t e : A) := rec e t b theorem dichotomy (b : bool) : b = ff ∨ b = tt := -cases_on b (or_inl (eq.refl ff)) (or_inr (eq.refl tt)) +cases_on b (or.inl (eq.refl ff)) (or.inr (eq.refl tt)) theorem cond_ff {A : Type} (t e : A) : cond ff t e = e := rfl @@ -80,8 +80,8 @@ theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt := rec (assume H : ff || b = tt, have Hb : b = tt, from (bor_ff_left b) ▸ H, - or_inr Hb) - (assume H, or_inl (eq.refl tt)) + or.inr Hb) + (assume H, or.inl (eq.refl tt)) a definition band (a b : bool) := @@ -118,7 +118,7 @@ cases_on a ... = tt && (b && c) : band_tt_left (b && c)⁻¹) theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt := -or_elim (dichotomy a) +or.elim (dichotomy a) (assume H0 : a = ff, absurd (calc ff = ff && b : (band_ff_left _)⁻¹ diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 4a95fbf53..c2fbc5190 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -71,7 +71,7 @@ have H2 : ¬ pr1 a ≥ pr2 a, from lt_imp_not_ge H, if_neg H2 theorem proj_le {a : ℕ × ℕ} (H : pr1 a ≤ pr2 a) : proj a = pair 0 (pr2 a - pr1 a) := -or_elim le_or_gt +or.elim le_or_gt (assume H2 : pr2 a ≤ pr1 a, have H3 : pr1 a = pr2 a, from le_antisym H H2, calc @@ -119,7 +119,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from ... = pr1 (proj a) : (proj_ge_pr1 H)⁻¹ ... = pr2 (flip (proj a)) : (flip_pr2 (proj a))⁻¹, prod_eq H3 H4, -or_elim le_total +or.elim le_total (assume H : pr2 a ≤ pr1 a, special a H) (assume H : pr1 a ≤ pr2 a, have H2 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H, @@ -129,7 +129,7 @@ or_elim le_total ... = flip (proj a) : {flip_flip a}) theorem proj_rel (a : ℕ × ℕ) : rel a (proj a) := -or_elim le_total +or.elim le_total (assume H : pr2 a ≤ pr1 a, calc pr1 a + pr2 (proj a) = pr1 a + 0 : {proj_ge_pr2 H} @@ -163,7 +163,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from pr2 (proj a) = 0 : proj_ge_pr2 H2 ... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹}, prod_eq H5 H6, -or_elim le_total +or.elim le_total (assume H2 : pr2 a ≤ pr1 a, special a b H2 H) (assume H2 : pr1 a ≤ pr2 a, have H3 : pr2 (flip a) ≤ pr1 (flip a), from P_flip H2, @@ -175,9 +175,9 @@ theorem proj_inj {a b : ℕ × ℕ} (H : proj a = proj b) : rel a b := representative_map_equiv_inj rel_equiv proj_rel @proj_congr H theorem proj_zero_or (a : ℕ × ℕ) : pr1 (proj a) = 0 ∨ pr2 (proj a) = 0 := -or_elim le_total - (assume H : pr2 a ≤ pr1 a, or_inr (proj_ge_pr2 H)) - (assume H : pr1 a ≤ pr2 a, or_inl (proj_le_pr1 H)) +or.elim le_total + (assume H : pr2 a ≤ pr1 a, or.inr (proj_ge_pr2 H)) + (assume H : pr1 a ≤ pr2 a, or.inl (proj_le_pr1 H)) theorem proj_idempotent (a : ℕ × ℕ) : proj (proj a) = proj a := representative_map_idempotent_equiv proj_rel @proj_congr a @@ -222,7 +222,7 @@ have H : ∀v w : ℕ × ℕ, rel v w → dist (pr1 v) (pr2 v) = dist (pr1 w) (p from take v w H, dist_eq_intro H, have H2 : ∀v : ℕ × ℕ, (to_nat (psub v)) = dist (pr1 v) (pr2 v), from take v, (comp_constant quotient H rel_refl), -iff_mp (by simp) H2 (pair n m) +iff.mp (by simp) H2 (pair n m) -- add_rewrite to_nat_comp --local @@ -278,7 +278,7 @@ by simp -- add_rewrite neg_neg neg_zero theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b := -iff_mp (by simp) (congr_arg neg H) +iff.mp (by simp) (congr_arg neg H) theorem neg_move {a b : ℤ} (H : -a = b) : -b = a := H ▸ neg_neg a @@ -289,7 +289,7 @@ by simp theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 := have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, rfl, -have H3 : psub (pair n 0) = psub (pair 0 m), from iff_mp (by simp) H, +have H3 : psub (pair n 0) = psub (pair 0 m), from iff.mp (by simp) H, have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient @rel_refl H3, have H5 : n + m = 0, from calc @@ -306,7 +306,7 @@ opaque_hint (exposing int) theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - n) := have Hrep : proj (rep a) = rep a, from @idempotent_image_fix _ proj proj_idempotent a, -or_imp_or (or_swap (proj_zero_or (rep a))) +or.imp_or (or.swap (proj_zero_or (rep a))) (assume H : pr2 (proj (rep a)) = 0, have H2 : pr2 (rep a) = 0, from Hrep ▸ H, exists_intro (pr1 (rep a)) @@ -330,14 +330,14 @@ opaque_hint (hiding int) ---rename to by_cases in Lean 0.2 (for now using this to avoid name clash) theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) : P a := -or_elim (cases a) +or.elim (cases a) (assume H, obtain (n : ℕ) (H3 : a = n), from H, H3⁻¹ ▸ H1 n) (assume H, obtain (n : ℕ) (H3 : a = -n), from H, H3⁻¹ ▸ H2 n) ---reverse equalities, rename theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) := -or_elim (cases a) - (assume H : (∃n : ℕ, a = of_nat n), or_inl H) +or.elim (cases a) + (assume H : (∃n : ℕ, a = of_nat n), or.inl H) (assume H, obtain (n : ℕ) (H2 : a = -(of_nat n)), from H, discriminate @@ -347,15 +347,15 @@ or_elim (cases a) a = -(of_nat n) : H2 ... = -(of_nat 0) : {H3} ... = of_nat 0 : neg_zero, - or_inl (exists_intro 0 H4)) + or.inl (exists_intro 0 H4)) (take k : ℕ, assume H3 : n = succ k, have H4 : a = -(of_nat (succ k)), from H3 ▸ H2, - or_inr (exists_intro k H4))) + or.inr (exists_intro k H4))) theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a := -or_elim (cases_succ a) +or.elim (cases_succ a) (assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, H3⁻¹ ▸ H1 n) (assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, H3⁻¹ ▸ H2 n) @@ -731,28 +731,28 @@ have H2 : (to_nat a) * (to_nat b) = 0, from ... = (to_nat 0) : {H} ... = 0 : to_nat_of_nat 0, have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul_eq_zero H2, -or_imp_or H3 +or.imp_or H3 (assume H : (to_nat a) = 0, to_nat_eq_zero H) (assume H : (to_nat b) = 0, to_nat_eq_zero H) theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c := have H2 : a * (b - c) = 0, by simp, have H3 : a = 0 ∨ b - c = 0, from mul_eq_zero H2, -or_imp_or_right H3 (assume H4 : b - c = 0, sub_eq_zero H4) +or.imp_or_right H3 (assume H4 : b - c = 0, sub_eq_zero H4) theorem mul_cancel_left {a b c : ℤ} (H1 : a ≠ 0) (H2 : a * b = a * c) : b = c := -resolve_right (mul_cancel_left_or H2) H1 +or.resolve_right (mul_cancel_left_or H2) H1 theorem mul_cancel_right_or {a b c : ℤ} (H : b * a = c * a) : a = 0 ∨ b = c := mul_cancel_left_or ((H ▸ (mul_comm b a)) ▸ mul_comm c a) theorem mul_cancel_right {a b c : ℤ} (H1 : c ≠ 0) (H2 : a * c = b * c) : a = b := -resolve_right (mul_cancel_right_or H2) H1 +or.resolve_right (mul_cancel_right_or H2) H1 theorem mul_ne_zero {a b : ℤ} (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 := not_intro (assume H : a * b = 0, - or_elim (mul_eq_zero H) + or.elim (mul_eq_zero H) (assume H2 : a = 0, absurd H2 Ha) (assume H2 : b = 0, absurd H2 Hb)) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 4f83ec698..3e1a13d9c 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -33,7 +33,7 @@ theorem le_refl (a : ℤ) : a ≤ a := le_intro (add_zero_right a) theorem le_of_nat (n m : ℕ) : (of_nat n ≤ of_nat m) ↔ (n ≤ m) := -iff_intro +iff.intro (assume H : of_nat n ≤ of_nat m, obtain (k : ℕ) (Hk : of_nat n + of_nat k = of_nat m), from le_elim H, have H2 : n + k = m, from of_nat_inj ((add_of_nat n k)⁻¹ ⬝ Hk), @@ -121,7 +121,7 @@ discriminate a = a + 0 : (add_zero_right a)⁻¹ ... = a + n : {H2⁻¹} ... = b : Hn, - or_inr H3) + or.inr H3) (take k : ℕ, assume H2 : n = succ k, have H3 : a + 1 + k = b, from @@ -129,7 +129,7 @@ discriminate a + 1 + k = a + succ k : by simp ... = a + n : by simp ... = b : Hn, - or_inl (le_intro H3)) + or.inl (le_intro H3)) -- ### interaction with neg and sub @@ -173,7 +173,7 @@ le_neg_inv (add_le_cancel_left ((add_neg_right _ _)⁻¹ ▸ (add_neg_right _ _)⁻¹ ▸ H)) theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a := -iff_intro +iff.intro (assume H, sub_self _ ▸ sub_le_right H a) (assume H, sub_add_inverse _ _ ▸ add_zero_left _ ▸ add_le_right H a) @@ -191,13 +191,13 @@ definition gt (a b : ℤ) := b < a infix `>` := int.gt theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b := -iff_refl (a < b) +iff.refl (a < b) theorem gt_def (n m : ℕ) : n > m ↔ m < n := -iff_refl (n > m) +iff.refl (n > m) theorem ge_def (n m : ℕ) : n ≥ m ↔ m ≤ n := -iff_refl (n ≥ m) +iff.refl (n ≥ m) -- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2 @@ -236,7 +236,7 @@ theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) := calc (of_nat n + 1 ≤ of_nat m) ↔ (of_nat (succ n) ≤ of_nat m) : by simp ... ↔ (succ n ≤ m) : le_of_nat (succ n) m - ... ↔ (n < m) : iff_symm (eq_to_iff (nat.lt_def n m)) + ... ↔ (n < m) : iff.symm (eq_to_iff (nat.lt_def n m)) theorem gt_of_nat (n m : ℕ) : (of_nat n > of_nat m) ↔ (n > m) := lt_of_nat m n @@ -260,7 +260,7 @@ theorem le_imp_lt_or_eq {a b : ℤ} (H : a ≤ b) : a < b ∨ a = b := le_imp_succ_le_or_eq H theorem le_ne_imp_lt {a b : ℤ} (H1 : a ≤ b) (H2 : a ≠ b) : a < b := -resolve_left (le_imp_lt_or_eq H1) H2 +or.resolve_left (le_imp_lt_or_eq H1) H2 theorem le_imp_lt_succ {a b : ℤ} (H : a ≤ b) : a < b + 1 := add_le_right H 1 @@ -369,34 +369,34 @@ int_by_cases a show n ≤ -succ m ∨ n > -succ m, from have H0 : -succ m < -m, from lt_neg ((of_nat_succ m)⁻¹ ▸ self_lt_succ m), have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n), - or_inr H)) + or.inr H)) (take n : ℕ, int_by_cases_succ b (take m : ℕ, show -n ≤ m ∨ -n > m, from - or_inl (neg_le_pos n m)) + or.inl (neg_le_pos n m)) (take m : ℕ, show -n ≤ -succ m ∨ -n > -succ m, from - or_imp_or le_or_gt + or.imp_or le_or_gt (assume H : succ m ≤ n, - le_neg (iff_elim_left (iff_symm (le_of_nat (succ m) n)) H)) + le_neg (iff.elim_left (iff.symm (le_of_nat (succ m) n)) H)) (assume H : succ m > n, - lt_neg (iff_elim_left (iff_symm (lt_of_nat n (succ m))) H)))) + lt_neg (iff.elim_left (iff.symm (lt_of_nat n (succ m))) H)))) theorem trichotomy_alt (a b : ℤ) : (a < b ∨ a = b) ∨ a > b := -or_imp_or_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H) +or.imp_or_left (le_or_gt a b) (assume H : a ≤ b, le_imp_lt_or_eq H) theorem trichotomy (a b : ℤ) : a < b ∨ a = b ∨ a > b := -iff_elim_left or_assoc (trichotomy_alt a b) +iff.elim_left or.assoc (trichotomy_alt a b) theorem le_total (a b : ℤ) : a ≤ b ∨ b ≤ a := -or_imp_or_right (le_or_gt a b) (assume H : b < a, lt_imp_le H) +or.imp_or_right (le_or_gt a b) (assume H : b < a, lt_imp_le H) theorem not_lt_imp_le {a b : ℤ} (H : ¬ a < b) : b ≤ a := -resolve_left (le_or_gt b a) H +or.resolve_left (le_or_gt b a) H theorem not_le_imp_lt {a b : ℤ} (H : ¬ a ≤ b) : b < a := -resolve_right (le_or_gt a b) H +or.resolve_right (le_or_gt a b) H -- (non)positivity and (non)negativity -- ------------------------------------- @@ -420,17 +420,17 @@ obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H, Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n) theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 := -iff_mp (iff_symm (le_of_nat _ _)) zero_le +iff.mp (iff.symm (le_of_nat _ _)) zero_le theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) := have aux : ∀x, decidable (0 ≤ x), from take x, have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from - iff_intro + iff.intro (assume H1, to_nat_nonneg_eq H1) (assume H1, H1 ▸ of_nat_nonneg (to_nat x)), - decidable_iff_equiv _ (iff_symm H), -decidable_iff_equiv (aux _) (iff_symm (le_iff_sub_nonneg a b)) + decidable_iff_equiv _ (iff.symm H), +decidable_iff_equiv (aux _) (iff.symm (le_iff_sub_nonneg a b)) theorem ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) theorem lt_decidable [instance] {a b : ℤ} : decidable (a < b) @@ -446,7 +446,7 @@ calc ... = -a : (neg_move (Hn⁻¹))⁻¹ theorem to_nat_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) := -or_imp_or (le_total 0 a) +or.imp_or (le_total 0 a) (assume H : a ≥ 0, (to_nat_nonneg_eq H)⁻¹) (assume H : a ≤ 0, (neg_move ((to_nat_negative H)⁻¹))⁻¹) @@ -517,7 +517,7 @@ lt_trans (mul_lt_right_neg Hb Hc) (mul_lt_left_neg (lt_trans Hc Ha) Hd) -- theorem mul_le_lt_neg and mul_lt_le_neg? theorem mul_lt_cancel_left_nonneg {a b c : ℤ} (Hc : c ≥ 0) (H : c * a < c * b) : a < b := -or_elim (le_or_gt b a) +or.elim (le_or_gt b a) (assume H2 : b ≤ a, have H3 : c * b ≤ c * a, from mul_le_left_nonneg Hc H2, absurd H3 (lt_imp_not_ge H)) @@ -537,7 +537,7 @@ theorem mul_lt_cancel_right_nonpos {a b c : ℤ} (Hc : c ≤ 0) (H : b * c < a * mul_lt_cancel_left_nonpos Hc (mul_comm b c ▸ mul_comm a c ▸ H) theorem mul_le_cancel_left_pos {a b c : ℤ} (Hc : c > 0) (H : c * a ≤ c * b) : a ≤ b := -or_elim (le_or_gt a b) +or.elim (le_or_gt a b) (assume H2 : a ≤ b, H2) (assume H2 : a > b, have H3 : c * a > c * b, from mul_lt_left_pos Hc H2, @@ -563,7 +563,7 @@ have H2 : (to_nat a) * (to_nat b) = 1, from ... = (to_nat 1) : {H} ... = 1 : to_nat_of_nat 1, have H3 : (to_nat a) = 1, from mul_eq_one_left H2, -or_imp_or (to_nat_cases a) +or.imp_or (to_nat_cases a) (assume H4 : a = (to_nat a), H3 ▸ H4) (assume H4 : a = - (to_nat a), H3 ▸ H4) @@ -576,10 +576,6 @@ mul_eq_one_left (mul_comm a b ▸ H) definition sign (a : ℤ) : ℤ := if a > 0 then 1 else (if a < 0 then - 1 else 0) --- TODO: for kernel -theorem or_elim3 {a b c d : Prop} (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d := -or_elim H Ha (assume H2,or_elim H2 Hb Hc) - theorem sign_pos {a : ℤ} (H : a > 0) : sign a = 1 := if_pos H @@ -594,17 +590,17 @@ if_neg (lt_irrefl 0) ⬝ if_neg (lt_irrefl 0) theorem mul_sign_to_nat (a : ℤ) : sign a * (to_nat a) = a := have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le, have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le, -or_elim3 (trichotomy a 0) +or.elim3 (trichotomy a 0) (assume H : a < 0, by simp) (assume H : a = 0, by simp) (assume H : a > 0, by simp) -- TODO: show decidable for equality (and avoid classical library) theorem sign_mul (a b : ℤ) : sign (a * b) = sign a * sign b := -or_elim (em (a = 0)) +or.elim (em (a = 0)) (assume Ha : a = 0, by simp) (assume Ha : a ≠ 0, - or_elim (em (b = 0)) + or.elim (em (b = 0)) (assume Hb : b = 0, by simp) (assume Hb : b ≠ 0, have H : sign (a * b) * (to_nat (a * b)) = sign a * sign b * (to_nat (a * b)), from @@ -621,21 +617,21 @@ or_elim (em (a = 0)) --set_option pp::coercion true theorem sign_idempotent (a : ℤ) : sign (sign a) = sign a := -have temp : of_nat 1 > 0, from iff_elim_left (iff_symm (lt_of_nat 0 1)) succ_pos, +have temp : of_nat 1 > 0, from iff.elim_left (iff.symm (lt_of_nat 0 1)) succ_pos, --this should be done with simp -or_elim3 (trichotomy a 0) sorry sorry sorry +or.elim3 (trichotomy a 0) sorry sorry sorry -- (by simp) -- (by simp) -- (by simp) theorem sign_succ (n : ℕ) : sign (succ n) = 1 := -sign_pos (iff_elim_left (iff_symm (lt_of_nat 0 (succ n))) succ_pos) +sign_pos (iff.elim_left (iff.symm (lt_of_nat 0 (succ n))) succ_pos) --this should be done with simp theorem sign_neg (a : ℤ) : sign (-a) = - sign a := have temp1 : a > 0 → -a < 0, from neg_lt_zero, have temp2 : a < 0 → -a > 0, from zero_lt_neg, -or_elim3 (trichotomy a 0) sorry sorry sorry +or.elim3 (trichotomy a 0) sorry sorry sorry -- (by simp) -- (by simp) -- (by simp) @@ -643,7 +639,7 @@ or_elim3 (trichotomy a 0) sorry sorry sorry -- add_rewrite sign_neg theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 := -or_elim3 (trichotomy a 0) sorry +or.elim3 (trichotomy a 0) sorry -- (by simp) (assume H2 : a = 0, absurd H2 H) sorry @@ -652,7 +648,7 @@ or_elim3 (trichotomy a 0) sorry theorem sign_to_nat (a : ℤ) : sign (to_nat a) = to_nat (sign a) := have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le, have temp2 : ∀a : ℤ, a > 0 → a ≥ 0, from take a, lt_imp_le, -or_elim3 (trichotomy a 0) sorry sorry sorry +or.elim3 (trichotomy a 0) sorry sorry sorry -- (by simp) -- (by simp) -- (by simp) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 8f07abc57..98daa1e25 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -186,42 +186,42 @@ definition mem (x : T) : list T → Prop := rec false (fun y l H, x = y ∨ H) infix `∈` := mem -- TODO: constructively, equality is stronger. Use that? -theorem mem_nil {x : T} : x ∈ nil ↔ false := iff_rfl +theorem mem_nil {x : T} : x ∈ nil ↔ false := iff.rfl -theorem mem_cons {x y : T} {l : list T} : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff_rfl +theorem mem_cons {x y : T} {l : list T} : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff.rfl theorem mem_concat_imp_or {x : T} {s t : list T} : x ∈ s ++ t → x ∈ s ∨ x ∈ t := -induction_on s or_inr +induction_on s or.inr (take y s, assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t, assume H1 : x ∈ (y :: s) ++ t, have H2 : x = y ∨ x ∈ s ++ t, from H1, - have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or_imp_or_right H2 IH, - iff_elim_right or_assoc H3) + have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or.imp_or_right H2 IH, + iff.elim_right or.assoc H3) theorem mem_or_imp_concat {x : T} {s t : list T} : x ∈ s ∨ x ∈ t → x ∈ s ++ t := induction_on s - (take H, or_elim H false_elim (assume H, H)) + (take H, or.elim H false_elim (assume H, H)) (take y s, assume IH : x ∈ s ∨ x ∈ t → x ∈ s ++ t, assume H : x ∈ y :: s ∨ x ∈ t, - or_elim H + or.elim H (assume H1, - or_elim H1 - (take H2 : x = y, or_inl H2) - (take H2 : x ∈ s, or_inr (IH (or_inl H2)))) - (assume H1 : x ∈ t, or_inr (IH (or_inr H1)))) + or.elim H1 + (take H2 : x = y, or.inl H2) + (take H2 : x ∈ s, or.inr (IH (or.inl H2)))) + (assume H1 : x ∈ t, or.inr (IH (or.inr H1)))) theorem mem_concat {x : T} {s t : list T} : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t -:= iff_intro mem_concat_imp_or mem_or_imp_concat +:= iff.intro mem_concat_imp_or mem_or_imp_concat theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x :: t) := induction_on l - (take H : x ∈ nil, false_elim (iff_elim_left mem_nil H)) + (take H : x ∈ nil, false_elim (iff.elim_left mem_nil H)) (take y l, assume IH : x ∈ l → ∃s t : list T, l = s ++ (x :: t), assume H : x ∈ y :: l, - or_elim H + or.elim H (assume H1 : x = y, exists_intro nil (exists_intro l (H1 ▸ rfl))) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 4cc73d896..edcd4e3a1 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -73,19 +73,19 @@ opaque_hint (hiding pred) theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n - (or_inl rfl) - (take m IH, or_inr + (or.inl rfl) + (take m IH, or.inr (show succ m = succ (pred (succ m)), from congr_arg succ pred_succ⁻¹)) theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k := -or_imp_or (zero_or_succ_pred n) (assume H, H) +or.imp_or (zero_or_succ_pred n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H) theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n := induction_on n H1 (take m IH, H2 m) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B := -or_elim (zero_or_succ_pred n) +or.elim (zero_or_succ_pred n) (take H3 : n = 0, H1 H3) (take H3 : n = succ (pred n), H2 (pred n) H3) @@ -350,11 +350,11 @@ calc theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 := discriminate - (take Hn : n = 0, or_inl Hn) + (take Hn : n = 0, or.inl Hn) (take (k : ℕ), assume (Hk : n = succ k), discriminate - (take (Hm : m = 0), or_inr Hm) + (take (Hm : m = 0), or.inr Hm) (take (l : ℕ), assume (Hl : m = succ l), have Heq : succ (k * succ l + l) = n * m, from diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 8edd2566c..9c6a32c08 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -164,8 +164,8 @@ show lhs = rhs, from lhs = 0 : if_pos H1 ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2a : y ≠ 0, from assume H, H1 (or_inl H), - have H2b : ¬ x < y, from assume H, H1 (or_inr H), + have H2a : y ≠ 0, from assume H, H1 (or.inl H), + have H2b : ¬ x < y, from assume H, H1 (or.inr H), have ypos : y > 0, from ne_zero_imp_pos H2a, have xgey : x ≥ y, from not_lt_imp_ge H2b, have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -183,12 +183,12 @@ definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x infixl `div` := idivide theorem div_zero {x : ℕ} : x div 0 = 0 := -div_aux_spec _ _ ⬝ if_pos (or_inl rfl) +div_aux_spec _ _ ⬝ if_pos (or.inl rfl) -- add_rewrite div_zero theorem div_less {x y : ℕ} (H : x < y) : x div y = 0 := -div_aux_spec _ _ ⬝ if_pos (or_inr H) +div_aux_spec _ _ ⬝ if_pos (or.inr H) -- add_rewrite div_less @@ -201,7 +201,7 @@ theorem div_rec {x y : ℕ} (H1 : y > 0) (H2 : x ≥ y) : x div y = succ ((x - y have H3 : ¬ (y = 0 ∨ x < y), from not_intro (assume H4 : y = 0 ∨ x < y, - or_elim H4 + or.elim H4 (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1)) (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)), div_aux_spec _ _ ⬝ if_neg H3 @@ -240,8 +240,8 @@ show lhs = rhs, from lhs = x : if_pos H1 ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2a : y ≠ 0, from assume H, H1 (or_inl H), - have H2b : ¬ x < y, from assume H, H1 (or_inr H), + have H2a : y ≠ 0, from assume H, H1 (or.inl H), + have H2b : ¬ x < y, from assume H, H1 (or.inr H), have ypos : y > 0, from ne_zero_imp_pos H2a, have xgey : x ≥ y, from not_lt_imp_ge H2b, have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -259,12 +259,12 @@ definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x infixl `mod` := modulo theorem mod_zero {x : ℕ} : x mod 0 = x := -mod_aux_spec _ _ ⬝ if_pos (or_inl rfl) +mod_aux_spec _ _ ⬝ if_pos (or.inl rfl) -- add_rewrite mod_zero theorem mod_lt_eq {x y : ℕ} (H : x < y) : x mod y = x := -mod_aux_spec _ _ ⬝ if_pos (or_inr H) +mod_aux_spec _ _ ⬝ if_pos (or.inr H) -- add_rewrite mod_lt_eq @@ -277,7 +277,7 @@ theorem mod_rec {x y : ℕ} (H1 : y > 0) (H2 : x ≥ y) : x mod y = (x - y) mod have H3 : ¬ (y = 0 ∨ x < y), from not_intro (assume H4 : y = 0 ∨ x < y, - or_elim H4 + or.elim H4 (assume H5 : y = 0, not_elim lt_irrefl (H5 ▸ H1)) (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)), mod_aux_spec _ _ ⬝ if_neg H3 @@ -494,7 +494,7 @@ show x mod y = 0, from ... = 0 : mul_zero_left) theorem dvd_iff_exists_mul {x y : ℕ} : x | y ↔ ∃z, z * x = y := -iff_intro +iff.intro (assume H : x | y, show ∃z, z * x = y, from exists_intro _ (dvd_imp_div_mul_eq H)) (assume H : ∃z, z * x = y, diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 340853826..3968248a6 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -138,7 +138,7 @@ discriminate n = n + 0 : add_zero_right⁻¹ ... = n + k : {H3⁻¹} ... = m : Hk, - or_inr Heq) + or.inr Heq) (take l : nat, assume H3 : k = succ l, have Hlt : succ n ≤ m, from @@ -147,13 +147,13 @@ discriminate succ n + l = n + succ l : add_move_succ ... = n + k : {H3⁻¹} ... = m : Hk)), - or_inl Hlt) + or.inl Hlt) theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m := -resolve_left (le_imp_succ_le_or_eq H1) H2 +or.resolve_left (le_imp_succ_le_or_eq H1) H2 theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m := -or_imp_or_left (le_imp_succ_le_or_eq H) +or.imp_or_left (le_imp_succ_le_or_eq H) (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m := @@ -198,7 +198,7 @@ discriminate theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m := discriminate (take Hn : n = 0, - or_inl (Hn⁻¹ ▸ zero_le)) + or.inl (Hn⁻¹ ▸ zero_le)) (take k : ℕ, assume Hn : n = succ k, have H2 : pred n = k, @@ -208,7 +208,7 @@ discriminate have H3 : k ≤ m, from H2 ▸ H, have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, show n ≤ m ∨ n = succ m, from - or_imp_or H4 + or.imp_or H4 (take H5 : succ k ≤ m, show n ≤ m, from Hn⁻¹ ▸ H5) (take H5 : k = m, show n = succ m, from H5 ▸ Hn)) @@ -382,10 +382,10 @@ theorem lt_imp_lt_succ {n m : ℕ} (H : n < m) : n < succ m theorem le_or_gt {n m : ℕ} : n ≤ m ∨ n > m := induction_on n - (or_inl zero_le) + (or.inl zero_le) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, - or_elim IH + or.elim IH (assume H : k ≤ m, obtain (l : ℕ) (Hl : k + l = m), from le_elim H, discriminate @@ -396,7 +396,7 @@ induction_on n ... = k + 0 : {H2} ... = k : add_zero_right, have H4 : m < succ k, from H3 ▸ self_lt_succ, - or_inr H4) + or.inr H4) (take l2 : ℕ, assume H2 : l = succ l2, have H3 : succ k + l2 = m, @@ -404,23 +404,23 @@ induction_on n succ k + l2 = k + succ l2 : add_move_succ ... = k + l : {H2⁻¹} ... = m : Hl, - or_inl (le_intro H3))) - (assume H : m < k, or_inr (lt_imp_lt_succ H))) + or.inl (le_intro H3))) + (assume H : m < k, or.inr (lt_imp_lt_succ H))) theorem trichotomy_alt {n m : ℕ} : (n < m ∨ n = m) ∨ n > m := -or_imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H) +or.imp_or_left le_or_gt (assume H : n ≤ m, le_imp_lt_or_eq H) theorem trichotomy {n m : ℕ} : n < m ∨ n = m ∨ n > m := -iff_elim_left or_assoc trichotomy_alt +iff.elim_left or.assoc trichotomy_alt theorem le_total {n m : ℕ} : n ≤ m ∨ m ≤ n := -or_imp_or_right le_or_gt (assume H : m < n, lt_imp_le H) +or.imp_or_right le_or_gt (assume H : m < n, lt_imp_le H) theorem not_lt_imp_ge {n m : ℕ} (H : ¬ n < m) : n ≥ m := -resolve_left le_or_gt H +or.resolve_left le_or_gt H theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m := -resolve_right le_or_gt H +or.resolve_right le_or_gt H -- The following three theorems are automatically proved using the instance le_decidable theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m) @@ -442,7 +442,7 @@ have H1 : ∀ {n m : nat}, m < n → P m, from show ∀m, m < succ n' → P m, from take m, assume H3 : m < succ n', - or_elim (le_imp_lt_or_eq (lt_succ_imp_le H3)) + or.elim (le_imp_lt_or_eq (lt_succ_imp_le H3)) (assume H4: m < n', IH H4) (assume H4: m = n', H4⁻¹ ▸ H2)), H1 self_lt_succ @@ -470,15 +470,15 @@ theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀ {y : nat case y H0 (take y, H1 succ_pos) theorem zero_or_pos {n : ℕ} : n = 0 ∨ n > 0 := -or_imp_or_left - (or_swap (le_imp_lt_or_eq zero_le)) +or.imp_or_left + (or.swap (le_imp_lt_or_eq zero_le)) (take H : 0 = n, H⁻¹) theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 := H⁻¹ ▸ succ_pos theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 := -or_elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) +or.elim zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 := ne.symm (lt_imp_ne H) @@ -541,7 +541,7 @@ have H4 : k * m < k * l, from mul_lt_left (le_lt_trans zero_le H1) H2, le_lt_trans H3 H4 theorem mul_lt_cancel_left {n m k : ℕ} (H : k * n < k * m) : n < m := -or_elim le_or_gt +or.elim le_or_gt (assume H2 : m ≤ n, have H3 : k * m ≤ k * n, from mul_le_left H2 k, absurd H3 (lt_imp_not_ge H)) @@ -567,7 +567,7 @@ have H5 : k ≤ m, from mul_le_cancel_left Hn H3, le_antisym H4 H5 theorem mul_cancel_left_or {n m k : ℕ} (H : n * m = n * k) : n = 0 ∨ m = k := -or_imp_or_right zero_or_pos +or.imp_or_right zero_or_pos (assume Hn : n > 0, mul_cancel_left Hn H) theorem mul_cancel_right {n m k : ℕ} (Hm : m > 0) (H : n * m = k * m) : n = k := @@ -580,7 +580,7 @@ theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 := have H2 : n * m > 0, from H⁻¹ ▸ succ_pos, have H3 : n > 0, from mul_pos_imp_pos_left H2, have H4 : m > 0, from mul_pos_imp_pos_right H2, -or_elim le_or_gt +or.elim le_or_gt (assume H5 : n ≤ 1, show n = 1, from le_antisym H5 H3) (assume H5 : n > 1, diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index a41a0975d..93192d600 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -220,18 +220,18 @@ theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := add_comm ▸ add_sub_ge theorem le_add_sub_left {n m : ℕ} : n ≤ n + (m - n) := -or_elim le_total +or.elim le_total (assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ H) (assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ le_refl) theorem le_add_sub_right {n m : ℕ} : m ≤ n + (m - n) := -or_elim le_total +or.elim le_total (assume H : n ≤ m, (add_sub_le H)⁻¹ ▸ le_refl) (assume H : m ≤ n, (add_sub_ge H)⁻¹ ▸ H) theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) : P (n - m) := -or_elim le_total +or.elim le_total (assume H3 : n ≤ m, (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 H3)) (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) @@ -277,7 +277,7 @@ sub_split theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) := -or_elim le_total +or.elim le_total (assume H3 : n ≤ m, le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) (assume H3 : m ≤ n, @@ -305,7 +305,7 @@ obtain (x' : ℕ) (xeq : x = succ x'), from pos_imp_eq_succ xpos, theorem sub_le_right {n m : ℕ} (H : n ≤ m) (k : nat) : n - k ≤ m - k := obtain (l : ℕ) (Hl : n + l = m), from le_elim H, -or_elim le_total +or.elim le_total (assume H2 : n ≤ k, (le_imp_sub_eq_zero H2)⁻¹ ▸ zero_le) (assume H2 : k ≤ n, have H3 : n - k + l = m - k, from @@ -488,7 +488,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l ... = dist (n * k) (n * l + (m * k - m * l)) : {add_comm} ... = dist (n * k) (n * l + m * k - m * l) : {(add_sub_assoc H2 (n * l))⁻¹} ... = dist (n * k + m * l) (n * l + m * k) : dist_sub_move_add' H3 _, -or_elim le_total +or.elim le_total (assume H : k ≤ l, dist_comm ▸ dist_comm ▸ aux l k H) (assume H : l ≤ k, aux k l H) diff --git a/library/data/prod.lean b/library/data/prod.lean index 1f687c91f..fa74c51f0 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -56,10 +56,10 @@ section theorem prod_eq_decidable [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v)) (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) := have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from - iff_intro + iff.intro (assume H, H ▸ and.intro rfl rfl) (assume H, and.elim H (assume H4 H5, prod_eq H4 H5)), - decidable_iff_equiv _ (iff_symm H3) + decidable_iff_equiv _ (iff.symm H3) end diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index 7adc991de..0ff1008c5 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -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) @@ -58,23 +58,23 @@ 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 := -iff_elim_right (R_iff Q r s) (and.intro H1 (and.intro H2 H3)) +iff.elim_right (R_iff Q r s) (and.intro H1 (and.intro H2 H3)) theorem R_intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) (H1 : reflexive R) {r s : A} (H2 : abs r = abs s) : R r s := -iff_elim_right (R_iff Q r s) (and.intro (H1 r) (and.intro (H1 s) H2)) +iff.elim_right (R_iff Q r s) (and.intro (H1 r) (and.intro (H1 s) H2)) theorem rep_eq {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {a b : B} (H : R (rep a) (rep b)) : a = b := @@ -235,7 +235,7 @@ open eq_ops theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A) : (f a = f a') ↔ (fun_image f a = fun_image f a') := -iff_intro +iff.intro (assume H : f a = f a', tag_eq H) (assume H : fun_image f a = fun_image f a', (congr_arg elt_of H ▸ elt_of_fun_image f a) ▸ elt_of_fun_image f a') @@ -246,7 +246,7 @@ obtain (a : A) (Ha : fun_image f a = u), from fun_image_surj u, calc fun_image f (elt_of u) = fun_image f (elt_of (fun_image f a)) : {Ha⁻¹} ... = fun_image f (f a) : {elt_of_fun_image f a} - ... = fun_image f a : {iff_elim_left (fun_image_eq f (f a) a) (H a)} + ... = fun_image f a : {iff.elim_left (fun_image_eq f (f a) a) (H a)} ... = u : Ha theorem idempotent_image_fix {A : Type} {f : A → A} (H : ∀a, f (f a) = f a) (u : image f) @@ -264,7 +264,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 := -(and.elim_right (and.elim_right (iff_elim_left (H2 a (f a)) (H1 a))))⁻¹ +(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) : @@ -321,7 +321,7 @@ representative_map_to_quotient (take a b, have reflR : reflexive R, from rel_refl R, have H3 : f a = f b → R a b, from representative_map_equiv_inj equiv H1 H2, - have H4 : R a b ↔ f a = f b, from iff_intro (H2 a b) H3, + have H4 : R a b ↔ f a = f b, from iff.intro (H2 a b) H3, have H5 : R a b ↔ R b b ∧ f a = f b, from subst (symm (and_absorb_left _ (reflR b))) H4, subst (symm (and_absorb_left _ (reflR a))) H5) diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean index 4378ea3d5..ae1278b11 100644 --- a/library/data/quotient/classical.lean +++ b/library/data/quotient/classical.lean @@ -31,7 +31,7 @@ have symmR : symmetric R, from is_symmetric.infer R, have transR : transitive R, from is_transitive.infer R, have H3 : ∀c, R a c ↔ R b c, from take c, - iff_intro + iff.intro (assume H4 : R a c, transR (symmR H2) H4) (assume H4 : R b c, transR H2 H4), have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)), diff --git a/library/data/set.lean b/library/data/set.lean index 0ad383bcc..c54f68047 100644 --- a/library/data/set.lean +++ b/library/data/set.lean @@ -18,13 +18,13 @@ definition eqv {T : Type} (A B : set T) : Prop := infixl `∼`:50 := eqv theorem eqv_refl {T : Type} (A : set T) : A ∼ A := -take x, iff_rfl +take x, iff.rfl theorem eqv_symm {T : Type} {A B : set T} (H : A ∼ B) : B ∼ A := -take x, iff_symm (H x) +take x, iff.symm (H x) theorem eqv_trans {T : Type} {A B C : set T} (H1 : A ∼ B) (H2 : B ∼ C) : A ∼ C := -take x, iff_trans (H1 x) (H2 x) +take x, iff.trans (H1 x) (H2 x) definition empty {T : Type} : set T := λx, ff @@ -44,7 +44,7 @@ definition inter {T : Type} (A B : set T) : set T := infixl `∩` := inter theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := -iff_intro +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, @@ -52,46 +52,46 @@ iff_intro show A x && B x = tt, from e1⁻¹ ▸ e2⁻¹ ▸ band_tt_left tt) theorem inter_id {T : Type} (A : set T) : A ∩ A ∼ A := -take x, band_id (A x) ▸ iff_rfl +take x, band_id (A x) ▸ iff.rfl theorem inter_empty_right {T : Type} (A : set T) : A ∩ ∅ ∼ ∅ := -take x, band_ff_right (A x) ▸ iff_rfl +take x, band_ff_right (A x) ▸ iff.rfl theorem inter_empty_left {T : Type} (A : set T) : ∅ ∩ A ∼ ∅ := -take x, band_ff_left (A x) ▸ iff_rfl +take x, band_ff_left (A x) ▸ iff.rfl theorem inter_comm {T : Type} (A B : set T) : A ∩ B ∼ B ∩ A := -take x, band_comm (A x) (B x) ▸ iff_rfl +take x, band_comm (A x) (B x) ▸ iff.rfl theorem inter_assoc {T : Type} (A B C : set T) : (A ∩ B) ∩ C ∼ A ∩ (B ∩ C) := -take x, band_assoc (A x) (B x) (C x) ▸ iff_rfl +take x, band_assoc (A x) (B x) (C x) ▸ iff.rfl definition union {T : Type} (A B : set T) : set T := λx, A x || B x infixl `∪` := union theorem mem_union {T : Type} (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) := -iff_intro +iff.intro (assume H, bor_to_or H) - (assume H, or_elim H + (assume H, or.elim H (assume Ha : A x = tt, show A x || B x = tt, from Ha⁻¹ ▸ bor_tt_left (B x)) (assume Hb : B x = tt, show A x || B x = tt, from Hb⁻¹ ▸ bor_tt_right (A x))) theorem union_id {T : Type} (A : set T) : A ∪ A ∼ A := -take x, bor_id (A x) ▸ iff_rfl +take x, bor_id (A x) ▸ iff.rfl theorem union_empty_right {T : Type} (A : set T) : A ∪ ∅ ∼ A := -take x, bor_ff_right (A x) ▸ iff_rfl +take x, bor_ff_right (A x) ▸ iff.rfl theorem union_empty_left {T : Type} (A : set T) : ∅ ∪ A ∼ A := -take x, bor_ff_left (A x) ▸ iff_rfl +take x, bor_ff_left (A x) ▸ iff.rfl theorem union_comm {T : Type} (A B : set T) : A ∪ B ∼ B ∪ A := -take x, bor_comm (A x) (B x) ▸ iff_rfl +take x, bor_comm (A x) (B x) ▸ iff.rfl theorem union_assoc {T : Type} (A B C : set T) : (A ∪ B) ∪ C ∼ A ∪ (B ∪ C) := -take x, bor_assoc (A x) (B x) (C x) ▸ iff_rfl +take x, bor_assoc (A x) (B x) (C x) ▸ iff.rfl end set diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 4672fc847..0eebdd1c3 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -45,8 +45,8 @@ section theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x}) (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) := have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from - iff_intro (assume H, eq.subst H rfl) (assume H, subtype_eq H), - decidable_iff_equiv _ (iff_symm H1) + iff.intro (assume H, eq.subst H rfl) (assume H, subtype_eq H), + decidable_iff_equiv _ (iff.symm H1) end diff --git a/library/data/sum.lean b/library/data/sum.lean index e0b260b5e..fc645ba13 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -70,14 +70,14 @@ rec_on s1 (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) (take b2, have H3 : (inl B a1 = inr A b2) ↔ false, - from iff_intro inl_neq_inr (assume H4, false_elim H4), - show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3))) + from iff.intro inl_neq_inr (assume H4, false_elim H4), + show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3))) (take b1, show decidable (inr A b1 = s2), from rec_on s2 (take a2, have H3 : (inr A b1 = inl B a2) ↔ false, - from iff_intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4), - show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3)) + from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4), + show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3)) (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) end sum diff --git a/library/general_notation.lean b/library/general_notation.lean index 297951c53..6ffd9c480 100644 --- a/library/general_notation.lean +++ b/library/general_notation.lean @@ -30,7 +30,6 @@ precedence `↔`:25 precedence `=`:50 precedence `≠`:50 -precedence `rfl`:max -- shorthand for reflexivity precedence `≈`:50 -- used for path in hott precedence `∼`:50 diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index 47760a71f..60c9ab9b8 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -12,7 +12,7 @@ open eq_ops axiom prop_complete (a : Prop) : a = true ∨ a = false theorem cases (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a := -or_elim (prop_complete a) +or.elim (prop_complete a) (assume Ht : a = true, Ht⁻¹ ▸ H1) (assume Hf : a = false, Hf⁻¹ ▸ H2) @@ -21,27 +21,27 @@ cases P H1 H2 a -- this supercedes the em in decidable theorem em (a : Prop) : a ∨ ¬a := -or_elim (prop_complete a) - (assume Ht : a = true, or_inl (eq_true_elim Ht)) - (assume Hf : a = false, or_inr (eq_false_elim Hf)) +or.elim (prop_complete a) + (assume Ht : a = true, or.inl (eq_true_elim Ht)) + (assume Hf : a = false, or.inr (eq_false_elim Hf)) theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true := cases (λ x, x = false ∨ x = true) - (or_inr rfl) - (or_inl rfl) + (or.inr rfl) + (or.inl rfl) a theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b := -or_elim (prop_complete a) - (assume Hat, or_elim (prop_complete b) +or.elim (prop_complete a) + (assume Hat, or.elim (prop_complete b) (assume Hbt, Hat ⬝ Hbt⁻¹) (assume Hbf, false_elim (Hbf ▸ (Hab (eq_true_elim Hat))))) - (assume Haf, or_elim (prop_complete b) + (assume Haf, or.elim (prop_complete b) (assume Hbt, false_elim (Haf ▸ (Hba (eq_true_elim Hbt)))) (assume Hbf, Haf ⬝ Hbf⁻¹)) theorem iff_to_eq {a b : Prop} (H : a ↔ b) : a = b := -iff_elim (assume H1 H2, propext H1 H2) H +iff.elim (assume H1 H2, propext H1 H2) H theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := propext diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean index 3b4b1b0bd..a89448758 100644 --- a/library/logic/axioms/examples/diaconescu.lean +++ b/library/logic/axioms/examples/diaconescu.lean @@ -18,28 +18,28 @@ definition u [private] := epsilon (λx, x = true ∨ p) definition v [private] := epsilon (λx, x = false ∨ p) lemma u_def [private] : u = true ∨ p := -epsilon_spec (exists_intro true (or_inl rfl)) +epsilon_spec (exists_intro true (or.inl rfl)) lemma v_def [private] : v = false ∨ p := -epsilon_spec (exists_intro false (or_inl rfl)) +epsilon_spec (exists_intro false (or.inl rfl)) lemma uv_implies_p [private] : ¬(u = v) ∨ p := -or_elim u_def - (assume Hut : u = true, or_elim v_def +or.elim u_def + (assume Hut : u = true, or.elim v_def (assume Hvf : v = false, have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false, - or_inl Hne) - (assume Hp : p, or_inr Hp)) - (assume Hp : p, or_inr Hp) + or.inl Hne) + (assume Hp : p, or.inr Hp)) + (assume Hp : p, or.inr Hp) lemma p_implies_uv [private] : p → u = v := assume Hp : p, have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from funext (take x : Prop, have Hl : (x = true ∨ p) → (x = false ∨ p), from - assume A, or_inr Hp, + assume A, or.inr Hp, have Hr : (x = false ∨ p) → (x = true ∨ p), from - assume A, or_inr Hp, + assume A, or.inr Hp, show (x = true ∨ p) = (x = false ∨ p), from propext Hl Hr), show u = v, from @@ -47,7 +47,7 @@ assume Hp : p, theorem em : p ∨ ¬p := have H : ¬(u = v) → ¬p, from mt p_implies_uv, - or_elim uv_implies_p - (assume Hne : ¬(u = v), or_inr (H Hne)) - (assume Hp : p, or_inl Hp) + or.elim uv_implies_p + (assume Hne : ¬(u = v), or.inr (H Hne)) + (assume Hp : p, or.inl Hp) end diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index e6d88b561..affa6efcd 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -68,7 +68,7 @@ in exists_intro f H theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} : (∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) := -iff_intro +iff.intro (assume H : (∀x, ∃y, P x y), axiom_of_choice H) (assume H : (∃f, (∀x, P x (f x))), take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H, diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index d469c826b..1e452dbc0 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -13,7 +13,7 @@ open decidable inhabited nonempty -- First, we show that (decidable a) is inhabited for any 'a' using the excluded middle theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) := nonempty_imp_inhabited - (or_elim (em a) + (or.elim (em a) (assume Ha, nonempty.intro (inl Ha)) (assume Hna, nonempty.intro (inr Hna))) diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean index 38ae2ea8c..766891e16 100644 --- a/library/logic/classes/decidable.lean +++ b/library/logic/classes/decidable.lean @@ -36,13 +36,13 @@ decidable.rec d1 theorem em (p : Prop) {H : decidable p} : p ∨ ¬p := -induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp) +induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) theorem by_cases {a b : Prop} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b := -or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna) +or.elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna) theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p := -or_elim (em p) +or.elim (em p) (assume H1 : p, H1) (assume H1 : ¬p, false_elim (H H1)) @@ -57,10 +57,10 @@ rec_on Ha theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) := rec_on Ha - (assume Ha : a, inl (or_inl Ha)) + (assume Ha : a, inl (or.inl Ha)) (assume Hna : ¬a, rec_on Hb - (assume Hb : b, inl (or_inr Hb)) - (assume Hnb : ¬b, inr (or_not_intro Hna Hnb))) + (assume Hb : b, inl (or.inr Hb)) + (assume Hnb : ¬b, inr (or.not_intro Hna Hnb))) theorem not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) := rec_on Ha @@ -71,12 +71,12 @@ theorem iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable decidable (a ↔ b) := rec_on Ha (assume Ha, rec_on Hb - (assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha))) - (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_elim_left H Ha) Hnb))) + (assume Hb : b, inl (iff.intro (assume H, Hb) (assume H, Ha))) + (assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff.elim_left H Ha) Hnb))) (assume Hna, rec_on Hb - (assume Hb : b, inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna)) + (assume Hb : b, inr (assume H : a ↔ b, absurd (iff.elim_right H Hb) Hna)) (assume Hnb : ¬b, inl - (iff_intro (assume Ha, absurd Ha Hna) (assume Hb, absurd Hb Hnb)))) + (iff.intro (assume Ha, absurd Ha Hna) (assume Hb, absurd Hb Hnb)))) theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) := @@ -88,8 +88,8 @@ rec_on Ha theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b := rec_on Ha - (assume Ha : a, inl (iff_elim_left H Ha)) - (assume Hna : ¬a, inr (iff_elim_left (iff_flip_sign H) Hna)) + (assume Ha : a, inl (iff.elim_left H Ha)) + (assume Hna : ¬a, inr (iff.elim_left (iff.flip_sign H) Hna)) theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b := decidable_iff_equiv Ha (eq_to_iff H) diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index 11911955c..48172a12d 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -6,176 +6,191 @@ import general_notation .eq -- and -- --- - inductive and (a b : Prop) : Prop := -intro : a → b → and a b + intro : a → b → and a b infixr `/\` := and infixr `∧` := and namespace and -theorem elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c := -rec H2 H1 + theorem elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c := + rec H2 H1 -theorem elim_left {a b : Prop} (H : a ∧ b) : a := -rec (λa b, a) H + theorem elim_left {a b : Prop} (H : a ∧ b) : a := + rec (λa b, a) H -theorem elim_right {a b : Prop} (H : a ∧ b) : b := -rec (λa b, b) H + theorem elim_right {a b : Prop} (H : a ∧ b) : b := + rec (λa b, b) H -theorem swap {a b : Prop} (H : a ∧ b) : b ∧ a := -intro (elim_right H) (elim_left H) + theorem swap {a b : Prop} (H : a ∧ b) : b ∧ a := + intro (elim_right H) (elim_left H) -theorem not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := -assume H : a ∧ b, absurd (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 not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := -assume H : a ∧ b, absurd (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 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 {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_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_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)) + 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 -- -- - inductive or (a b : Prop) : Prop := -intro_left : a → or a b, -intro_right : b → or a b + intro_left : a → or a b, + intro_right : b → or a b infixr `\/` := or infixr `∨` := or -theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or.intro_left b Ha -theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or.intro_right a Hb +namespace or + theorem inl {a b : Prop} (Ha : a) : a ∨ b := + intro_left b Ha -theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := -or.rec H2 H3 H1 + theorem inr {a b : Prop} (Hb : b) : a ∨ b := + intro_right a Hb -theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b := -or_elim H1 (assume Ha, absurd Ha H2) (assume Hb, Hb) + theorem elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := + rec H2 H3 H1 -theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a := -or_elim H1 (assume Ha, Ha) (assume Hb, absurd Hb H2) + theorem elim3 {a b c d : Prop} (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d := + elim H Ha (assume H2, elim H2 Hb Hc) -theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a := -or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb) + theorem resolve_right {a b : Prop} (H1 : a ∨ b) (H2 : ¬a) : b := + elim H1 (assume Ha, absurd Ha H2) (assume Hb, Hb) -theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := -assume H : a ∨ b, or_elim H - (assume Ha, absurd Ha Hna) - (assume Hb, absurd Hb Hnb) + theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a := + elim H1 (assume Ha, Ha) (assume Hb, absurd Hb H2) -theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d := -or_elim H1 - (assume Ha : a, or_inl (H2 Ha)) - (assume Hb : b, or_inr (H3 Hb)) + theorem swap {a b : Prop} (H : a ∨ b) : b ∨ a := + elim H (assume Ha, inr Ha) (assume Hb, inl Hb) -theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c := -or_elim H1 - (assume H2 : a, or_inl (H H2)) - (assume H2 : c, or_inr H2) + theorem not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) := + assume H : a ∨ b, elim H + (assume Ha, absurd Ha Hna) + (assume Hb, absurd Hb Hnb) -theorem or_imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b := -or_elim H1 - (assume H2 : c, or_inl H2) - (assume H2 : a, or_inr (H H2)) + theorem imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d := + elim H1 + (assume Ha : a, inl (H2 Ha)) + (assume Hb : b, inr (H3 Hb)) + + theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c := + elim H1 + (assume H2 : a, inl (H H2)) + (assume H2 : c, inr H2) + + theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b := + elim H1 + (assume H2 : c, inl H2) + (assume H2 : a, inr (H H2)) +end or theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) := assume not_em : ¬(p ∨ ¬p), have Hnp : ¬p, from - assume Hp : p, absurd (or_inl Hp) not_em, - absurd (or_inr Hnp) not_em + assume Hp : p, absurd (or.inl Hp) not_em, + absurd (or.inr Hnp) not_em -- iff -- --- - definition iff (a b : Prop) := (a → b) ∧ (b → a) + infix `<->` := iff infix `↔` := iff -theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl +namespace iff + theorem def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := + rfl -theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and.intro H1 H2 + theorem intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := + and.intro H1 H2 -theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and.rec H1 H2 + theorem elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := + and.rec H1 H2 -theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b := -iff_elim (assume H1 H2, H1) H + theorem elim_left {a b : Prop} (H : a ↔ b) : a → b := + elim (assume H1 H2, H1) H -abbreviation iff_mp := @iff_elim_left + abbreviation mp := @elim_left -theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a := -iff_elim (assume H1 H2, H2) H + theorem elim_right {a b : Prop} (H : a ↔ b) : b → a := + elim (assume H1 H2, H2) H -theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b := -iff_intro - (assume Hna, mt (iff_elim_right H1) Hna) - (assume Hnb, mt (iff_elim_left H1) Hnb) + theorem flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b := + intro + (assume Hna, mt (elim_right H1) Hna) + (assume Hnb, mt (elim_left H1) Hnb) -theorem iff_refl (a : Prop) : a ↔ a := -iff_intro (assume H, H) (assume H, H) + theorem refl (a : Prop) : a ↔ a := + intro (assume H, H) (assume H, H) -theorem iff_rfl {a : Prop} : a ↔ a := -iff_refl a + theorem rfl {a : Prop} : a ↔ a := + refl a -theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c := -iff_intro - (assume Ha, iff_elim_left H2 (iff_elim_left H1 Ha)) - (assume Hc, iff_elim_right H1 (iff_elim_right H2 Hc)) + theorem trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c := + intro + (assume Ha, elim_left H2 (elim_left H1 Ha)) + (assume Hc, elim_right H1 (elim_right H2 Hc)) -theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a := -iff_intro - (assume Hb, iff_elim_right H Hb) - (assume Ha, iff_elim_left H Ha) + theorem symm {a b : Prop} (H : a ↔ b) : b ↔ a := + intro + (assume Hb, elim_right H Hb) + (assume Ha, elim_left H Ha) -calc_refl iff_refl -calc_trans iff_trans + theorem true_elim {a : Prop} (H : a ↔ true) : a := + mp (symm H) trivial -theorem iff_true_elim {a : Prop} (H : a ↔ true) : a := -iff_mp (iff_symm H) trivial + theorem false_elim {a : Prop} (H : a ↔ false) : ¬a := + assume Ha : a, mp H Ha +end iff -theorem iff_false_elim {a : Prop} (H : a ↔ false) : ¬a := -assume Ha : a, iff_mp H Ha +calc_refl iff.refl +calc_trans iff.trans open eq_ops theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b := -iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) +iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb) -- comm and assoc for and / or -- --------------------------- -theorem and_comm {a b : Prop} : a ∧ b ↔ b ∧ a := -iff_intro (λH, and.swap H) (λH, and.swap H) +namespace and + theorem comm {a b : Prop} : a ∧ b ↔ b ∧ a := + iff.intro (λH, swap H) (λH, 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))) - (assume H, and.intro - (and.intro (and.elim_left H) (and.elim_left (and.elim_right H))) - (and.elim_right (and.elim_right H))) + theorem assoc {a b c : Prop} : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := + iff.intro + (assume H, intro + (elim_left (elim_left H)) + (intro (elim_right (elim_left H)) (elim_right H))) + (assume H, intro + (intro (elim_left H) (elim_left (elim_right H))) + (elim_right (elim_right H))) +end and -theorem or_comm {a b : Prop} : a ∨ b ↔ b ∨ a := -iff_intro (λH, or_swap H) (λH, or_swap H) +namespace or + theorem comm {a b : Prop} : a ∨ b ↔ b ∨ a := + iff.intro (λH, swap H) (λH, swap H) -theorem or_assoc {a b c : Prop} : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := -iff_intro - (assume H, or_elim H - (assume H1, or_elim H1 - (assume Ha, or_inl Ha) - (assume Hb, or_inr (or_inl Hb))) - (assume Hc, or_inr (or_inr Hc))) - (assume H, or_elim H - (assume Ha, (or_inl (or_inl Ha))) - (assume H1, or_elim H1 - (assume Hb, or_inl (or_inr Hb)) - (assume Hc, or_inr Hc))) + theorem assoc {a b c : Prop} : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := + iff.intro + (assume H, elim H + (assume H1, elim H1 + (assume Ha, inl Ha) + (assume Hb, inr (inl Hb))) + (assume Hc, inr (inr Hc))) + (assume H, elim H + (assume Ha, (inl (inl Ha))) + (assume H1, elim H1 + (assume Hb, inl (inr Hb)) + (assume Hc, inr Hc))) +end or diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean index 3faec157c..09c01ac7b 100644 --- a/library/logic/core/eq.lean +++ b/library/logic/core/eq.lean @@ -16,7 +16,7 @@ inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a infix `=` := eq -notation `rfl` := eq.refl _ +abbreviation rfl {A : Type} {a : A} := eq.refl a namespace eq theorem id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) := diff --git a/library/logic/core/identities.lean b/library/logic/core/identities.lean index 53e2198ab..c47e0ddf0 100644 --- a/library/logic/core/identities.lean +++ b/library/logic/core/identities.lean @@ -14,75 +14,75 @@ open relation decidable relation.iff_ops theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := calc - (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc - ... ↔ a ∨ (c ∨ b) : {or_comm} - ... ↔ (a ∨ c) ∨ b : iff_symm or_assoc + (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc + ... ↔ a ∨ (c ∨ b) : {or.comm} + ... ↔ (a ∨ c) ∨ b : iff.symm or.assoc theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) := calc - a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff_symm or_assoc - ... ↔ (b ∨ a) ∨ c : {or_comm} - ... ↔ b ∨ (a ∨ c) : or_assoc + a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff.symm or.assoc + ... ↔ (b ∨ a) ∨ c : {or.comm} + ... ↔ b ∨ (a ∨ c) : or.assoc theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b := calc - (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and_assoc - ... ↔ a ∧ (c ∧ b) : {and_comm} - ... ↔ (a ∧ c) ∧ b : iff_symm and_assoc + (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc + ... ↔ a ∧ (c ∧ b) : {and.comm} + ... ↔ (a ∧ c) ∧ b : iff.symm and.assoc theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) := calc - a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm and_assoc - ... ↔ (b ∧ a) ∧ c : {and_comm} - ... ↔ b ∧ (a ∧ c) : and_assoc + a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff.symm and.assoc + ... ↔ (b ∧ a) ∧ c : {and.comm} + ... ↔ b ∧ (a ∧ c) : and.assoc theorem not_not_iff {a : Prop} {D : decidable a} : (¬¬a) ↔ a := -iff_intro +iff.intro (assume H : ¬¬a, by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H)) (assume H : a, assume H', H' H) theorem not_not_elim {a : Prop} {D : decidable a} (H : ¬¬a) : a := -iff_mp not_not_iff H +iff.mp not_not_iff H theorem not_true : (¬true) ↔ false := -iff_intro (assume H, H trivial) false_elim +iff.intro (assume H, H trivial) false_elim theorem not_false : (¬false) ↔ true := -iff_intro (assume H, trivial) (assume H H', H') +iff.intro (assume H, trivial) (assume H H', H') theorem not_or {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) := -iff_intro - (assume H, or_elim (em a) - (assume Ha, absurd (or_inl Ha) H) - (assume Hna, or_elim (em b) - (assume Hb, absurd (or_inr Hb) H) +iff.intro + (assume H, or.elim (em a) + (assume Ha, absurd (or.inl Ha) H) + (assume Hna, or.elim (em b) + (assume Hb, absurd (or.inr Hb) H) (assume Hnb, and.intro Hna Hnb))) (assume (H : ¬a ∧ ¬b) (N : a ∨ b), - or_elim N + or.elim N (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 - (assume H, or_elim (em a) - (assume Ha, or_elim (em b) +iff.intro + (assume H, or.elim (em a) + (assume Ha, or.elim (em b) (assume Hb, absurd (and.intro Ha Hb) H) - (assume Hnb, or_inr Hnb)) - (assume Hna, or_inl Hna)) + (assume Hnb, or.inr Hnb)) + (assume Hna, or.inl Hna)) (assume (H : ¬a ∨ ¬b) (N : a ∧ b), - or_elim H + or.elim H (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 - (assume H : a → b, (or_elim (em a) - (assume Ha : a, or_inr (H Ha)) - (assume Hna : ¬a, or_inl Hna))) +iff.intro + (assume H : a → b, (or.elim (em a) + (assume Ha : a, or.inr (H Ha)) + (assume Hna : ¬a, or.inl Hna))) (assume (H : ¬a ∨ b) (Ha : a), - resolve_right H (not_not_iff⁻¹ ▸ Ha)) + or.resolve_right H (not_not_iff⁻¹ ▸ Ha)) theorem not_implies {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a → b)) ↔ (a ∧ ¬b) := calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or} @@ -97,7 +97,7 @@ assume H, by_contradiction (assume Hna : ¬a, theorem not_exists_forall {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)} (H : ¬∃x, P x) : ∀x, ¬P x := -- TODO: when type class instances can use quantifiers, we can use write em -take x, or_elim (@em _ (D x)) +take x, or.elim (@em _ (D x)) (assume Hp : P x, absurd (exists_intro x Hp) H) (assume Hn : ¬P x, Hn) @@ -110,17 +110,17 @@ theorem not_forall_exists {A : Type} {P : A → Prop} {D : ∀x, decidable (P x) absurd H3 H) theorem iff_true_intro {a : Prop} (H : a) : a ↔ true := -iff_intro +iff.intro (assume H1 : a, trivial) (assume H2 : true, H) theorem iff_false_intro {a : Prop} (H : ¬a) : a ↔ false := -iff_intro +iff.intro (assume H1 : a, absurd H1 H) (assume H2 : false, false_elim H2) theorem a_neq_a {A : Type} (a : A) : (a ≠ a) ↔ false := -iff_intro +iff.intro (assume H, a_neq_a_elim H) (assume H, false_elim H) @@ -131,7 +131,7 @@ theorem heq_id {A : Type} (a : A) : (a == a) ↔ true := iff_true_intro (hrefl a) theorem a_iff_not_a (a : Prop) : (a ↔ ¬a) ↔ false := -iff_intro +iff.intro (assume H, have H' : ¬a, from assume Ha, (H ▸ Ha) Ha, H' (H⁻¹ ▸ H')) @@ -144,7 +144,7 @@ theorem false_eq_true : (false ↔ true) ↔ false := not_false ▸ (a_iff_not_a false) theorem a_eq_true (a : Prop) : (a ↔ true) ↔ a := -iff_intro (assume H, iff_true_elim H) (assume H, iff_true_intro H) +iff.intro (assume H, iff.true_elim H) (assume H, iff_true_intro H) theorem a_eq_false (a : Prop) : (a ↔ false) ↔ ¬a := -iff_intro (assume H, iff_false_elim H) (assume H, iff_false_intro H) +iff.intro (assume H, iff.false_elim H) (assume H, iff_false_intro H) diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean index cfb188dd9..ce104db86 100644 --- a/library/logic/core/if.lean +++ b/library/logic/core/if.lean @@ -41,9 +41,9 @@ theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidab decidable.rec_on H₁ (assume Hc₁ : c₁, decidable.rec_on H₂ (assume Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹) - (assume Hnc₂ : ¬c₂, absurd (iff_elim_left Heq Hc₁) Hnc₂)) + (assume Hnc₂ : ¬c₂, absurd (iff.elim_left Heq Hc₁) Hnc₂)) (assume Hnc₁ : ¬c₁, decidable.rec_on H₂ - (assume Hc₂ : c₂, absurd (iff_elim_right Heq Hc₂) Hnc₁) + (assume Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁) (assume Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹)) theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A} diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean index f027bdf39..4267536f7 100644 --- a/library/logic/core/instances.lean +++ b/library/logic/core/instances.lean @@ -17,43 +17,43 @@ open relation theorem congruence_not : congruence iff iff not := congruence.mk (take a b, - assume H : a ↔ b, iff_intro - (assume H1 : ¬a, assume H2 : b, H1 (iff_elim_right H H2)) - (assume H1 : ¬b, assume H2 : a, H1 (iff_elim_left H H2))) + assume H : a ↔ b, iff.intro + (assume H1 : ¬a, assume H2 : b, H1 (iff.elim_right H H2)) + (assume H1 : ¬b, assume H2 : a, H1 (iff.elim_left H H2))) theorem congruence_and : congruence2 iff iff iff and := 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))) + 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))) theorem congruence_or : congruence2 iff iff iff or := congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff_intro - (assume H3 : a1 ∨ a2, or_imp_or H3 (iff_elim_left H1) (iff_elim_left H2)) - (assume H3 : b1 ∨ b2, or_imp_or H3 (iff_elim_right H1) (iff_elim_right H2))) + iff.intro + (assume H3 : a1 ∨ a2, or.imp_or H3 (iff.elim_left H1) (iff.elim_left H2)) + (assume H3 : b1 ∨ b2, or.imp_or H3 (iff.elim_right H1) (iff.elim_right H2))) theorem congruence_imp : congruence2 iff iff iff imp := congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff_intro - (assume H3 : a1 → a2, assume Hb1 : b1, iff_elim_left H2 (H3 ((iff_elim_right H1) Hb1))) - (assume H3 : b1 → b2, assume Ha1 : a1, iff_elim_right H2 (H3 ((iff_elim_left H1) Ha1)))) + iff.intro + (assume H3 : a1 → a2, assume Hb1 : b1, iff.elim_left H2 (H3 ((iff.elim_right H1) Hb1))) + (assume H3 : b1 → b2, assume Ha1 : a1, iff.elim_right H2 (H3 ((iff.elim_left H1) Ha1)))) theorem congruence_iff : congruence2 iff iff iff iff := congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, - iff_intro - (assume H3 : a1 ↔ a2, iff_trans (iff_symm H1) (iff_trans H3 H2)) - (assume H3 : b1 ↔ b2, iff_trans H1 (iff_trans H3 (iff_symm H2)))) + iff.intro + (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2)) + (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2)))) --- theorem congruence_const_iff [instance] := congruence.const iff iff_refl +-- theorem congruence_const_iff [instance] := congruence.const iff iff.refl definition congruence_not_compose [instance] := congruence.compose congruence_not definition congruence_and_compose [instance] := congruence.compose21 congruence_and definition congruence_or_compose [instance] := congruence.compose21 congruence_or @@ -69,7 +69,7 @@ definition congruence_iff_compose [instance] := congruence.compose21 congruence_ namespace general_operations theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ {C : congruence R iff P} - {a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (congruence.app C H) H1 + {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (congruence.app C H) H1 end general_operations @@ -94,43 +94,43 @@ relation.is_equivalence.mk _ _ _ -- ------------------------------ theorem is_reflexive_iff [instance] : relation.is_reflexive iff := -relation.is_reflexive.mk (@iff_refl) +relation.is_reflexive.mk (@iff.refl) theorem is_symmetric_iff [instance] : relation.is_symmetric iff := -relation.is_symmetric.mk (@iff_symm) +relation.is_symmetric.mk (@iff.symm) theorem is_transitive_iff [instance] : relation.is_transitive iff := -relation.is_transitive.mk (@iff_trans) +relation.is_transitive.mk (@iff.trans) -- Mp-like for iff -- --------------- theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : @relation.mp_like iff a b H := -relation.mp_like.mk (iff_elim_left H) +relation.mp_like.mk (iff.elim_left H) -- Substition for iff -- ------------------ - -theorem subst_iff {P : Prop → Prop} {C : congruence iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) : +namespace iff +theorem subst {P : Prop → Prop} {C : congruence iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) : P b := @general_operations.subst Prop iff P C a b H H1 - +end iff -- Support for calculations with iff -- ---------------- -calc_subst subst_iff +calc_subst iff.subst namespace iff_ops - postfix `⁻¹`:100 := iff_symm - infixr `⬝`:75 := iff_trans - infixr `▸`:75 := subst_iff - abbreviation refl := iff_refl - abbreviation symm := @iff_symm - abbreviation trans := @iff_trans - abbreviation subst := @subst_iff - abbreviation mp := @iff_mp + postfix `⁻¹`:100 := iff.symm + infixr `⬝`:75 := iff.trans + infixr `▸`:75 := iff.subst + abbreviation refl := iff.refl + abbreviation symm := @iff.symm + abbreviation trans := @iff.trans + abbreviation subst := @iff.subst + abbreviation mp := @iff.mp end iff_ops end relation diff --git a/library/logic/core/quantifiers.lean b/library/logic/core/quantifiers.lean index 5109cc316..e4fc8e03c 100644 --- a/library/logic/core/quantifiers.lean +++ b/library/logic/core/quantifiers.lean @@ -41,44 +41,44 @@ obtain w Hw, from H2, 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 - (assume Hl, take x, iff_elim_left (H x) (Hl x)) - (assume Hr, take x, iff_elim_right (H x) (Hr x)) +iff.intro + (assume Hl, take x, iff.elim_left (H x) (Hl x)) + (assume Hr, take x, iff.elim_right (H x) (Hr x)) theorem exists_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∃x, φ x) ↔ (∃x, ψ x) := -iff_intro +iff.intro (assume Hex, obtain w Pw, from Hex, - exists_intro w (iff_elim_left (H w) Pw)) + exists_intro w (iff.elim_left (H w) Pw)) (assume Hex, obtain w Qw, from Hex, - exists_intro w (iff_elim_right (H w) Qw)) + exists_intro w (iff.elim_right (H w) Qw)) theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true := -iff_intro (assume H, trivial) (assume H, take x, trivial) +iff.intro (assume H, trivial) (assume H, take x, trivial) theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p := -iff_intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr) +iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr) theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p := -iff_intro +iff.intro (assume Hl, obtain a Hp, from Hl, Hp) (assume Hr, inhabited.destruct H (take a, exists_intro a Hr)) theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) : (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) := -iff_intro +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)) theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) := -iff_intro +iff.intro (assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H, - or_elim Hw - (assume Hw1 : φ w, or_inl (exists_intro w Hw1)) - (assume Hw2 : ψ w, or_inr (exists_intro w Hw2))) - (assume H, or_elim H + or.elim Hw + (assume Hw1 : φ w, or.inl (exists_intro w Hw1)) + (assume Hw2 : ψ w, or.inr (exists_intro w Hw2))) + (assume H, or.elim H (assume H1, obtain (w : A) (Hw : φ w), from H1, - exists_intro w (or_inl Hw)) + exists_intro w (or.inl Hw)) (assume H2, obtain (w : A) (Hw : ψ w), from H2, - exists_intro w (or_inr Hw))) + exists_intro w (or.inr Hw))) theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := obtain w Hw, from H, nonempty.intro w diff --git a/library/logic/examples/nuprl_examples.lean b/library/logic/examples/nuprl_examples.lean index cddd9aabc..b10b70805 100644 --- a/library/logic/examples/nuprl_examples.lean +++ b/library/logic/examples/nuprl_examples.lean @@ -42,7 +42,7 @@ assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q), -- 4. Conjunction and Disjunction theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) := assume (em : P ∨ ¬P) (Hnn : ¬¬P), - or_elim em + or.elim em (assume Hp, Hp) (assume Hn, absurd Hn Hnn) @@ -50,32 +50,32 @@ theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) := assume Hnem : ¬(P ∨ ¬P), have Hnp : ¬P, from assume Hp : P, - have Hem : P ∨ ¬P, from or_inl Hp, + have Hem : P ∨ ¬P, from or.inl Hp, absurd Hem Hnem, - have Hem : P ∨ ¬P, from or_inr Hnp, + have Hem : P ∨ ¬P, from or.inr Hnp, absurd Hem Hnem theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q) := assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q), - or_elim H + or.elim H (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), - have Hnp : ¬P, from assume Hp : P, absurd (or_inl Hp) H, - have Hnq : ¬Q, from assume Hq : Q, absurd (or_inr Hq) H, + have Hnp : ¬P, from assume Hp : P, absurd (or.inl Hp) H, + have Hnq : ¬Q, from assume Hq : Q, absurd (or.inr Hq) H, and.intro Hnp Hnq theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) := assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q), - or_elim Hn + or.elim Hn (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), - or_elim Hor + or.elim Hor (assume Hnp : ¬P, absurd Hp Hnp) (assume Hq : Q, Hq) @@ -88,13 +88,13 @@ assume (Hpq : P → Q) (Hn : ¬(¬P ∨ Q)), 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) - (assume Hem1 : P ∨ ¬P, or_elim Hem1 - (assume Hp : P, or_inr (Hpq Hp)) - (assume Hnp : ¬P, or_inl Hnp)) - (assume Hem2 : Q ∨ ¬Q, or_elim Hem2 - (assume Hq : Q, or_inr Hq) - (assume Hnq : ¬Q, or_inl (mt Hpq Hnq))) + 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)) + (assume Hem2 : Q ∨ ¬Q, or.elim Hem2 + (assume Hq : Q, or.inr Hq) + (assume Hnq : ¬Q, or.inl (mt Hpq Hnq))) -- 5. First-Order Logic: All and Exists section @@ -122,7 +122,7 @@ assume (H1 : ∀x, P x → C) (H2 : ∃x, P x), theorem thm19a : (C ∨ ¬C) → (∃x : T, true) → (C → (∃x, P x)) → (∃x, C → P x) := assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x), - or_elim Hem + or.elim Hem (assume Hc : C, obtain (w : T) (Hw : P w), from H1 Hc, have Hr : C → P w, from assume Hc, Hw, @@ -139,7 +139,7 @@ assume (H : ∃x, C → P x) (Hc : C), theorem thm20a : (C ∨ ¬C) → (∃x : T, true) → ((¬∀x, P x) → ∃x, ¬P x) → ((∀x, P x) → C) → (∃x, P x → C) := assume Hem Hin Hnf H, - or_elim Hem + or.elim Hem (assume Hc : C, obtain (w : T) (Hw : true), from Hin, exists_intro w (assume H : P w, Hc)) @@ -156,37 +156,37 @@ assume Hex Hall, theorem thm21a : (∃x : T, true) → ((∃x, P x) ∨ C) → (∃x, P x ∨ C) := assume Hin H, - or_elim H + or.elim H (assume Hex : ∃x, P x, obtain (w : T) (Hw : P w), from Hex, - exists_intro w (or_inl Hw)) + exists_intro w (or.inl Hw)) (assume Hc : C, obtain (w : T) (Hw : true), from Hin, - exists_intro w (or_inr Hc)) + exists_intro w (or.inr Hc)) theorem thm21b : (∃x, P x ∨ C) → ((∃x, P x) ∨ C) := assume H, obtain (w : T) (Hw : P w ∨ C), from H, - or_elim Hw - (assume H : P w, or_inl (exists_intro w H)) - (assume Hc : C, or_inr Hc) + or.elim Hw + (assume H : P w, or.inl (exists_intro w H)) + (assume Hc : C, or.inr Hc) theorem thm22a : (∀x, P x) ∨ C → ∀x, P x ∨ C := assume H, take x, - or_elim H - (assume Hl, or_inl (Hl x)) - (assume Hr, or_inr Hr) + or.elim H + (assume Hl, or.inl (Hl x)) + (assume Hr, or.inr Hr) theorem thm22b : (C ∨ ¬C) → (∀x, P x ∨ C) → ((∀x, P x) ∨ C) := assume Hem H1, - or_elim Hem - (assume Hc : C, or_inr Hc) + or.elim Hem + (assume Hc : C, or.inr Hc) (assume Hnc : ¬C, have Hx : ∀x, P x, from take x, have H1 : P x ∨ C, from H1 x, - resolve_left H1 Hnc, - or_inl Hx) + or.resolve_left H1 Hnc, + or.inl Hx) theorem thm23a : (∃x, P x) ∧ C → (∃x, P x ∧ C) := assume H, diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index d6e1d0273..554a85b4d 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -22,9 +22,9 @@ static std::string g_resolve_opcode("Res"); static expr g_or(Const("or")); static expr g_not(Const("not")); static expr g_false(Const("false")); -static expr g_or_elim(Const("or_elim")); -static expr g_or_intro_left(Const("or_intro_left")); -static expr g_or_intro_right(Const("or_intro_right")); +static expr g_or_elim(Const(name("or", "elim"))); +static expr g_or_intro_left(Const(name("or", "intro_left"))); +static expr g_or_intro_right(Const(name("or", "intro_right"))); static expr g_absurd_elim(Const("absurd_elim")); static expr g_var_0(mk_var(0)); /** @@ -46,7 +46,7 @@ static expr g_var_0(mk_var(0)); It also assumes that the symbol 'or' is opaque. 'not' and 'false' do not need to be opaque. The macro can be expanded into a term built using - or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c + or.elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c or_intro_left {a : Prop} (H : a) (b : Prop) : a ∨ b or_intro_right {b : Prop} (a : Prop) (H : b) : a ∨ b absurd_elim {a : Prop} (b : Prop) (H1 : a) (H2 : ¬ a) : b diff --git a/tests/lean/interactive/in4.input.expected.out b/tests/lean/interactive/in4.input.expected.out index e0ab2f797..336d7eefa 100644 --- a/tests/lean/interactive/in4.input.expected.out +++ b/tests/lean/interactive/in4.input.expected.out @@ -1,8 +1,8 @@ -- BEGININFO -- TYPE|9|0 -∀ (a : A), eq a a +eq (tst.foo a b) (tst.foo a b) -- ACK --- SYMBOL|9|0 +-- IDENTIFIER|9|0 rfl -- ACK -- ENDINFO @@ -13,9 +13,9 @@ rfl -- ENDINFO -- BEGININFO -- TYPE|9|0 -∀ (a : A), eq a a +eq (tst.foo a b) (tst.foo a b) -- ACK --- SYMBOL|9|0 +-- IDENTIFIER|9|0 rfl -- ACK -- ENDINFO diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index e65640b49..56116b48a 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -34,14 +34,14 @@ theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n) m theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero -:= or_elim (dichotomy x) +:= or.elim (dichotomy x) (assume Hz : x = zero, Hz) (assume Hs : (∃ n, x = succ n), exists_elim Hs (λ (w : nat) (Hw : x = succ w), absurd H (eq.subst (symm Hw) (not_is_zero_succ w)))) theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n -:= or_elim (dichotomy x) +:= or.elim (dichotomy x) (assume Hz : x = zero, absurd (eq.subst (symm Hz) is_zero_zero) H) (assume Hs, Hs) diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index 8f4072230..bde9bdd5b 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -39,7 +39,7 @@ take T1 R1 c, congruence.mk (take x y H1, H c) -- congruences for logic theorem congr_const_iff [instance] (T1 : Type) (R1 : T1 → T1 → Prop) (c : Prop) : - congruence R1 iff (const T1 c) := congr_const iff iff_refl T1 R1 c + congruence R1 iff (const T1 c) := congr_const iff iff.refl T1 R1 c theorem congr_or [instance] (T : Type) (R : T → T → Prop) (f1 f2 : T → Prop) (H1 : congruence R iff f1) (H2 : congruence R iff f2) : @@ -60,7 +60,7 @@ theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop) theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congruence R iff P} {a b : T} (H : R a b) (H1 : P a) : P b := -- iff_mp_left (congruence.rec id C a b H) H1 -iff_elim_left (@congr_app _ _ R iff P C a b H) H1 +iff.elim_left (@congr_app _ _ R iff P C a b H) H1 theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) := subst_iff H1 H2 diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean index 8a365d090..9221b8162 100644 --- a/tests/lean/run/rel.lean +++ b/tests/lean/run/rel.lean @@ -2,7 +2,6 @@ import logic struc.relation open relation namespace is_equivalence - inductive cls {T : Type} (R : T → T → Type) : Prop := mk : is_reflexive R → is_symmetric R → is_transitive R → cls R @@ -22,16 +21,16 @@ 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 +iff.subst H1 H2 theorem test2 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : Q ↔ (S ∧ Q) := -iff_symm (and_inhabited_left Q H1) +iff.symm (and_inhabited_left Q H1) theorem test3 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) := -subst_iff (test2 Q R S H3 H1) H3 +iff.subst (test2 Q R S H3 H1) H3 theorem test4 (Q R S : Prop) (H3 : R ↔ Q) (H1 : S) : R ↔ (S ∧ Q) := -subst_iff (iff_symm (and_inhabited_left Q H1)) H3 +iff.subst (iff.symm (and_inhabited_left Q H1)) H3 diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index 8dd6c8a2a..f8caa84ab 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -57,14 +57,14 @@ rec_on s1 (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) (take b2, have H3 : (inl B a1 = inr A b2) ↔ false, - from iff_intro inl_neq_inr (assume H4, false_elim H4), - show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3))) + from iff.intro inl_neq_inr (assume H4, false_elim H4), + show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3))) (take b1, show decidable (inr A b1 = s2), from rec_on s2 (take a2, have H3 : (inr A b1 = inl B a2) ↔ false, - from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim H4), - show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3)) + from iff.intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim H4), + show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3)) (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) end sum diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean index 4724467e8..061d6be3b 100644 --- a/tests/lean/run/tactic10.lean +++ b/tests/lean/run/tactic10.lean @@ -2,8 +2,8 @@ import logic open tactic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a -:= by apply iff_intro; - apply (assume Hb, iff_elim_right H Hb); - apply (assume Ha, iff_elim_left H Ha) +:= by apply iff.intro; + apply (assume Hb, iff.elim_right H Hb); + apply (assume Ha, iff.elim_left H Ha) check tst diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index e7ec0b014..8b41c6e41 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -3,7 +3,7 @@ open tactic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := have H1 [fact] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics - from iff_elim_left H, - by apply iff_intro; - apply (assume Hb, iff_elim_right H Hb); + from iff.elim_left H, + by apply iff.intro; + apply (assume Hb, iff.elim_right H Hb); apply (assume Ha, H1 Ha) diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index 1728c6481..7798f0684 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -5,7 +5,7 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := by apply and.intro; apply not_intro; exact - (assume Ha, or_elim H + (assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) (assume Hnb, @absurd _ false Hb Hnb)); assumption diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index 7a8c5d816..34bbd1f10 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -5,7 +5,7 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin apply and.intro, apply not_intro, - assume Ha, or_elim H + assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) (assume Hnb, @absurd _ false Hb Hnb), assumption diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index 08058a12b..dd52822cf 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -8,7 +8,7 @@ set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each ele theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin - assume Ha, or_elim H + assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) (assume Hnb, @absurd _ false Hb Hnb) end diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index 325afacc7..5de70078a 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -66,13 +66,13 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) (show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹))) theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k -:= or_imp_or (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H) +:= or.imp_or (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H) theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n := induction_on n H1 (take m IH, H2 m) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B -:= or_elim (zero_or_succ n) +:= or.elim (zero_or_succ n) (take H3 : n = 0, H1 H3) (take H3 : n = succ (pred n), H2 (pred n) H3) @@ -508,10 +508,10 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m or_intro_left _ Hlt) theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= resolve_left (succ_le_left_or H1) H2 +:= or.resolve_left (succ_le_left_or H1) H2 theorem succ_le_right_inv {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_imp_or (succ_le_left_or H) +:= or.imp_or (succ_le_left_or H) (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) (take H2 : n = succ m, H2) @@ -567,7 +567,7 @@ theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m have H3 : k ≤ m, from subst H2 H, have H4 : succ k ≤ m ∨ k = m, from succ_le_left_or H3, show n ≤ m ∨ n = succ m, from - or_imp_or H4 + or.imp_or H4 (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) (take H5 : k = m, show n = succ m, from subst H5 Hn)) @@ -595,7 +595,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m or_intro_left _ Hlt) theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= resolve_left (le_imp_succ_le_or_eq H1) H2 +:= or.resolve_left (le_imp_succ_le_or_eq H1) H2 theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m := @@ -626,7 +626,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su have H3 : k ≤ m, from subst H2 H, have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, show n ≤ m ∨ n = succ m, from - or_imp_or H4 + or.imp_or H4 (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) (take H5 : k = m, show n = succ m, from subst H5 Hn)) @@ -789,7 +789,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n (or_intro_left _ (zero_le m)) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, - or_elim IH + or.elim IH (assume H : k ≤ m, obtain (l : ℕ) (Hl : k + l = m), from le_elim H, discriminate @@ -812,13 +812,13 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n (assume H : m < k, or_intro_right _ (succ_lt_right H))) theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n -:= or_imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) +:= or.imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ m < n -:= iff_elim_left or_assoc (trichotomy_alt n m) +:= iff.elim_left or.assoc (trichotomy_alt n m) theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n -:= or_imp_or (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) +:= or.imp_or (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) -- interaction with mul under "positivity" @@ -838,7 +838,7 @@ theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < assume IHl : ∀k, k ≤ l → P k, take k : ℕ, assume H : k ≤ succ l, - or_elim (succ_le_right_inv H) + or.elim (succ_le_right_inv H) (assume H2 : k ≤ l, show P k, from IHl k H2) (assume H2 : k = succ l, have H3 : ∀m, m < k → P m, from @@ -877,13 +877,13 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0 ---------- basic theorem zero_or_positive (n : ℕ) : n = 0 ∨ n > 0 -:= or_imp_or (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) +:= or.imp_or (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0 := subst (symm H) (lt_zero m) theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0 -:= or_elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) +:= or.elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l := discriminate @@ -960,7 +960,7 @@ theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k n * m = n * 0 : H ... = 0 : mul_zero_right n, have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - resolve_right H3 (ne.symm (lt_ne Hn))) + or.resolve_right H3 (ne.symm (lt_ne Hn))) (take (l : ℕ), assume (IH : ∀ m, n * m = n * l → m = l), take (m : ℕ), @@ -1051,7 +1051,7 @@ theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 have H2 : n * m > 0, from subst (symm H) (lt_zero 0), have H3 : n > 0, from mul_positive_inv_left H2, have H4 : m > 0, from mul_positive_inv_right H2, - or_elim (le_or_lt n 1) + or.elim (le_or_lt n 1) (assume H5 : n ≤ 1, show n = 1, from le_antisym H5 H3) (assume H5 : n > 1, @@ -1258,18 +1258,18 @@ theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := subst (add_comm m (n - m)) add_sub_ge theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H : n ≤ m, subst (symm (add_sub_le H)) H) (assume H : m ≤ n, subst (symm (add_sub_ge H)) (le_refl n)) theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m)) (assume H : m ≤ n, subst (symm (add_sub_ge H)) H) theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) : P (n - m) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3)) (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) @@ -1317,7 +1317,7 @@ theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H3 : n ≤ m, le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) (assume H3 : m ≤ n, diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index ac8153428..5823e1dc5 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -61,13 +61,13 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) (show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹))) theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k -:= or_imp_or (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H) +:= or.imp_or (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H) theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n := induction_on n H1 (take m IH, H2 m) theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B -:= or_elim (zero_or_succ n) +:= or.elim (zero_or_succ n) (take H3 : n = 0, H1 H3) (take H3 : n = succ (pred n), H2 (pred n) H3) @@ -503,10 +503,10 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m or.intro_left _ Hlt) theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= resolve_left (succ_le_left_or H1) H2 +:= or.resolve_left (succ_le_left_or H1) H2 theorem succ_le_right_inv {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_imp_or (succ_le_left_or H) +:= or.imp_or (succ_le_left_or H) (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) (take H2 : n = succ m, H2) @@ -562,7 +562,7 @@ theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m have H3 : k ≤ m, from subst H2 H, have H4 : succ k ≤ m ∨ k = m, from succ_le_left_or H3, show n ≤ m ∨ n = succ m, from - or_imp_or H4 + or.imp_or H4 (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) (take H5 : k = m, show n = succ m, from subst H5 Hn)) @@ -590,10 +590,10 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m or.intro_left _ Hlt) theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m -:= resolve_left (le_imp_succ_le_or_eq H1) H2 +:= or.resolve_left (le_imp_succ_le_or_eq H1) H2 theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m -:= or_imp_or_left (le_imp_succ_le_or_eq H) +:= or.imp_or_left (le_imp_succ_le_or_eq H) (take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2) theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m @@ -625,7 +625,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su have H3 : k ≤ m, from subst H2 H, have H4 : succ k ≤ m ∨ k = m, from le_imp_succ_le_or_eq H3, show n ≤ m ∨ n = succ m, from - or_imp_or H4 + or.imp_or H4 (take H5 : succ k ≤ m, show n ≤ m, from subst (symm Hn) H5) (take H5 : k = m, show n = succ m, from subst H5 Hn)) @@ -788,7 +788,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n (or.intro_left _ (zero_le m)) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, - or_elim IH + or.elim IH (assume H : k ≤ m, obtain (l : ℕ) (Hl : k + l = m), from le_elim H, discriminate @@ -811,13 +811,13 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n (assume H : m < k, or.intro_right _ (succ_lt_right H))) theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n -:= or_imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) +:= or.imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) theorem trichotomy (n m : ℕ) : n < m ∨ n = m ∨ m < n -:= iff_elim_left or_assoc (trichotomy_alt n m) +:= iff.elim_left or.assoc (trichotomy_alt n m) theorem le_total (n m : ℕ) : n ≤ m ∨ m ≤ n -:= or_imp_or (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) +:= or.imp_or (le_or_lt n m) (assume H : n ≤ m, H) (assume H : m < n, lt_imp_le H) -- interaction with mul under "positivity" @@ -837,7 +837,7 @@ theorem strong_induction_on {P : ℕ → Prop} (n : ℕ) (IH : ∀n, (∀m, m < assume IHl : ∀k, k ≤ l → P k, take k : ℕ, assume H : k ≤ succ l, - or_elim (succ_le_right_inv H) + or.elim (succ_le_right_inv H) (assume H2 : k ≤ l, show P k, from IHl k H2) (assume H2 : k = succ l, have H3 : ∀m, m < k → P m, from @@ -876,13 +876,13 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0 ---------- basic theorem zero_or_positive (n : ℕ) : n = 0 ∨ n > 0 -:= or_imp_or (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) +:= or.imp_or (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) (take H : n > 0, H) theorem succ_positive {n m : ℕ} (H : n = succ m) : n > 0 := subst (symm H) (lt_zero m) theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0 -:= or_elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) +:= or.elim (zero_or_positive n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l := discriminate @@ -913,13 +913,13 @@ theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 := case y H0 (take y', H1 _ (succ_pos _)) theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0 -:= or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) +:= or.imp_or_left (or.swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H) theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 := subst (symm H) (succ_pos m) theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 -:= or_elim (zero_or_pos n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) +:= or.elim (zero_or_pos n) (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2) theorem add_pos_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n := subst (add_zero_right n) (add_lt_left H n) @@ -965,7 +965,7 @@ theorem mul_left_inj {n m k : ℕ} (Hn : n > 0) (H : n * m = n * k) : m = k n * m = n * 0 : H ... = 0 : mul_zero_right n, have H3 : n = 0 ∨ m = 0, from mul_eq_zero H2, - resolve_right H3 (ne.symm (lt_ne Hn))) + or.resolve_right H3 (ne.symm (lt_ne Hn))) (take (l : ℕ), assume (IH : ∀ m, n * m = n * l → m = l), take (m : ℕ), @@ -1056,7 +1056,7 @@ theorem mul_eq_one_left {n m : ℕ} (H : n * m = 1) : n = 1 have H2 : n * m > 0, from subst (symm H) (lt_zero 0), have H3 : n > 0, from mul_positive_inv_left H2, have H4 : m > 0, from mul_positive_inv_right H2, - or_elim (le_or_lt n 1) + or.elim (le_or_lt n 1) (assume H5 : n ≤ 1, show n = 1, from le_antisym H5 H3) (assume H5 : n > 1, @@ -1263,18 +1263,18 @@ theorem add_sub_le_left {n m : ℕ} : n ≤ m → n - m + m = m := subst (add_comm m (n - m)) add_sub_ge theorem le_add_sub_left (n m : ℕ) : n ≤ n + (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H : n ≤ m, subst (symm (add_sub_le H)) H) (assume H : m ≤ n, subst (symm (add_sub_ge H)) (le_refl n)) theorem le_add_sub_right (n m : ℕ) : m ≤ n + (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H : n ≤ m, subst (symm (add_sub_le H)) (le_refl m)) (assume H : m ≤ n, subst (symm (add_sub_ge H)) H) theorem sub_split {P : ℕ → Prop} {n m : ℕ} (H1 : n ≤ m → P 0) (H2 : ∀k, m + k = n -> P k) : P (n - m) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H3 : n ≤ m, subst (symm (le_imp_sub_eq_zero H3)) (H1 H3)) (assume H3 : m ≤ n, H2 (n - m) (add_sub_le H3)) @@ -1322,7 +1322,7 @@ theorem sub_eq_zero_imp_le {n m : ℕ} : n - m = 0 → n ≤ m theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + k -> P k 0) (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) -:= or_elim (le_total n m) +:= or.elim (le_total n m) (assume H3 : n ≤ m, le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) (assume H3 : m ≤ n, diff --git a/tests/lua/res1.lua b/tests/lua/res1.lua index 4aea6a4f0..8e9d15299 100644 --- a/tests/lua/res1.lua +++ b/tests/lua/res1.lua @@ -14,9 +14,9 @@ function init_env(env) env = add_decl(env, mk_var_decl("or", mk_arrow(Prop, Prop, Prop))) env = add_decl(env, mk_var_decl("not", mk_arrow(Prop, Prop))) env = add_decl(env, mk_var_decl("false", Prop)) - env = add_decl(env, mk_axiom("or_elim", Pi(a, b, c, mk_arrow(Or(a, b), mk_arrow(a, c), mk_arrow(b, c), c)))) - env = add_decl(env, mk_axiom("or_intro_left", Pi(a, Ha, b, Or(a, b)))) - env = add_decl(env, mk_axiom("or_intro_right", Pi(b, a, Hb, Or(a, b)))) + env = add_decl(env, mk_axiom({"or", "elim"}, Pi(a, b, c, mk_arrow(Or(a, b), mk_arrow(a, c), mk_arrow(b, c), c)))) + env = add_decl(env, mk_axiom({"or", "intro_left"}, Pi(a, Ha, b, Or(a, b)))) + env = add_decl(env, mk_axiom({"or", "intro_right"}, Pi(b, a, Hb, Or(a, b)))) env = add_decl(env, mk_axiom("absurd_elim", Pi(a, b, mk_arrow(a, Not(a), b)))) return env end @@ -132,5 +132,3 @@ local a = Const("a") assert(not pcall(function() a:macro_num_args() end)) assert(not pcall(function() a:let_name() end)) assert(not pcall(function() mk_arrow(a) end)) - -