diff options
Diffstat (limited to 'test-suite/complexity/constructor.v')
| -rw-r--r-- | test-suite/complexity/constructor.v | 216 |
1 files changed, 216 insertions, 0 deletions
diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v new file mode 100644 index 00000000..c5e19538 --- /dev/null +++ b/test-suite/complexity/constructor.v @@ -0,0 +1,216 @@ +(* Checks that constructor does not repeat the reduction of the conclusion *) +(* Expected time < 3.00s *) + +(* Note: on i7 2.2GZ, time decreases from 85s to 0.1s *) + +Inductive T : bool -> Prop := +| C000 : T true | C001 : T true | C002 : T true | C003 : T true | C004 : T true +| C005 : T true | C006 : T true | C007 : T true | C008 : T true | C009 : T true +| C010 : T true | C011 : T true | C012 : T true | C013 : T true | C014 : T true +| C015 : T true | C016 : T true | C017 : T true | C018 : T true | C019 : T true +| C020 : T true | C021 : T true | C022 : T true | C023 : T true | C024 : T true +| C025 : T true | C026 : T true | C027 : T true | C028 : T true | C029 : T true +| C030 : T true | C031 : T true | C032 : T true | C033 : T true | C034 : T true +| C035 : T true | C036 : T true | C037 : T true | C038 : T true | C039 : T true +| C040 : T true | C041 : T true | C042 : T true | C043 : T true | C044 : T true +| C045 : T true | C046 : T true | C047 : T true | C048 : T true | C049 : T true +| C050 : T true | C051 : T true | C052 : T true | C053 : T true | C054 : T true +| C055 : T true | C056 : T true | C057 : T true | C058 : T true | C059 : T true +| C060 : T true | C061 : T true | C062 : T true | C063 : T true | C064 : T true +| C065 : T true | C066 : T true | C067 : T true | C068 : T true | C069 : T true +| C070 : T true | C071 : T true | C072 : T true | C073 : T true | C074 : T true +| C075 : T true | C076 : T true | C077 : T true | C078 : T true | C079 : T true +| C080 : T true | C081 : T true | C082 : T true | C083 : T true | C084 : T true +| C085 : T true | C086 : T true | C087 : T true | C088 : T true | C089 : T true +| C090 : T true | C091 : T true | C092 : T true | C093 : T true | C094 : T true +| C095 : T true | C096 : T true | C097 : T true | C098 : T true | C099 : T true +| C100 : T true | C101 : T true | C102 : T true | C103 : T true | C104 : T true +| C105 : T true | C106 : T true | C107 : T true | C108 : T true | C109 : T true +| C110 : T true | C111 : T true | C112 : T true | C113 : T true | C114 : T true +| C115 : T true | C116 : T true | C117 : T true | C118 : T true | C119 : T true +| C120 : T true | C121 : T true | C122 : T true | C123 : T true | C124 : T true +| C125 : T true | C126 : T true | C127 : T true | C128 : T true | C129 : T true +| C130 : T true | C131 : T true | C132 : T true | C133 : T true | C134 : T true +| C135 : T true | C136 : T true | C137 : T true | C138 : T true | C139 : T true +| C140 : T true | C141 : T true | C142 : T true | C143 : T true | C144 : T true +| C145 : T true | C146 : T true | C147 : T true | C148 : T true | C149 : T true +| C150 : T true | C151 : T true | C152 : T true | C153 : T true | C154 : T true +| C155 : T true | C156 : T true | C157 : T true | C158 : T true | C159 : T true +| C160 : T true | C161 : T true | C162 : T true | C163 : T true | C164 : T true +| C165 : T true | C166 : T true | C167 : T true | C168 : T true | C169 : T true +| C170 : T true | C171 : T true | C172 : T true | C173 : T true | C174 : T true +| C175 : T true | C176 : T true | C177 : T true | C178 : T true | C179 : T true +| C180 : T true | C181 : T true | C182 : T true | C183 : T true | C184 : T true +| C185 : T true | C186 : T true | C187 : T true | C188 : T true | C189 : T true +| C190 : T true | C191 : T true | C192 : T true | C193 : T true | C194 : T true +| C195 : T true | C196 : T true | C197 : T true | C198 : T true | C199 : T true +| C200 : T true | C201 : T true | C202 : T true | C203 : T true | C204 : T true +| C205 : T true | C206 : T true | C207 : T true | C208 : T true | C209 : T true +| C210 : T true | C211 : T true | C212 : T true | C213 : T true | C214 : T true +| C215 : T true | C216 : T true | C217 : T true | C218 : T true | C219 : T true +| C220 : T true | C221 : T true | C222 : T true | C223 : T true | C224 : T true +| C225 : T true | C226 : T true | C227 : T true | C228 : T true | C229 : T true +| C230 : T true | C231 : T true | C232 : T true | C233 : T true | C234 : T true +| C235 : T true | C236 : T true | C237 : T true | C238 : T true | C239 : T true +| C240 : T true | C241 : T true | C242 : T true | C243 : T true | C244 : T true +| C245 : T true | C246 : T true | C247 : T true | C248 : T true | C249 : T true +| C250 : T true | C251 : T true | C252 : T true | C253 : T true | C254 : T true +| C255 : T true | C256 : T true | C257 : T true | C258 : T true | C259 : T true +| C260 : T true | C261 : T true | C262 : T true | C263 : T true | C264 : T true +| C265 : T true | C266 : T true | C267 : T true | C268 : T true | C269 : T true +| C270 : T true | C271 : T true | C272 : T true | C273 : T true | C274 : T true +| C275 : T true | C276 : T true | C277 : T true | C278 : T true | C279 : T true +| C280 : T true | C281 : T true | C282 : T true | C283 : T true | C284 : T true +| C285 : T true | C286 : T true | C287 : T true | C288 : T true | C289 : T true +| C290 : T true | C291 : T true | C292 : T true | C293 : T true | C294 : T true +| C295 : T true | C296 : T true | C297 : T true | C298 : T true | C299 : T true +| C300 : T true | C301 : T true | C302 : T true | C303 : T true | C304 : T true +| C305 : T true | C306 : T true | C307 : T true | C308 : T true | C309 : T true +| C310 : T true | C311 : T true | C312 : T true | C313 : T true | C314 : T true +| C315 : T true | C316 : T true | C317 : T true | C318 : T true | C319 : T true +| C320 : T true | C321 : T true | C322 : T true | C323 : T true | C324 : T true +| C325 : T true | C326 : T true | C327 : T true | C328 : T true | C329 : T true +| C330 : T true | C331 : T true | C332 : T true | C333 : T true | C334 : T true +| C335 : T true | C336 : T true | C337 : T true | C338 : T true | C339 : T true +| C340 : T true | C341 : T true | C342 : T true | C343 : T true | C344 : T true +| C345 : T true | C346 : T true | C347 : T true | C348 : T true | C349 : T true +| C350 : T true | C351 : T true | C352 : T true | C353 : T true | C354 : T true +| C355 : T true | C356 : T true | C357 : T true | C358 : T true | C359 : T true +| C360 : T true | C361 : T true | C362 : T true | C363 : T true | C364 : T true +| C365 : T true | C366 : T true | C367 : T true | C368 : T true | C369 : T true +| C370 : T true | C371 : T true | C372 : T true | C373 : T true | C374 : T true +| C375 : T true | C376 : T true | C377 : T true | C378 : T true | C379 : T true +| C380 : T true | C381 : T true | C382 : T true | C383 : T true | C384 : T true +| C385 : T true | C386 : T true | C387 : T true | C388 : T true | C389 : T true +| C390 : T true | C391 : T true | C392 : T true | C393 : T true | C394 : T true +| C395 : T true | C396 : T true | C397 : T true | C398 : T true | C399 : T true +| C400 : T true | C401 : T true | C402 : T true | C403 : T true | C404 : T true +| C405 : T true | C406 : T true | C407 : T true | C408 : T true | C409 : T true +| C410 : T true | C411 : T true | C412 : T true | C413 : T true | C414 : T true +| C415 : T true | C416 : T true | C417 : T true | C418 : T true | C419 : T true +| C420 : T true | C421 : T true | C422 : T true | C423 : T true | C424 : T true +| C425 : T true | C426 : T true | C427 : T true | C428 : T true | C429 : T true +| C430 : T true | C431 : T true | C432 : T true | C433 : T true | C434 : T true +| C435 : T true | C436 : T true | C437 : T true | C438 : T true | C439 : T true +| C440 : T true | C441 : T true | C442 : T true | C443 : T true | C444 : T true +| C445 : T true | C446 : T true | C447 : T true | C448 : T true | C449 : T true +| C450 : T true | C451 : T true | C452 : T true | C453 : T true | C454 : T true +| C455 : T true | C456 : T true | C457 : T true | C458 : T true | C459 : T true +| C460 : T true | C461 : T true | C462 : T true | C463 : T true | C464 : T true +| C465 : T true | C466 : T true | C467 : T true | C468 : T true | C469 : T true +| C470 : T true | C471 : T true | C472 : T true | C473 : T true | C474 : T true +| C475 : T true | C476 : T true | C477 : T true | C478 : T true | C479 : T true +| C480 : T true | C481 : T true | C482 : T true | C483 : T true | C484 : T true +| C485 : T true | C486 : T true | C487 : T true | C488 : T true | C489 : T true +| C490 : T true | C491 : T true | C492 : T true | C493 : T true | C494 : T true +| C495 : T true | C496 : T true | C497 : T true | C498 : T true | C499 : T true +| C500 : T true | C501 : T true | C502 : T true | C503 : T true | C504 : T true +| C505 : T true | C506 : T true | C507 : T true | C508 : T true | C509 : T true +| C510 : T true | C511 : T true | C512 : T true | C513 : T true | C514 : T true +| C515 : T true | C516 : T true | C517 : T true | C518 : T true | C519 : T true +| C520 : T true | C521 : T true | C522 : T true | C523 : T true | C524 : T true +| C525 : T true | C526 : T true | C527 : T true | C528 : T true | C529 : T true +| C530 : T true | C531 : T true | C532 : T true | C533 : T true | C534 : T true +| C535 : T true | C536 : T true | C537 : T true | C538 : T true | C539 : T true +| C540 : T true | C541 : T true | C542 : T true | C543 : T true | C544 : T true +| C545 : T true | C546 : T true | C547 : T true | C548 : T true | C549 : T true +| C550 : T true | C551 : T true | C552 : T true | C553 : T true | C554 : T true +| C555 : T true | C556 : T true | C557 : T true | C558 : T true | C559 : T true +| C560 : T true | C561 : T true | C562 : T true | C563 : T true | C564 : T true +| C565 : T true | C566 : T true | C567 : T true | C568 : T true | C569 : T true +| C570 : T true | C571 : T true | C572 : T true | C573 : T true | C574 : T true +| C575 : T true | C576 : T true | C577 : T true | C578 : T true | C579 : T true +| C580 : T true | C581 : T true | C582 : T true | C583 : T true | C584 : T true +| C585 : T true | C586 : T true | C587 : T true | C588 : T true | C589 : T true +| C590 : T true | C591 : T true | C592 : T true | C593 : T true | C594 : T true +| C595 : T true | C596 : T true | C597 : T true | C598 : T true | C599 : T true +| C600 : T true | C601 : T true | C602 : T true | C603 : T true | C604 : T true +| C605 : T true | C606 : T true | C607 : T true | C608 : T true | C609 : T true +| C610 : T true | C611 : T true | C612 : T true | C613 : T true | C614 : T true +| C615 : T true | C616 : T true | C617 : T true | C618 : T true | C619 : T true +| C620 : T true | C621 : T true | C622 : T true | C623 : T true | C624 : T true +| C625 : T true | C626 : T true | C627 : T true | C628 : T true | C629 : T true +| C630 : T true | C631 : T true | C632 : T true | C633 : T true | C634 : T true +| C635 : T true | C636 : T true | C637 : T true | C638 : T true | C639 : T true +| C640 : T true | C641 : T true | C642 : T true | C643 : T true | C644 : T true +| C645 : T true | C646 : T true | C647 : T true | C648 : T true | C649 : T true +| C650 : T true | C651 : T true | C652 : T true | C653 : T true | C654 : T true +| C655 : T true | C656 : T true | C657 : T true | C658 : T true | C659 : T true +| C660 : T true | C661 : T true | C662 : T true | C663 : T true | C664 : T true +| C665 : T true | C666 : T true | C667 : T true | C668 : T true | C669 : T true +| C670 : T true | C671 : T true | C672 : T true | C673 : T true | C674 : T true +| C675 : T true | C676 : T true | C677 : T true | C678 : T true | C679 : T true +| C680 : T true | C681 : T true | C682 : T true | C683 : T true | C684 : T true +| C685 : T true | C686 : T true | C687 : T true | C688 : T true | C689 : T true +| C690 : T true | C691 : T true | C692 : T true | C693 : T true | C694 : T true +| C695 : T true | C696 : T true | C697 : T true | C698 : T true | C699 : T true +| C700 : T true | C701 : T true | C702 : T true | C703 : T true | C704 : T true +| C705 : T true | C706 : T true | C707 : T true | C708 : T true | C709 : T true +| C710 : T true | C711 : T true | C712 : T true | C713 : T true | C714 : T true +| C715 : T true | C716 : T true | C717 : T true | C718 : T true | C719 : T true +| C720 : T true | C721 : T true | C722 : T true | C723 : T true | C724 : T true +| C725 : T true | C726 : T true | C727 : T true | C728 : T true | C729 : T true +| C730 : T true | C731 : T true | C732 : T true | C733 : T true | C734 : T true +| C735 : T true | C736 : T true | C737 : T true | C738 : T true | C739 : T true +| C740 : T true | C741 : T true | C742 : T true | C743 : T true | C744 : T true +| C745 : T true | C746 : T true | C747 : T true | C748 : T true | C749 : T true +| C750 : T true | C751 : T true | C752 : T true | C753 : T true | C754 : T true +| C755 : T true | C756 : T true | C757 : T true | C758 : T true | C759 : T true +| C760 : T true | C761 : T true | C762 : T true | C763 : T true | C764 : T true +| C765 : T true | C766 : T true | C767 : T true | C768 : T true | C769 : T true +| C770 : T true | C771 : T true | C772 : T true | C773 : T true | C774 : T true +| C775 : T true | C776 : T true | C777 : T true | C778 : T true | C779 : T true +| C780 : T true | C781 : T true | C782 : T true | C783 : T true | C784 : T true +| C785 : T true | C786 : T true | C787 : T true | C788 : T true | C789 : T true +| C790 : T true | C791 : T true | C792 : T true | C793 : T true | C794 : T true +| C795 : T true | C796 : T true | C797 : T true | C798 : T true | C799 : T true +| C800 : T true | C801 : T true | C802 : T true | C803 : T true | C804 : T true +| C805 : T true | C806 : T true | C807 : T true | C808 : T true | C809 : T true +| C810 : T true | C811 : T true | C812 : T true | C813 : T true | C814 : T true +| C815 : T true | C816 : T true | C817 : T true | C818 : T true | C819 : T true +| C820 : T true | C821 : T true | C822 : T true | C823 : T true | C824 : T true +| C825 : T true | C826 : T true | C827 : T true | C828 : T true | C829 : T true +| C830 : T true | C831 : T true | C832 : T true | C833 : T true | C834 : T true +| C835 : T true | C836 : T true | C837 : T true | C838 : T true | C839 : T true +| C840 : T true | C841 : T true | C842 : T true | C843 : T true | C844 : T true +| C845 : T true | C846 : T true | C847 : T true | C848 : T true | C849 : T true +| C850 : T true | C851 : T true | C852 : T true | C853 : T true | C854 : T true +| C855 : T true | C856 : T true | C857 : T true | C858 : T true | C859 : T true +| C860 : T true | C861 : T true | C862 : T true | C863 : T true | C864 : T true +| C865 : T true | C866 : T true | C867 : T true | C868 : T true | C869 : T true +| C870 : T true | C871 : T true | C872 : T true | C873 : T true | C874 : T true +| C875 : T true | C876 : T true | C877 : T true | C878 : T true | C879 : T true +| C880 : T true | C881 : T true | C882 : T true | C883 : T true | C884 : T true +| C885 : T true | C886 : T true | C887 : T true | C888 : T true | C889 : T true +| C890 : T true | C891 : T true | C892 : T true | C893 : T true | C894 : T true +| C895 : T true | C896 : T true | C897 : T true | C898 : T true | C899 : T true +| C900 : T true | C901 : T true | C902 : T true | C903 : T true | C904 : T true +| C905 : T true | C906 : T true | C907 : T true | C908 : T true | C909 : T true +| C910 : T true | C911 : T true | C912 : T true | C913 : T true | C914 : T true +| C915 : T true | C916 : T true | C917 : T true | C918 : T true | C919 : T true +| C920 : T true | C921 : T true | C922 : T true | C923 : T true | C924 : T true +| C925 : T true | C926 : T true | C927 : T true | C928 : T true | C929 : T true +| C930 : T true | C931 : T true | C932 : T true | C933 : T true | C934 : T true +| C935 : T true | C936 : T true | C937 : T true | C938 : T true | C939 : T true +| C940 : T true | C941 : T true | C942 : T true | C943 : T true | C944 : T true +| C945 : T true | C946 : T true | C947 : T true | C948 : T true | C949 : T true +| C950 : T true | C951 : T true | C952 : T true | C953 : T true | C954 : T true +| C955 : T true | C956 : T true | C957 : T true | C958 : T true | C959 : T true +| C960 : T true | C961 : T true | C962 : T true | C963 : T true | C964 : T true +| C965 : T true | C966 : T true | C967 : T true | C968 : T true | C969 : T true +| C970 : T true | C971 : T true | C972 : T true | C973 : T true | C974 : T true +| C975 : T true | C976 : T true | C977 : T true | C978 : T true | C979 : T true +| C980 : T true | C981 : T true | C982 : T true | C983 : T true | C984 : T true +| C985 : T true | C986 : T true | C987 : T true | C988 : T true | C989 : T true +| C990 : T true | C991 : T true | C992 : T true | C993 : T true | C994 : T true +| C995 : T true | C996 : T true | C997 : T true | C998 : T true | C999 : T true +| C1000 : T false. + +Fixpoint expand (n : nat) : Prop := + match n with + | O => T false + | S n => expand n + end. + +Example Expand : expand 2500. +Time constructor. (* ~0.45 secs *) |