fix(tests/lean): adjust tests to new library structure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

doc/lean/calc.org

@@ -25,7 +25,7 @@ in =<expr>_{i-1}=.
 Here is an example
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   variables a b c d e : nat.
   axiom Ax1 : a = b.
@@ -52,7 +52,7 @@ gaps in our calculational proofs. In the previous examples, we can use =_= as ar
 Here is the same example using placeholders.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   variables a b c d e : nat.
   axiom Ax1 : a = b.
@@ -73,7 +73,7 @@ The =calc= command can be configured for any relation that supports
 some form of transitivity. It can even combine different relations.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   theorem T2 (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0

doc/lean/tutorial.org

@@ -29,7 +29,7 @@ As a more complex example, the next example defines a function that doubles
 the input value.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   -- defines the double function
   definition double (x : nat) := x + x
@@ -56,7 +56,7 @@ proposition, =Prop= is the type of propositions.
 The command =import= loads existing libraries and extensions.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   check nat.ge
 #+END_SRC
 
@@ -69,7 +69,7 @@ the following command creates aliases for all objects starting with
 =nat=, and imports all notations defined in this namespace.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   check ge -- display the type of nat.ge
 #+END_SRC
@@ -78,7 +78,7 @@ The command =variable= assigns a type to an identifier. The following command po
 that =n=, =m= and =o= have type =nat=.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   variable n : nat
   variable m : nat
@@ -95,7 +95,7 @@ expressions is also available for manipulating proofs. For example, =refl n= is
 for =n = n=. In Lean, =refl= is the reflexivity theorem.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   variable n : nat
   check refl n
@@ -107,7 +107,7 @@ The following commands postulate two axioms =Ax1= and =Ax2= that state that =n =
 =n = o=, where =trans= is the transitivity theorem.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   variables m n o : nat
   axiom Ax1 : n = m
@@ -131,7 +131,7 @@ extensions are loaded, the _excluded middle_ is a theorem,
 and =em p= is a proof for =p ∨ ¬ p=.
 
 #+BEGIN_SRC lean
-  import classical
+  import logic.axioms.classical
   variable p : Prop
   check em p
 #+END_SRC
@@ -145,7 +145,7 @@ called =nat_trans3=, and then use it to prove something else. In this
 example, =symm= is the symmetry theorem.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   theorem nat_trans3 (a b c d : nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
@@ -174,7 +174,7 @@ In the following example, we define the theorem =nat_trans3i= using
 implicit arguments.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
@@ -209,7 +209,7 @@ We can also instruct Lean to display all implicit arguments when it prints expre
 This is useful when debugging non-trivial problems.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   variables a b c : nat
@@ -360,7 +360,7 @@ may or may not contain =x=, one can construct the so-called _lambda abstraction_
 examples.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   check fun x : nat, x + 1
@@ -374,7 +374,7 @@ In many cases, Lean can automatically infer the type of the variable. Actually,
 In all examples above, the type can be inferred automatically.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   check fun x, x + 1
@@ -391,7 +391,7 @@ The following example shows how to use lambda abstractions in
 function applications
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   check (fun x y, x + 2 * y) 1
   check (fun x y, x + 2 * y) 1 2
@@ -419,7 +419,7 @@ checking types/proofs. So, we can prove that two definitionally equal terms
 are equal using just =refl=. Here is a simple example.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1 := refl (a+1)
@@ -652,7 +652,7 @@ forall =x=.
 Then we instantiate the axiom using function application.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   variable f : nat → nat
@@ -668,7 +668,7 @@ abstraction. In the following example, we create a proof term showing that for a
 =x= and =y=, =f x = f y=.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   variable f : nat → nat
@@ -693,7 +693,7 @@ We say =w= is the witness for the existential introduction. In previous examples
 for =∃ a : nat, a = w= using
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   theorem nat_trans3i {a b c d : nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
@@ -720,7 +720,7 @@ the implicit arguments using the option =pp.implicit=. We see that each instance
 has different values for the implicit argument =P=.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   check @exists_intro
@@ -751,7 +751,7 @@ In the following example, we define =even a= as =∃ b, a = 2*b=, and then we sh
 of two even numbers is an even number.
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
 
   definition even (a : nat) := ∃ b, a = 2*b
@@ -772,7 +772,7 @@ In Lean, we can use =obtain _, from _, _= as syntax sugar for =exists_elim=.
 With this macro we can write the example above in a more natural way
 
 #+BEGIN_SRC lean
-  import nat
+  import data.nat
   using nat
   definition even (a : nat) := ∃ b, a = 2*b
   theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=

tests/lean/empty.lean

@@ -1,4 +1,4 @@
-import logic hilbert
+import logic logic.axioms.hilbert
 
 definition v1 : Prop := epsilon (λ x, true)
 inductive Empty : Type

tests/lean/have1.lean

@@ -1,4 +1,4 @@
-import logic bool tactic
+import standard
 using bool eq_proofs tactic
 
 variables a b c : bool

tests/lean/run/coercion_bug.lean

@@ -1,4 +1,4 @@
-import nat
+import data.nat
 using nat
 
 definition tst1  : Prop := zero = 0

tests/lean/run/coercion_bug2.lean

@@ -1,4 +1,4 @@
-import nat
+import data.nat
 using nat
 
 inductive list (T : Type) : Type :=

tests/lean/run/decidable.lean

@@ -1,4 +1,4 @@
-import standard unit decidable if
+import standard data.unit
 using bool unit decidable
 
 variables a b c : bool

tests/lean/run/elab_bug1.lean

@@ -4,8 +4,7 @@
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
 
-import logic
-import function
+import standard
 
 using function
 
@@ -61,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_mp_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

tests/lean/run/fun.lean

@@ -1,4 +1,4 @@
-import function logic num bool
+import standard
 using function num bool
 
 

tests/lean/run/list_elab1.lean

@@ -9,7 +9,7 @@
 --
 -- Basic properties of lists.
 
-import nat
+import data.nat
 using nat eq_proofs
 set_option unifier.expensive true
 inductive list (T : Type) : Type :=

tests/lean/run/nat_bug.lean

@@ -1,4 +1,4 @@
-import logic decidable
+import logic
 using decidable
 
 inductive nat : Type :=

tests/lean/run/nat_bug2.lean

@@ -1,4 +1,4 @@
-import logic num
+import standard
 using num eq_proofs
 
 inductive nat : Type :=

tests/lean/run/nat_bug3.lean

@@ -1,4 +1,4 @@
-import logic num
+import standard
 using num eq_proofs
 
 inductive nat : Type :=

tests/lean/run/nat_bug4.lean

@@ -1,4 +1,4 @@
-import logic num
+import standard
 using num eq_proofs
 
 inductive nat : Type :=

tests/lean/run/nat_bug5.lean

@@ -1,4 +1,4 @@
-import logic num
+import standard
 using num eq_proofs
 
 inductive nat : Type :=

tests/lean/run/nat_bug6.lean

@@ -1,4 +1,4 @@
-import logic num
+import standard
 using eq_proofs
 
 inductive nat : Type :=

tests/lean/run/not_bug1.lean

@@ -1,4 +1,4 @@
-import bool
+import standard
 using bool
 
 variable list : Type.{1}

tests/lean/run/num.lean

@@ -1,4 +1,4 @@
-import num
+import standard
 check 14
 check 0
 check 3

tests/lean/run/set.lean

@@ -1,4 +1,4 @@
-import standard bool
+import standard
 using bool
 
 definition set {{T : Type}} := T → bool

tests/lean/run/set2.lean

@@ -1,4 +1,4 @@
-import standard bool
+import standard
 using bool
 
 namespace set

tests/lean/run/string.lean

@@ -1,3 +1,3 @@
-import string
+import data.string
 check "aaa"
 check "B"

tests/lean/run/tactic10.lean

@@ -3,7 +3,7 @@ using tactic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := by apply iff_intro;
-      apply (assume Hb, iff_mp_right H Hb);
-      apply (assume Ha, iff_mp_left H Ha)
+      apply (assume Hb, iff_elim_right H Hb);
+      apply (assume Ha, iff_elim_left H Ha)
 
 check tst

tests/lean/run/tactic11.lean

@@ -5,5 +5,5 @@ 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_mp_right H Hb);
+      apply (assume Hb, iff_elim_right H Hb);
       apply (assume Ha, H1 Ha)

tests/lean/show1.lean

@@ -1,4 +1,4 @@
-import logic bool tactic
+import standard
 using bool eq_proofs tactic
 
 variables a b c : bool

tests/lean/slow/list_elab2.lean

@@ -9,8 +9,7 @@
 --
 -- Basic properties of lists.
 
-import tactic
-import nat
+import logic data.nat
 -- import congr
 
 set_option unifier.expensive true

tests/lean/slow/nat_wo_hints.lean

@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
-import logic num tactic decidable binary
+import standard struc.binary
 using tactic num binary eq_proofs
 using decidable