From e8a0abe45ec196e775d421b2d42a75aa254f7a15 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 5 Jul 2016 17:29:32 -0700 Subject: [PATCH] test(tests/lean/run): add three perf tests --- tests/lean/perf/perm_ac_commring_50.lean | 7 +++++++ tests/lean/perf/perm_ac_dlof_50.lean | 7 +++++++ tests/lean/perf/perm_ac_op_50.lean | 9 +++++++++ 3 files changed, 23 insertions(+) create mode 100644 tests/lean/perf/perm_ac_commring_50.lean create mode 100644 tests/lean/perf/perm_ac_dlof_50.lean create mode 100644 tests/lean/perf/perm_ac_op_50.lean diff --git a/tests/lean/perf/perm_ac_commring_50.lean b/tests/lean/perf/perm_ac_commring_50.lean new file mode 100644 index 0000000000..ea415d8a2f --- /dev/null +++ b/tests/lean/perf/perm_ac_commring_50.lean @@ -0,0 +1,7 @@ +import algebra.ring +open tactic simplifier.ac +constants (A : Type.{1}) (A_inst : comm_ring A) +attribute A_inst [instance] +set_option simplify.max_steps 1000000 +constants (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 : A) +example : x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21 + x22 + x23 + x24 + x25 + x26 + x27 + x28 + x29 + x30 + x31 + x32 + x33 + x34 + x35 + x36 + x37 + x38 + x39 + x40 + x41 + x42 + x43 + x44 + x45 + x46 + x47 + x48 + x49 + x50 + 0 = x50 + x49 + x48 + x47 + x46 + x45 + x44 + x43 + x42 + x41 + x40 + x39 + x38 + x37 + x36 + x35 + x34 + x33 + x32 + x31 + x30 + x29 + x28 + x27 + x26 + x25 + x24 + x23 + x22 + x21 + x20 + x19 + x18 + x17 + x16 + x15 + x14 + x13 + x12 + x11 + x10 + x9 + x8 + x7 + x6 + x5 + x4 + x3 + x2 + x1 + x0 + 0 := by simp >> triv diff --git a/tests/lean/perf/perm_ac_dlof_50.lean b/tests/lean/perf/perm_ac_dlof_50.lean new file mode 100644 index 0000000000..d666d61148 --- /dev/null +++ b/tests/lean/perf/perm_ac_dlof_50.lean @@ -0,0 +1,7 @@ +import algebra.ordered_field +open tactic simplifier.ac +constants (A : Type.{1}) (A_inst : discrete_linear_ordered_field A) +attribute A_inst [instance] +set_option simplify.max_steps 1000000 +constants (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 : A) +example : x0 + x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 + x11 + x12 + x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 + x21 + x22 + x23 + x24 + x25 + x26 + x27 + x28 + x29 + x30 + x31 + x32 + x33 + x34 + x35 + x36 + x37 + x38 + x39 + x40 + x41 + x42 + x43 + x44 + x45 + x46 + x47 + x48 + x49 + x50 + 0 = x50 + x49 + x48 + x47 + x46 + x45 + x44 + x43 + x42 + x41 + x40 + x39 + x38 + x37 + x36 + x35 + x34 + x33 + x32 + x31 + x30 + x29 + x28 + x27 + x26 + x25 + x24 + x23 + x22 + x21 + x20 + x19 + x18 + x17 + x16 + x15 + x14 + x13 + x12 + x11 + x10 + x9 + x8 + x7 + x6 + x5 + x4 + x3 + x2 + x1 + x0 + 0 := by simp >> triv diff --git a/tests/lean/perf/perm_ac_op_50.lean b/tests/lean/perf/perm_ac_op_50.lean new file mode 100644 index 0000000000..106febafb1 --- /dev/null +++ b/tests/lean/perf/perm_ac_op_50.lean @@ -0,0 +1,9 @@ +open tactic +constants (A : Type.{1}) +constants (op : A → A → A) (op.comm : ∀ x y, op x y = op y x) (op.assoc : ∀ x y z, op (op x y) z = op x (op y z)) (op.left_comm : ∀ x y z, op x (op y z) = op y (op x z)) +attribute op.comm [simp] +attribute op.assoc [simp] +attribute op.left_comm [simp] +set_option simplify.max_steps 1000000 +constants (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 : A) +example : (op x1 (op x2 (op x3 (op x4 (op x5 (op x6 (op x7 (op x8 (op x9 (op x10 (op x11 (op x12 (op x13 (op x14 (op x15 (op x16 (op x17 (op x18 (op x19 (op x20 (op x21 (op x22 (op x23 (op x24 (op x25 (op x26 (op x27 (op x28 (op x29 (op x30 (op x31 (op x32 (op x33 (op x34 (op x35 (op x36 (op x37 (op x38 (op x39 (op x40 (op x41 (op x42 (op x43 (op x44 (op x45 (op x46 (op x47 (op x48 (op x49 (op x50 x0)))))))))))))))))))))))))))))))))))))))))))))))))) = (op x50 (op x49 (op x48 (op x47 (op x46 (op x45 (op x44 (op x43 (op x42 (op x41 (op x40 (op x39 (op x38 (op x37 (op x36 (op x35 (op x34 (op x33 (op x32 (op x31 (op x30 (op x29 (op x28 (op x27 (op x26 (op x25 (op x24 (op x23 (op x22 (op x21 (op x20 (op x19 (op x18 (op x17 (op x16 (op x15 (op x14 (op x13 (op x12 (op x11 (op x10 (op x9 (op x8 (op x7 (op x6 (op x5 (op x4 (op x3 (op x2 (op x1 x0)))))))))))))))))))))))))))))))))))))))))))))))))) := by simp >> triv