From d536475e493d66b004daedbc6de51ffd6296bd15 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Aug 2014 11:10:04 -0700 Subject: [PATCH] refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg Signed-off-by: Leonardo de Moura --- library/data/int/basic.lean | 8 ++-- library/data/int/order.lean | 16 +++---- library/data/list/basic.lean | 10 ++--- library/data/nat/basic.lean | 8 ++-- library/data/nat/div.lean | 60 +++++++++++++-------------- library/data/nat/order.lean | 10 ++--- library/data/nat/sub.lean | 4 +- library/logic/core/connectives.lean | 9 ++-- library/logic/core/identities.lean | 24 +++++------ library/logic/core/if.lean | 12 +++--- tests/lean/run/occurs_check_bug1.lean | 2 +- tests/lean/slow/nat_wo_hints.lean | 2 +- 12 files changed, 82 insertions(+), 83 deletions(-) diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 91f8129393..22188740ad 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -71,11 +71,11 @@ definition proj (a : ℕ × ℕ) : ℕ × ℕ := if pr1 a ≥ pr2 a then pair (pr1 a - pr2 a) 0 else pair 0 (pr2 a - pr1 a) theorem proj_ge {a : ℕ × ℕ} (H : pr1 a ≥ pr2 a) : proj a = pair (pr1 a - pr2 a) 0 := -if_pos H _ _ +if_pos H theorem proj_lt {a : ℕ × ℕ} (H : pr1 a < pr2 a) : proj a = pair 0 (pr2 a - pr1 a) := have H2 : ¬ pr1 a ≥ pr2 a, from lt_imp_not_ge H, -if_neg H2 _ _ +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 @@ -344,7 +344,7 @@ or_elim (cases a) ---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_intro_left _ H) + (assume H : (∃n : ℕ, a = of_nat n), or_inl H) (assume H, obtain (n : ℕ) (H2 : a = -(of_nat n)), from H, discriminate @@ -354,7 +354,7 @@ or_elim (cases a) a = -(of_nat n) : H2 ... = -(of_nat 0) : {H3} ... = of_nat 0 : neg_zero, - or_intro_left _ (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 subst H3 H2, diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 1d862a2e84..33bc9999c1 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -12,7 +12,7 @@ import .basic using nat (hiding case) using decidable using fake_simplifier -using int +using int eq_ops namespace int @@ -121,7 +121,7 @@ discriminate a = a + 0 : symm (add_zero_right a) ... = a + n : {symm H2} ... = b : Hn, - or_intro_right _ 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_intro_left _ (le_intro H3)) + or_inl (le_intro H3)) -- ### interaction with neg and sub @@ -376,7 +376,7 @@ int_by_cases a int_by_cases_succ b (take m : ℕ, show -n ≤ m ∨ -n > m, from - or_intro_left _ (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 @@ -389,7 +389,7 @@ 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) 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) @@ -583,13 +583,13 @@ theorem or_elim3 {a b c d : Prop} (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → or_elim H Ha (assume H2,or_elim H2 Hb Hc) theorem sign_pos {a : ℤ} (H : a > 0) : sign a = 1 := -if_pos H _ _ +if_pos H theorem sign_negative {a : ℤ} (H : a < 0) : sign a = - 1 := -trans (if_neg (lt_antisym H) _ _) (if_pos H _ _) +if_neg (lt_antisym H) ⬝ if_pos H theorem sign_zero : sign 0 = 0 := -trans (if_neg (lt_irrefl 0) _ _) (if_neg (lt_irrefl 0) _ _) +if_neg (lt_irrefl 0) ⬝ if_neg (lt_irrefl 0) -- add_rewrite sign_negative sign_pos to_nat_negative to_nat_nonneg_eq sign_zero mul_to_nat diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index af7be38b8f..fa451558d9 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -197,13 +197,13 @@ theorem mem_nil (x : T) : x ∈ nil ↔ false := iff_refl _ theorem mem_cons (x : T) (y : T) (l : list T) : mem x (cons y l) ↔ (x = y ∨ mem x l) := iff_refl _ theorem mem_concat_imp_or (x : T) (s t : list T) : x ∈ s ++ t → x ∈ s ∨ x ∈ t := -list_induction_on s (or_intro_right _) +list_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) + iff_elim_right or_assoc H3) theorem mem_or_imp_concat (x : T) (s t : list T) : x ∈ s ∨ x ∈ t → x ∈ s ++ t := list_induction_on s @@ -214,9 +214,9 @@ list_induction_on s or_elim H (assume H1, or_elim H1 - (take H2 : x = y, or_intro_left _ H2) - (take H2 : x ∈ s, or_intro_right _ (IH (or_intro_left _ H2)))) - (assume H1 : x ∈ t, or_intro_right _ (IH (or_intro_right _ 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 _ _ _) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index f87814387b..fd1f1d212b 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -67,7 +67,7 @@ definition pred (n : ℕ) := nat_rec 0 (fun m x, m) n theorem pred_zero : pred 0 = 0 -theorem pred_succ (n : ℕ) : pred (succ n) = n +theorem pred_succ {n : ℕ} : pred (succ n) = n opaque_hint (hiding pred) @@ -75,7 +75,7 @@ theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n (or_inl (refl 0)) (take m IH, or_inr - (show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹))) + (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) @@ -91,9 +91,9 @@ or_elim (zero_or_succ_pred n) theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m := calc - n = pred (succ n) : pred_succ n⁻¹ + n = pred (succ n) : pred_succ⁻¹ ... = pred (succ m) : {H} - ... = m : pred_succ m + ... = m : pred_succ theorem succ_ne_self {n : ℕ} : succ n ≠ n := induction_on n diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index b8db3f007c..7ae7db7ec5 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -48,12 +48,12 @@ if measure x < m then f x else default theorem restrict_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom) (m : ℕ) (x : dom) (H : measure x < m) : restrict default measure f m x = f x := -if_pos H _ _ +if_pos H theorem restrict_not_lt_eq {dom codom : Type} (default : codom) (measure : dom → ℕ) (f : dom → codom) (m : ℕ) (x : dom) (H : ¬ measure x < m) : restrict default measure f m x = default := -if_neg H _ _ +if_neg H definition rec_measure_aux {dom codom : Type} (default : codom) (measure : dom → ℕ) (rec_val : dom → (dom → codom) → codom) : ℕ → dom → codom := @@ -81,7 +81,7 @@ case_strong_induction_on m funext (take x, have H3 [fact]: ¬ measure x < 0, from not_lt_zero, - show restrict default measure f 0 x = default, from if_neg H3 _ _), + show restrict default measure f 0 x = default, from if_neg H3), show f' 0 = restrict default measure f 0, from trans H1 (symm H2)) (take m, assume IH: ∀n, n ≤ m → f' n = restrict default measure f n, @@ -93,16 +93,16 @@ case_strong_induction_on m have H2 [fact] : f' (succ m) x = rec_val x f, from calc f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl - ... = rec_val x (f' m) : if_pos H1 _ _ + ... = rec_val x (f' m) : if_pos H1 ... = rec_val x (restrict default measure f m) : {IH m le_refl} ... = rec_val x f : symm (rec_decreasing _ _ _ (lt_succ_imp_le H1)), have H3 : restrict default measure f (succ m) x = rec_val x f, from let m' := measure x in calc - restrict default measure f (succ m) x = f x : if_pos H1 _ _ + restrict default measure f (succ m) x = f x : if_pos H1 ... = f' (succ m') x : refl _ ... = if measure x < succ m' then rec_val x (f' m') else default : rfl - ... = rec_val x (f' m') : if_pos self_lt_succ _ _ + ... = rec_val x (f' m') : if_pos self_lt_succ ... = rec_val x (restrict default measure f m') : {IH m' (lt_succ_imp_le H1)} ... = rec_val x f : (rec_decreasing _ _ _ le_refl)⁻¹, show f' (succ m) x = restrict default measure f (succ m) x, @@ -111,9 +111,9 @@ case_strong_induction_on m have H2 : f' (succ m) x = default, from calc f' (succ m) x = if measure x < succ m then rec_val x (f' m) else default : rfl - ... = default : if_neg H1 _ _, + ... = default : if_neg H1, have H3 : restrict default measure f (succ m) x = default, - from if_neg H1 _ _, + from if_neg H1, show f' (succ m) x = restrict default measure f (succ m) x, from trans H2 (symm H3)))) @@ -130,7 +130,7 @@ let m := measure x in calc f x = f' (succ m) x : rfl ... = if measure x < succ m then rec_val x (f' m) else default : rfl - ... = rec_val x (f' m) : if_pos self_lt_succ _ _ + ... = rec_val x (f' m) : if_pos self_lt_succ ... = rec_val x (restrict default measure f m) : {rec_measure_aux_spec _ _ _ rec_decreasing _} ... = rec_val x f : (rec_decreasing _ _ _ le_refl)⁻¹ @@ -154,8 +154,8 @@ show lhs = rhs, from by_cases -- (y = 0 ∨ x < y) (assume H1 : y = 0 ∨ x < y, calc - lhs = 0 : if_pos H1 _ _ - ... = rhs : symm (if_pos H1 _ _)) + lhs = 0 : if_pos H1 + ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), have H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1, have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2), @@ -163,9 +163,9 @@ show lhs = rhs, from have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, have H5 : x - y < m, from lt_le_trans H4 H, symm (calc - rhs = succ (restrict 0 (fun x, x) g m (x - y)) : if_neg H1 _ _ + rhs = succ (restrict 0 (fun x, x) g m (x - y)) : if_neg H1 ... = succ (g (x - y)) : {restrict_lt_eq _ _ _ _ _ H5} - ... = lhs : symm (if_neg H1 _ _))) + ... = lhs : (if_neg H1)⁻¹)) theorem div_aux_spec (y : ℕ) (x : ℕ) : div_aux y x = if (y = 0 ∨ x < y) then 0 else succ (div_aux y (x - y)) := @@ -176,12 +176,12 @@ definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x infixl `div` := idivide -- copied from Isabelle theorem div_zero {x : ℕ} : x div 0 = 0 := -trans (div_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _) +trans (div_aux_spec _ _) (if_pos (or_inl rfl)) -- add_rewrite div_zero theorem div_less {x y : ℕ} (H : x < y) : x div y = 0 := -trans (div_aux_spec _ _) (if_pos (or_intro_right _ H) _ _) +trans (div_aux_spec _ _) (if_pos (or_inr H)) -- add_rewrite div_less @@ -197,7 +197,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from or_elim H4 (assume H5 : y = 0, not_elim lt_irrefl (subst H5 H1)) (assume H5 : x < y, not_elim (lt_imp_not_ge H5) H2)), -trans (div_aux_spec _ _) (if_neg H3 _ _) +trans (div_aux_spec _ _) (if_neg H3) theorem div_add_self_right {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) := have H1 : z ≤ x + z, by simp, @@ -230,8 +230,8 @@ show lhs = rhs, from by_cases -- (y = 0 ∨ x < y) (assume H1 : y = 0 ∨ x < y, calc - lhs = x : if_pos H1 _ _ - ... = rhs : symm (if_pos H1 _ _)) + lhs = x : if_pos H1 + ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), have H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1, have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2), @@ -239,9 +239,9 @@ show lhs = rhs, from have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, have H5 : x - y < m, from lt_le_trans H4 H, symm (calc - rhs = restrict 0 (fun x, x) g m (x - y) : if_neg H1 _ _ + rhs = restrict 0 (fun x, x) g m (x - y) : if_neg H1 ... = g (x - y) : restrict_lt_eq _ _ _ _ _ H5 - ... = lhs : symm (if_neg H1 _ _))) + ... = lhs : (if_neg H1)⁻¹)) theorem mod_aux_spec (y : ℕ) (x : ℕ) : mod_aux y x = if (y = 0 ∨ x < y) then x else mod_aux y (x - y) := @@ -252,12 +252,12 @@ definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x infixl `mod` := modulo theorem mod_zero {x : ℕ} : x mod 0 = x := -trans (mod_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _) +trans (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 := -trans (mod_aux_spec _ _) (if_pos (or_intro_right _ H) _ _) +trans (mod_aux_spec _ _) (if_pos (or_inr H)) -- add_rewrite mod_lt_eq @@ -273,7 +273,7 @@ have H3 : ¬ (y = 0 ∨ x < y), from 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)), -trans (mod_aux_spec _ _) (if_neg H3 _ _) +(mod_aux_spec _ _) ⬝ (if_neg H3) -- need more of these, add as rewrite rules theorem mod_add_self_right {x z : ℕ} (H : z > 0) : (x + z) mod z = x mod z := @@ -598,17 +598,17 @@ show lhs = rhs, from by_cases -- (y = 0) (assume H1 : y = 0, calc - lhs = x : if_pos H1 _ _ - ... = rhs : (if_pos H1 _ _)⁻¹) + lhs = x : if_pos H1 + ... = rhs : (if_pos H1)⁻¹) (assume H1 : y ≠ 0, have ypos : y > 0, from ne_zero_imp_pos H1, have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _, have H3 : gcd_aux_measure p' < gcd_aux_measure p, from H2⁻¹ ▸ (mod_lt ypos), have H4: gcd_aux_measure p' < m, from lt_le_trans H3 H, symm (calc - rhs = restrict 0 gcd_aux_measure g m p' : if_neg H1 _ _ + rhs = restrict 0 gcd_aux_measure g m p' : if_neg H1 ... = g p' : restrict_lt_eq _ _ _ _ _ H4 - ... = lhs : (if_neg H1 _ _)⁻¹)) + ... = lhs : (if_neg H1)⁻¹)) theorem gcd_aux_spec (p : ℕ × ℕ) : gcd_aux p = let x := pr1 p, y := pr2 p in @@ -625,12 +625,12 @@ calc ... = if y = 0 then x else gcd y (x mod y) : rfl theorem gcd_zero (x : ℕ) : gcd x 0 = x := -(gcd_def x 0) ⬝ (if_pos rfl _ _) +(gcd_def x 0) ⬝ (if_pos rfl) -- add_rewrite gcd_zero theorem gcd_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m mod n) := -(gcd_def m n) ⬝ (if_neg (pos_imp_ne_zero H) _ _) +gcd_def m n ⬝ if_neg (pos_imp_ne_zero H) theorem gcd_zero_left (x : ℕ) : gcd 0 x = x := case x (by simp) (take x, (gcd_def _ _) ⬝ (by simp)) @@ -650,7 +650,7 @@ have aux : ∀m, P m n, from aux m theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := -gcd_def _ _ ⬝ if_neg succ_ne_zero _ _ +gcd_def _ _ ⬝ if_neg succ_ne_zero theorem gcd_one (n : ℕ) : gcd n 1 = 1 := sorry -- (by simp) (gcd_succ n 0) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 2ec64b470b..66a1ce0f10 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -173,7 +173,7 @@ obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H), theorem le_pred_self {n : ℕ} : pred n ≤ n := case n (pred_zero⁻¹ ▸ le_refl) - (take k : ℕ, (pred_succ k)⁻¹ ▸ self_le_succ) + (take k : ℕ, pred_succ⁻¹ ▸ self_le_succ) theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m := discriminate @@ -189,8 +189,8 @@ discriminate have H2 : pred n + l = pred m, from calc pred n + l = pred (succ k) + l : {Hn} - ... = k + l : {pred_succ k} - ... = pred (succ (k + l)) : (pred_succ (k + l))⁻¹ + ... = k + l : {pred_succ} + ... = pred (succ (k + l)) : pred_succ⁻¹ ... = pred (succ k + l) : {add_succ_left⁻¹} ... = pred (n + l) : {Hn⁻¹} ... = pred m : {Hl}, @@ -205,7 +205,7 @@ discriminate have H2 : pred n = k, from calc pred n = pred (succ k) : {Hn} - ... = k : pred_succ k, + ... = k : pred_succ, 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 @@ -412,7 +412,7 @@ 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) 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) diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 466f3534ae..a80aeef73c 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -43,7 +43,7 @@ induction_on m (calc succ n - 1 = pred (succ n - 0) : sub_succ_right ... = pred (succ n) : {sub_zero_right} - ... = n : pred_succ _ + ... = n : pred_succ ... = n - 0 : sub_zero_right⁻¹) (take k : nat, assume IH : succ n - succ k = n - k, @@ -139,7 +139,7 @@ induction_on n (take k : nat, assume IH : pred k * m = k * m - m, calc - pred (succ k) * m = k * m : {pred_succ _} + pred (succ k) * m = k * m : {pred_succ} ... = k * m + m - m : sub_add_left⁻¹ ... = succ k * m - m : {mul_succ_left⁻¹}) diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index b941ad5924..7800052252 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -4,7 +4,6 @@ import general_notation .eq - -- and -- --- @@ -145,10 +144,10 @@ iff_intro (λ Ha, subst H Ha) (λ Hb, subst (symm H) Hb) -- comm and assoc for and / or -- --------------------------- -theorem and_comm (a b : Prop) : a ∧ b ↔ b ∧ a := +theorem and_comm {a b : Prop} : a ∧ b ↔ b ∧ a := iff_intro (λH, and_swap H) (λH, and_swap H) -theorem and_assoc (a b c : Prop) : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := +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)) @@ -157,10 +156,10 @@ iff_intro (and_intro (and_elim_left H) (and_elim_left (and_elim_right H))) (and_elim_right (and_elim_right H))) -theorem or_comm (a b : Prop) : a ∨ b ↔ b ∨ a := +theorem or_comm {a b : Prop} : a ∨ b ↔ b ∨ a := iff_intro (λH, or_swap H) (λH, or_swap H) -theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) := +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 diff --git a/library/logic/core/identities.lean b/library/logic/core/identities.lean index e76336253c..2a8029e4d6 100644 --- a/library/logic/core/identities.lean +++ b/library/logic/core/identities.lean @@ -14,24 +14,24 @@ using relation 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 b c} - ... ↔ (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 a b} - ... ↔ 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 b c} - ... ↔ (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 a b} - ... ↔ 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 diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean index 9f770dc718..ce72ff1661 100644 --- a/library/logic/core/if.lean +++ b/library/logic/core/if.lean @@ -12,13 +12,13 @@ rec_on H (assume Hc, t) (assume Hnc, e) notation `if` c `then` t `else` e:45 := ite c t e -theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} (t e : A) : (if c then t else e) = t := +theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := decidable_rec (assume Hc : c, refl (@ite c (inl Hc) A t e)) (assume Hnc : ¬c, absurd Hc Hnc) H -theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} (t e : A) : (if c then t else e) = e := +theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e := decidable_rec (assume Hc : c, absurd Hc Hnc) (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e)) @@ -31,20 +31,20 @@ decidable_rec H theorem if_true {A : Type} (t e : A) : (if true then t else e) = t := -if_pos trivial t e +if_pos trivial theorem if_false {A : Type} (t e : A) : (if false then t else e) = e := -if_neg not_false_trivial t e +if_neg not_false_trivial theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} (Heq : c₁ ↔ c₂) {A : Type} (t e : A) : (if c₁ then t else e) = (if c₂ then t else e) := rec_on H₁ (assume Hc₁ : c₁, rec_on H₂ - (assume Hc₂ : c₂, (if_pos Hc₁ t e) ⬝ (if_pos Hc₂ t e)⁻¹) + (assume Hc₂ : c₂, if_pos Hc₁ ⬝ (if_pos Hc₂)⁻¹) (assume Hnc₂ : ¬c₂, absurd (iff_elim_left Heq Hc₁) Hnc₂)) (assume Hnc₁ : ¬c₁, rec_on H₂ (assume Hc₂ : c₂, absurd (iff_elim_right Heq Hc₂) Hnc₁) - (assume Hnc₂ : ¬c₂, (if_neg Hnc₁ t e) ⬝ (if_neg Hnc₂ t e)⁻¹)) + (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} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index 1dd8eb5cd8..83ba9654a4 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -14,4 +14,4 @@ theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (decidable_eq (pr2 (pair x sorry theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := -trans (gcd_def _ _) (if_neg succ_ne_zero _ _) +trans (gcd_def _ _) (if_neg succ_ne_zero) diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 18dcd8847d..056d58f5da 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -813,7 +813,7 @@ 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) 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)