From 94519b48b15f6d62919257b676bed07e34cb51de Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Jan 2015 11:37:17 -0800 Subject: [PATCH] fix(tests/lean): adjust tests to reflect changes in the standard library --- tests/lean/interactive/eq2.lean | 72 ++++++------------------------- tests/lean/run/nat_bug3.lean | 2 +- tests/lean/slow/nat_bug2.lean | 14 +++--- tests/lean/slow/nat_wo_hints.lean | 14 +++--- 4 files changed, 27 insertions(+), 75 deletions(-) diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean index 2e6b672b8..5000440e9 100644 --- a/tests/lean/interactive/eq2.lean +++ b/tests/lean/interactive/eq2.lean @@ -6,16 +6,15 @@ -- ==================== -- Equality. - -import logic.prop - +prelude +definition Prop := Type.{0} -- eq -- -- inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a -infix `=` := eq +infix `=`:50 := eq definition rfl {A : Type} {a : A} := eq.refl a -- proof irrelevance is built in @@ -43,9 +42,9 @@ calc_refl eq.refl calc_trans eq.trans namespace eq_ops - postfix `⁻¹` := eq.symm - reserve infixr `⬝`:75 infixr `⬝` := eq.trans - infixr `▸` := eq.subst + postfix `⁻¹`:1024 := eq.symm + infixr `⬝`:75 := eq.trans + infixr `▸`:75 := eq.subst end eq_ops open eq_ops @@ -77,7 +76,7 @@ namespace eq (u : P a) : drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u := (show ∀(H2 : b = c), drec_on H2 (drec_on H1 u) = drec_on (trans H1 H2) u, - from drec_on H2 (take (H2 : b = b), drec_on_id H2 _)) + from drec_on H2 (fun (H2 : b = b), drec_on_id H2 _)) H2 end eq @@ -127,6 +126,7 @@ theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A} ... = f a₁ b₂ : {H₂}) b₂ H₁ H₂ + theorem congr_arg3_dep {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Type} {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (f : Πa b, C a b → D) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ := @@ -143,7 +143,7 @@ theorem congr_arg3_ndep_dep {A B : Type} {C : A → B → Type} {D : Type} {a₁ congr_arg3_dep f H₁ (drec_on_constant H₁ b₁ ⬝ H₂) H₃ theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := -take x, congr_fun H x +fun x, congr_fun H x theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b := H1 ▸ H2 @@ -151,59 +151,11 @@ H1 ▸ H2 theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a := H1⁻¹ ▸ H2 -theorem eq_true_elim {a : Prop} (H : a = true) : a := -H⁻¹ ▸ trivial - -theorem eq_false_elim {a : Prop} (H : a = false) : ¬a := -assume Ha : a, H ▸ Ha - theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c := -assume Ha, H2 (H1 Ha) +fun Ha, H2 (H1 Ha) theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c := -assume Ha, H2 ▸ (H1 Ha) +fun Ha, H2 ▸ (H1 Ha) theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c := -assume Ha, H2 (H1 ▸ Ha) - --- ne --- -- - -definition ne {A : Type} (a b : A) := ¬(a = b) -infix `≠` := ne - -namespace ne - theorem intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := - H - - theorem elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := - H1 H2 - - theorem irrefl {A : Type} {a : A} (H : a ≠ a) : false := - H rfl - - theorem symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a := - assume H1 : b = a, H (H1⁻¹) -end ne - -theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := -H rfl - -theorem eq_ne_trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := -H1⁻¹ ▸ H2 - -theorem ne_eq_trans {A : Type} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := -H2 ▸ H1 - -calc_trans eq_ne_trans -calc_trans ne_eq_trans - -theorem p_ne_false {p : Prop} (Hp : p) : p ≠ false := -assume Heq : p = false, Heq ▸ Hp - -theorem p_ne_true {p : Prop} (Hnp : ¬p) : p ≠ true := -assume Heq : p = true, absurd trivial (Heq ▸ Hnp) - -theorem true_ne_false : ¬true = false := -assume H : true = false, - H ▸ trivial +fun Ha, H2 (H1 ▸ Ha) diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean index 83b5b1540..d6da95388 100644 --- a/tests/lean/run/nat_bug3.lean +++ b/tests/lean/run/nat_bug3.lean @@ -20,7 +20,7 @@ axiom add_one (n:nat) : n + (succ zero) = succ n axiom add_le_right_inv {n m k : nat} (H : n + k ≤ m + k) : n ≤ m theorem succ_le_cancel {n m : nat} (H : succ n ≤ succ m) : n ≤ m -:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) +:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) end nat end experiment diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index 883f3b33a..3865ee2e8 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -57,7 +57,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n (or.intro_left _ (refl 0)) (take m IH, or.intro_right _ - (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 m)⁻¹))) theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k := or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) @@ -72,7 +72,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ 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 n)⁻¹ ... = pred (succ m) : {H} ... = m : pred_succ m @@ -473,7 +473,7 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := add_one m ▸ add_one n ▸ add_le_right H 1 theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m -:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) +:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) theorem self_le_succ (n : ℕ) : n ≤ succ n := le_intro (add_one n) @@ -757,7 +757,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l := add_lt_le H1 (lt_imp_le H2) theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m -:= add_le_left_inv (add_succ k n⁻¹ ▸ H) +:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H) theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m := add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H) @@ -768,7 +768,7 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m := add_one m ▸ add_one n ▸ add_lt_right H 1 theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m -:= add_lt_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) +:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) theorem lt_self_succ (n : ℕ) : n < succ n := le_refl (succ n) @@ -1313,9 +1313,9 @@ theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) := or.elim (le_total n m) (assume H3 : n ≤ m, - le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) + (le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹))) (assume H3 : m ≤ n, - le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹))) + (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹))) theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m := have H2 : k - n + n = m + n, from diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 07c200530..e4ea3f413 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -51,7 +51,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n (or.intro_left _ (eq.refl 0)) (take m IH, or.intro_right _ - (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 m)⁻¹))) theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k := or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H) @@ -66,7 +66,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ 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 n)⁻¹ ... = pred (succ m) : {H} ... = m : pred_succ m @@ -467,7 +467,7 @@ theorem succ_le {n m : ℕ} (H : n ≤ m) : succ n ≤ succ m := add_one m ▸ add_one n ▸ add_le_right H 1 theorem succ_le_cancel {n m : ℕ} (H : succ n ≤ succ m) : n ≤ m -:= add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) +:= add_le_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) theorem self_le_succ (n : ℕ) : n ≤ succ n := le_intro (add_one n) @@ -755,7 +755,7 @@ theorem add_lt {n m k l : ℕ} (H1 : n < k) (H2 : m < l) : n + m < k + l := add_lt_le H1 (lt_imp_le H2) theorem add_lt_left_inv {n m k : ℕ} (H : k + n < k + m) : n < m -:= add_le_left_inv (add_succ k n⁻¹ ▸ H) +:= add_le_left_inv ((add_succ k n)⁻¹ ▸ H) theorem add_lt_right_inv {n m k : ℕ} (H : n + k < m + k) : n < m := add_lt_left_inv (add_comm m k ▸ add_comm n k ▸ H) @@ -766,7 +766,7 @@ theorem succ_lt {n m : ℕ} (H : n < m) : succ n < succ m := add_one m ▸ add_one n ▸ add_lt_right H 1 theorem succ_lt_inv {n m : ℕ} (H : succ n < succ m) : n < m -:= add_lt_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) +:= add_lt_right_inv ((add_one m)⁻¹ ▸ (add_one n)⁻¹ ▸ H) theorem lt_self_succ (n : ℕ) : n < succ n := le_refl (succ n) @@ -1317,9 +1317,9 @@ theorem sub_sub_split {P : ℕ → ℕ → Prop} {n m : ℕ} (H1 : ∀k, n = m + (H2 : ∀k, m = n + k → P 0 k) : P (n - m) (m - n) := or.elim (le_total n m) (assume H3 : n ≤ m, - le_imp_sub_eq_zero H3⁻¹ ▸ (H2 (m - n) (add_sub_le H3⁻¹))) + (le_imp_sub_eq_zero H3)⁻¹ ▸ (H2 (m - n) ((add_sub_le H3)⁻¹))) (assume H3 : m ≤ n, - le_imp_sub_eq_zero H3⁻¹ ▸ (H1 (n - m) (add_sub_le H3⁻¹))) + (le_imp_sub_eq_zero H3)⁻¹ ▸ (H1 (n - m) ((add_sub_le H3)⁻¹))) theorem sub_intro {n m k : ℕ} (H : n + m = k) : k - n = m := have H2 : k - n + n = m + n, from