From 81618e30f3fb1631accdd2c339aa6f848b5cd4ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 15:39:03 -0700 Subject: [PATCH] fix(tests/lean/run): adjust some tests to changes in the standard library --- tests/lean/run/252.lean | 2 +- tests/lean/run/331.lean | 2 +- tests/lean/run/505.lean | 6 +- tests/lean/run/511a.lean | 2 +- tests/lean/run/568.lean | 8 +- tests/lean/run/668.lean | 6 +- tests/lean/run/695e.lean | 3 +- tests/lean/run/791.lean | 5 +- tests/lean/run/801.lean | 2 +- tests/lean/run/809.lean | 2 +- tests/lean/run/alg_rw.lean | 5 +- tests/lean/run/algebra3.lean | 9 -- tests/lean/run/all_goals.lean | 1 - tests/lean/run/all_goals2.lean | 2 +- tests/lean/run/app_builder.lean | 2 +- tests/lean/run/assert_tac2.lean | 2 +- tests/lean/run/atomic_notation.lean | 2 +- tests/lean/run/bquant.lean | 6 +- tests/lean/run/choose_test.lean | 2 +- tests/lean/run/class5.lean | 2 +- tests/lean/run/class_coe.lean | 6 -- tests/lean/run/constr_tac.lean | 2 +- tests/lean/run/contra1.lean | 6 +- tests/lean/run/diag.lean | 2 +- tests/lean/run/div_wf.lean | 2 +- tests/lean/run/eq15.lean | 2 +- tests/lean/run/eq16.lean | 2 +- tests/lean/run/eq25.lean | 6 +- tests/lean/run/eq6.lean | 2 +- tests/lean/run/ex.lean | 3 +- tests/lean/run/export2.lean | 2 +- tests/lean/run/fib_brec.lean | 4 +- tests/lean/run/finset.lean | 2 +- tests/lean/run/forest_height.lean | 2 +- tests/lean/run/gcd.lean | 2 +- tests/lean/run/group.lean | 4 +- tests/lean/run/group2.lean | 4 +- tests/lean/run/imp2.lean | 4 +- tests/lean/run/interp.lean | 4 +- tests/lean/run/is_true.lean | 10 +- tests/lean/run/issue332.lean | 2 +- tests/lean/run/let_tac.lean | 1 + tests/lean/run/localcoe.lean | 3 +- tests/lean/run/matrix.lean | 14 +-- tests/lean/run/matrix2.lean | 8 +- tests/lean/run/measurable.lean | 2 +- tests/lean/run/nat_bug2.lean | 2 +- tests/lean/run/nested_rec.lean | 2 +- tests/lean/run/new_obtains.lean | 10 -- tests/lean/run/num_sub.lean | 138 +++++++++++++------------- tests/lean/run/occurs_check_bug1.lean | 4 +- tests/lean/run/one.lean | 6 +- tests/lean/run/one2.lean | 6 +- tests/lean/run/over_subst.lean | 6 +- tests/lean/run/pickle1.lean | 2 +- tests/lean/run/ppbeta.lean | 6 +- tests/lean/run/ptst.lean | 6 +- tests/lean/run/rat_coe.lean | 2 +- tests/lean/run/rat_rfl.lean | 4 +- tests/lean/run/reducible.lean | 18 ++-- tests/lean/run/rewrite8.lean | 2 +- tests/lean/run/rewriter12.lean | 4 +- tests/lean/run/rewriter14.lean | 2 +- tests/lean/run/secnot.lean | 6 +- tests/lean/run/set.lean | 4 +- tests/lean/run/show2.lean | 2 +- tests/lean/run/st_options.lean | 18 ---- tests/lean/run/struct_inst_exprs.lean | 4 +- tests/lean/run/tactic23.lean | 5 +- tests/lean/run/tree.lean | 8 +- tests/lean/run/tree2.lean | 8 +- tests/lean/run/tree3.lean | 8 +- tests/lean/run/tree_height.lean | 6 +- tests/lean/run/tree_subterm_pred.lean | 6 +- tests/lean/run/trick.lean | 2 +- tests/lean/run/tt1.lean | 4 +- tests/lean/run/unfold_rec.lean | 2 - tests/lean/run/unzip_bug.lean | 2 +- tests/lean/run/vector.lean | 2 +- 79 files changed, 214 insertions(+), 265 deletions(-) diff --git a/tests/lean/run/252.lean b/tests/lean/run/252.lean index fa47afd32..585d5fceb 100644 --- a/tests/lean/run/252.lean +++ b/tests/lean/run/252.lean @@ -6,7 +6,7 @@ node : tree A → tree A → tree A check tree.node -definition size {A : Type} (t : tree A) := +definition size {A : Type} (t : tree A) : nat := tree.rec (λ a, 1) (λ t₁ t₂ n₁ n₂, n₁ + n₂) t check size diff --git a/tests/lean/run/331.lean b/tests/lean/run/331.lean index 7a92864d6..4e5a70407 100644 --- a/tests/lean/run/331.lean +++ b/tests/lean/run/331.lean @@ -9,7 +9,7 @@ open nat check less.rec_on namespace foo1 -protected definition foo2.bar := 10 +protected definition foo2.bar : nat := 10 end foo1 example : foo1.foo2.bar = 10 := diff --git a/tests/lean/run/505.lean b/tests/lean/run/505.lean index 57c5e5f05..da2043cef 100644 --- a/tests/lean/run/505.lean +++ b/tests/lean/run/505.lean @@ -1,5 +1,5 @@ import data.set -open set +open set nat section variable {A : Type} @@ -13,8 +13,8 @@ section notation `⦃` s:(foldr `,` (a t, insert a t) ∅) `⦄` := s notation `{` `{` s:(foldr `,` (a t, insert a t) ∅) `}` `}` := s - check ⦃1, 2, 3⦄ - check {{1, 2, 3}} + check ⦃(1:nat), 2, 3⦄ + check {{(1:nat), 2, 3}} definition foo {X : Type} {{ x : X }} : X := x end diff --git a/tests/lean/run/511a.lean b/tests/lean/run/511a.lean index 6c39434fa..00077163d 100644 --- a/tests/lean/run/511a.lean +++ b/tests/lean/run/511a.lean @@ -5,7 +5,7 @@ example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 := by rewrite [add_one, h] example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 := -by xrewrite h +by krewrite h definition g (a : nat) := a + 1 definition h (a : nat) := a diff --git a/tests/lean/run/568.lean b/tests/lean/run/568.lean index d79773020..b5ea19483 100644 --- a/tests/lean/run/568.lean +++ b/tests/lean/run/568.lean @@ -1,15 +1,15 @@ namespace f1 - definition flip := 20 + definition flip := (20:num) end f1 namespace f2 - definition flip := 10 + definition flip := (10:num) end f2 namespace f3 export [declarations] f1 - export -[declarations] f2 + export - [declarations] f2 end f3 export [declarations] f1 -export -[declarations] f2 +export - [declarations] f2 diff --git a/tests/lean/run/668.lean b/tests/lean/run/668.lean index 77bdee3e4..e121876af 100644 --- a/tests/lean/run/668.lean +++ b/tests/lean/run/668.lean @@ -4,7 +4,7 @@ namespace Nat constant Nat : Type₁ constant num2Nat : num → Nat attribute num2Nat [coercion] - check (0 : Nat) + definition foo : Nat := (0:num) end Nat constant Int : Type₁ @@ -13,8 +13,8 @@ namespace Int open Nat constant Nat2Int : Nat → Int attribute Nat2Int [coercion] - check (0 : Int) + definition foo : Int := (0:num) end Int open Int -check (0 : Int) +definition foo : Int := (0:num) diff --git a/tests/lean/run/695e.lean b/tests/lean/run/695e.lean index ab1ad4c1b..450d76a56 100644 --- a/tests/lean/run/695e.lean +++ b/tests/lean/run/695e.lean @@ -1,3 +1,4 @@ +import data.nat open nat example (n : ℕ) : n + 1 = succ n := -by rewrite [ 3 := +theorem ex : ∃ x : nat, x > 3 := exists.intro 6 dec_trivial reveal ex diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean index b84395a0d..91d3336d2 100644 --- a/tests/lean/run/class5.lean +++ b/tests/lean/run/class5.lean @@ -44,7 +44,7 @@ section -- check mul_struct nat << This is an error, we opened only the notation from algebra variables a b c : nat check a*b*c - definition tst3 : nat := #nat a*b*c + definition tst3 : nat := a*b*c end section diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean index d1afe5947..c453df10d 100644 --- a/tests/lean/run/class_coe.lean +++ b/tests/lean/run/class_coe.lean @@ -40,12 +40,6 @@ check x + i check n + x check x + n check x + i + n -check n + 0 -check 0 + n -check 0 + i -check i + 0 -check 0 + x -check x + 0 namespace foo constant eq {A : Type} : A → A → Prop infixl `=` := eq diff --git a/tests/lean/run/constr_tac.lean b/tests/lean/run/constr_tac.lean index 6d5b4b298..1c94e9dd0 100644 --- a/tests/lean/run/constr_tac.lean +++ b/tests/lean/run/constr_tac.lean @@ -45,7 +45,7 @@ end open nat -example (a : nat) : a > 0 → ∃ x, x > 0 := +example (a : nat) : a > 0 → ∃ x : nat, x > 0 := begin intro Ha, existsi a, diff --git a/tests/lean/run/contra1.lean b/tests/lean/run/contra1.lean index cd22b35f5..d90ade779 100644 --- a/tests/lean/run/contra1.lean +++ b/tests/lean/run/contra1.lean @@ -1,10 +1,12 @@ +open nat + example (a b : nat) (h : false) : a = b := by contradiction example : ∀ (a b : nat), false → a = b := by contradiction -example : ∀ (a b : nat), 0 = 1 → a = b := +example : ∀ (a b : nat), (0:nat) = 1 → a = b := by contradiction definition id {A : Type} (a : A) := a @@ -12,5 +14,5 @@ definition id {A : Type} (a : A) := a example : ∀ (a b : nat), id false → a = b := by contradiction -example : ∀ (a b : nat), id (0 = 1) → a = b := +example : ∀ (a b : nat), id ((0:nat) = 1) → a = b := by contradiction diff --git a/tests/lean/run/diag.lean b/tests/lean/run/diag.lean index 628d3c16a..730a56100 100644 --- a/tests/lean/run/diag.lean +++ b/tests/lean/run/diag.lean @@ -11,7 +11,7 @@ nat.rec_on n let t₁ : vector (vector A n₁) n₁ := map tail (tail v) in h₁ :: r t₁) -example : diag ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil) = 1 :: 5 :: 9 :: nil := +example : diag ((1 :: 2 :: 3 :: nil) :: (4 :: 5 :: 6 :: nil) :: (7 :: 8 :: 9 :: nil) :: nil) = (1 :: 5 :: 9 :: nil : vector num 3) := rfl end vector diff --git a/tests/lean/run/div_wf.lean b/tests/lean/run/div_wf.lean index 9ae7f6bfc..9c4f45ccc 100644 --- a/tests/lean/run/div_wf.lean +++ b/tests/lean/run/div_wf.lean @@ -26,7 +26,7 @@ rfl -- The actual definitional package would not do that. -- It will always pack things. -definition pair_nat.lt := lex lt lt -- Could also be (lex lt empty_rel) +definition pair_nat.lt := lex nat.lt nat.lt -- Could also be (lex lt empty_rel) definition pair_nat.lt.wf [instance] : well_founded pair_nat.lt := prod.lex.wf lt.wf lt.wf infixl `≺`:50 := pair_nat.lt diff --git a/tests/lean/run/eq15.lean b/tests/lean/run/eq15.lean index 7e695acf9..90198cb42 100644 --- a/tests/lean/run/eq15.lean +++ b/tests/lean/run/eq15.lean @@ -13,5 +13,5 @@ rfl theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := rfl -example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/eq16.lean b/tests/lean/run/eq16.lean index 23e68b163..03cff7869 100644 --- a/tests/lean/run/eq16.lean +++ b/tests/lean/run/eq16.lean @@ -14,5 +14,5 @@ rfl theorem append_cons (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := rfl -example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : append ((1:num) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean index 6ec2f1648..ff7f72f3a 100644 --- a/tests/lean/run/eq25.lean +++ b/tests/lean/run/eq25.lean @@ -6,6 +6,6 @@ definition Nat := N open N -definition add : Nat → Nat → Nat -| add O b := b -| add (S a) b := S (add a b) +definition add1 : Nat → Nat → Nat +| add1 O b := b +| add1 (S a) b := S (add1 a b) diff --git a/tests/lean/run/eq6.lean b/tests/lean/run/eq6.lean index fbd73ecae..abef80185 100644 --- a/tests/lean/run/eq6.lean +++ b/tests/lean/run/eq6.lean @@ -11,5 +11,5 @@ rfl theorem append_cons {A : Type} (h : A) (t l : list A) : append (h :: t) l = h :: (append t l) := rfl -example : append (1 :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := +example : append ((1:nat) :: 2 :: nil) (3 :: 4 :: 5 :: nil) = (1 :: 2 :: 3 :: 4 :: 5 :: nil) := rfl diff --git a/tests/lean/run/ex.lean b/tests/lean/run/ex.lean index 6bad54d9b..965fa4d87 100644 --- a/tests/lean/run/ex.lean +++ b/tests/lean/run/ex.lean @@ -1,3 +1,4 @@ import standard set_option pp.implicit true -check ∃x, x = 0 \ No newline at end of file +check ∃x, x = (0:num) +check ∃x:num, x = 0 diff --git a/tests/lean/run/export2.lean b/tests/lean/run/export2.lean index d81d5f0ed..3472483fa 100644 --- a/tests/lean/run/export2.lean +++ b/tests/lean/run/export2.lean @@ -1,6 +1,6 @@ open nat -definition foo := 30 +definition foo : nat := 30 namespace foo definition x : nat := 10 diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean index ecd88c82b..c6ae2a010 100644 --- a/tests/lean/run/fib_brec.lean +++ b/tests/lean/run/fib_brec.lean @@ -19,9 +19,9 @@ namespace nat definition fib (n : nat) := nat.brec_on n (λ (n : nat), nat.cases_on n - (λ (b₀ : nat.below zero), succ zero) + (λ (b₀ : nat.below 0), succ 0) (λ (n₁ : nat), nat.cases_on n₁ - (λ b₁ : nat.below (succ zero), succ zero) + (λ b₁ : nat.below (succ 0), succ zero) (λ (n₂ : nat) (b₂ : nat.below (succ (succ n₂))), pr₁ b₂ + pr₁ (pr₂ b₂)))) theorem fib_0 : fib 0 = 1 := diff --git a/tests/lean/run/finset.lean b/tests/lean/run/finset.lean index 81a517553..384453fbe 100644 --- a/tests/lean/run/finset.lean +++ b/tests/lean/run/finset.lean @@ -167,7 +167,7 @@ namespace finset theorem empty_union {A : Type} (s : finset A) : ∅ ∪ s = s := quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_left)) - example : to_finset (1::2::nil) ∪ to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ := + example : to_finset ((1:nat)::2::nil) ∪ to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ := rfl example : to_finset [(1:nat), 1, 2, 3] = to_finset [2, 3, 1, 2, 2, 3] := diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean index 574a55714..f5c0dad7e 100644 --- a/tests/lean/run/forest_height.lean +++ b/tests/lean/run/forest_height.lean @@ -1,5 +1,5 @@ import data.nat data.sum data.sigma data.bool -open nat sigma +open nat sigma algebra inductive tree (A : Type) : Type := | node : A → forest A → tree A diff --git a/tests/lean/run/gcd.lean b/tests/lean/run/gcd.lean index 917626a10..b1060595a 100644 --- a/tests/lean/run/gcd.lean +++ b/tests/lean/run/gcd.lean @@ -4,7 +4,7 @@ open nat well_founded decidable prod eq.ops namespace playground -- Setup -definition pair_nat.lt := lex lt lt +definition pair_nat.lt := lex nat.lt nat.lt definition pair_nat.lt.wf [instance] : well_founded pair_nat.lt := intro_k (prod.lex.wf lt.wf lt.wf) 20 -- the '20' is for being able to execute the examples... it means 20 recursive call without proof computation infixl `≺`:50 := pair_nat.lt diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index 02323593b..3f370912e 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -26,10 +26,10 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul {A : Type} {s : group_struct A} (a b : A) : A +definition mul1 {A : Type} {s : group_struct A} (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b -infixl `*` := mul +infixl `*` := mul1 constant G1 : group.{1} constant G2 : group.{1} diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index a609eeb8a..7a6509c3f 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -28,10 +28,10 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul {A : Type} [s : group_struct A] (a b : A) : A +definition mul1 {A : Type} [s : group_struct A] (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b -infixl `*` := mul +infixl `*` := mul1 section variable G1 : group diff --git a/tests/lean/run/imp2.lean b/tests/lean/run/imp2.lean index e097a0106..75d488d44 100644 --- a/tests/lean/run/imp2.lean +++ b/tests/lean/run/imp2.lean @@ -1,4 +1,4 @@ import data.num -check (λ {A : Type.{1}} (a : A), a) 10 +check (λ {A : Type.{1}} (a : A), a) (10:num) check (λ {A} a, a) 10 -check (λ a, a) 10 +check (λ a, a) (10:num) diff --git a/tests/lean/run/interp.lean b/tests/lean/run/interp.lean index aeecc41c5..fbf9259c4 100644 --- a/tests/lean/run/interp.lean +++ b/tests/lean/run/interp.lean @@ -8,7 +8,7 @@ inductive univ := open univ -definition interp : univ → Type₁ +definition interp [reducible] : univ → Type₁ | ubool := bool | unat := nat | (uarrow fr to) := interp fr → interp to @@ -23,7 +23,7 @@ definition is_even : nat → bool | zero := tt | (succ n) := bnot (is_even n) -example : foo unat 10 = 11 := rfl +example : foo unat (10:nat) = 11 := rfl example : foo ubool tt = ff := rfl example : foo (uarrow unat ubool) (λ x : nat, is_even x) 3 = tt := rfl example : foo (uarrow unat ubool) (λ x : nat, is_even x) 4 = ff := rfl diff --git a/tests/lean/run/is_true.lean b/tests/lean/run/is_true.lean index 537c8a122..0614c69e6 100644 --- a/tests/lean/run/is_true.lean +++ b/tests/lean/run/is_true.lean @@ -1,8 +1,8 @@ import data.nat open nat -example : is_true (2 = 2) := trivial -example : is_false (3 = 2) := trivial -example : is_true (2 < 3) := trivial -example : is_true (3 ∣ 9) := trivial -example : is_false (3 ∣ 7) := trivial +example : is_true (2 = (2:nat)) := trivial +example : is_false (3 = (2:nat)) := trivial +example : is_true (2 < (3:nat)) := trivial +example : is_true (3 ∣ (9:nat)) := trivial +example : is_false (3 ∣ (7:nat)) := trivial diff --git a/tests/lean/run/issue332.lean b/tests/lean/run/issue332.lean index 693102e2e..e22e0ed05 100644 --- a/tests/lean/run/issue332.lean +++ b/tests/lean/run/issue332.lean @@ -7,5 +7,5 @@ intro a, exact a end check @foo -example : foo 10 = 10 := +example : foo 10 = (10:num) := rfl diff --git a/tests/lean/run/let_tac.lean b/tests/lean/run/let_tac.lean index f4c63f817..c64acc5ca 100644 --- a/tests/lean/run/let_tac.lean +++ b/tests/lean/run/let_tac.lean @@ -1,4 +1,5 @@ import data.nat +open algebra example (a b : Prop) : a → b → a ∧ b := begin diff --git a/tests/lean/run/localcoe.lean b/tests/lean/run/localcoe.lean index e8f8a7514..e7748e4a2 100644 --- a/tests/lean/run/localcoe.lean +++ b/tests/lean/run/localcoe.lean @@ -12,5 +12,6 @@ section local attribute foo [coercion] - check s 10 + check let a : nat := 10 in s a + end diff --git a/tests/lean/run/matrix.lean b/tests/lean/run/matrix.lean index 2086d80be..597b2b6be 100644 --- a/tests/lean/run/matrix.lean +++ b/tests/lean/run/matrix.lean @@ -2,18 +2,18 @@ import logic constant matrix.{l} : Type.{l} → Type.{l} constant same_dim {A : Type} : matrix A → matrix A → Prop -constant add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A +constant add1 {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A -theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add A m1 m2 H1 = @add A m1 m2 H2 := +theorem same_dim_irrel {A : Type} {m1 m2 : matrix A} {H1 H2 : same_dim m1 m2} : @add1 A m1 m2 H1 = @add1 A m1 m2 H2 := rfl open eq theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := subst H1 (subst H2 H) -theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) := -have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from +theorem add1_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add1 A m1 m2 H = @add1 A m1' m2' (same_dim_eq_args H1 H2 H) := +have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add1 A m1 m2 H = @add1 A m1 m2 (eq.rec (eq.rec H H1) H2), from assume H1 H2, rfl, -have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from +have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add1 A m1 m2 H = @add1 A m1' m2' (eq.rec (eq.rec H H1) H2), from subst H1 (subst H2 base), -calc @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2) : general H1 H2 - ... = @add A m1' m2' (same_dim_eq_args H1 H2 H) : same_dim_irrel +calc @add1 A m1 m2 H = @add1 A m1' m2' (eq.rec (eq.rec H H1) H2) : general H1 H2 + ... = @add1 A m1' m2' (same_dim_eq_args H1 H2 H) : same_dim_irrel diff --git a/tests/lean/run/matrix2.lean b/tests/lean/run/matrix2.lean index 5ec9a504e..024135ce6 100644 --- a/tests/lean/run/matrix2.lean +++ b/tests/lean/run/matrix2.lean @@ -2,14 +2,14 @@ import logic constant matrix.{l} : Type.{l} → Type.{l} constant same_dim {A : Type} : matrix A → matrix A → Prop -constant add {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A +constant add1 {A : Type} (m1 m2 : matrix A) {H : same_dim m1 m2} : matrix A open eq theorem same_dim_eq_args {A : Type} {m1 m2 m1' m2' : matrix A} (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : same_dim m1' m2' := subst H1 (subst H2 H) -theorem add_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add A m1 m2 H = @add A m1' m2' (same_dim_eq_args H1 H2 H) := -have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add A m1 m2 H = @add A m1 m2 (eq.rec (eq.rec H H1) H2), from +theorem add1_congr {A : Type} (m1 m2 m1' m2' : matrix A) (H1 : m1 = m1') (H2 : m2 = m2') (H : same_dim m1 m2) : @add1 A m1 m2 H = @add1 A m1' m2' (same_dim_eq_args H1 H2 H) := +have base : ∀ (H1 : m1 = m1) (H2 : m2 = m2), @add1 A m1 m2 H = @add1 A m1 m2 (eq.rec (eq.rec H H1) H2), from assume H1 H2, rfl, -have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add A m1 m2 H = @add A m1' m2' (eq.rec (eq.rec H H1) H2), from +have general : ∀ (H1 : m1 = m1') (H2 : m2 = m2'), @add1 A m1 m2 H = @add1 A m1' m2' (eq.rec (eq.rec H H1) H2), from subst H1 (subst H2 base), general H1 H2 diff --git a/tests/lean/run/measurable.lean b/tests/lean/run/measurable.lean index 95b6c9af4..6bf30f1d2 100644 --- a/tests/lean/run/measurable.lean +++ b/tests/lean/run/measurable.lean @@ -3,5 +3,5 @@ open prod nat example (a b : nat) : size_of (a, true, bool.tt, (λ c d : nat, c + d), option.some b) = a + b := rfl -example : size_of (pair (pair (pair 2 true) (λ a : nat, a)) (option.some 3)) = 5 := +example : size_of (pair (pair (pair (2:nat) true) (λ a : nat, a)) (option.some (3:nat))) = 5 := rfl diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean index dc37a99b0..2edc8f77b 100644 --- a/tests/lean/run/nat_bug2.lean +++ b/tests/lean/run/nat_bug2.lean @@ -20,7 +20,7 @@ axiom add_one (n:nat) : n + (succ zero) = succ n axiom add_le_right {n m : nat} (H : n ≤ m) (k : nat) : n + k ≤ m + k theorem succ_le {n m : nat} (H : n ≤ m) : succ n ≤ succ m -:= add_one m ▸ add_one n ▸ add_le_right H 1 +:= add_one m ▸ add_one n ▸ add_le_right H (1:num) end nat end experiment diff --git a/tests/lean/run/nested_rec.lean b/tests/lean/run/nested_rec.lean index ba9a6c6eb..950127fb4 100644 --- a/tests/lean/run/nested_rec.lean +++ b/tests/lean/run/nested_rec.lean @@ -34,7 +34,7 @@ calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl theorem g_all_zero (a : nat) : g a = zero := nat.induction_on a g_zero - (λ a₁ (ih : g a₁ = zero), calc + (λ a₁ (ih : g a₁ = 0), calc g (succ a₁) = g (g a₁) : g_succ ... = g 0 : ih ... = 0 : g_zero) diff --git a/tests/lean/run/new_obtains.lean b/tests/lean/run/new_obtains.lean index d7f7ac651..3f51fa8d6 100644 --- a/tests/lean/run/new_obtains.lean +++ b/tests/lean/run/new_obtains.lean @@ -63,14 +63,4 @@ exists.intro (x+y) (calc a+b = 2*x + 2*y : by rewrite [Hx, Hy] ... = 2*(x+y) : by rewrite mul.left_distrib) - -theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m ∣ n₁ + n₂) (H₂ : m ∣ n₁) : m ∣ n₂ := -obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁, -obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂, -have aux : m * (c₁ - c₂) = n₂, from calc - m * (c₁ - c₂) = m * c₁ - m * c₂ : by rewrite mul_sub_left_distrib - ... = n₁ + n₂ - m * c₂ : Hc₁ - ... = n₁ + n₂ - n₁ : Hc₂ - ... = n₂ : add_sub_cancel_left, -dvd.intro aux end hidden diff --git a/tests/lean/run/num_sub.lean b/tests/lean/run/num_sub.lean index f40c01cc1..cead32597 100644 --- a/tests/lean/run/num_sub.lean +++ b/tests/lean/run/num_sub.lean @@ -1,83 +1,83 @@ open num bool -example : le 0 0 = tt := rfl -example : le 0 1 = tt := rfl -example : le 0 2 = tt := rfl -example : le 0 3 = tt := rfl +example : num.le 0 0 = tt := rfl +example : num.le 0 1 = tt := rfl +example : num.le 0 2 = tt := rfl +example : num.le 0 3 = tt := rfl -example : le 1 0 = ff := rfl -example : le 1 1 = tt := rfl -example : le 1 2 = tt := rfl -example : le 1 3 = tt := rfl +example : num.le 1 0 = ff := rfl +example : num.le 1 1 = tt := rfl +example : num.le 1 2 = tt := rfl +example : num.le 1 3 = tt := rfl -example : le 2 0 = ff := rfl -example : le 2 1 = ff := rfl -example : le 2 2 = tt := rfl -example : le 2 3 = tt := rfl -example : le 2 4 = tt := rfl -example : le 2 5 = tt := rfl +example : num.le 2 0 = ff := rfl +example : num.le 2 1 = ff := rfl +example : num.le 2 2 = tt := rfl +example : num.le 2 3 = tt := rfl +example : num.le 2 4 = tt := rfl +example : num.le 2 5 = tt := rfl -example : le 3 0 = ff := rfl -example : le 3 1 = ff := rfl -example : le 3 2 = ff := rfl -example : le 3 3 = tt := rfl -example : le 3 4 = tt := rfl -example : le 3 5 = tt := rfl +example : num.le 3 0 = ff := rfl +example : num.le 3 1 = ff := rfl +example : num.le 3 2 = ff := rfl +example : num.le 3 3 = tt := rfl +example : num.le 3 4 = tt := rfl +example : num.le 3 5 = tt := rfl -example : le 4 0 = ff := rfl -example : le 4 1 = ff := rfl -example : le 4 2 = ff := rfl -example : le 4 3 = ff := rfl -example : le 4 4 = tt := rfl -example : le 4 5 = tt := rfl +example : num.le 4 0 = ff := rfl +example : num.le 4 1 = ff := rfl +example : num.le 4 2 = ff := rfl +example : num.le 4 3 = ff := rfl +example : num.le 4 4 = tt := rfl +example : num.le 4 5 = tt := rfl -example : le 5 0 = ff := rfl -example : le 5 1 = ff := rfl -example : le 5 2 = ff := rfl -example : le 5 3 = ff := rfl -example : le 5 4 = ff := rfl -example : le 5 5 = tt := rfl -example : le 5 6 = tt := rfl +example : num.le 5 0 = ff := rfl +example : num.le 5 1 = ff := rfl +example : num.le 5 2 = ff := rfl +example : num.le 5 3 = ff := rfl +example : num.le 5 4 = ff := rfl +example : num.le 5 5 = tt := rfl +example : num.le 5 6 = tt := rfl -example : 0 - 0 = 0 := rfl -example : 0 - 1 = 0 := rfl -example : 0 - 2 = 0 := rfl -example : 0 - 3 = 0 := rfl +example : num.sub 0 0 = 0 := rfl +example : num.sub 0 1 = 0 := rfl +example : num.sub 0 2 = 0 := rfl +example : num.sub 0 3 = 0 := rfl -example : 1 - 0 = 1 := rfl -example : 1 - 1 = 0 := rfl -example : 1 - 2 = 0 := rfl -example : 1 - 3 = 0 := rfl +example : num.sub 1 0 = 1 := rfl +example : num.sub 1 1 = 0 := rfl +example : num.sub 1 2 = 0 := rfl +example : num.sub 1 3 = 0 := rfl -example : 2 - 0 = 2 := rfl -example : 2 - 1 = 1 := rfl -example : 2 - 2 = 0 := rfl -example : 2 - 3 = 0 := rfl -example : 2 - 4 = 0 := rfl +example : num.sub 2 0 = 2 := rfl +example : num.sub 2 1 = 1 := rfl +example : num.sub 2 2 = 0 := rfl +example : num.sub 2 3 = 0 := rfl +example : num.sub 2 4 = 0 := rfl -example : 3 - 0 = 3 := rfl -example : 3 - 1 = 2 := rfl -example : 3 - 2 = 1 := rfl -example : 3 - 3 = 0 := rfl -example : 3 - 4 = 0 := rfl -example : 3 - 5 = 0 := rfl +example : num.sub 3 0 = 3 := rfl +example : num.sub 3 1 = 2 := rfl +example : num.sub 3 2 = 1 := rfl +example : num.sub 3 3 = 0 := rfl +example : num.sub 3 4 = 0 := rfl +example : num.sub 3 5 = 0 := rfl -example : 4 - 0 = 4 := rfl -example : 4 - 1 = 3 := rfl -example : 4 - 2 = 2 := rfl -example : 4 - 3 = 1 := rfl -example : 4 - 4 = 0 := rfl -example : 4 - 5 = 0 := rfl +example : num.sub 4 0 = 4 := rfl +example : num.sub 4 1 = 3 := rfl +example : num.sub 4 2 = 2 := rfl +example : num.sub 4 3 = 1 := rfl +example : num.sub 4 4 = 0 := rfl +example : num.sub 4 5 = 0 := rfl -example : 5 - 0 = 5 := rfl -example : 5 - 1 = 4 := rfl -example : 5 - 2 = 3 := rfl -example : 5 - 3 = 2 := rfl -example : 5 - 4 = 1 := rfl -example : 5 - 5 = 0 := rfl +example : num.sub 5 0 = 5 := rfl +example : num.sub 5 1 = 4 := rfl +example : num.sub 5 2 = 3 := rfl +example : num.sub 5 3 = 2 := rfl +example : num.sub 5 4 = 1 := rfl +example : num.sub 5 5 = 0 := rfl -example : 11 - 5 = 6 := rfl -example : 5 - 11 = 0 := rfl -example : 12 - 7 = 5 := rfl -example : 120 - 12 = 108 := rfl -example : 111 - 11 = 100 := rfl +example : num.sub 11 5 = 6 := rfl +example : num.sub 5 11 = 0 := rfl +example : num.sub 12 7 = 5 := rfl +example : num.sub 120 12 = 108 := rfl +example : num.sub 111 11 = 100 := rfl diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index 11fdd9d0d..e22d0401d 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -3,8 +3,8 @@ import logic data.nat data.prod open nat prod open decidable -constant modulo (x : ℕ) (y : ℕ) : ℕ -infixl `mod` := modulo +constant modulo1 (x : ℕ) (y : ℕ) : ℕ +infixl `mod` := modulo1 constant gcd_aux : ℕ × ℕ → ℕ diff --git a/tests/lean/run/one.lean b/tests/lean/run/one.lean index 177d9dc3c..c6dd52c48 100644 --- a/tests/lean/run/one.lean +++ b/tests/lean/run/one.lean @@ -1,8 +1,8 @@ -inductive one.{l} : Type.{max 1 l} := -unit : one.{l} +inductive one1.{l} : Type.{max 1 l} := +unit : one1.{l} set_option pp.universes true -check one +check one1 inductive one2.{l} : Type.{max 1 l} := diff --git a/tests/lean/run/one2.lean b/tests/lean/run/one2.lean index 340c5985f..91d7638b5 100644 --- a/tests/lean/run/one2.lean +++ b/tests/lean/run/one2.lean @@ -1,7 +1,7 @@ import data.num -inductive one.{l} : Type.{l} := -unit : one +inductive one1.{l} : Type.{l} := +unit : one1 inductive pone : Type.{0} := unit : pone @@ -17,7 +17,7 @@ inductive wrap2.{l} (A : Type.{l}) : Type.{max 1 l} := mk : A → wrap2 A set_option pp.universes true -check @one.rec +check @one1.rec check @pone.rec check @two.rec check @wrap.rec diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean index b211b8abf..d821251aa 100644 --- a/tests/lean/run/over_subst.lean +++ b/tests/lean/run/over_subst.lean @@ -15,12 +15,12 @@ namespace int constant int : Type.{1} constant add : int → int → int constant le : int → int → Prop -constant one : int +constant one1 : int infixl `+` := add infix `≤` := le axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c) axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b -definition lt (a b : int) := a + one ≤ b +definition lt (a b : int) := a + one1 ≤ b infix `<` := lt end int @@ -28,5 +28,5 @@ open int open nat open eq theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b := -subst (symm (add_assoc c a one)) (add_le_left H c) +subst (symm (add_assoc c a one1)) (add_le_left H c) end experiment diff --git a/tests/lean/run/pickle1.lean b/tests/lean/run/pickle1.lean index b2916d846..e46590d71 100644 --- a/tests/lean/run/pickle1.lean +++ b/tests/lean/run/pickle1.lean @@ -3,5 +3,5 @@ open encodable decidable bool prod list nat option variable l : list (nat × bool) check encode l eval encode [2, 1] -example : decode (list nat) (encode [1, 1]) = some [1, 1] := +example : decode (list nat) (encode [(1:nat), 1]) = some [1, 1] := rfl diff --git a/tests/lean/run/ppbeta.lean b/tests/lean/run/ppbeta.lean index 1f10bacbc..cfb78da8d 100644 --- a/tests/lean/run/ppbeta.lean +++ b/tests/lean/run/ppbeta.lean @@ -1,9 +1,9 @@ import data.int -open [coercions] int +open [coercions] [classes] int open [coercions] nat -definition lt (a b : int) := int.le (int.add a 1) b -infix `<` := lt +definition lt1 (a b : int) := int.le (int.add a 1) b +infix `<` := lt1 infixl `+` := int.add theorem lt_add_succ2 (a : int) (n : nat) : a < a + nat.succ n := diff --git a/tests/lean/run/ptst.lean b/tests/lean/run/ptst.lean index dd4bdb8a0..af00782a2 100644 --- a/tests/lean/run/ptst.lean +++ b/tests/lean/run/ptst.lean @@ -1,5 +1,5 @@ -import logic data.prod -open prod +import data.nat logic data.prod +open prod nat -- Test tuple notation -check (3, false, 1, true) +check ((3:nat), false, (1:num), true) diff --git a/tests/lean/run/rat_coe.lean b/tests/lean/run/rat_coe.lean index 8f269965a..a911d2aea 100644 --- a/tests/lean/run/rat_coe.lean +++ b/tests/lean/run/rat_coe.lean @@ -1,5 +1,5 @@ import data.rat -open rat +open rat int attribute rat.of_int [coercion] diff --git a/tests/lean/run/rat_rfl.lean b/tests/lean/run/rat_rfl.lean index 068bc12b2..8ba14931d 100644 --- a/tests/lean/run/rat_rfl.lean +++ b/tests/lean/run/rat_rfl.lean @@ -1,7 +1,5 @@ import data.rat open rat -attribute rat.of_int [coercion] - -example : 1 + 2⁻¹ + 3 = 3 + 2⁻¹ + 1⁻¹ := +example : (1:rat) + 2⁻¹ + 3 = 3 + 2⁻¹ + 1⁻¹ := rfl diff --git a/tests/lean/run/reducible.lean b/tests/lean/run/reducible.lean index 5a719cb03..d87258157 100644 --- a/tests/lean/run/reducible.lean +++ b/tests/lean/run/reducible.lean @@ -1,7 +1,9 @@ -definition x [reducible] := 10 -definition y := 20 -definition z [irreducible] := 30 -definition w := 40 +open nat +definition x [reducible] := (10:nat) +definition y := (20:nat) +definition z [irreducible] := (30:nat) +definition w := (40:nat) + (* local env = get_env() @@ -21,8 +23,6 @@ definition w := 40 assert(tc:whnf(w) == w) -- Opaque and definitions marked as irreducibled are not unfolded local tc = non_irreducible_type_checker(env) - assert(tc:whnf(x) == val_x) - assert(tc:whnf(y) == val_y) assert(tc:whnf(z) == z) -- Only definitions marked as reducible are unfolded local tc = reducible_type_checker(env) @@ -30,12 +30,6 @@ definition w := 40 assert(tc:whnf(y) == y) assert(tc:whnf(z) == z) assert(tc:whnf(w) == w) - -- Default: only opaque definitions are not unfolded. - -- Opaqueness is a feature of the kernel. - local tc = type_checker(env) - assert(tc:whnf(x) == val_x) - assert(tc:whnf(y) == val_y) - assert(tc:whnf(z) == val_z) *) eval [whnf] x diff --git a/tests/lean/run/rewrite8.lean b/tests/lean/run/rewrite8.lean index c398f6d3c..b90ced567 100644 --- a/tests/lean/run/rewrite8.lean +++ b/tests/lean/run/rewrite8.lean @@ -3,4 +3,4 @@ open nat constant f : nat → nat theorem tst1 (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y := -by rewrite [▸* at H1, ^add at H1, H1] +by rewrite [▸* at H1, add_zero at H1, H1] diff --git a/tests/lean/run/rewriter12.lean b/tests/lean/run/rewriter12.lean index 82d0c807e..d2575ba8b 100644 --- a/tests/lean/run/rewriter12.lean +++ b/tests/lean/run/rewriter12.lean @@ -3,7 +3,7 @@ open nat constant f : nat → nat example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y := -by rewrite [▸* at H1, ^ [add, nat.rec_on, of_num] at H1, H1] +by rewrite [▸* at H1, add_zero at H1, H1] example (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y := -by rewrite [▸* at H1, ↑[add, nat.rec_on, of_num] at H1, H1] +by rewrite [▸* at H1, add_zero at H1, H1] diff --git a/tests/lean/run/rewriter14.lean b/tests/lean/run/rewriter14.lean index 4672933c4..ddf85622a 100644 --- a/tests/lean/run/rewriter14.lean +++ b/tests/lean/run/rewriter14.lean @@ -8,5 +8,5 @@ attribute of_num [unfold 1] example (x y : nat) (H1 : f x 0 0 = 0) : x = 0 := begin - rewrite [▸* at H1, 4>add_zero at H1, H1] + rewrite [↑f at H1, 4>add_zero at H1, H1] end diff --git a/tests/lean/run/secnot.lean b/tests/lean/run/secnot.lean index 5a7e276f8..e2af2e6f8 100644 --- a/tests/lean/run/secnot.lean +++ b/tests/lean/run/secnot.lean @@ -16,10 +16,10 @@ namespace list section variable {T : Type} notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l -check [10, 20, 30] +check [(10:num), 20, 30] end end list open list -check [10, 20, 40] -check 10 ◀ 20 +check [(10:num), 20, 40] +check (10:num) ◀ 20 diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean index da5048241..afbcc93f7 100644 --- a/tests/lean/run/set.lean +++ b/tests/lean/run/set.lean @@ -1,7 +1,7 @@ import logic -open bool +open bool nat definition set {{T : Type}} := T → bool infix `∈` := λx A, A x = tt -check 1 ∈ (λ x, tt) +check 1 ∈ (λ x : nat, tt) diff --git a/tests/lean/run/show2.lean b/tests/lean/run/show2.lean index bac2639eb..07d3dd57c 100644 --- a/tests/lean/run/show2.lean +++ b/tests/lean/run/show2.lean @@ -1,7 +1,7 @@ import data.nat open nat -example : ∀ a b, a + b = b + a := +example : ∀ a b : nat, a + b = b + a := show ∀ a b : nat, a + b = b + a | 0 0 := rfl | 0 (succ b) := by rewrite zero_add diff --git a/tests/lean/run/st_options.lean b/tests/lean/run/st_options.lean index f59581b23..3dcdee85b 100644 --- a/tests/lean/run/st_options.lean +++ b/tests/lean/run/st_options.lean @@ -1,24 +1,6 @@ set_option structure.eta_thm true set_option structure.proj_mk_thm true -structure has_mul [class] (A : Type) := -(mul : A → A → A) - -structure has_add [class] (A : Type) := -(add : A → A → A) - -structure has_one [class] (A : Type) := -(one : A) - -structure has_zero [class] (A : Type) := -(zero : A) - -structure has_inv [class] (A : Type) := -(inv : A → A) - -structure has_neg [class] (A : Type) := -(neg : A → A) - structure semigroup [class] (A : Type) extends has_mul A := (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)) diff --git a/tests/lean/run/struct_inst_exprs.lean b/tests/lean/run/struct_inst_exprs.lean index 36b310924..8c85a3d77 100644 --- a/tests/lean/run/struct_inst_exprs.lean +++ b/tests/lean/run/struct_inst_exprs.lean @@ -7,11 +7,11 @@ definition s : nat × nat := pair 10 20 structure test := (A : Type) (a : A) (B : A → Type) (b : B a) -definition s2 := ⦃ test, a := 3, b := 10 ⦄ +definition s2 := ⦃ test, a := (3:nat), b := (10:nat) ⦄ eval s2 -definition s3 := {| test, a := 20, s2 |} +definition s3 := {| test, a := (20:nat), s2 |} eval s3 diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 2bbf670c5..0f2673436 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -19,13 +19,12 @@ definition num_to_nat (n : num) : nat := num.rec zero (λ n, pos_num_to_nat n) n attribute num_to_nat [coercion] --- Now we can write 2 + 3, the coercion will be applied -check 2 + 3 +check (2:num) + 3 -- Define an assump as an alias for the eassumption tactic definition assump : tactic := tactic.eassumption -theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) +theorem T1 {p : nat → Prop} {a : nat } (H : p (a+(2:num))) : ∃ x, p (succ x) := by apply exists.intro; assump definition is_zero (n : nat) diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean index 10844e949..90b76db4c 100644 --- a/tests/lean/run/tree.lean +++ b/tests/lean/run/tree.lean @@ -5,8 +5,8 @@ inductive tree (A : Type) := | leaf : A → tree A | node : tree A → tree A → tree A -inductive one.{l} : Type.{max 1 l} := -star : one +inductive one1.{l} : Type.{max 1 l} := +star : one1 set_option pp.universes true @@ -17,7 +17,7 @@ namespace manual variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one1.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -27,7 +27,7 @@ namespace manual definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from tree.rec_on t - (λa, (H (leaf a) one.star, one.star)) + (λa, (H (leaf a) one1.star, one1.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr), diff --git a/tests/lean/run/tree2.lean b/tests/lean/run/tree2.lean index 2d641efb0..42b65fa37 100644 --- a/tests/lean/run/tree2.lean +++ b/tests/lean/run/tree2.lean @@ -5,8 +5,8 @@ inductive tree (A : Type) := | leaf : A → tree A | node : tree A → tree A → tree A -inductive one.{l} : Type.{max 1 l} := -star : one +inductive one1.{l} : Type.{max 1 l} := +star : one1 set_option pp.universes true @@ -17,7 +17,7 @@ namespace tree variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one1.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -27,7 +27,7 @@ namespace tree definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from tree.rec_on t - (λa, (H (leaf a) one.star, one.star)) + (λa, (H (leaf a) one1.star, one1.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr), diff --git a/tests/lean/run/tree3.lean b/tests/lean/run/tree3.lean index cc2f84bcc..7b38d11f0 100644 --- a/tests/lean/run/tree3.lean +++ b/tests/lean/run/tree3.lean @@ -5,8 +5,8 @@ inductive tree (A : Type) := | leaf : A → tree A | node : tree A → tree A → tree A -inductive one.{l} : Type.{max 1 l} := -star : one +inductive one1.{l} : Type.{max 1 l} := +star : one1 set_option pp.universes true @@ -17,7 +17,7 @@ namespace tree variable {A : Type.{l₁}} variable (C : tree A → Type.{l₂}) definition below (t : tree A) : Type := - tree.rec_on t (λ a, one.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) + tree.rec_on t (λ a, one1.{l₂}) (λ t₁ t₂ r₁ r₂, C t₁ × C t₂ × r₁ × r₂) end section @@ -27,7 +27,7 @@ namespace tree definition below_rec_on (t : tree A) (H : Π (n : tree A), below C n → C n) : C t := have general : C t × below C t, from tree.rec_on t - (λa, (H (leaf a) one.star, one.star)) + (λa, (H (leaf a) one1.star, one1.star)) (λ (l r : tree A) (Hl : C l × below C l) (Hr : C r × below C r), have b : below C (node l r), from (pr₁ Hl, pr₁ Hr, pr₂ Hl, pr₂ Hr), diff --git a/tests/lean/run/tree_height.lean b/tests/lean/run/tree_height.lean index af93029df..1a4976950 100644 --- a/tests/lean/run/tree_height.lean +++ b/tests/lean/run/tree_height.lean @@ -1,5 +1,5 @@ import logic data.nat -open eq.ops nat +open eq.ops nat algebra inductive tree (A : Type) := | leaf : A → tree A @@ -27,10 +27,10 @@ lt_succ_of_le (le_max_right (height t₁) (height t₂)) theorem height_lt.trans {A : Type} : transitive (@height_lt A) := inv_image.trans lt height @lt.trans -example : height_lt (leaf 2) (node (leaf 1) (leaf 2)) := +example : height_lt (leaf (2:nat)) (node (leaf 1) (leaf 2)) := !height_lt.node_right -example : height_lt (leaf 2) (node (node (leaf 1) (leaf 2)) (leaf 3)) := +example : height_lt (leaf (2:nat)) (node (node (leaf 1) (leaf 2)) (leaf 3)) := height_lt.trans !height_lt.node_right !height_lt.node_left end tree diff --git a/tests/lean/run/tree_subterm_pred.lean b/tests/lean/run/tree_subterm_pred.lean index 3c8d7df95..95feacd30 100644 --- a/tests/lean/run/tree_subterm_pred.lean +++ b/tests/lean/run/tree_subterm_pred.lean @@ -36,11 +36,11 @@ definition subterm {A : Type} : tree A → tree A → Prop := tc (@direct_subter definition subterm.wf {A : Type} : well_founded (@subterm A) := tc.wf (@direct_subterm.wf A) - -example : subterm (leaf 2) (node (leaf 1) (leaf 2)) := +open nat +example : subterm (leaf (2:nat)) (node (leaf 1) (leaf 2)) := !tc.base !direct_subterm.node_r -example : subterm (leaf 2) (node (node (leaf 1) (leaf 2)) (leaf 3)) := +example : subterm (leaf (2:nat)) (node (node (leaf 1) (leaf 2)) (leaf 3)) := have s₁ : subterm (leaf 2) (node (leaf 1) (leaf 2)), from !tc.base !direct_subterm.node_r, have s₂ : subterm (node (leaf 1) (leaf 2)) (node (node (leaf 1) (leaf 2)) (leaf 3)), from diff --git a/tests/lean/run/trick.lean b/tests/lean/run/trick.lean index 9588d1987..a04787bd7 100644 --- a/tests/lean/run/trick.lean +++ b/tests/lean/run/trick.lean @@ -1,7 +1,7 @@ import logic definition proj1 (x : num) (y : num) := x -definition One := 1 +definition One : num := 1 (* local num = Const("num") diff --git a/tests/lean/run/tt1.lean b/tests/lean/run/tt1.lean index c8a30b668..2ded6fdac 100644 --- a/tests/lean/run/tt1.lean +++ b/tests/lean/run/tt1.lean @@ -1,7 +1,7 @@ import data.prod data.num logic.quantifiers -open prod +open prod nat -check (true, false, 10) +check (true, false, (10:nat)) -- definition a f := f diff --git a/tests/lean/run/unfold_rec.lean b/tests/lean/run/unfold_rec.lean index 4cba6a278..fa4c4cfd1 100644 --- a/tests/lean/run/unfold_rec.lean +++ b/tests/lean/run/unfold_rec.lean @@ -7,8 +7,6 @@ variable {n : nat} theorem tst1 : ∀ n m, succ n + succ m = succ (succ (n + m)) := begin intro n m, - esimp [add], - state, rewrite [succ_add] end diff --git a/tests/lean/run/unzip_bug.lean b/tests/lean/run/unzip_bug.lean index f5fcad27b..914789109 100644 --- a/tests/lean/run/unzip_bug.lean +++ b/tests/lean/run/unzip_bug.lean @@ -10,5 +10,5 @@ definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n (va, vb) := (a :: va, b :: vb) end -example : unzip ((1, 20) :: (2, 30) :: nil) = (1 :: 2 :: nil, 20 :: 30 :: nil) := +example : unzip ((1, 20) :: ((2, 30) : nat × nat) :: nil) = (1 :: 2 :: nil, 20 :: 30 :: nil) := rfl diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean index a02d78c6d..6c270907c 100644 --- a/tests/lean/run/vector.lean +++ b/tests/lean/run/vector.lean @@ -75,7 +75,7 @@ namespace vector (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : bw (vcons a₁ v₁)), vcons a₁ (pr₁ B))) - example : append (1 :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil := + example : append ((1:nat) :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil := rfl definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=