diff options
Diffstat (limited to 'test-suite')
71 files changed, 1080 insertions, 1189 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd3..b99d80e95f 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/Makefile b/test-suite/Makefile index c10cd4ed44..39ef05269f 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -31,11 +31,12 @@ BIN := ../bin/ LIB := $(shell cd ..; pwd) coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite -bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite -bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite +coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite +coqtopbyte := $(BIN)coqtop.byte -command := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source -coqc := $(coqtop) -compile +coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source +coqtopcompile := $(coqtop) -compile coqdep := $(BIN)coqdep -coqlib $(LIB) SHOW := $(if $(VERBOSE),@true,@echo) @@ -52,7 +53,7 @@ get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_ # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1))) has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) -get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqc),$(command)) +get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) bogomips:= @@ -219,7 +220,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -249,7 +250,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -405,79 +406,26 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log +misc: $(patsubst %.sh,%.log,$(wildcard misc/*.sh)) -# Check that both coqdep and coqtop/coqc supports -R -# Check that both coqdep and coqtop/coqc takes the later -R -# See bugs 2242, 2337, 2339 -deps-order: misc/deps-order.log -misc/deps-order.log: - @echo "TEST misc/deps-order" - $(HIDE){ \ - echo $(call log_intro,deps-order); \ - rm -f misc/deps/*/*.vo; \ - tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(coqdep) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ - | head -n 1 > $$tmpoutput; \ - diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ - $(bincoqc) -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1; \ - $(bincoqc) -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ - $(coqtop) -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ - S=$$?; times; \ - if [ $$R = 0 -a $$S = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-order...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-order...Error! (unexpected order)"; \ - fi; \ - rm $$tmpoutput; \ - } > "$@" - -deps-checksum: misc/deps-checksum.log -misc/deps-checksum.log: - @echo "TEST misc/deps-checksum" - $(HIDE){ \ - echo $(call log_intro,deps-checksum); \ - rm -f misc/deps/*/*.vo; \ - $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \ - $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \ - $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ - if [ $$? = 0 ]; then \ - echo $(log_success); \ - echo " misc/deps-checksum...Ok"; \ - else \ - echo $(log_failure); \ - echo " misc/deps-checksum...Error!"; \ - fi; \ - } > "$@" - - -# Sort universes for the whole standard library -EXPECTED_UNIVERSES := 4 # Prop is not counted -universes: misc/universes.log -misc/universes.log: misc/universes/all_stdlib.v - @echo "TEST misc/universes" +$(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) + @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -R misc/universes Universes misc/universes/all_stdlib 2>&1; \ - $(bincoqc) -R misc/universes Universes misc/universes/universes 2>&1; \ - mv universes.txt misc/universes; \ - N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ - times; \ - if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \ + echo $(call log_intro,$<); \ + export coqc="$(coqc)"; \ + export coqtop="$(coqtop)"; \ + export coqdep="$(coqdep)"; \ + export coqtopbyte="$(coqtopbyte)"; \ + "$<" 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ echo $(log_success); \ - echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \ + echo " $<...Ok"; \ else \ echo $(log_failure); \ - echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \ + echo " $<...Error!"; \ fi; \ } > "$@" -misc/universes/all_stdlib.v: - cd .. && $(MAKE) test-suite/$@ - - # IDE : some tests of backtracking for coqtop -ideslave ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @@ -501,9 +449,9 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) %.vio.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -quick -R vio vio $* 2>&1 && \ + $(coqc) -quick -R vio vio $* 2>&1 && \ $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \ - $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ + $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -518,8 +466,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v)) %.chk.log:%.v @echo "TEST $<" $(HIDE){ \ - $(bincoqc) -R coqchk coqchk $* 2>&1 && \ - $(bincoqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ + $(coqc) -R coqchk coqchk $* 2>&1 && \ + $(coqchk) -R coqchk coqchk -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v deleted file mode 100644 index 5c64716c72..0000000000 --- a/test-suite/bench/lists-100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v deleted file mode 100644 index 5c64716c72..0000000000 --- a/test-suite/bench/lists_100.v +++ /dev/null @@ -1,107 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. -Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. -Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. -Inductive list3 : Set := nil3 : list3 | cons3 : Set -> list3 -> list3. -Inductive list4 : Set := nil4 : list4 | cons4 : Set -> list4 -> list4. -Inductive list5 : Set := nil5 : list5 | cons5 : Set -> list5 -> list5. -Inductive list6 : Set := nil6 : list6 | cons6 : Set -> list6 -> list6. -Inductive list7 : Set := nil7 : list7 | cons7 : Set -> list7 -> list7. -Inductive list8 : Set := nil8 : list8 | cons8 : Set -> list8 -> list8. -Inductive list9 : Set := nil9 : list9 | cons9 : Set -> list9 -> list9. -Inductive list10 : Set := nil10 : list10 | cons10 : Set -> list10 -> list10. -Inductive list11 : Set := nil11 : list11 | cons11 : Set -> list11 -> list11. -Inductive list12 : Set := nil12 : list12 | cons12 : Set -> list12 -> list12. -Inductive list13 : Set := nil13 : list13 | cons13 : Set -> list13 -> list13. -Inductive list14 : Set := nil14 : list14 | cons14 : Set -> list14 -> list14. -Inductive list15 : Set := nil15 : list15 | cons15 : Set -> list15 -> list15. -Inductive list16 : Set := nil16 : list16 | cons16 : Set -> list16 -> list16. -Inductive list17 : Set := nil17 : list17 | cons17 : Set -> list17 -> list17. -Inductive list18 : Set := nil18 : list18 | cons18 : Set -> list18 -> list18. -Inductive list19 : Set := nil19 : list19 | cons19 : Set -> list19 -> list19. -Inductive list20 : Set := nil20 : list20 | cons20 : Set -> list20 -> list20. -Inductive list21 : Set := nil21 : list21 | cons21 : Set -> list21 -> list21. -Inductive list22 : Set := nil22 : list22 | cons22 : Set -> list22 -> list22. -Inductive list23 : Set := nil23 : list23 | cons23 : Set -> list23 -> list23. -Inductive list24 : Set := nil24 : list24 | cons24 : Set -> list24 -> list24. -Inductive list25 : Set := nil25 : list25 | cons25 : Set -> list25 -> list25. -Inductive list26 : Set := nil26 : list26 | cons26 : Set -> list26 -> list26. -Inductive list27 : Set := nil27 : list27 | cons27 : Set -> list27 -> list27. -Inductive list28 : Set := nil28 : list28 | cons28 : Set -> list28 -> list28. -Inductive list29 : Set := nil29 : list29 | cons29 : Set -> list29 -> list29. -Inductive list30 : Set := nil30 : list30 | cons30 : Set -> list30 -> list30. -Inductive list31 : Set := nil31 : list31 | cons31 : Set -> list31 -> list31. -Inductive list32 : Set := nil32 : list32 | cons32 : Set -> list32 -> list32. -Inductive list33 : Set := nil33 : list33 | cons33 : Set -> list33 -> list33. -Inductive list34 : Set := nil34 : list34 | cons34 : Set -> list34 -> list34. -Inductive list35 : Set := nil35 : list35 | cons35 : Set -> list35 -> list35. -Inductive list36 : Set := nil36 : list36 | cons36 : Set -> list36 -> list36. -Inductive list37 : Set := nil37 : list37 | cons37 : Set -> list37 -> list37. -Inductive list38 : Set := nil38 : list38 | cons38 : Set -> list38 -> list38. -Inductive list39 : Set := nil39 : list39 | cons39 : Set -> list39 -> list39. -Inductive list40 : Set := nil40 : list40 | cons40 : Set -> list40 -> list40. -Inductive list41 : Set := nil41 : list41 | cons41 : Set -> list41 -> list41. -Inductive list42 : Set := nil42 : list42 | cons42 : Set -> list42 -> list42. -Inductive list43 : Set := nil43 : list43 | cons43 : Set -> list43 -> list43. -Inductive list44 : Set := nil44 : list44 | cons44 : Set -> list44 -> list44. -Inductive list45 : Set := nil45 : list45 | cons45 : Set -> list45 -> list45. -Inductive list46 : Set := nil46 : list46 | cons46 : Set -> list46 -> list46. -Inductive list47 : Set := nil47 : list47 | cons47 : Set -> list47 -> list47. -Inductive list48 : Set := nil48 : list48 | cons48 : Set -> list48 -> list48. -Inductive list49 : Set := nil49 : list49 | cons49 : Set -> list49 -> list49. -Inductive list50 : Set := nil50 : list50 | cons50 : Set -> list50 -> list50. -Inductive list51 : Set := nil51 : list51 | cons51 : Set -> list51 -> list51. -Inductive list52 : Set := nil52 : list52 | cons52 : Set -> list52 -> list52. -Inductive list53 : Set := nil53 : list53 | cons53 : Set -> list53 -> list53. -Inductive list54 : Set := nil54 : list54 | cons54 : Set -> list54 -> list54. -Inductive list55 : Set := nil55 : list55 | cons55 : Set -> list55 -> list55. -Inductive list56 : Set := nil56 : list56 | cons56 : Set -> list56 -> list56. -Inductive list57 : Set := nil57 : list57 | cons57 : Set -> list57 -> list57. -Inductive list58 : Set := nil58 : list58 | cons58 : Set -> list58 -> list58. -Inductive list59 : Set := nil59 : list59 | cons59 : Set -> list59 -> list59. -Inductive list60 : Set := nil60 : list60 | cons60 : Set -> list60 -> list60. -Inductive list61 : Set := nil61 : list61 | cons61 : Set -> list61 -> list61. -Inductive list62 : Set := nil62 : list62 | cons62 : Set -> list62 -> list62. -Inductive list63 : Set := nil63 : list63 | cons63 : Set -> list63 -> list63. -Inductive list64 : Set := nil64 : list64 | cons64 : Set -> list64 -> list64. -Inductive list65 : Set := nil65 : list65 | cons65 : Set -> list65 -> list65. -Inductive list66 : Set := nil66 : list66 | cons66 : Set -> list66 -> list66. -Inductive list67 : Set := nil67 : list67 | cons67 : Set -> list67 -> list67. -Inductive list68 : Set := nil68 : list68 | cons68 : Set -> list68 -> list68. -Inductive list69 : Set := nil69 : list69 | cons69 : Set -> list69 -> list69. -Inductive list70 : Set := nil70 : list70 | cons70 : Set -> list70 -> list70. -Inductive list71 : Set := nil71 : list71 | cons71 : Set -> list71 -> list71. -Inductive list72 : Set := nil72 : list72 | cons72 : Set -> list72 -> list72. -Inductive list73 : Set := nil73 : list73 | cons73 : Set -> list73 -> list73. -Inductive list74 : Set := nil74 : list74 | cons74 : Set -> list74 -> list74. -Inductive list75 : Set := nil75 : list75 | cons75 : Set -> list75 -> list75. -Inductive list76 : Set := nil76 : list76 | cons76 : Set -> list76 -> list76. -Inductive list77 : Set := nil77 : list77 | cons77 : Set -> list77 -> list77. -Inductive list78 : Set := nil78 : list78 | cons78 : Set -> list78 -> list78. -Inductive list79 : Set := nil79 : list79 | cons79 : Set -> list79 -> list79. -Inductive list80 : Set := nil80 : list80 | cons80 : Set -> list80 -> list80. -Inductive list81 : Set := nil81 : list81 | cons81 : Set -> list81 -> list81. -Inductive list82 : Set := nil82 : list82 | cons82 : Set -> list82 -> list82. -Inductive list83 : Set := nil83 : list83 | cons83 : Set -> list83 -> list83. -Inductive list84 : Set := nil84 : list84 | cons84 : Set -> list84 -> list84. -Inductive list85 : Set := nil85 : list85 | cons85 : Set -> list85 -> list85. -Inductive list86 : Set := nil86 : list86 | cons86 : Set -> list86 -> list86. -Inductive list87 : Set := nil87 : list87 | cons87 : Set -> list87 -> list87. -Inductive list88 : Set := nil88 : list88 | cons88 : Set -> list88 -> list88. -Inductive list89 : Set := nil89 : list89 | cons89 : Set -> list89 -> list89. -Inductive list90 : Set := nil90 : list90 | cons90 : Set -> list90 -> list90. -Inductive list91 : Set := nil91 : list91 | cons91 : Set -> list91 -> list91. -Inductive list92 : Set := nil92 : list92 | cons92 : Set -> list92 -> list92. -Inductive list93 : Set := nil93 : list93 | cons93 : Set -> list93 -> list93. -Inductive list94 : Set := nil94 : list94 | cons94 : Set -> list94 -> list94. -Inductive list95 : Set := nil95 : list95 | cons95 : Set -> list95 -> list95. -Inductive list96 : Set := nil96 : list96 | cons96 : Set -> list96 -> list96. -Inductive list97 : Set := nil97 : list97 | cons97 : Set -> list97 -> list97. -Inductive list98 : Set := nil98 : list98 | cons98 : Set -> list98 -> list98. -Inductive list99 : Set := nil99 : list99 | cons99 : Set -> list99 -> list99. diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 0000000000..b2f00ffc65 --- /dev/null +++ b/test-suite/bugs/closed/2417.v @@ -0,0 +1,15 @@ +Parameter x y : nat. +Axiom H : x = y. +Hint Rewrite H : mybase. + +Ltac bar base := autorewrite with base. + +Tactic Notation "foo" ident(base) := autorewrite with base. + +Goal x = 0. + bar mybase. + now_show (y = 0). + Undo 2. + foo mybase. + now_show (y = 0). +Abort. diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v deleted file mode 100644 index da0cc68a4e..0000000000 --- a/test-suite/bugs/closed/2640.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Testing consistency of globalization and interpretation in some - extreme cases *) - -Section sect. - - (* Simplification of the initial example *) - Hypothesis Other: True. - - Lemma C2 : True. - proof. - Fail have True using Other. - Abort. - - (* Variant of the same problem *) - Lemma C2 : True. - Fail clear; Other. - Abort. diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 90182a4881..73709268a4 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index 367d380ec3..179f81e668 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -2,7 +2,9 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). Delimit Scope type_scope with type. diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index a8bf950ff2..b236846710 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -4,6 +4,8 @@ Unset Strict Universe Declaration. (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) +Declare ML Module "ltac_plugin". + Set Universe Polymorphism. Class Contr_internal (A : Type) := BuildContr { center : A }. Arguments center A {_}. @@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}. Check @contr_paths_contr0@{i}. Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *) -(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file +(** It should have length 1, just like contr_paths_contr0 *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 4fab9d44f3..117d6523a8 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -5,6 +5,7 @@ then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index ccef1c3040..c3e0da1117 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -5,6 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -223,4 +224,4 @@ v = _) r, | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" | [ |- ?G ] => fail 1 "bad" G end. - Fail rewrite concat_p_pp.
\ No newline at end of file + Fail rewrite concat_p_pp. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 82f1e3fe73..4ad53bc629 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -1004,4 +1005,4 @@ Proof. Fail Timeout 1 Time rewrite !loops_functor_group. (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) Timeout 1 do 3 rewrite loops_functor_group. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v new file mode 100644 index 0000000000..f7cec1a0cf --- /dev/null +++ b/test-suite/bugs/closed/5219.v @@ -0,0 +1,10 @@ +(* Test surgical use of beta-iota in the type of variables coming from + pattern-matching for refine *) + +Goal forall x : sigT (fun x => x = 1), True. + intro x; refine match x with + | existT _ x' e' => _ + end. + lazymatch goal with + | [ H : _ = _ |- _ ] => idtac + end. diff --git a/test-suite/bugs/closed/5277.v b/test-suite/bugs/closed/5277.v new file mode 100644 index 0000000000..7abc38bfce --- /dev/null +++ b/test-suite/bugs/closed/5277.v @@ -0,0 +1,11 @@ +(* Scheme Equality not robust wrt names *) + +Module A1. + Inductive A (T : Type) := C (a : T). + Scheme Equality for A. (* success *) +End A1. + +Module A2. + Inductive A (x : Type) := C (a : x). + Scheme Equality for A. +End A2. diff --git a/test-suite/bugs/closed/5321.v b/test-suite/bugs/closed/5321.v new file mode 100644 index 0000000000..03514e23b1 --- /dev/null +++ b/test-suite/bugs/closed/5321.v @@ -0,0 +1,18 @@ +Definition proj1_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v) + : proj1_sig u = proj1_sig v + := f_equal (@proj1_sig _ _) p. + +Definition proj2_sig_path {A} {P : A -> Prop} {u v : sig P} (p : u = v) + : eq_rect _ _ (proj2_sig u) _ (proj1_sig_path p) = proj2_sig v + := match p with eq_refl => eq_refl end. + +Goal forall sz : nat, + let sz' := sz in + forall pf : sz = sz', + let feq_refl := exist (fun x : nat => sz = x) sz' eq_refl in + let fpf := exist (fun x : nat => sz = x) sz' pf in feq_refl = fpf -> +proj2_sig feq_refl = proj2_sig fpf. +Proof. + intros. + etransitivity; [ | exact (proj2_sig_path H) ]. + Fail clearbody fpf. diff --git a/test-suite/bugs/closed/5359.v b/test-suite/bugs/closed/5359.v new file mode 100644 index 0000000000..87e69565e3 --- /dev/null +++ b/test-suite/bugs/closed/5359.v @@ -0,0 +1,218 @@ +Require Import Coq.nsatz.Nsatz. +Goal False. + + (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *) + let sugar := constr:( 0%Z ) in + let nparams := constr:( (-1)%Z ) in + let reified_goal := constr:( + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) ) in + let power := constr:( N.one ) in + let reified_givens := constr:( + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 9)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) (Ring_polynom.PEX Z 8))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3)))) :: nil)%list ) in + Nsatz.nsatz_compute + (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). + + let sugar := constr:( 0%Z ) in + let nparams := constr:( (-1)%Z ) in + let reified_goal := constr:( + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) ) in + let power := constr:( N.one ) in + let reified_givens := constr:( + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + :: Ring_polynom.PEadd + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 6)) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 5)))) (Ring_polynom.PEX Z 7)) + (Ring_polynom.PEsub + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 6)) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)))) + (Ring_polynom.PEX Z 8)) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) (Ring_polynom.PEX Z 9)) + (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3)))) :: nil)%list ) in + Nsatz.nsatz_compute + (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v new file mode 100644 index 0000000000..d7fc2aaa00 --- /dev/null +++ b/test-suite/bugs/closed/5449.v @@ -0,0 +1,6 @@ +(* An example of decide equality which was failing due to a lhs dep into the rhs *) + +Require Import Coq.PArith.BinPos. +Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}. +intros. +decide equality. diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v new file mode 100644 index 0000000000..b2d9d943bc --- /dev/null +++ b/test-suite/bugs/closed/5476.v @@ -0,0 +1,28 @@ +Require Setoid. + +Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ : +Prop, Prop) + (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop) + (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ : +T) (_ : Prop), Prop) + (o : forall _ : P0, option T1) + (_ : P3 + (fun (k : P0) (_ : T0) (_ : Prop) => + match o k return Prop with + | Some _ => True + | None => False + end) m' P) (_ : P2 (P1 x0 m)) + (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2 +: T) + (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P) +(f k e (P3 f m1 P))), False. +Proof. + intros ???????????? H0 H H1. + rewrite H1 in H0; eauto with nocore. + { lazymatch goal with + | H : match ?X with _ => _ end |- _ + => first [ lazymatch goal with + | [ H' : context[X] |- _ ] => idtac H + end + | fail 1 "could not find" X ] + end. diff --git a/test-suite/bugs/closed/5501.v b/test-suite/bugs/closed/5501.v new file mode 100644 index 0000000000..24739a3658 --- /dev/null +++ b/test-suite/bugs/closed/5501.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. + +Record Pred@{A} := + { car :> Type@{A} + ; P : car -> Prop + }. + +Class All@{A} (A : Pred@{A}) : Type := + { proof : forall (a : A), P A a + }. + +Record Pred_All@{A} : Type := + { P' :> Pred@{A} + ; P'_All : All P' + }. + +Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A. + +Definition Pred_All_proof {A : Pred_All} (a : A) : P A a. +Proof. +solve[auto using proof]. diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index b62f9b6867..bb9579d487 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,6 +1,5 @@ -(* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic - in Prop *) +(* This was working in version 8.1beta (bug in template polymorphism), + but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop with bool : Type := true : bool | false : bool. diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v deleted file mode 100644 index ea3920551d..0000000000 --- a/test-suite/ide/undo.v +++ /dev/null @@ -1,103 +0,0 @@ -(* Here are a sequences of scripts to test interactively with undo and - replay in coqide proof sessions *) - -(* Undoing arbitrary commands, as first step *) - -Theorem a : O=O. (* 2 *) -Ltac f x := x. (* 1 * 3 *) -assert True by trivial. -trivial. -Qed. - -(* Undoing arbitrary commands, as non-first step *) - -Theorem b : O=O. -assert True by trivial. -Ltac g x := x. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* was bugged in 8.1 *) - -Theorem c : O=O. -Inductive T : Type := I. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* new in 8.2 *) - -Theorem d : O=O. -Definition e := O. -Definition f := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as non-first step *) -(* new in 8.2 *) - -Theorem h : O=O. -assert True by trivial. -Definition i := O. -Definition j := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps *) -(* new in 8.2 *) - -Theorem k : O=O. -assert True by trivial. -Definition l := O. -assert True by trivial. -Definition m := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps and commands *) -(* new in 8.2 *) - -Theorem n : O=O. -assert True by trivial. -Definition o := O. -Ltac h x := x. -assert True by trivial. -Focus. -Definition p := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, not in proof *) - -Definition q := O. -Definition r := O. - -(* Bug 2082 : Follow the numbers *) -(* Broken due to proof engine rewriting *) - -Variable A : Prop. -Variable B : Prop. - -Axiom OR : A \/ B. - -Lemma MyLemma2 : True. -proof. -per cases of (A \/ B) by OR. -suppose A. - then (1 = 1). - then H1 : thesis. (* 4 *) - thus thesis by H1. (* 2 *) -suppose B. (* 1 *) (* 3 *) - then (1 = 1). - then H2 : thesis. - thus thesis by H2. -end cases. -end proof. -Qed. (* 5 if you made it here, there is no regression *) - diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake deleted file mode 100644 index 0be439b272..0000000000 --- a/test-suite/ide/undo011.fake +++ /dev/null @@ -1,34 +0,0 @@ -# Script simulating a dialog between coqide and coqtop -ideslave -# Run it via fake_ide -# -# Bug 2082 -# Broken due to proof engine rewriting -# -ADD { Variable A : Prop. } -ADD { Variable B : Prop. } -ADD { Axiom OR : A \/ B. } -ADD { Lemma MyLemma2 : True. } -ADD { proof. } -ADD { per cases of (A \/ B) by OR. } -ADD { suppose A. } -ADD { then (1 = 1). } -ADD there { then H1 : thesis. } -ADD here { thus thesis by H1. } -ADD { suppose B. } -QUERY { Show. } -EDIT_AT here -# <replay> -ADD { suppose B. } -# </replay> -EDIT_AT there -# <replay> -ADD { thus thesis by H1. } -ADD { suppose B. } -# </replay> -QUERY { Show. } -ADD { then (1 = 1). } -ADD { then H2 : thesis. } -ADD { thus thesis by H2. } -ADD { end cases. } -ADD { end proof. } -ADD { Qed. } diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv deleted file mode 100644 index bd1cc49f86..0000000000 --- a/test-suite/kernel/inds.mv +++ /dev/null @@ -1,3 +0,0 @@ -Inductive [] nat : Set := O : nat | S : nat->nat. -Check Construct nat 0 1. -Check Construct nat 0 2. diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v deleted file mode 100644 index a64db4dab7..0000000000 --- a/test-suite/misc/berardi_test.v +++ /dev/null @@ -1,153 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This file formalizes Berardi's paradox which says that in - the calculus of constructions, excluded middle (EM) and axiom of - choice (AC) imply proof irrelevance (PI). - Here, the axiom of choice is not necessary because of the use - of inductive types. -<< -@article{Barbanera-Berardi:JFP96, - author = {F. Barbanera and S. Berardi}, - title = {Proof-irrelevance out of Excluded-middle and Choice - in the Calculus of Constructions}, - journal = {Journal of Functional Programming}, - year = {1996}, - volume = {6}, - number = {3}, - pages = {519-525} -} ->> *) - -Set Implicit Arguments. - -Section Berardis_paradox. - -(** Excluded middle *) -Hypothesis EM : forall P:Prop, P \/ ~ P. - -(** Conditional on any proposition. *) -Definition IFProp (P B:Prop) (e1 e2:P) := - match EM B with - | or_introl _ => e1 - | or_intror _ => e2 - end. - -(** Axiom of choice applied to disjunction. - Provable in Coq because of dependent elimination. *) -Lemma AC_IF : - forall (P B:Prop) (e1 e2:P) (Q:P -> Prop), - (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2). -Proof. -intros P B e1 e2 Q p1 p2. -unfold IFProp. -case (EM B); assumption. -Qed. - - -(** We assume a type with two elements. They play the role of booleans. - The main theorem under the current assumptions is that [T=F] *) -Variable Bool : Prop. -Variable T : Bool. -Variable F : Bool. - -(** The powerset operator *) -Definition pow (P:Prop) := P -> Bool. - - -(** A piece of theory about retracts *) -Section Retracts. - -Variables A B : Prop. - -Record retract : Prop := - {i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}. - -Record retract_cond : Prop := - {i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}. - - -(** The dependent elimination above implies the axiom of choice: *) -Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a. -Proof. -intros r. -case r; simpl. -trivial. -Qed. - -End Retracts. - -(** This lemma is basically a commutation of implication and existential - quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x)) - which is provable in classical logic ( => is already provable in - intuitionnistic logic). *) - -Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B). -Proof. -intros A B. -destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf]. - exists f0 g0; trivial. - exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros; - destruct hf; auto. -Qed. - - -(** The paradoxical set *) -Definition U := forall P:Prop, pow P. - -(** Bijection between [U] and [(pow U)] *) -Definition f (u:U) : pow U := u U. - -Definition g (h:pow U) : U := - fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h). - -(** We deduce that the powerset of [U] is a retract of [U]. - This lemma is stated in Berardi's article, but is not used - afterwards. *) -Lemma retract_pow_U_U : retract (pow U) U. -Proof. -exists g f. -intro a. -unfold f, g; simpl. -apply AC. -exists (fun x:pow U => x) (fun x:pow U => x). -trivial. -Qed. - -(** Encoding of Russel's paradox *) - -(** The boolean negation. *) -Definition Not_b (b:Bool) := IFProp (b = T) F T. - -(** the set of elements not belonging to itself *) -Definition R : U := g (fun u:U => Not_b (u U u)). - - -Lemma not_has_fixpoint : R R = Not_b (R R). -Proof. -unfold R at 1. -unfold g. -rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)). -trivial. -exists (fun x:pow U => x) (fun x:pow U => x); trivial. -Qed. - - -Theorem classical_proof_irrelevence : T = F. -Proof. -generalize not_has_fixpoint. -unfold Not_b. -apply AC_IF. -intros is_true is_false. -elim is_true; elim is_false; trivial. - -intros not_true is_true. -elim not_true; trivial. -Qed. - -End Berardis_paradox. diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh new file mode 100755 index 0000000000..1e2afb7540 --- /dev/null +++ b/test-suite/misc/deps-checksum.sh @@ -0,0 +1,5 @@ +rm -f misc/deps/*/*.vo +$coqc -R misc/deps/A A misc/deps/A/A.v +$coqc -R misc/deps/B A misc/deps/B/A.v +$coqc -R misc/deps/B A misc/deps/B/B.v +$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh new file mode 100755 index 0000000000..375b706f0a --- /dev/null +++ b/test-suite/misc/deps-order.sh @@ -0,0 +1,20 @@ +# Check that both coqdep and coqtop/coqc supports -R +# Check that both coqdep and coqtop/coqc takes the later -R +# See bugs 2242, 2337, 2339 +rm -f misc/deps/*/*.vo +tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput +diff -u misc/deps/deps.out $tmpoutput 2>&1 +R=$? +times +$coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 +$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +S=$? +if [ $R = 0 -a $S = 0 ]; then + printf "coqdep and coqtop agree\n" + exit 0 +else + printf "coqdep and coqtop disagree\n" + exit 1 +fi diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh new file mode 100755 index 0000000000..cea1de862f --- /dev/null +++ b/test-suite/misc/exitstatus.sh @@ -0,0 +1,7 @@ +$coqtop -load-vernac-source misc/exitstatus/illtyped.v +N=$? +$coqc misc/exitstatus/illtyped.v +P=$? +printf "On ill-typed input, coqtop returned $N.\n" +printf "On ill-typed input, coqc returned $P.\n" +if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/exitstatus/illtyped.v b/test-suite/misc/exitstatus/illtyped.v new file mode 100644 index 0000000000..df6bbb389c --- /dev/null +++ b/test-suite/misc/exitstatus/illtyped.v @@ -0,0 +1 @@ +Check S S. diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh new file mode 100755 index 0000000000..c822d0eb37 --- /dev/null +++ b/test-suite/misc/printers.sh @@ -0,0 +1,3 @@ +printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep Unbound +if [ $? = 0 ]; then exit 1; else exit 0; fi + diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh new file mode 100755 index 0000000000..d87a86035c --- /dev/null +++ b/test-suite/misc/universes.sh @@ -0,0 +1,8 @@ +# Sort universes for the whole standard library +EXPECTED_UNIVERSES=4 # Prop is not counted +$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 +$coqc -R misc/universes Universes misc/universes/universes 2>&1 +mv universes.txt misc/universes +N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` +printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index a2ee2d4c8e..979396969a 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -97,8 +97,8 @@ Expands to: Constant Top.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: -Error: Unknown interpretation for notation "$". +Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra arguments: _, _. +Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b084ad4984..4df21ae353 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. @@ -103,15 +103,15 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: Argument lists should agree on the names they provide. +Argument lists should agree on the names they provide. The command has indeed failed with message: -Error: Sequences of implicit arguments must be of different lengths. +Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Error: Some argument names are duplicated: F +Some argument names are duplicated: F The command has indeed failed with message: -Error: Argument z cannot be declared implicit. +Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra arguments: y. +Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out index 851ecd9306..776dfeb550 100644 --- a/test-suite/output/ErrorInModule.out +++ b/test-suite/output/ErrorInModule.out @@ -1,2 +1,3 @@ File "stdin", line 3, characters 20-31: Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out index 851ecd9306..776dfeb550 100644 --- a/test-suite/output/ErrorInSection.out +++ b/test-suite/output/ErrorInSection.out @@ -1,2 +1,3 @@ File "stdin", line 3, characters 20-31: Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 06a6b2d157..38d055b28e 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. -Error: Instance is not well-typed in the environment of ?x. +Instance is not well-typed in the environment of ?x. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 0000000000..8d2a125c1d --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,19 @@ +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Already an intensional equality. +The command has indeed failed with message: +In nested Ltac calls to "extensionality in (var)" and +"clearbody (ne_var_list)", last call failed. +Hypothesis e depends on the body of H' diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v new file mode 100644 index 0000000000..7658ce718e --- /dev/null +++ b/test-suite/output/FunExt.v @@ -0,0 +1,168 @@ +Require Import FunctionalExtensionality. + +(* Basic example *) +Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z). +intro H. +extensionality in H. +symmetry in H. +assumption. +Qed. + +(* Test rejection of non-equality *) +Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''. +intros H H' H''. +Fail extensionality in H. +clear H'. +Fail extensionality in H. +Fail extensionality in H''. +Abort. + +(* Test success on dependent equality *) +Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. +intros p H. +extensionality in p. +assumption. +Qed. + +(* Test dependent functional extensionality *) +Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b), + (forall x y, f x y = g x y) -> f = g. +intros * H. +extensionality in H. +assumption. +Qed. + +(* Other tests, courtesy of Jason Gross *) + +Goal forall A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c), (forall a b c, f a b c = g a b c) -> f = g. +Proof. + intros A B C D f g H. + extensionality in H. + match type of H with f = g => idtac end. + exact H. +Qed. + +Section test_section. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = g a b c). + Goal f = g. + Proof. + extensionality in H. + match type of H with f = g => idtac end. + exact H. + Qed. +End test_section. + +Section test2. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + extensionality in H. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H. + Qed. +End test2. + +Section test3. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a c, (fun b => f a b c) = (fun b => g a b c)). + Goal (fun a c b => f a b c) = (fun a c b => g a b c). + Proof. + extensionality in H. + match type of H with (fun a c b => f a b c) = (fun a' c' b' => g a' b' c') => idtac end. + exact H. + Qed. +End test3. + +Section test4. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c -> Type) + (H : forall b, (forall a c d, f a b c d) = (forall a c d, g a b c d)). + Goal (fun b => forall a c d, f a b c d) = (fun b => forall a c d, g a b c d). + Proof. + extensionality in H. + exact H. + Qed. +End test4. + +Section test5. + Goal nat -> True. + Proof. + intro n. + Fail extensionality in n. + constructor. + Qed. +End test5. + +Section test6. + Goal let f := fun A (x : A) => x in let pf := fun A x => @eq_refl _ (f A x) in f = f. + Proof. + intros f pf. + extensionality in pf. + match type of pf with f = f => idtac end. + exact pf. + Qed. +End test6. + +Section test7. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, True -> f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun a b c (_ : True) => f a b c) = (fun a' b' c' (_ : True) => g a' b' c') => idtac end. + constructor. + Qed. +End test7. + +Section test8. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : True -> forall a b c, f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun (_ : True) => f) = (fun (_ : True) => g) => idtac end. + constructor. + Qed. +End test8. + +Section test9. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + pose H as H'. + extensionality in H. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H'. + Qed. +End test9. + +Section test10. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : f = g). + Goal True. + Proof. + Fail extensionality in H. + constructor. + Qed. +End test10. + +Section test11. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = f a b c). + Goal True. + Proof. + pose H as H'. + pose (eq_refl : H = H') as e. + extensionality in H. + Fail extensionality in H'. + clear e. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + lazymatch type of H with f = f => idtac end. + constructor. + Qed. +End test11. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 26eaca8272..9d106d2dac 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -Error: x should not be bound in a recursive pattern of the right-hand side. +x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: The reference w was not found in the current environment. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -Error: z is expected to occur in binding position in the right-hand side. +z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: -Error: as y is a non-closed binder, no such "," is allowed to occur. +as y is a non-closed binder, no such "," is allowed to occur. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Both ends of the recursive pattern are the same. +Both ends of the recursive pattern are the same. SUM (nat * nat) nat : Set FST (0; 1) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ad60aeccce..1ec701ae81 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index c012a86b01..95be04c32c 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop +fun (pat : nat) '(x, y) => x + y = pat + : nat -> nat * nat -> Prop diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 6fa357a90c..0bad472f41 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). End Suboptimal. + +(** Test risk of collision for internal name *) +Check fun pat => fun '(x,y) => x+y = pat. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index c17b285bc9..7446c17d98 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,108 +1,116 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m +le_n_S: forall n m : nat, n <= m -> S n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n le_ind: forall (n : nat) (P : nat -> Prop), P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 -le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n -le_n_S: forall n m : nat, n <= m -> S n <= S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -true: bool false: bool -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b -bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -andb: bool -> bool -> bool -orb: bool -> bool -> bool -implb: bool -> bool -> bool -xorb: bool -> bool -> bool +true: bool +is_true: bool -> Prop negb: bool -> bool -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true eq_true: bool -> Prop -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +BoolSpec: Prop -> Prop -> bool -> Prop +Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -is_true: bool -> Prop -eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true -eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true -BoolSpec: Prop -> Prop -> bool -> Prop +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool -Nat.even: nat -> bool -Nat.odd: nat -> bool -Nat.testbit: nat -> nat -> bool -Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +n_Sn: forall n : nat, n <> S n pred_Sn: forall n : nat, n = Nat.pred (S n) +O_S: forall n : nat, 0 <> S n +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_S: forall x y : nat, x = y -> S x = S y eq_add_S: forall n m : nat, S n = S m -> n = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y not_eq_S: forall n m : nat, n <> m -> S n <> S m -O_S: forall n : nat, 0 <> S n -n_Sn: forall n : nat, n <> S n +mult_n_Sm: forall n m : nat, n * m + n = n * S m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n -plus_n_Sm: forall n m : nat, S (n + m) = n + S m -plus_Sn_m: forall n m : nat, S n + m = S (n + m) -f_equal2_mult: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true +h: n <> newdef n h': newdef n <> n h: n <> newdef n h': newdef n <> n h: n <> newdef n h: n <> newdef n h: n <> newdef n -h': ~ P n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. h: P n h': ~ P n h: P n h': ~ P n h: P n +h': ~ P n h: P n h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2a0f0b407c..82096f29bf 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. - intros n h h'. + cut False. + intros _ n h h'. Search n. (* search hypothesis *) Search newdef. (* search hypothesis *) Search ( _ <> newdef _). (* search hypothesis, pattern *) Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 0d5924ec61..7038eac22c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -1,39 +1,39 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n le_n_S: forall n m : nat, n <= m -> S n <= S m -true: bool +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +Nat.eqb: nat -> nat -> bool +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y eq_add_S: forall n m : nat, S n = S m -> n = m -f_equal2_plus: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m h: newdef n h: P n diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index f3c12effca..45ff5e73b6 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,77 +1,77 @@ -true: bool false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -O: nat -S: nat -> nat -length: forall A : Type, list A -> nat +Nat.eqb: nat -> nat -> bool +Nat.two: nat Nat.zero: nat Nat.one: nat -Nat.two: nat -Nat.succ: nat -> nat +O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat +Nat.div2: nat -> nat +Nat.log2: nat -> nat Nat.pred: nat -> nat +Nat.square: nat -> nat +S: nat -> nat +Nat.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.sub: nat -> nat -> nat Nat.max: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat Nat.div: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.min: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.div2: nat -> nat +Nat.sqrt: nat -> nat +Nat.log2: nat -> nat +Nat.double: nat -> nat +Nat.pred: nat -> nat +Nat.square: nat -> nat +Nat.succ: nat -> nat +S: nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat -S: nat -> nat -Nat.succ: nat -> nat -Nat.pred: nat -> nat -Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.div: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.div: nat -> nat -> nat Nat.modulo: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat +Nat.max: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -identity_refl: forall (A : Type) (a : A), identity a a iff_refl: forall A : Prop, A <-> A +le_n: forall n : nat, n <= n +identity_refl: forall (A : Type) (a : A), identity a a eq_refl: forall (A : Type) (x : A), x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -le_n: forall n : nat, n <= n -pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat h: n <> newdef n h: n <> newdef n diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out new file mode 100644 index 0000000000..2d4be8bce7 --- /dev/null +++ b/test-suite/output/ShowProof.out @@ -0,0 +1 @@ +(fun x : Type => conj I ?Goal) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 0000000000..73ecaf2200 --- /dev/null +++ b/test-suite/output/ShowProof.v @@ -0,0 +1,6 @@ +(* Was #4524 *) +Definition foo (x : Type) : True /\ True. +Proof. +split. +- exact I. + Show Proof. (* Was not finding an evar name at some time *) diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out new file mode 100644 index 0000000000..a5b55a9993 --- /dev/null +++ b/test-suite/output/auto.out @@ -0,0 +1,20 @@ +(* info auto: *) +simple apply or_intror (in core). + intro. + assumption. +Debug: (* debug auto: *) +Debug: * assumption. (*fail*) +Debug: * intro. (*fail*) +Debug: * simple apply or_intror (in core). (*success*) +Debug: ** assumption. (*fail*) +Debug: ** intro. (*success*) +Debug: ** assumption. (*success*) +(* info eauto: *) +simple apply or_intror. + intro. + exact H. +Debug: (* debug eauto: *) +Debug: 1 depth=5 +Debug: 1.1 depth=4 simple apply or_intror +Debug: 1.1.1 depth=4 intro +Debug: 1.1.1.1 depth=4 exact H diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v new file mode 100644 index 0000000000..a77b7b82e6 --- /dev/null +++ b/test-suite/output/auto.v @@ -0,0 +1,11 @@ +(* testing info/debug auto/eauto *) + +Goal False \/ (True -> True). +info_auto. +Undo. +debug auto. +Undo. +info_eauto. +Undo. +debug eauto. +Qed. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 576fbd7c0b..c70467912f 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n : T n in ?y ?y0 : T n +fun n : nat => let x : T n := A n in ?t ?y : T n : forall n : nat, T n where -?y : [n : nat x := A n : T n |- ?T -> T n] -?y0 : [n : nat x := A n : T n |- ?T] -fun n : nat => ?y ?y0 : T n +?t : [n : nat x := A n : T n |- ?T -> T n] +?y : [n : nat x := A n : T n |- ?T] +fun n : nat => ?t ?y : T n : forall n : nat, T n where -?y : [n : nat |- ?T -> T n] -?y0 : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?y : [n : nat |- ?T] diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 1ff09e3af6..35c3057d84 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,4 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize @@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. Hx nat nat diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..172612405f --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,20 @@ +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing arguments for variables y and _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..8ecd97aa56 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort.
\ No newline at end of file diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out index 9300c3f546..e9c70d1efc 100644 --- a/test-suite/output/qualification.out +++ b/test-suite/output/qualification.out @@ -1,3 +1,4 @@ File "stdin", line 19, characters 0-7: Error: Signature components for label test do not match: expected type "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". + diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index c29e529783..e59828defe 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -1,5 +1,5 @@ (* This used to fail in Coq version 8.1 beta due to a non variable - universe (issued by the inductive sort-polymorphism) being sent by + universe (issued by template polymorphism) being sent by pretyping to the kernel (bug #1182) *) Variable T : Type. diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index a759674115..6abfca4c3f 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -38,3 +38,10 @@ Abort. Goal ~ identity 0 1. discriminate. Qed. + +(* Check discriminate on types with local definitions *) + +Inductive A := B (T := unit) (x y : bool) (z := x). +Goal forall x y, B x true = B y false -> False. +discriminate. +Qed. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index f702aa62f1..f07773f8bd 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (* Test sharing information between different hypotheses *) Parameters (a:_) (b:a=0). + +(* These examples were failing due to a lifting wrongly taking let-in into account *) + +Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl. + +Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index da2183841d..78652fb64b 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -150,6 +150,13 @@ match goal with end. Abort. +(* Injection in the presence of local definitions *) +Inductive A := B (T := unit) (x y : bool) (z := x). +Goal forall x y x' y', B x y = B x' y' -> y = y'. +intros * [= H1 H2]. +exact H2. +Qed. + (* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. diff --git a/test-suite/success/abstract_chain.v b/test-suite/success/abstract_chain.v new file mode 100644 index 0000000000..0ff61e87f8 --- /dev/null +++ b/test-suite/success/abstract_chain.v @@ -0,0 +1,43 @@ +Lemma foo1 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo2 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. + +Set Universe Polymorphism. + +Lemma foo3 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo4 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v new file mode 100644 index 0000000000..fafe272925 --- /dev/null +++ b/test-suite/success/boundvars.v @@ -0,0 +1,14 @@ +(* An example showing a bug in the detection of free variables *) +(* "x" is not free in the common type of "x" and "y" *) + +Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x. + +(* An example showing a bug in the detection of bound variables *) + +Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl. +intro. +match goal with +|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end. +intro. +Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *) +Abort. diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v new file mode 100644 index 0000000000..874abf49f1 --- /dev/null +++ b/test-suite/success/change_pattern.v @@ -0,0 +1,34 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Axiom vector : Type -> nat -> Type. + +Record KleeneStore i j a := kleeneStore + { dim : nat + ; peek : vector j dim -> a + ; pos : vector i dim + }. + +Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b := + kleeneStore (fun v => f (peek v)) (pos s). + +Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg + { coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }. + +Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x). +Axiom t : Type -> Type. +Axiom traverse : KleeneCoalg (fun x => x) t. + +Definition size a (x:t a) : nat := dim (traverse a a x). + +Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False. +Proof. +destruct y. +pose (X := KSmap (traverse a unit) (traverse unit a x)). +set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))). +clearbody e. +(** The pattern generated by change must have holes where there were implicit + arguments in the original user-provided term. This particular example fails + if this is not the case because the inferred argument does not coincide with + the one in the considered term. *) +progress (change (dim (traverse unit a x)) with (dim X) in e). diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v deleted file mode 100644 index 58f79d45ec..0000000000 --- a/test-suite/success/decl_mode.v +++ /dev/null @@ -1,182 +0,0 @@ -(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *) - -Set Firstorder Depth 1. -Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt. - -Lemma double_div2: forall n, div2 (double n) = n. -proof. - assume n:nat. - per induction on n. - suppose it is 0. - suffices (0=0) to show thesis. - thus thesis. - suppose it is (S m) and Hrec:thesis for m. - have (div2 (double (S m))= div2 (S (S (double m)))). - ~= (S (div2 (double m))). - thus ~= (S m) by Hrec. - end induction. -end proof. -Show Script. -Qed. - -Lemma double_inv : forall n m, double n = double m -> n = m . -proof. - let n, m be such that H:(double n = double m). -have (n = div2 (double n)) by double_div2,H. - ~= (div2 (double m)) by H. - thus ~= m by double_div2. -end proof. -Qed. - -Lemma double_mult_l : forall n m, (double (n * m)=n * double m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= (n * (m+m)) by * using ring. - thus ~= (n * double m). -end proof. -Qed. - -Lemma double_mult_r : forall n m, (double (n * m)=double n * m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= ((n + n) * m) by * using ring. - thus ~= (double n * m). -end proof. -Qed. - -Lemma even_is_even_times_even: forall n, even (n*n) -> even n. -proof. - let n be such that H:(even (n*n)). - per cases of (even n \/ odd n) by even_or_odd. - suppose (odd n). - hence thesis by H,even_mult_inv_r. - end cases. -end proof. -Qed. - -Lemma main_thm_aux: forall n,even n -> -double (double (div2 n *div2 n))=n*n. -proof. - given n such that H:(even n). - *** have (double (double (div2 n * div2 n)) - = double (div2 n) * double (div2 n)) - by double_mult_l,double_mult_r. - thus ~= (n*n) by H,even_double. -end proof. -Qed. - -Require Import Omega. - -Lemma even_double_n: (forall m, even (double m)). -proof. - assume m:nat. - per induction on m. - suppose it is 0. - thus thesis. - suppose it is (S mm) and thesis for mm. - then H:(even (S (S (mm+mm)))). - have (S (S (mm + mm)) = S mm + S mm) using omega. - hence (even (S mm +S mm)) by H. - end induction. -end proof. -Qed. - -Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0. -proof. - assume n0:nat. - define P n as (forall p, n*n=double (p*p) -> p=0). - claim rec_step: (forall n, (forall m,m<n-> P m) -> P n). - let n be such that H:(forall m : nat, m < n -> P m) and p:nat . - per cases of ({n=0}+{n<>0}) by eq_nat_dec. - suppose H1:(n=0). - per cases on p. - suppose it is (S p'). - assume (n * n = double (S p' * S p')). - =~ 0 by H1,mult_n_O. - ~= (S ( p' + p' * S p' + S p'* S p')) - by plus_n_Sm. - hence thesis . - suppose it is 0. - thus thesis. - end cases. - suppose H1:(n<>0). - assume H0:(n*n=double (p*p)). - have (even (double (p*p))) by even_double_n . - then (even (n*n)) by H0. - then H2:(even n) by even_is_even_times_even. - then (double (double (div2 n *div2 n))=n*n) - by main_thm_aux. - ~= (double (p*p)) by H0. - then H':(double (div2 n *div2 n)= p*p) by double_inv. - have (even (double (div2 n *div2 n))) by even_double_n. - then (even (p*p)) by even_double_n,H'. - then H3:(even p) by even_is_even_times_even. - have (double(double (div2 n * div2 n)) = n*n) - by H2,main_thm_aux. - ~= (double (p*p)) by H0. - ~= (double(double (double (div2 p * div2 p)))) - by H3,main_thm_aux. - then H'':(div2 n * div2 n = double (div2 p * div2 p)) - by double_inv. - then (div2 n < n) by lt_div2,neq_O_lt,H1. - then H4:(div2 p=0) by (H (div2 n)),H''. - then (double (div2 p) = double 0). - =~ p by even_double,H3. - thus ~= 0. - end cases. - end claim. - hence thesis by (lt_wf_ind n0 P). -end proof. -Qed. - -Require Import Reals Field. -(*Coercion INR: nat >->R. -Coercion IZR: Z >->R.*) - -Open Scope R_scope. - -Lemma square_abs_square: - forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p). -proof. - assume p:Z. - per cases on p. - suppose it is (0%Z). - thus thesis. - suppose it is (Zpos z). - thus thesis. - suppose it is (Zneg z). - have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) = - (IZR (Zpos z) * IZR (Zpos z))). - ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). - thus ~= (IZR (Zneg z) * IZR (Zneg z)). - end cases. -end proof. -Qed. - -Definition irrational (x:R):Prop := - forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q). - -Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)). -proof. - let p:Z,q:nat be such that H:(q<>0%nat) - and H0:(sqrt (INR 2%nat)=(IZR p/INR q)). - have H_in_R:(INR q<>0:>R) by H. - have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. - have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. - have (INR (Z.abs_nat p * Z.abs_nat p) - = (INR (Z.abs_nat p) * INR (Z.abs_nat p))) - by mult_INR. - ~= (IZR p* IZR p) by square_abs_square. - ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) - ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. - ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. - ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. - then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat. - ~= ((q*q)+(q*q))%nat. - ~= (Div2.double (q*q)). - then (q=0%nat) by main_theorem. - hence thesis by H. -end proof. -Qed. diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v deleted file mode 100644 index 46174e4810..0000000000 --- a/test-suite/success/decl_mode2.v +++ /dev/null @@ -1,249 +0,0 @@ -Theorem this_is_trivial: True. -proof. - thus thesis. -end proof. -Qed. - -Theorem T: (True /\ True) /\ True. - split. split. -proof. (* first subgoal *) - thus thesis. -end proof. -trivial. (* second subgoal *) -proof. (* third subgoal *) - thus thesis. -end proof. -Abort. - -Theorem this_is_not_so_trivial: False. -proof. -end proof. (* here a warning is issued *) -Fail Qed. (* fails: the proof in incomplete *) -Admitted. (* Oops! *) - -Theorem T: True. -proof. -escape. -auto. -return. -Abort. - -Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). -intros a b. -proof. -assume H:(if a then True else False). -reconsider H as False. -reconsider thesis as True. -Abort. - -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -have H':(2+x=2+2) by H. -Abort. - -Theorem T: forall x, x=2 -> 2+x=4. -proof. -let x be such that H:(x=2). -then (2+x=2+2). -Abort. - -Theorem T: forall x, x=2 -> x + x = x * x. -proof. -let x be such that H:(x=2). -have (4 = 4). - ~= (2 * 2). - ~= (x * x) by H. - =~ (2 + 2). - =~ H':(x + x) by H. -Abort. - -Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. -proof. -let x be such that H:(x + x = x * x). -claim H':((x - 2) * x = 0). -thus thesis. -end claim. -Abort. - -Theorem T: forall (A B:Prop), A -> B -> A /\ B. -intros A B HA HB. -proof. -hence B. -Abort. - -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. -intros A B C HA HB HC. -proof. -thus B by HB. -Abort. - -Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. -intros A B C HA HB HC. -proof. -Fail hence C. (* fails *) -Abort. - -Theorem T: forall (A B:Prop), B -> A \/ B. -intros A B HB. -proof. -hence B. -Abort. - -Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). -intros A B C D HC HD. -proof. -thus C by HC. -Abort. - -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -take 2. -Abort. - -Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. -intros P HP. -proof. -hence (P 2). -Abort. - -Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. -intros P R HP HR. -proof. -thus (P 2) by HP. -Abort. - -Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. -intros A B P HP HA. -proof. -suffices to have x such that HP':(P x) to show B by HP,HP'. -Abort. - -Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). -intros A P HP HA. -proof. -(* BUG: the next line fails when it should succeed. -Waiting for someone to investigate the bug. -focus on (forall x, x = 2 -> P x). -let x be such that (x = 2). -hence thesis by HP. -end focus. -*) -Abort. - -Theorem T: forall x, x = 0 -> x + x = x * x. -proof. -let x be such that H:(x = 0). -define sqr x as (x * x). -reconsider thesis as (x + x = sqr x). -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -let x:nat. -assume HP:(P x). -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -Fail let x. (* fails because x's type is not clear *) -let x be such that HP:(P x). (* here x's type is inferred from (P x) *) -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. -proof. -let P:(nat -> Prop). -let x:nat. -assume (P x). (* temporary name created *) -Abort. - -Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. -proof. -let P:(nat -> Prop). -let x be such that (P x). (* temporary name created *) -Abort. - -Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. -proof. -let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). -consider x such that HP:(P x) and HA:A from H. -Abort. - -(* Here is an example with pairs: *) - -Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). -proof. -let p:(nat * nat)%type. -consider x:nat,y:nat from p. -reconsider thesis as (x >= y \/ x < y). -Abort. - -Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> -(exists m, P m) -> P 0. -proof. -let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). -given m such that Hm:(P m). -Abort. - -Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. -proof. -let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). -assume HAB:(A \/ B). -per cases on HAB. -suppose A. - hence thesis by HAC. -suppose HB:B. - thus thesis by HB,HBC. -end cases. -Abort. - -Section Coq. - -Hypothesis EM : forall P:Prop, P \/ ~ P. - -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -per cases of (A \/ ~A) by EM. -suppose (~A). - hence thesis by HNAC. -suppose A. - hence thesis by HAC. -end cases. -Abort. - -Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. -proof. -let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). -per cases on (EM A). -suppose (~A). -Abort. -End Coq. - -Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. -proof. -let A:Prop,B:Prop,x:bool. -per cases on x. -suppose it is true. - assume A. - hence A. -suppose it is false. - assume B. - hence B. -end cases. -Abort. - -Theorem T: forall (n:nat), n + 0 = n. -proof. -let n:nat. -per induction on n. -suppose it is 0. - thus (0 + 0 = 0). -suppose it is (S m) and H:thesis for m. - then (S (m + 0) = S m). - thus =~ (S m + 0). -end induction. -Abort.
\ No newline at end of file diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 0000000000..f12b4d1f45 --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,14 @@ +Definition x := 0. + +Hint Unfold x : mybase. + +Ltac autounfoldify base := autounfold with base. + +Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base. + +Goal x = 0. + progress autounfoldify mybase. + Undo. + progress autounfoldify_bis mybase. + trivial. +Qed. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v new file mode 100644 index 0000000000..f5c25540ef --- /dev/null +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -0,0 +1,15 @@ +Parameter Foo : Prop. +Axiom H : Foo. + +Hint Resolve H : mybase. + +Ltac foo base := eauto with base. + +Tactic Notation "bar" ident(base) := + typeclasses eauto with base. + +Goal Foo. + progress foo mybase. + Undo. + progress bar mybase. +Qed.
\ No newline at end of file diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v new file mode 100644 index 0000000000..01e35810b0 --- /dev/null +++ b/test-suite/success/old_typeclass.v @@ -0,0 +1,13 @@ +Require Import Setoid Coq.Classes.Morphisms. +Set Typeclasses Legacy Resolution. + +Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. + +Axiom In : Prop. +Axiom union_spec : In <-> True. + +Lemma foo : In /\ True. +Proof. +progress rewrite union_spec. +repeat constructor. +Qed. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 878875bd92..66ff55edcb 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl. -End Hurkens'.
\ No newline at end of file +End Hurkens'. + +Module Anonymous. + Set Universe Polymorphism. + + Definition defaultid := (fun x => x) : Type -> Type. + Definition collapseid := defaultid@{_ _}. + Check collapseid@{_}. + + Definition anonid := (fun x => x) : Type -> Type@{_}. + Check anonid@{_}. + + Definition defaultalg := (fun x : Type => x) (Type : Type). + Definition usedefaultalg := defaultalg@{_ _ _}. + Check usedefaultalg@{_ _}. + + Definition anonalg := (fun x : Type@{_} => x) (Type : Type). + Check anonalg@{_ _}. + + Definition unrelated@{i j} := nat. + Definition useunrelated := unrelated@{_ _}. + Check useunrelated@{_ _}. + + Definition inthemiddle@{i j k} := + let _ := defaultid@{i j} in + anonalg@{k j}. + (* i <= j < k *) + Definition collapsethemiddle := inthemiddle@{i _ j}. + Check collapsethemiddle@{_ _}. + +End Anonymous. diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v index db2bbb0dc7..07a5bc0606 100644 --- a/test-suite/success/record_syntax.v +++ b/test-suite/success/record_syntax.v @@ -45,3 +45,11 @@ Record Foo := { foo : unit; }. Definition foo_ := {| foo := tt; |}. End E. + +Module F. + +Record Foo := { foo : nat * nat -> nat -> nat }. + +Definition foo_ := {| foo '(x,y) n := x+y+n |}. + +End F. diff --git a/test-suite/success/rewrite_evar.v b/test-suite/success/rewrite_evar.v new file mode 100644 index 0000000000..f7ad261cbb --- /dev/null +++ b/test-suite/success/rewrite_evar.v @@ -0,0 +1,8 @@ +Require Import Coq.Setoids.Setoid. + +Goal forall (T2 MT1 MT2 : Type) (x : T2) (M2 m2 : MT2) (M1 m1 : MT1) (F : T2 -> MT1 -> MT2 -> Prop), + (forall (defaultB : T2) (m3 : MT1) (m4 : MT2), F defaultB m3 m4 <-> True) -> F x M1 M2 -> F x m1 m2. + intros ????????? H' H. + rewrite (H' _) in *. + (** The above rewrite should also rewrite in H. *) + Fail progress rewrite H' in H. diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v new file mode 100644 index 0000000000..ff4509c4a8 --- /dev/null +++ b/test-suite/success/transparent_abstract.v @@ -0,0 +1,21 @@ +Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T. +Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances. + +Goal True /\ True. +Proof. + split. + transparent_abstract exact I using foo. + let x := (eval hnf in foo) in constr_eq x I. + let x := constr:(ltac:(constructor) : True) in + let T := type of x in + let x := constr:(_ : by_transparent_abstract x) in + let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in + pose x as x'. + simpl in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac. + hnf in x'. + let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0. + exact x'. +Defined. +Check eq_refl : I = foo. +Eval compute in foo. diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 296686e16e..6f7498d659 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -188,3 +188,14 @@ Proof. apply idpath. apply idpath. Defined. + +(* An example where it is necessary to evar-normalize the instance of + an evar to evaluate if it is a pattern *) + +Check + let a := ?[P] in + fun (H : forall y (P : nat -> Prop), y = 0 -> P y) + x (p:x=0) => + H ?[y] a p : x = 0. +(* We have to solve "?P ?y[x] == x = 0" knowing from + "p : (x=0) == (?y[x] = 0)" that "?y := x" *) |