From 7e0844a9e61eda7e3e187b3dce30cf7e98062277 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jul 2015 15:05:01 -0700 Subject: [PATCH] fix(tests): to reflect recent changes in the standard library --- doc/lean/tutorial.org | 6 +++++- tests/lean/550.lean | 2 +- tests/lean/interactive/alias.input.expected.out | 4 ++++ tests/lean/run/congr_imp_bug.lean | 1 - tests/lean/run/elab_bug1.lean | 2 +- tests/lean/run/fun.lean | 2 +- tests/lean/run/group3.lean | 2 +- tests/lean/run/group4.lean | 2 +- tests/lean/run/group5.lean | 2 +- tests/lean/run/injective_decidable.lean | 2 +- tests/lean/run/interp.lean | 1 - tests/lean/run/new_obtains.lean | 2 ++ tests/lean/run/parity.lean | 8 ++++++-- tests/lean/run/rewrite10.lean | 3 +++ tests/lean/tactic_id_bug.lean | 2 +- 15 files changed, 28 insertions(+), 13 deletions(-) diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 764595edd..690657d1a 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -753,6 +753,7 @@ of two even numbers is an even number. import data.nat open nat + namespace hide definition even (a : nat) := ∃ b, a = 2*b theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) := exists.elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1), @@ -761,7 +762,7 @@ of two even numbers is an even number. (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} ... = 2*(w1 + w2) : eq.symm !mul.left_distrib))) - + end hide #+END_SRC The example above also uses [[./calc.org][calculational proofs]] to show that =a + b = 2*(w1 + w2)=. @@ -773,6 +774,8 @@ With this macro we can write the example above in a more natural way #+BEGIN_SRC lean import data.nat open nat + + namespace hide definition even (a : nat) := ∃ b, a = 2*b theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) := obtain (w1 : nat) (Hw1 : a = 2*w1), from H1, @@ -781,4 +784,5 @@ With this macro we can write the example above in a more natural way (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} ... = 2*(w1 + w2) : eq.symm !mul.left_distrib) + end hide #+END_SRC diff --git a/tests/lean/550.lean b/tests/lean/550.lean index d0f159231..27c204396 100644 --- a/tests/lean/550.lean +++ b/tests/lean/550.lean @@ -1,4 +1,4 @@ -import algebra.function +-- open function diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out index 65e026a2d..40b110b43 100644 --- a/tests/lean/interactive/alias.input.expected.out +++ b/tests/lean/interactive/alias.input.expected.out @@ -6,6 +6,8 @@ bool.bor_tt|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a bool.tt|bool +bool.eq_tt_of_bnot_eq_ff|eq (bool.bnot ?a) bool.ff → eq ?a bool.tt +bool.eq_ff_of_bnot_eq_tt|eq (bool.bnot ?a) bool.tt → eq ?a bool.ff tactic.lettac|tactic.identifier → tactic.expr → tactic bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt @@ -23,6 +25,8 @@ tt_bor|∀ (a : bool), eq (bor tt a) tt tt_band|∀ (a : bool), eq (band tt a) a bor_tt|∀ (a : bool), eq (bor a tt) tt band_tt|∀ (a : bool), eq (band a tt) a +eq_tt_of_bnot_eq_ff|eq (bnot ?a) ff → eq ?a tt +eq_ff_of_bnot_eq_tt|eq (bnot ?a) tt → eq ?a ff tactic.lettac|tactic.identifier → tactic.expr → tactic absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B eq_tt_of_ne_ff|ne ?a ff → eq ?a tt diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean index 50ce6df7c..a9ec9ef30 100644 --- a/tests/lean/run/congr_imp_bug.lean +++ b/tests/lean/run/congr_imp_bug.lean @@ -3,7 +3,6 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad ---------------------------------------------------------------------------------------------------- -import algebra.function open function namespace congr diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index 9afb4341d..edca3f166 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -4,7 +4,7 @@ --- Author: Jeremy Avigad ---------------------------------------------------------------------------------------------------- -import logic algebra.function +import logic open eq open function diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean index d312505a7..bc27d5df6 100644 --- a/tests/lean/run/fun.lean +++ b/tests/lean/run/fun.lean @@ -1,4 +1,4 @@ -import logic algebra.function +import logic open function bool diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean index d8c3828aa..b5f3fb351 100644 --- a/tests/lean/run/group3.lean +++ b/tests/lean/run/group3.lean @@ -9,7 +9,7 @@ import logic.eq import data.unit data.sigma data.prod -import algebra.function algebra.binary +import algebra.binary open eq diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean index 3a0856e03..12cb77474 100644 --- a/tests/lean/run/group4.lean +++ b/tests/lean/run/group4.lean @@ -9,7 +9,7 @@ import logic.eq import data.unit data.sigma data.prod -import algebra.function algebra.binary +import algebra.binary open eq diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean index 9cb0f67c0..92788f18a 100644 --- a/tests/lean/run/group5.lean +++ b/tests/lean/run/group5.lean @@ -9,7 +9,7 @@ import logic.eq import data.unit data.sigma data.prod -import algebra.function algebra.binary +import algebra.binary open eq diff --git a/tests/lean/run/injective_decidable.lean b/tests/lean/run/injective_decidable.lean index 150497b18..79bad0970 100644 --- a/tests/lean/run/injective_decidable.lean +++ b/tests/lean/run/injective_decidable.lean @@ -1,4 +1,4 @@ -import data.fintype algebra.function +import data.fintype open function section test diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean index a5ddb61ed..aeecc41c5 100644 --- a/tests/lean/run/interp.lean +++ b/tests/lean/run/interp.lean @@ -1,4 +1,3 @@ -import algebra.function open bool nat open function diff --git a/tests/lean/run/new_obtains.lean b/tests/lean/run/new_obtains.lean index c35c3fc80..d7f7ac651 100644 --- a/tests/lean/run/new_obtains.lean +++ b/tests/lean/run/new_obtains.lean @@ -53,6 +53,7 @@ obtain x y [[pxy qxy] qyx], from ex, open nat +namespace hidden definition even (a : nat) := ∃ x, a = 2*x example (a b : nat) (H₁ : even a) (H₂ : even b) : even (a+b) := @@ -72,3 +73,4 @@ have aux : m * (c₁ - c₂) = n₂, from calc ... = n₁ + n₂ - n₁ : Hc₂ ... = n₂ : add_sub_cancel_left, dvd.intro aux +end hidden diff --git a/tests/lean/run/parity.lean b/tests/lean/run/parity.lean index 76fb68b17..c5664ea34 100644 --- a/tests/lean/run/parity.lean +++ b/tests/lean/run/parity.lean @@ -1,6 +1,8 @@ import data.nat open nat +namespace foo + inductive Parity : nat → Type := | even : ∀ n : nat, Parity (2 * n) | odd : ∀ n : nat, Parity (2 * n + 1) @@ -14,12 +16,12 @@ definition parity : Π (n : nat), Parity n have aux : Parity n, from parity n, cases aux with [k, k], begin - apply (odd k) + apply (Parity.odd k) end, begin change (Parity (2*k + 2*1)), rewrite -mul.left_distrib, - apply (even (k+1)) + apply (Parity.even (k+1)) end end @@ -30,3 +32,5 @@ match ⟨n, parity n⟩ with | ⟨⌞2 * k⌟, even k⟩ := k | ⟨⌞2 * k + 1⌟, odd k⟩ := k end + +end foo diff --git a/tests/lean/run/rewrite10.lean b/tests/lean/run/rewrite10.lean index a6b0e7028..5fa5f4268 100644 --- a/tests/lean/run/rewrite10.lean +++ b/tests/lean/run/rewrite10.lean @@ -11,6 +11,7 @@ end example (x y : ℕ) : (x + y) * (x + y) = x * x + y * x + x * y + y * y := by rewrite [*mul.left_distrib, *mul.right_distrib, -add.assoc] +namespace tst definition even (a : nat) := ∃b, a = 2*b theorem even_plus_even {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) := @@ -25,3 +26,5 @@ theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 := calc a = succ c : by rewrite [H1, H2, add_one] ... ≠ 0 : succ_ne_zero c + +end tst diff --git a/tests/lean/tactic_id_bug.lean b/tests/lean/tactic_id_bug.lean index 24180186c..a820d7b1e 100644 --- a/tests/lean/tactic_id_bug.lean +++ b/tests/lean/tactic_id_bug.lean @@ -1,4 +1,4 @@ -import algebra.function +-- open function