From b36ce49f2b01291fd08fad04d5aba4ad0a09177d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2015 23:52:16 -0800
Subject: [PATCH] fix(tests,doc): adjust tests to changes in the standard
 library

---
 doc/lean/library_style.org                    | 15 ++------
 library/algebra/order.lean                    |  6 +--
 tests/lean/interactive/coe.lean               |  2 +-
 .../consume_args.input.expected.out           |  2 +-
 tests/lean/run/abs.lean                       |  3 +-
 tests/lean/run/blast_cc8.lean                 |  2 +-
 tests/lean/run/blast_ematch3.lean             |  3 +-
 tests/lean/run/blast_ematch6.lean             |  2 +-
 tests/lean/run/blast_ematch8.lean             |  3 +-
 tests/lean/run/constr_tac4.lean               |  3 +-
 tests/lean/run/local_ctx_bug.lean             |  2 +-
 tests/lean/run/print_inductive.lean           |  2 +-
 tests/lean/run/rewrite5.lean                  |  3 +-
 tests/lean/run/struct_infer.lean              |  3 +-
 tests/lean/simplifier12.lean                  |  2 +-
 tests/lean/simplifier14.lean                  |  3 +-
 tests/lean/simplifier15.lean                  |  2 +-
 tests/lean/simplifier15.lean.expected.out     | 37 +++++++++----------
 tests/lean/simplifier18.lean                  |  2 +-
 tests/lean/simplifier19.lean                  |  2 +-
 tests/lean/simplifier_norm_num.lean           |  1 -
 21 files changed, 47 insertions(+), 53 deletions(-)

diff --git a/doc/lean/library_style.org b/doc/lean/library_style.org
index b4811ed7b..1acf49001 100644
--- a/doc/lean/library_style.org
+++ b/doc/lean/library_style.org
@@ -20,19 +20,17 @@ multiplication are put in a namespace that begins with the name of the
 operation:
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
 
 check and.comm
 check mul.comm
 check and.assoc
 check mul.assoc
-check @algebra.mul.left_cancel  -- multiplication is left cancelative
+check @mul.left_cancel  -- multiplication is left cancelative
 #+END_SRC
 In particular, this includes =intro= and =elim= operations for logical
 connectives, and properties of relations:
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
 
 check and.intro
 check and.elim
@@ -49,8 +47,7 @@ For the most part, however, we rely on descriptive names. Often the
 name of theorem simply describes the conclusion:
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
-
+open nat
 check succ_ne_zero
 check mul_zero
 check mul_one
@@ -61,7 +58,6 @@ If only a prefix of the description is enough to convey the meaning,
 the name may be made even shorter:
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
 
 check @neg_neg
 check nat.pred_succ
@@ -75,8 +71,7 @@ intended reference, it is necessary to describe some of the
 hypotheses. The word "of" is used to separate these hypotheses:
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
-
+open nat
 check lt_of_succ_le
 check lt_of_not_ge
 check lt_of_le_of_ne
@@ -87,8 +82,7 @@ with. For example, we use =pos=, =neg=, =nonpos=, =nonneg= rather than
 =zero_lt=, =lt_zero=, =le_zero=, and =zero_le=.
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
-
+open nat
 check mul_pos
 check mul_nonpos_of_nonneg_of_nonpos
 check add_lt_of_lt_of_nonpos
@@ -105,7 +99,6 @@ Sometimes the word "left" or "right" is helpful to describe variants
 of a theorem.
 #+BEGIN_SRC lean
 import standard algebra.ordered_ring
-open nat algebra
 
 check add_le_add_left
 check add_le_add_right
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index f9f8e9d05..1e300c813 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -52,7 +52,7 @@ section
   theorem lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
   theorem not_lt_self (a : A) : ¬ a < a := !lt.irrefl   -- alternate syntax
 
-  theorem lt_self_iff_false [simp] (a : A) : a < a ↔ false :=
+  theorem lt_self_iff_false (a : A) : a < a ↔ false :=
   iff_false_intro (lt.irrefl a)
 
   theorem lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
@@ -333,10 +333,10 @@ section
     (assume H : a ≤ b, by rewrite [↑max, if_pos H]; apply H₂)
     (assume H : ¬ a ≤ b, by rewrite [↑max, if_neg H]; apply H₁)
 
-  theorem le_max_left_iff_true [simp] (a b : A) : a ≤ max a b ↔ true :=
+  theorem le_max_left_iff_true (a b : A) : a ≤ max a b ↔ true :=
   iff_true_intro (le_max_left a b)
 
-  theorem le_max_right_iff_true [simp] (a b : A) : b ≤ max a b ↔ true :=
+  theorem le_max_right_iff_true (a b : A) : b ≤ max a b ↔ true :=
   iff_true_intro (le_max_right a b)
 
   /- these are also proved for lattices, but with inf and sup in place of min and max -/
diff --git a/tests/lean/interactive/coe.lean b/tests/lean/interactive/coe.lean
index a305ab32d..d65992caf 100644
--- a/tests/lean/interactive/coe.lean
+++ b/tests/lean/interactive/coe.lean
@@ -1,7 +1,7 @@
 import data.int
 open int
 
-protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
+protected theorem has_decidable_eq₁ [instance] : decidable_eq ℤ :=
 take (a b : ℤ), _
 
 constant n : nat
diff --git a/tests/lean/interactive/consume_args.input.expected.out b/tests/lean/interactive/consume_args.input.expected.out
index 4b37e79ab..b1006903d 100644
--- a/tests/lean/interactive/consume_args.input.expected.out
+++ b/tests/lean/interactive/consume_args.input.expected.out
@@ -44,7 +44,7 @@ b
 a + c + b = a + (c + b)
 -- ACK
 -- IDENTIFIER|7|33
-algebra.add.assoc
+add.assoc
 -- ACK
 -- TYPE|7|43
 a + c + b = a + (c + b) → a + (c + b) = a + c + b
diff --git a/tests/lean/run/abs.lean b/tests/lean/run/abs.lean
index 209f5a47d..45f4f472e 100644
--- a/tests/lean/run/abs.lean
+++ b/tests/lean/run/abs.lean
@@ -1,7 +1,8 @@
 import data.int
 open int
-
+namespace foo
 constant abs : int → int
 notation `|` A `|` := abs A
 constants a b c : int
 check |a + |b| + c|
+end foo
diff --git a/tests/lean/run/blast_cc8.lean b/tests/lean/run/blast_cc8.lean
index 7e41d81a8..4cc0d2406 100644
--- a/tests/lean/run/blast_cc8.lean
+++ b/tests/lean/run/blast_cc8.lean
@@ -1,4 +1,4 @@
-import data.finset
+import data.finset data.set
 open set finset
 
 structure finite_set [class] {T : Type} (xs : set T) :=
diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean
index 25b7c897e..c337e523a 100644
--- a/tests/lean/run/blast_ematch3.lean
+++ b/tests/lean/run/blast_ematch3.lean
@@ -1,6 +1,6 @@
 import algebra.ring data.nat
-open algebra
 
+namespace foo
 variables {A : Type}
 
 section
@@ -36,3 +36,4 @@ set_option blast.ematch true
 theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
 by blast
 end
+end foo
diff --git a/tests/lean/run/blast_ematch6.lean b/tests/lean/run/blast_ematch6.lean
index 0ce360390..d1bb16f7a 100644
--- a/tests/lean/run/blast_ematch6.lean
+++ b/tests/lean/run/blast_ematch6.lean
@@ -16,7 +16,7 @@ attribute mul.assoc    [forward]
 attribute mul.left_inv [forward]
 attribute one_mul      [forward]
 
-theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
+theorem inv_eq_of_mul_eq_one₁ {a b : A} (H : a * b = 1) : a⁻¹ = b :=
 -- This is the kind of theorem that can be easily proved using superposition,
 -- but cannot to be proved using E-matching.
 -- To prove it using E-matching, we must provide the following auxiliary assertion.
diff --git a/tests/lean/run/blast_ematch8.lean b/tests/lean/run/blast_ematch8.lean
index 386951248..a52a4c23e 100644
--- a/tests/lean/run/blast_ematch8.lean
+++ b/tests/lean/run/blast_ematch8.lean
@@ -4,7 +4,7 @@ open algebra
 variables {A : Type}
 variables [s : group A]
 include s
-
+namespace foo
 set_option blast.ematch true
 set_option blast.subst  false
 set_option blast.simp   false
@@ -47,3 +47,4 @@ theorem eq_of_mul_inv_eq_one₂ {a b : A} (H : a * b⁻¹ = 1) : a = b :=
 calc
   a = a * b⁻¹ * b : by blast
 ... = b           : by blast
+end foo
diff --git a/tests/lean/run/constr_tac4.lean b/tests/lean/run/constr_tac4.lean
index ad18713d7..e3a62d79a 100644
--- a/tests/lean/run/constr_tac4.lean
+++ b/tests/lean/run/constr_tac4.lean
@@ -1,7 +1,7 @@
 import data.nat
 
 open nat
-
+namespace foo
 definition lt.trans {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
 have aux : a < b → a < c, from
   le.rec_on H₂
@@ -18,3 +18,4 @@ definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
 le.rec_on H
   (by constructor; constructor)
   (λ b h ih, by constructor; exact ih)
+end foo
diff --git a/tests/lean/run/local_ctx_bug.lean b/tests/lean/run/local_ctx_bug.lean
index 5a78c928c..3e167f520 100644
--- a/tests/lean/run/local_ctx_bug.lean
+++ b/tests/lean/run/local_ctx_bug.lean
@@ -1,5 +1,5 @@
 import data.finset data.finset.card data.finset.equiv
-open nat nat.finset decidable
+open nat decidable
 
 namespace finset
 variable {A : Type}
diff --git a/tests/lean/run/print_inductive.lean b/tests/lean/run/print_inductive.lean
index 8c1c78dea..5e5b6359d 100644
--- a/tests/lean/run/print_inductive.lean
+++ b/tests/lean/run/print_inductive.lean
@@ -2,6 +2,6 @@ import data.list algebra.group
 
 print inductive nat
 
-print inductive algebra.group
+print inductive group
 
 print inductive list
diff --git a/tests/lean/run/rewrite5.lean b/tests/lean/run/rewrite5.lean
index acfb30b7e..a88f6dcae 100644
--- a/tests/lean/run/rewrite5.lean
+++ b/tests/lean/run/rewrite5.lean
@@ -1,9 +1,8 @@
 import algebra.group
-open algebra
 
 variable {A : Type}
 variable [s : group A]
 include s
 
-theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
+theorem mul.right_inv₁ (a : A) : a * a⁻¹ = 1 :=
 by rewrite [-{a}inv_inv at {1}, mul.left_inv]
diff --git a/tests/lean/run/struct_infer.lean b/tests/lean/run/struct_infer.lean
index 2497229f8..d4f3dae89 100644
--- a/tests/lean/run/struct_infer.lean
+++ b/tests/lean/run/struct_infer.lean
@@ -1,6 +1,6 @@
 import data.nat.basic
 open nat
-
+namespace foo
 definition associative {A : Type} (op : A → A → A) := ∀a b c, op (op a b) c = op a (op b c)
 
 structure semigroup [class] (A : Type) :=
@@ -19,3 +19,4 @@ definition s := semigroup2.mk nat nat.mul nat.mul_assoc
 
 example (a b c : nat) : (a * b) * c = a * (b * c) :=
 semigroup2.mul_assoc nat s a b c
+end foo
diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean
index d402c6bcc..0948a4bbb 100644
--- a/tests/lean/simplifier12.lean
+++ b/tests/lean/simplifier12.lean
@@ -3,7 +3,7 @@ open algebra
 
 set_option simplify.max_steps 1000
 universe l
-constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (T : Type.{l}) (s : comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 
diff --git a/tests/lean/simplifier14.lean b/tests/lean/simplifier14.lean
index 836b0df1c..dab78ea2c 100644
--- a/tests/lean/simplifier14.lean
+++ b/tests/lean/simplifier14.lean
@@ -1,9 +1,8 @@
 -- Basic fusion
 import algebra.ring
-open algebra
 
 universe l
-constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (T : Type.{l}) (s : comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 set_option simplify.max_steps 50000
diff --git a/tests/lean/simplifier15.lean b/tests/lean/simplifier15.lean
index 5f6442cc0..e8c8fbd47 100644
--- a/tests/lean/simplifier15.lean
+++ b/tests/lean/simplifier15.lean
@@ -3,7 +3,7 @@ import algebra.ring
 open algebra
 
 universe l
-constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (T : Type.{l}) (s : comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 
diff --git a/tests/lean/simplifier15.lean.expected.out b/tests/lean/simplifier15.lean.expected.out
index 134429183..639019d15 100644
--- a/tests/lean/simplifier15.lean.expected.out
+++ b/tests/lean/simplifier15.lean.expected.out
@@ -1,24 +1,23 @@
 (refl): x1
-(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1
-(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+(refl): @add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1
+(refl): @add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1)
   x1
-(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
-     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
+(refl): @add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s))
+  (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s))
+     (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1)
      x1)
   x1
-(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
-     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
-     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
+(refl): @add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s))
+  (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s))
+     (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1)
+     (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1))
   x1
-@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
-@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
-@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-  (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-     (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
-        (@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)))
+@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1)
+@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+     (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1))
+@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+  (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+     (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1
+        (@add.{l} T (@has_add.mk.{l} T (@comm_ring.add.{l} T s)) x1 x1)))
diff --git a/tests/lean/simplifier18.lean b/tests/lean/simplifier18.lean
index b0437baad..7ba2caaaf 100644
--- a/tests/lean/simplifier18.lean
+++ b/tests/lean/simplifier18.lean
@@ -3,7 +3,7 @@ import algebra.ring
 open algebra
 
 universe l
-constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (T : Type.{l}) (s : comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 set_option simplify.max_steps 50000
diff --git a/tests/lean/simplifier19.lean b/tests/lean/simplifier19.lean
index 96f0ba699..b1b25b6f0 100644
--- a/tests/lean/simplifier19.lean
+++ b/tests/lean/simplifier19.lean
@@ -3,7 +3,7 @@ import algebra.ring
 open algebra
 
 universe l
-constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (T : Type.{l}) (s : comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 set_option simplify.max_steps 50000
diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean
index 2ae5721b7..92d10e46f 100644
--- a/tests/lean/simplifier_norm_num.lean
+++ b/tests/lean/simplifier_norm_num.lean
@@ -1,5 +1,4 @@
 import algebra.ring
-open algebra
 
 set_option simplify.max_steps 5000000
 -- TODO(dhs): we need to create the simplifier.numeral namespace incrementally.