max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/lean/run): add three perf tests

Browse source
This commit is contained in:
Daniel Selsam 2016-07-05 17:29:32 -07:00 • committed by Leonardo de Moura
parent ab4e1548f2
commit e8a0abe45e
3 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/perf/perm_ac_commring_50.lean Normal file
View file

@ -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

7
tests/lean/perf/perm_ac_dlof_50.lean Normal file
View file

@ -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

9
tests/lean/perf/perm_ac_op_50.lean Normal file
View file

@ -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