diff options
| author |  Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
|---|---|---|
| committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
| commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
| tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite | |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite')
164 files changed, 7141 insertions, 0 deletions
diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v new file mode 100644 index 00000000..4accbf34 --- /dev/null +++ b/test-suite/bench/lists-100.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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 new file mode 100644 index 00000000..4accbf34 --- /dev/null +++ b/test-suite/bench/lists_100.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \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/check b/test-suite/check new file mode 100755 index 00000000..1c7822d1 --- /dev/null +++ b/test-suite/check @@ -0,0 +1,129 @@ +#!/bin/sh + +# Automatic test of Coq + +if [ "$1" = -byte ]; then + command7="../bin/coqtop.byte -translate -q -batch -load-vernac-source" +else + command7="../bin/coqtop -translate -q -batch -load-vernac-source" +fi + +if [ "$1" = -byte ]; then + command="../bin/coqtop.byte -q -batch -load-vernac-source" +else + command="../bin/coqtop -q -batch -load-vernac-source" +fi + +# on compte le nombre de tests et de succès +nbtests=0 +nbtestsok=0 + +# La fonction suivante teste le compilateur sur des fichiers qu'il doit +# accepter +test_success() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command7 $f > /dev/null 2>&1 + if [ $? = 0 ]; then + mv "$f"8 tmp8.v + $command tmp8.v > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "V8 Error! (should be accepted)" + fi + rm tmp8.v + else + echo "V7 Error! (should be accepted)" + fi + done + for f in $1/*.v8; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + cp $f tmp8.v + $command tmp8.v > /dev/null 2>&1 + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "V8 Error! (should be accepted)" + fi + rm tmp8.v + done +} + +# La fonction suivante teste le compilateur sur des fichiers qu'il doit +# refuser +test_failure() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + $command7 $f > /dev/null 2>&1 + if [ $? != 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (should be rejected)" + fi + done +} + +# La fonction suivante teste la sortie des fichiers qu'elle exécute +test_output() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` + $command7 $f | tail +3 > $tmpoutput 2>&1 + foutput=`dirname $f`/`basename $f .v`.out + diff $tmpoutput $foutput > /dev/null + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (unexpected output)" + fi + done +} + +# La fonction suivante teste l'analyseur syntaxique fournit par "parser" +# Elle fonctionne comme test_output +test_parser() { + if [ -d $1 ]; then + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` + foutput=`dirname $f`/`basename $f .v`.out + echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 + perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ + $tmpoutput | grep -i error > /dev/null + if [ $? = 0 ] ; then + echo "Error! (unexpected output)" + else + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + fi + done + fi +} + +# Programme principal + +# echo "Output tests" +# test_output output +echo "[Output tests are off]" +echo "Success tests" +test_success success +echo "Failure tests" +test_failure failure +echo "Parser tests" +test_parser parser +pourcentage=`expr 100 \* $nbtestsok / $nbtests` +echo +echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %" + + + diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v new file mode 100644 index 00000000..fafcafc1 --- /dev/null +++ b/test-suite/failure/Case1.v @@ -0,0 +1 @@ +Type Cases O of x => O | O => (S O) end. diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v new file mode 100644 index 00000000..ee47544d --- /dev/null +++ b/test-suite/failure/Case10.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b) end. diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v new file mode 100644 index 00000000..c39a76ca --- /dev/null +++ b/test-suite/failure/Case11.v @@ -0,0 +1 @@ +Type [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end. diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v new file mode 100644 index 00000000..b56eac0d --- /dev/null +++ b/test-suite/failure/Case12.v @@ -0,0 +1,7 @@ + +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => x + end + end. + diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v new file mode 100644 index 00000000..8a4d75b6 --- /dev/null +++ b/test-suite/failure/Case13.v @@ -0,0 +1,5 @@ +Type [x:nat]<nat> Cases x of + ((S x) as b) => <nat>Cases x of + x => (S b x) + end + end. diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v new file mode 100644 index 00000000..a198d068 --- /dev/null +++ b/test-suite/failure/Case14.v @@ -0,0 +1,8 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Definition NIL := (Nil nat). +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | _ => NIL + end. diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v new file mode 100644 index 00000000..a27b07f8 --- /dev/null +++ b/test-suite/failure/Case15.v @@ -0,0 +1,6 @@ +(* Non exhaustive pattern-matching *) + +Check [x]Cases x x of + O (S (S y)) => true + | O (S x) => false + | (S y) O => true end.
\ No newline at end of file diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v new file mode 100644 index 00000000..f994a8f2 --- /dev/null +++ b/test-suite/failure/Case16.v @@ -0,0 +1,9 @@ +(* Check for redundant clauses *) + +Check [x]Cases x x of + O (S (S y)) => true + | (S _) (S (S y)) => true + | _ (S (S x)) => false + | (S y) O => true + | _ _ => true +end. diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v new file mode 100644 index 00000000..183f612b --- /dev/null +++ b/test-suite/failure/Case2.v @@ -0,0 +1,13 @@ +Inductive IFExpr : Set := + Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. + +Type [F:IFExpr] + <Prop>Cases F of + (IfE (Var _) H I) => True + | (IfE _ _ _) => False + | _ => True + end. + diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v new file mode 100644 index 00000000..2c651b87 --- /dev/null +++ b/test-suite/failure/Case3.v @@ -0,0 +1,7 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type [l:(List nat)]<nat>Cases l of + (Nil nat) =>O + | (Cons a l) => (S a) + end. diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v new file mode 100644 index 00000000..d00c9a05 --- /dev/null +++ b/test-suite/failure/Case4.v @@ -0,0 +1,7 @@ + +Definition Berry := [x,y,z:bool] + Cases x y z of + true false _ => O + | false _ true => (S O) + | _ true false => (S (S O)) +end. diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v new file mode 100644 index 00000000..bdb5544b --- /dev/null +++ b/test-suite/failure/Case5.v @@ -0,0 +1,3 @@ +Inductive MS: Set := X:MS->MS | Y:MS->MS. + +Type [p:MS]<nat>Cases p of (X x) => O end. diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v new file mode 100644 index 00000000..f588d275 --- /dev/null +++ b/test-suite/failure/Case6.v @@ -0,0 +1,10 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + + +Type <(List nat)>Cases (Nil nat) of + NIL => NIL + | (CONS _ _) => NIL + + end. + diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v new file mode 100644 index 00000000..3718f198 --- /dev/null +++ b/test-suite/failure/Case7.v @@ -0,0 +1,22 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Definition length1:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + +Type [n:nat] + [l:(listn n)] + <nat>Cases n of + O => O + | (S n) => + <([_:nat]nat)>Cases l of + niln => (S O) + | l' => (length1 (S n) l') + end + end. + diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v new file mode 100644 index 00000000..7f6bb615 --- /dev/null +++ b/test-suite/failure/Case8.v @@ -0,0 +1,8 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Type <nat>Cases (Nil nat) of + ((Nil_) as b) =>b + |((Cons _ _ _) as d) => d + end. + diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v new file mode 100644 index 00000000..e8d8e89a --- /dev/null +++ b/test-suite/failure/Case9.v @@ -0,0 +1,6 @@ +Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. +Type <nat>Cases (compare O O) of + (* k<i *) (left _ _ (left _ _ _)) => O + | (* k=i *) (left _ _ _) => O + | (* k>i *) (right _ _ _) => O end. + diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v new file mode 100644 index 00000000..ca8e3c68 --- /dev/null +++ b/test-suite/failure/ClearBody.v @@ -0,0 +1,8 @@ +(* ClearBody must check that removing the body of definition does not + invalidate the well-typabilility of the visible goal *) + +Goal True. +LetTac n:=O. +LetTac I:=(refl_equal nat O). +Change (n=O) in (Type of I). +ClearBody n. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v new file mode 100644 index 00000000..fb9a27bb --- /dev/null +++ b/test-suite/failure/Tauto.v @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(**** Tactics Tauto and Intuition ****) + +(**** Tauto: + Tactic for automating proof in Intuionnistic Propositional Calculus, based on + the contraction-free LJT of Dickhoff ****) + +(**** Intuition: + Simplifications of goals, based on LJT calcul ****) + +(* Fails because Tauto does not perform any Apply *) +Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Proof. + Tauto. diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v new file mode 100644 index 00000000..a27b07f8 --- /dev/null +++ b/test-suite/failure/cases.v @@ -0,0 +1,6 @@ +(* Non exhaustive pattern-matching *) + +Check [x]Cases x x of + O (S (S y)) => true + | O (S x) => false + | (S y) O => true end.
\ No newline at end of file diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v new file mode 100644 index 00000000..0bf7091c --- /dev/null +++ b/test-suite/failure/check.v @@ -0,0 +1,3 @@ +Implicits eq [1]. + +Check (eq bool true). diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v new file mode 100644 index 00000000..56cd73f4 --- /dev/null +++ b/test-suite/failure/clash_cons.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Teste la verification d'unicite des noms de constr *) + + +Inductive X : Set := + cons : X. + +Inductive Y : Set := + cons : Y. + diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v new file mode 100644 index 00000000..fcfd29fe --- /dev/null +++ b/test-suite/failure/clashes.v @@ -0,0 +1,8 @@ +(* Submitted by David Nowak *) + +(* Simpler to forbid the definition of n as a global than to write it + S.n to keep n accessible... *) + +Section S. +Variable n:nat. +Inductive P : Set := n : P. diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v new file mode 100644 index 00000000..2ac6c4f0 --- /dev/null +++ b/test-suite/failure/coqbugs0266.v @@ -0,0 +1,7 @@ +(* It is forbidden to erase a variable (or a local def) that is used in + the current goal. *) +Section S. +Local a:=O. +Definition b:=a. +Goal b=b. +Clear a. diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v new file mode 100644 index 00000000..742e9774 --- /dev/null +++ b/test-suite/failure/fixpoint1.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Fixpoint PreParadox [u:unit] : False := (PreParadox u). +Definition Paradox := (PreParadox tt).
\ No newline at end of file diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v new file mode 100644 index 00000000..aff43ff1 --- /dev/null +++ b/test-suite/failure/illtype1.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Check (S S). diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v new file mode 100644 index 00000000..d0256619 --- /dev/null +++ b/test-suite/failure/ltac1.v @@ -0,0 +1,5 @@ +(* Check all variables are different in a Context *) +Tactic Definition X := Match Context With [ x:?; x:? |- ? ] -> Apply x. +Goal True->True->True. +Intros. +X. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v new file mode 100644 index 00000000..55925a7a --- /dev/null +++ b/test-suite/failure/ltac2.v @@ -0,0 +1,6 @@ +(* Check that Match arguments are forbidden *) +Tactic Definition E x := Apply x. +Goal True->True. +E (Match Context With [ |- ? ] -> Intro H). +(* Should fail with "Immediate Match producing tactics not allowed in + local definitions" *) diff --git a/test-suite/failure/ltac3.v b/test-suite/failure/ltac3.v new file mode 100644 index 00000000..bfccc546 --- /dev/null +++ b/test-suite/failure/ltac3.v @@ -0,0 +1,2 @@ +(* Proposed by Benjamin *) +Definition A := Try REflexivity. diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v new file mode 100644 index 00000000..d1e4e892 --- /dev/null +++ b/test-suite/failure/ltac4.v @@ -0,0 +1,4 @@ +(* Check static globalisation of tactic names *) +(* Proposed by Benjamin (mars 2002) *) +Goal (n:nat)n=n. +Induction n; Try REflexivity. diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v new file mode 100644 index 00000000..20689128 --- /dev/null +++ b/test-suite/failure/params_ind.v @@ -0,0 +1,4 @@ +Inductive list [A:Set] : Set := + nil : (list A) +| cons : A -> (list A->A)-> (list A). + diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v new file mode 100644 index 00000000..b43eb899 --- /dev/null +++ b/test-suite/failure/positivity.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Inductive t:Set := c: (t -> nat) -> t. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v new file mode 100644 index 00000000..8f3aedac --- /dev/null +++ b/test-suite/failure/redef.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Definition toto := Set. +Definition toto := Set. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v new file mode 100644 index 00000000..e8ca8494 --- /dev/null +++ b/test-suite/failure/search.v @@ -0,0 +1,8 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +SearchPattern ? = ? outside n_existe_pas. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v new file mode 100644 index 00000000..01d46133 --- /dev/null +++ b/test-suite/failure/universes-buraliforti.v @@ -0,0 +1,227 @@ +(* Check that Burali-Forti paradox does not go through *) + +(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *) + +(* Some properties about relations on objects in Type *) + + Inductive ACC [A : Type; R : A->A->Prop] : A->Prop := + ACC_intro : (x:A)((y:A)(R y x)->(ACC A R y))->(ACC A R x). + + Lemma ACC_nonreflexive: + (A:Type)(R:A->A->Prop)(x:A)(ACC A R x)->(R x x)->False. +Induction 1; Intros. +Exact (H1 x0 H2 H2). +Save. + + Definition WF := [A:Type][R:A->A->Prop](x:A)(ACC A R x). + + +Section Inverse_Image. + + Variables A,B:Type; R:B->B->Prop; f:A->B. + + Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)). + + Remark ACC_lemma : (y:B)(ACC B R y)->(x:A)(y==(f x))->(ACC A Rof x). + Induction 1; Intros. + Constructor; Intros. + Apply (H1 (f y0)); Trivial. + Elim H2 using eqT_ind_r; Trivial. + Save. + + Lemma ACC_inverse_image : (x:A)(ACC B R (f x)) -> (ACC A Rof x). + Intros; Apply (ACC_lemma (f x)); Trivial. + Save. + + Lemma WF_inverse_image: (WF B R)->(WF A Rof). + Red; Intros; Apply ACC_inverse_image; Auto. + Save. + +End Inverse_Image. + + +(* Remark: the paradox is written in Type, but also works in Prop or Set. *) + +Section Burali_Forti_Paradox. + + Definition morphism := [A:Type][R:A->A->Prop][B:Type][S:B->B->Prop][f:A->B] + (x,y:A)(R x y)->(S (f x) (f y)). + + (* The hypothesis of the paradox: + assumes there exists an universal system of notations, i.e: + - A type A0 + - An injection i0 from relations on any type into A0 + - The proof that i0 is injective modulo morphism + *) + Variable A0 : Type. (* Type_i *) + Variable i0 : (X:Type)(X->X->Prop)->A0. (* X: Type_j *) + Hypothesis inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) + (i0 X1 R1)==(i0 X2 R2) + ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). + + (* Embedding of x in y: x and y are images of 2 well founded relations + R1 and R2, the ordinal of R2 being strictly greater than that of R1. + *) + Record emb [x,y:A0]: Prop := { + X1: Type; + R1: X1->X1->Prop; + eqx: x==(i0 X1 R1); + X2: Type; + R2: X2->X2->Prop; + eqy: y==(i0 X2 R2); + W2: (WF X2 R2); + f: X1->X2; + fmorph: (morphism X1 R1 X2 R2 f); + maj: X2; + majf: (z:X1)(R2 (f z) maj) }. + + + Lemma emb_trans: (x,y,z:A0)(emb x y)->(emb y z)->(emb x z). +Intros. +Case H; Intros. +Case H0; Intros. +Generalize eqx0; Clear eqx0. +Elim eqy using eqT_ind_r; Intro. +Case (inj ? ? ? ? eqx0); Intros. +Exists X1 R1 X3 R3 [x:X1](f0 (x0 (f x))) maj0; Trivial. +Red; Auto. +Defined. + + + Lemma ACC_emb: (X:Type)(R:X->X->Prop)(x:X)(ACC X R x) + ->(Y:Type)(S:Y->Y->Prop)(f:Y->X)(morphism Y S X R f) + ->((y:Y)(R (f y) x)) + ->(ACC A0 emb (i0 Y S)). +Induction 1; Intros. +Constructor; Intros. +Case H4; Intros. +Elim eqx using eqT_ind_r. +Case (inj X2 R2 Y S). +Apply sym_eqT; Assumption. + +Intros. +Apply H1 with y:=(f (x1 maj)) f:=[x:X1](f (x1 (f0 x))); Try Red; Auto. +Defined. + + (* The embedding relation is well founded *) + Lemma WF_emb: (WF A0 emb). +Constructor; Intros. +Case H; Intros. +Elim eqx using eqT_ind_r. +Apply ACC_emb with X:=X2 R:=R2 x:=maj f:=f; Trivial. +Defined. + + + (* The following definition enforces Type_j >= Type_i *) + Definition Omega: A0 := (i0 A0 emb). + + +Section Subsets. + + Variable a: A0. + + (* We define the type of elements of A0 smaller than a w.r.t embedding. + The Record is in Type, but it is possible to avoid such structure. *) + Record sub: Type := { + witness : A0; + emb_wit : (emb witness a) }. + + (* F is its image through i0 *) + Definition F : A0 := (i0 sub (Rof ? ? emb witness)). + + (* F is embedded in Omega: + - the witness projection is a morphism + - a is an upper bound because emb_wit proves that witness is + smaller than a. + *) + Lemma F_emb_Omega: (emb F Omega). +Exists sub (Rof ? ? emb witness) A0 emb witness a; Trivial. +Exact WF_emb. + +Red; Trivial. + +Exact emb_wit. +Defined. + +End Subsets. + + + Definition fsub: (a,b:A0)(emb a b)->(sub a)->(sub b):= + [_,_][H][x] + (Build_sub ? (witness ? x) (emb_trans ? ? ? (emb_wit ? x) H)). + + (* F is a morphism: a < b => F(a) < F(b) + - the morphism from F(a) to F(b) is fsub above + - the upper bound is a, which is in F(b) since a < b + *) + Lemma F_morphism: (morphism A0 emb A0 emb F). +Red; Intros. +Exists (sub x) (Rof ? ? emb (witness x)) (sub y) + (Rof ? ? emb (witness y)) (fsub x y H) (Build_sub ? x H); +Trivial. +Apply WF_inverse_image. +Exact WF_emb. + +Unfold morphism Rof fsub; Simpl; Intros. +Trivial. + +Unfold Rof fsub; Simpl; Intros. +Apply emb_wit. +Defined. + + + (* Omega is embedded in itself: + - F is a morphism + - Omega is an upper bound of the image of F + *) + Lemma Omega_refl: (emb Omega Omega). +Exists A0 emb A0 emb F Omega; Trivial. +Exact WF_emb. + +Exact F_morphism. + +Exact F_emb_Omega. +Defined. + + (* The paradox is that Omega cannot be embedded in itself, since + the embedding relation is well founded. + *) + Theorem Burali_Forti: False. +Apply ACC_nonreflexive with A0 emb Omega. +Apply WF_emb. + +Exact Omega_refl. + +Defined. + +End Burali_Forti_Paradox. + + + (* The following type seems to satisfy the hypothesis of the paradox. + But it does not! + *) + Record A0: Type := (* Type_i' *) + i0 { X0: Type; R0: X0->X0->Prop }. (* X0: Type_j' *) + + + (* Note: this proof uses a large elimination of A0. *) + Lemma inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) + (i0 X1 R1)==(i0 X2 R2) + ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). +Intros. +Change Cases (i0 X1 R1) (i0 X2 R2) of + (i0 x1 r1) (i0 x2 r2) => (EXT f | (morphism x1 r1 x2 r2 f)) + end. +Case H; Simpl. +Exists [x:X1]x. +Red; Trivial. +Defined. + +(* The following command raises 'Error: Universe Inconsistency'. + To allow large elimination of A0, i0 must not be a large constructor. + Hence, the constraint Type_j' < Type_i' is added, which is incompatible + with the constraint j >= i in the paradox. +*) + + Definition Paradox: False := (Burali_Forti A0 i0 inj). + diff --git a/test-suite/failure/universes-sections1.v b/test-suite/failure/universes-sections1.v new file mode 100644 index 00000000..c4eef34b --- /dev/null +++ b/test-suite/failure/universes-sections1.v @@ -0,0 +1,8 @@ +(* Check that constraints on definitions are preserved by discharging *) + +Section A. + Definition Type2 := Type. + Definition Type1 := Type : Type2. +End A. + +Definition Inconsistency := Type2 : Type1. diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v new file mode 100644 index 00000000..1872dac1 --- /dev/null +++ b/test-suite/failure/universes-sections2.v @@ -0,0 +1,10 @@ +(* Check that constraints on locals are preserved by discharging *) + +Definition Type2 := Type. + +Section A. + Local Type1 := Type : Type2. + Definition Type1' := Type1. +End A. + +Definition Inconsistency := Type2 : Type1'. diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v new file mode 100644 index 00000000..6fada6f1 --- /dev/null +++ b/test-suite/failure/universes.v @@ -0,0 +1,3 @@ +Definition Type2 := Type. +Definition Type1 := Type : Type2. +Definition Inconsistency := Type2 : Type1. diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v new file mode 100644 index 00000000..a6c8ba43 --- /dev/null +++ b/test-suite/failure/universes2.v @@ -0,0 +1,5 @@ +(* Example submitted by Randy Pollack *) + +Parameter K: (T:Type)T->T. +Check (K ((T:Type)T->T) K). +(* Universe Inconsistency *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v new file mode 100644 index 00000000..bba356f2 --- /dev/null +++ b/test-suite/ideal-features/Apply.v @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This needs unification on type *) + +Goal (n,m:nat)(eq nat (S m) (S n)). +Intros. +Apply f_equal. + +(* f_equal : (A,B:Set; f:(A->B); x,y:A)x=y->(f x)=(f y) *) +(* and A cannot be deduced from the goal but only from the type of f, x or y *) + + +(* This needs step by step unfolding *) + +Fixpoint T [n:nat] : Prop := Cases n of O => True | (S p) => n=n->(T p) end. +Require Arith. + +Goal (T (3))->(T (1)). +Intro H. +Apply H. diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v new file mode 100644 index 00000000..e9dba1e3 --- /dev/null +++ b/test-suite/ideal-features/Case3.v @@ -0,0 +1,28 @@ +Inductive Le : nat->nat->Set := + LeO: (n:nat)(Le O n) +| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)). + +Parameter iguales : (n,m:nat)(h:(Le n m))Prop . + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) (S y) H) => (iguales (S x) (S y) H) + | _ => False end. + + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) O H) => (iguales (S x) O H) + | _ => False end. + +Parameter discr_l : (n:nat) ~((S n)=O). + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. + diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v new file mode 100644 index 00000000..d8f14a4e --- /dev/null +++ b/test-suite/ideal-features/Case4.v @@ -0,0 +1,39 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Inductive empty : (n:nat)(listn n)-> Prop := + intro_empty: (empty O niln). + +Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn n O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | (consn n O y) => (or_intror (empty (S n) (consn n O y)) ? + (inv_empty n O y)) + | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? + (inv_empty n a y)) + + end. + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + diff --git a/test-suite/ideal-features/Case8.v b/test-suite/ideal-features/Case8.v new file mode 100644 index 00000000..73b55028 --- /dev/null +++ b/test-suite/ideal-features/Case8.v @@ -0,0 +1,40 @@ +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Inductive empty : (n:nat)(listn n)-> Prop := + intro_empty: (empty O niln). + +Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn n O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | (consn n O y) => (or_intror (empty (S n) (consn n O y)) ? + (inv_empty n O y)) + | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? + (inv_empty n a y)) + + end. + + + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. diff --git a/test-suite/kernel/inds.mv b/test-suite/kernel/inds.mv new file mode 100644 index 00000000..bd1cc49f --- /dev/null +++ b/test-suite/kernel/inds.mv @@ -0,0 +1,3 @@ +Inductive [] nat : Set := O : nat | S : nat->nat. +Check Construct nat 0 1. +Check Construct nat 0 2. diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v new file mode 100644 index 00000000..1e9273f0 --- /dev/null +++ b/test-suite/modules/Demo.v @@ -0,0 +1,55 @@ +Module M. + Definition t:=nat. + Definition x:=O. +End M. + +Print M.t. + + +Module Type SIG. + Parameter t:Set. + Parameter x:t. +End SIG. + + +Module F[X:SIG]. + Definition t:=X.t->X.t. + Definition x:t. + Intro. + Exact X.x. + Defined. + Definition y:=X.x. +End F. + + +Module N := F M. + +Print N.t. +Eval Compute in N.t. + + +Module N' : SIG := N. + +Print N'.t. +Eval Compute in N'.t. + + +Module N'' <: SIG := F N. + +Print N''.t. +Eval Compute in N''.t. + +Eval Compute in N''.x. + + +Module N''' : SIG with Definition t:=nat->nat := N. + +Print N'''.t. +Eval Compute in N'''.t. + +Print N'''.x. + + +Import N'''. + +Print t.
\ No newline at end of file diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v new file mode 100644 index 00000000..61966c7c --- /dev/null +++ b/test-suite/modules/Nametab.v @@ -0,0 +1,48 @@ +Module Q. + Module N. + Module K. + Definition id:=Set. + End K. + End N. +End Q. + +(* Bad *) Locate id. +(* Bad *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* Bad *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. + + + +Import Q.N. + + +(* Bad *) Locate id. +(* OK *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* OK *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v new file mode 100644 index 00000000..d3e98ae4 --- /dev/null +++ b/test-suite/modules/Nat.v @@ -0,0 +1,19 @@ +Definition T:=nat. + +Definition le:=Peano.le. + +Hints Unfold le. + +Lemma le_refl:(n:nat)(le n n). + Auto. +Qed. + +Require Le. + +Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k). + EAuto with arith. +Qed. + +Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m. + EAuto with arith. +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v new file mode 100644 index 00000000..9ba3fb2e --- /dev/null +++ b/test-suite/modules/PO.v @@ -0,0 +1,57 @@ +Implicit Arguments On. + +Implicits fst. +Implicits snd. + +Module Type PO. + Parameter T:Set. + Parameter le:T->T->Prop. + + Axiom le_refl : (x:T)(le x x). + Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z). + Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y). + + Hints Resolve le_refl le_trans le_antis. +End PO. + + +Module Pair[X:PO][Y:PO] <: PO. + Definition T:=X.T*Y.T. + Definition le:=[p1,p2] + (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)). + + Hints Unfold le. + + Lemma le_refl : (p:T)(le p p). + Info Auto. + Qed. + + Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3). + Unfold le; Intuition; Info EAuto. + Qed. + + Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2). + NewDestruct p1. + NewDestruct p2. + Unfold le. + Intuition. + CutRewrite t=t1. + CutRewrite t0=t2. + Reflexivity. + + Info Auto. + + Info Auto. + Qed. + +End Pair. + + + +Read Module Nat. + +Module NN := Pair Nat Nat. + +Lemma zz_min : (p:NN.T)(NN.le (O,O) p). + Info Auto with arith. +Qed. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v new file mode 100644 index 00000000..4f4c2066 --- /dev/null +++ b/test-suite/modules/Przyklad.v @@ -0,0 +1,193 @@ +Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T] + if s then [_]th else [_]el. + +Implicits ifte. + +Lemma Reflexivity_provable : + (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)). +Intros. +Elim s. +Intro x. +Split with x; Reflexivity. + +Intro. +Absurd a=a; Auto. + +Save. + +Lemma Disequality_provable : + (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)). +Intros. +Elim s. +Intro. +Absurd a=a; Auto. + +Intro. +Split with b0; Reflexivity. + +Save. + +Module Type ELEM. + Parameter T : Set. + Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. +End ELEM. + +Module Type SET[Elt : ELEM]. + Parameter T : Set. + Parameter empty : T. + Parameter add : Elt.T -> T -> T. + Parameter find : Elt.T -> T -> bool. + + (* Axioms *) + + Axiom find_empty_false : + (e:Elt.T) (find e empty) = false. + + Axiom find_add_true : + (s:T) (e:Elt.T) (find e (add e s)) = true. + + Axiom find_add_false : + (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> + (find e (add e' s))=(find e s). + +End SET. + +Module FuncDict[E : ELEM]. + Definition T := E.T -> bool. + Definition empty := [e':E.T] false. + Definition find := [e':E.T] [s:T] (s e'). + Definition add := [e:E.T][s:T][e':E.T] + (ifte (E.eq_dec e e') true (find e' s)). + + Lemma find_empty_false : (e:E.T) (find e empty) = false. + Auto. + Qed. + + Lemma find_add_true : + (s:T) (e:E.T) (find e (add e s)) = true. + + Intros. + Unfold find add. + Elim (Reflexivity_provable ? ? (E.eq_dec e e)). + Intros. + Rewrite H. + Auto. + + Qed. + + Lemma find_add_false : + (s:T) (e:E.T) (e':E.T) ~(e=e') -> + (find e (add e' s))=(find e s). + Intros. + Unfold add find. + Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)). + Intros. + Elim H0. + Intros. + Rewrite H1. + Unfold ifte. + Reflexivity. + + Apply Disequality_provable. + Auto. + + Qed. + +End FuncDict. + +Module F : SET := FuncDict. + + +Module Nat. + Definition T:=nat. + Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. + Decide Equality. + Qed. +End Nat. + + +Module SetNat:=F Nat. + + +Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. +Apply SetNat.find_empty_false. +Save. + +(***************************************************************************) +Module Lemmas[G:SET][E:ELEM]. + + Module ESet:=G E. + + Lemma commute : (S:ESet.T)(a1,a2:E.T) + let S1 = (ESet.add a1 (ESet.add a2 S)) in + let S2 = (ESet.add a2 (ESet.add a1 S)) in + (a:E.T)(ESet.find a S1)=(ESet.find a S2). + + Intros. + Unfold S1 S2. + Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2; + Try Rewrite <- H1; Try Rewrite <- H2; + Repeat + (Try (Rewrite ESet.find_add_true; Auto); + Try (Rewrite ESet.find_add_false; Auto); + Auto). + Save. +End Lemmas. + + +Inductive list [A:Set] : Set := nil : (list A) + | cons : A -> (list A) -> (list A). + +Module ListDict[E : ELEM]. + Definition T := (list E.T). + Definition elt := E.T. + + Definition empty := (nil elt). + Definition add := [e:elt][s:T] (cons elt e s). + Fixpoint find [e:elt; s:T] : bool := + Cases s of + nil => false + | (cons e' s') => (ifte (E.eq_dec e e') + true + (find e s')) + end. + + Definition find_empty_false := [e:elt] (refl_equal bool false). + + Lemma find_add_true : + (s:T) (e:E.T) (find e (add e s)) = true. + Intros. + Simpl. + Elim (Reflexivity_provable ? ? (E.eq_dec e e)). + Intros. + Rewrite H. + Auto. + + Qed. + + + Lemma find_add_false : + (s:T) (e:E.T) (e':E.T) ~(e=e') -> + (find e (add e' s))=(find e s). + Intros. + Simpl. + Elim (Disequality_provable ? ? ? H (E.eq_dec e e')). + Intros. + Rewrite H0. + Simpl. + Reflexivity. + Save. + + +End ListDict. + + +Module L : SET := ListDict. + + + + + + + + diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v new file mode 100644 index 00000000..13c28418 --- /dev/null +++ b/test-suite/modules/Tescik.v @@ -0,0 +1,30 @@ + +Module Type ELEM. + Parameter A:Set. + Parameter x:A. +End ELEM. + +Module Nat. + Definition A:=nat. + Definition x:=O. +End Nat. + +Module List[X:ELEM]. + Inductive list : Set := nil : list + | cons : X.A -> list -> list. + + Definition head := + [l:list]Cases l of + nil => X.x + | (cons x _) => x + end. + + Definition singl := [x:X.A] (cons x nil). + + Lemma head_singl : (x:X.A)(head (singl x))=x. + Auto. + Qed. + +End List. + +Module N:=(List Nat). diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v new file mode 100644 index 00000000..0f8eef84 --- /dev/null +++ b/test-suite/modules/fun_objects.v @@ -0,0 +1,32 @@ +Implicit Arguments On. + +Module Type SIG. + Parameter id:(A:Set)A->A. +End SIG. + +Module M[X:SIG]. + Definition idid := (X.id X.id). + Definition id := (idid X.id). +End M. + +Module N:=M. + +Module Nat. + Definition T := nat. + Definition x := O. + Definition id := [A:Set][x:A]x. +End Nat. + +Module Z:=(N Nat). + +Check (Z.idid O). + +Module P[Y:SIG] := N. + +Module Y:=P Nat Z. + +Check (Y.id O). + + + + diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v new file mode 100644 index 00000000..fb734b5d --- /dev/null +++ b/test-suite/modules/grammar.v @@ -0,0 +1,15 @@ +Module N. +Definition f:=plus. +Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E]. +Check (f O O). +End N. +Check (N.f O O). +Import N. +Check (N.f O O). +Check (f O O). +Module M:=N. +Check (f O O). +Check (N.f O O). +Import M. +Check (f O O). +Check (N.f O O). diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v new file mode 100644 index 00000000..94c344bb --- /dev/null +++ b/test-suite/modules/ind.v @@ -0,0 +1,13 @@ +Module Type SIG. + Inductive w:Set:=A:w. + Parameter f : w->w. +End SIG. + +Module M:SIG. + Inductive w:Set:=A:w. + Definition f:=[x]Cases x of A => A end. +End M. + +Module N:=M. + +Check (N.f M.A). diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v new file mode 100644 index 00000000..867b8a11 --- /dev/null +++ b/test-suite/modules/mod_decl.v @@ -0,0 +1,55 @@ +Module Type SIG. + Definition A:Set. (*error*) + Axiom A:Set. +End SIG. + +Module M0. + Definition A:Set. + Exact nat. + Save. +End M0. + +Module M1:SIG. + Definition A:=nat. +End M1. + +Module M2<:SIG. + Definition A:=nat. +End M2. + +Module M3:=M0. + +Module M4:SIG:=M0. + +Module M5<:SIG:=M0. + + +Module F[X:SIG]:=X. + + +Declare Module M6. + + +Module Type T. + + Declare Module M0. + Lemma A:Set (*error*). + Axiom A:Set. + End M0. + + Declare Module M1:SIG. + + Declare Module M2<:SIG. + Definition A:=nat. + End M2. + + Declare Module M3:=M0. + + Declare Module M4:SIG:=M0. (* error *) + + Declare Module M5<:SIG:=M0. + + Declare Module M6:=F M0. (* error *) + + Module M7. +End T.
\ No newline at end of file diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v new file mode 100644 index 00000000..73448dc7 --- /dev/null +++ b/test-suite/modules/modeq.v @@ -0,0 +1,22 @@ +Module M. + Definition T:=nat. + Definition x:T:=O. +End M. + +Module Type SIG. + Declare Module M:=Top.M. + Module Type SIG. + Parameter T:Set. + End SIG. + Declare Module N:SIG. +End SIG. + +Module Z. + Module M:=Top.M. + Module Type SIG. + Parameter T:Set. + End SIG. + Module N:=M. +End Z. + +Module A:SIG:=Z. diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v new file mode 100644 index 00000000..5612ea75 --- /dev/null +++ b/test-suite/modules/modul.v @@ -0,0 +1,39 @@ +Module M. + Parameter rel:nat -> nat -> Prop. + + Axiom w : (n:nat)(rel O (S n)). + + Hints Resolve w. + + Grammar constr constr8 := + not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ]. + + Print Hint *. + + Lemma w1 : (O#(S O)). + Auto. + Save. + +End M. + +(*Lemma w1 : (M.rel O (S O)). +Auto. +*) + +Import M. + +Print Hint *. +Lemma w1 : (O#(S O)). +Print Hint. +Print Hint *. + +Auto. +Save. + +Check (O#O). +Locate rel. + +Locate M. + +Module N:=Top.M. + diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v new file mode 100644 index 00000000..2231e084 --- /dev/null +++ b/test-suite/modules/obj.v @@ -0,0 +1,26 @@ +Implicit Arguments On. + +Module M. + Definition a:=[s:Set]s. + Print a. +End M. + +Print M.a. + +Module K. + Definition app:=[A,B:Set; f:(A->B); x:A](f x). + Module N. + Definition apap:=[A,B:Set](app (app 1!A 2!B)). + Print app. + Print apap. + End N. + Print N.apap. +End K. + +Print K.app. +Print K.N.apap. + +Module W:=K.N. + +Print W.apap. + diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v new file mode 100644 index 00000000..418ece44 --- /dev/null +++ b/test-suite/modules/objects.v @@ -0,0 +1,33 @@ +Module Type SET. + Axiom T:Set. + Axiom x:T. +End SET. + +Implicit Arguments On. + +Module M[X:SET]. + Definition T := nat. + Definition x := O. + Definition f := [A:Set][x:A]X.x. +End M. + +Module N:=M. + +Module Nat. + Definition T := nat. + Definition x := O. +End Nat. + +Module Z:=(N Nat). + +Check (Z.f O). + +Module P[Y:SET] := N. + +Module Y:=P Z Nat. + +Check (Y.f O). + + + + diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v new file mode 100644 index 00000000..6061ace3 --- /dev/null +++ b/test-suite/modules/pliczek.v @@ -0,0 +1,3 @@ +Require Export plik. + +Definition tutu := [X:Set](toto X). diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v new file mode 100644 index 00000000..f1f59df0 --- /dev/null +++ b/test-suite/modules/plik.v @@ -0,0 +1,4 @@ +Definition toto:=[x:Set]x. + +Grammar constr constr8 := + toto [ "#" constr7($b) ] -> [ (toto $b) ]. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v new file mode 100644 index 00000000..eb8736bb --- /dev/null +++ b/test-suite/modules/sig.v @@ -0,0 +1,29 @@ +Module M. + Module Type SIG. + Parameter T:Set. + Parameter x:T. + End SIG. + Module N:SIG. + Definition T:=nat. + Definition x:=O. + End N. +End M. + +Module N:=M. + +Module Type SPRYT. + Declare Module N. + Definition T:=M.N.T. + Parameter x:T. + End N. +End SPRYT. + +Module K:SPRYT:=N. +Module K':SPRYT:=M. + +Module Type SIG. + Definition T:Set:=M.N.T. + Parameter x:T. +End SIG. + +Module J:SIG:=M.N. diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v new file mode 100644 index 00000000..1bd4faef --- /dev/null +++ b/test-suite/modules/sub_objects.v @@ -0,0 +1,33 @@ +Set Implicit Arguments. + + +Module M. + Definition id:=[A:Set][x:A]x. + + Module Type SIG. + Parameter idid:(A:Set)A->A. + End SIG. + + Module N. + Definition idid:=[A:Set][x:A](id x). + Grammar constr constr8 := + not_eq [ "#" constr7($b) ] -> [ (idid $b) ]. + Notation inc := (plus (S O)). + End N. + + Definition zero:=(N.idid O). + +End M. + +Definition zero := (M.N.idid O). +Definition jeden := (M.N.inc O). + +Module Goly:=M.N. + +Definition Gole_zero := (Goly.idid O). +Definition Goly_jeden := (Goly.inc O). + +Module Ubrany : M.SIG := M.N. + +Definition Ubrane_zero := (Ubrany.idid O). + diff --git a/test-suite/output/Arith.out b/test-suite/output/Arith.out new file mode 100644 index 00000000..210dd6ad --- /dev/null +++ b/test-suite/output/Arith.out @@ -0,0 +1,4 @@ +[n:nat](S (S n)) + : nat->nat +[n:nat](S (plus n n)) + : nat->nat diff --git a/test-suite/output/Arith.v b/test-suite/output/Arith.v new file mode 100644 index 00000000..39989dfc --- /dev/null +++ b/test-suite/output/Arith.v @@ -0,0 +1,2 @@ +Check [n](S (S n)). +Check [n](S (plus n n)). diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out new file mode 100644 index 00000000..5f13caaf --- /dev/null +++ b/test-suite/output/Cases.out @@ -0,0 +1,4 @@ +t_rect = +[P:(t->Type); f:([x:=t](x0:x)(P x0)->(P (k x0)))] + Fix F{F [t:t] : (P t) := <P>Cases t of (k x x0) => (f x0 (F x0)) end} + : (P:(t->Type))([x:=t](x0:x)(P x0)->(P (k x0)))->(t:t)(P t) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v new file mode 100644 index 00000000..7483e8c4 --- /dev/null +++ b/test-suite/output/Cases.v @@ -0,0 +1,5 @@ +(* Cases with let-in in constructors types *) + +Inductive t : Set := k : [x:=t]x -> x. + +Print t_rect. diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out new file mode 100644 index 00000000..63e042d8 --- /dev/null +++ b/test-suite/output/Coercions.out @@ -0,0 +1,4 @@ +(P x) + : Prop +(R x x) + : Prop diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v new file mode 100644 index 00000000..61b69038 --- /dev/null +++ b/test-suite/output/Coercions.v @@ -0,0 +1,9 @@ +(* Submitted by Randy Pollack *) + +Record pred [S:Set]: Type := { sp_pred :> S -> Prop }. +Record rel [S:Set]: Type := { sr_rel :> S -> S -> Prop }. + +Section testSection. +Variables S: Set; P: (pred S); R: (rel S); x:S. +Check (P x). +Check (R x x). diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v new file mode 100644 index 00000000..270fff4e --- /dev/null +++ b/test-suite/output/Fixpoint.v @@ -0,0 +1,7 @@ +Require PolyList. + +Check Fix F { F/4 : (A,B:Set)(A->B)->(list A)->(list B) := + [_,_,f,l]Cases l of + nil => (nil ?) + | (cons a l) => (cons (f a) (F ? ? f l)) + end}. diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out new file mode 100644 index 00000000..f9cf9efc --- /dev/null +++ b/test-suite/output/Implicit.out @@ -0,0 +1,5 @@ +d2 = [x:nat](d1 1!x) + : (x,x0:nat)x0=x ->x0=x + +Positions [1; 2] are implicit +Argument scopes are [nat_scope nat_scope _] diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v new file mode 100644 index 00000000..2dea0d18 --- /dev/null +++ b/test-suite/output/Implicit.v @@ -0,0 +1,18 @@ +Set Implicit Arguments. + +(* Suggested by Pierre Casteran (bug #169) *) +(* Argument 3 is needed to typecheck and should be printed *) +Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). +Check (compose 3!nat S). + +(* Better to explicitly display the arguments inferable from a + position that could disappear after reduction *) +Inductive ex [A:Set;P:A->Prop] : Prop + := ex_intro : (x:A)(P x)->(ex P). +Check (ex_intro 2![_]True 3!O I). + +(* Test for V8 printing of implicit by names *) +Definition d1 [y;x;h:x=y:>nat] := h. +Definition d2 [x] := (!d1 x). + +Print d2. diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out new file mode 100644 index 00000000..d7120f89 --- /dev/null +++ b/test-suite/output/InitSyntax.out @@ -0,0 +1,6 @@ +Inductive sig2 [A : Set; P : A->Prop; Q : A->Prop] : Set := + exist2 : (x:A)(P x)->(Q x)->(sig2 A P Q) +(EX x:nat|x=x) + : Prop +[b:bool](if b then b else b) + : bool->bool diff --git a/test-suite/output/InitSyntax.v b/test-suite/output/InitSyntax.v new file mode 100644 index 00000000..90fad371 --- /dev/null +++ b/test-suite/output/InitSyntax.v @@ -0,0 +1,4 @@ +(* Soumis par Pierre *) +Print sig2. +Check (EX x:nat|x=x). +Check [b:bool]if b then b else b. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out new file mode 100644 index 00000000..cadb35c6 --- /dev/null +++ b/test-suite/output/Intuition.out @@ -0,0 +1,7 @@ +1 subgoal + + m : Z + n : Z + H : `m >= n` + ============================ + `m >= m` diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v new file mode 100644 index 00000000..c0508c90 --- /dev/null +++ b/test-suite/output/Intuition.v @@ -0,0 +1,5 @@ +Require ZArith_base. +Goal (m,n:Z) `m >= n` -> `m >= m` /\ `m >= n`. +Intros; Intuition. +Show. +Abort. diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out new file mode 100644 index 00000000..505821d7 --- /dev/null +++ b/test-suite/output/Nametab.out @@ -0,0 +1,28 @@ +id is not a defined object +K.id is not a defined object +N.K.id is not a defined object +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id +K is not a defined object +N.K is not a defined object +Module Top.Q.N.K +Module Top.Q.N.K +N is not a defined object +Module Top.Q.N +Module Top.Q.N +Module Top.Q +Module Top.Q +id is not a defined object +Constant Top.Q.N.K.id +N.K.id is not a defined object +Constant Top.Q.N.K.id +Constant Top.Q.N.K.id +Module Top.Q.N.K +N.K is not a defined object +Module Top.Q.N.K +Module Top.Q.N.K +N is not a defined object +Module Top.Q.N +Module Top.Q.N +Module Top.Q +Module Top.Q diff --git a/test-suite/output/Nametab.v b/test-suite/output/Nametab.v new file mode 100644 index 00000000..61966c7c --- /dev/null +++ b/test-suite/output/Nametab.v @@ -0,0 +1,48 @@ +Module Q. + Module N. + Module K. + Definition id:=Set. + End K. + End N. +End Q. + +(* Bad *) Locate id. +(* Bad *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* Bad *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. + + + +Import Q.N. + + +(* Bad *) Locate id. +(* OK *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* OK *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out new file mode 100644 index 00000000..fa30656b --- /dev/null +++ b/test-suite/output/RealSyntax.out @@ -0,0 +1,4 @@ +``32`` + : R +``-31`` + : R diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v new file mode 100644 index 00000000..d976dcc1 --- /dev/null +++ b/test-suite/output/RealSyntax.v @@ -0,0 +1,3 @@ +Require Reals. +Check ``32``. +Check ``-31``. diff --git a/test-suite/output/Remark2.out b/test-suite/output/Remark2.out new file mode 100644 index 00000000..adabc2fe --- /dev/null +++ b/test-suite/output/Remark2.out @@ -0,0 +1 @@ +B.C.t is not a defined object diff --git a/test-suite/output/Remark2.v b/test-suite/output/Remark2.v new file mode 100644 index 00000000..e1ef57a0 --- /dev/null +++ b/test-suite/output/Remark2.v @@ -0,0 +1,8 @@ +Section A. +Section B. +Section C. +Remark t : True. Proof I. +End C. +End B. +End A. +Locate B.C.t. diff --git a/test-suite/output/Sum.out b/test-suite/output/Sum.out new file mode 100644 index 00000000..22422602 --- /dev/null +++ b/test-suite/output/Sum.out @@ -0,0 +1,6 @@ +nat+nat+{True} + : Set +{True}+{True}+{True} + : Set +nat+{True}+{True} + : Set diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v new file mode 100644 index 00000000..aceadd12 --- /dev/null +++ b/test-suite/output/Sum.v @@ -0,0 +1,3 @@ +Check nat+nat+{True}. +Check {True}+{True}+{True}. +Check nat+{True}+{True}. diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out new file mode 100644 index 00000000..41e8648b --- /dev/null +++ b/test-suite/output/TranspModtype.out @@ -0,0 +1,10 @@ +TrM.A = M.A + : Set + +OpM.A = M.A + : Set + +TrM.B = M.B + : Set + +*** [ OpM.B : Set ] diff --git a/test-suite/output/TranspModtype.v b/test-suite/output/TranspModtype.v new file mode 100644 index 00000000..27b1fb9f --- /dev/null +++ b/test-suite/output/TranspModtype.v @@ -0,0 +1,22 @@ +Module Type SIG. + Axiom A:Set. + Axiom B:Set. +End SIG. + +Module M:SIG. + Definition A:=nat. + Definition B:=nat. +End M. + +Module N<:SIG:=M. + +Module TranspId[X:SIG] <: SIG with Definition A:=X.A := X. +Module OpaqueId[X:SIG] : SIG with Definition A:=X.A := X. + +Module TrM := TranspId M. +Module OpM := OpaqueId M. + +Print TrM.A. +Print OpM.A. +Print TrM.B. +Print OpM.B. diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out new file mode 100644 index 00000000..0fdc5b7e --- /dev/null +++ b/test-suite/output/ZSyntax.out @@ -0,0 +1,26 @@ +`32` + : Z +[f:(nat->Z)]`(f O)+0` + : (nat->Z)->Z +[x:positive](POS (xO x)) + : positive->Z +[x:positive]`(POS x)+1` + : positive->Z +[x:positive](POS x) + : positive->Z +[x:positive](NEG (xO x)) + : positive->Z +[x:positive]`(POS (xO x))+0` + : positive->Z +[x:positive]`(Zopp (POS (xO x)))` + : positive->Z +[x:positive]`(Zopp (POS (xO x)))+0` + : positive->Z +`(inject_nat (0))+1` + : Z +`0+(inject_nat (plus (0) (0)))` + : Z +`(inject_nat (0)) = 0` + : Prop +`0+(inject_nat (11))` + : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v new file mode 100644 index 00000000..49442b75 --- /dev/null +++ b/test-suite/output/ZSyntax.v @@ -0,0 +1,17 @@ +Require ZArith. +Check `32`. +Check [f:nat->Z]`(f O) + 0`. +Check [x:positive]`(POS (xO x))`. +Check [x:positive]`(POS x)+1`. +Check [x:positive]`(POS x)`. +Check [x:positive]`(NEG (xO x))`. +Check [x:positive]`(POS (xO x))+0`. +Check [x:positive]`(Zopp (POS (xO x)))`. +Check [x:positive]`(Zopp (POS (xO x)))+0`. +Check `(inject_nat O)+1`. +Check (Zplus `0` (inject_nat (plus O O))). +Check `(inject_nat O)=0`. + +(* Submitted by Pierre Casteran *) +Require Arith. +Check (Zplus `0` (inject_nat (11))). diff --git a/test-suite/output/implicits.out b/test-suite/output/implicits.out new file mode 100644 index 00000000..e4837199 --- /dev/null +++ b/test-suite/output/implicits.out @@ -0,0 +1,4 @@ +(compose 3!nat S) + : (nat->nat)->nat->nat +(ex_intro 2![_:nat]True 3!(0) I) + : (ex [_:nat]True) diff --git a/test-suite/output/implicits.v b/test-suite/output/implicits.v new file mode 100644 index 00000000..d7ea7227 --- /dev/null +++ b/test-suite/output/implicits.v @@ -0,0 +1,13 @@ +Set Implicit Arguments. + +(* Suggested by Pierre Casteran (bug #169) *) +(* Argument 3 is needed to typecheck and should be printed *) +Definition compose := [A,B,C:Set; f : A-> B ; g : B->C ; x : A] (g (f x)). +Check (compose 3!nat S). + +(* Better to explicitly display the arguments inferable from a + position that could disappear after reduction *) +Inductive ex [A:Set;P:A->Prop] : Prop + := ex_intro : (x:A)(P x)->(ex P). +Check (ex_intro 2![_]True 3!O I). + diff --git a/test-suite/success/Abstract.v8 b/test-suite/success/Abstract.v8 new file mode 100644 index 00000000..21a985bc --- /dev/null +++ b/test-suite/success/Abstract.v8 @@ -0,0 +1,26 @@ + +(* Cf coqbugs #546 *) + +Require Import Omega. + +Section S. + +Variables n m : nat. +Variable H : n<m. + +Inductive Dummy : nat -> Set := +| Dummy0 : Dummy 0 +| Dummy2 : Dummy 2 +| DummyApp : forall i j, Dummy i -> Dummy j -> Dummy (i+j). + +Definition Bug : Dummy (2*n). +Proof. +induction n. + simpl ; apply Dummy0. + replace (2 * S n0) with (2*n0 + 2) ; auto with arith. + apply DummyApp. + 2:exact Dummy2. + apply IHn0 ; abstract omega. +Defined. + +End S. diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v new file mode 100644 index 00000000..2d5a5134 --- /dev/null +++ b/test-suite/success/Case1.v @@ -0,0 +1,15 @@ +(* Testing eta-expansion of elimination predicate *) + +Section NATIND2. +Variable P : nat -> Type. +Variable H0 : (P O). +Variable H1 : (P (S O)). +Variable H2 : (n:nat)(P n)->(P (S (S n))). +Fixpoint nat_ind2 [n:nat] : (P n) := + <P>Cases n of + O => H0 + | (S O) => H1 + | (S (S n)) => (H2 n (nat_ind2 n)) + end. +End NATIND2. + diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v new file mode 100644 index 00000000..73413c47 --- /dev/null +++ b/test-suite/success/Case10.v @@ -0,0 +1,26 @@ +(* ============================================== *) +(* To test compilation of dependent case *) +(* Multiple Patterns *) +(* ============================================== *) +Inductive skel: Type := + PROP: skel + | PROD: skel->skel->skel. + +Parameter Can : skel -> Type. +Parameter default_can : (s:skel) (Can s). + + +Type [s1,s2:skel] + <[s1,_:skel](Can s1)>Cases s1 s2 of + PROP PROP => (default_can PROP) + | s1 _ => (default_can s1) + end. + + +Type [s1,s2:skel] +<[s1:skel][_:skel](Can s1)>Cases s1 s2 of + PROP PROP => (default_can PROP) +| (PROP as s) _ => (default_can s) +| ((PROD s1 s2) as s) PROP => (default_can s) +| ((PROD s1 s2) as s) _ => (default_can s) +end. diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v new file mode 100644 index 00000000..580cd87d --- /dev/null +++ b/test-suite/success/Case11.v @@ -0,0 +1,11 @@ +(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *) +(* Problème rapporté par Solange Coupet *) + +Section A. + +Variables Alpha:Set; Beta:Set. + +Definition nodep_prod_of_dep: (sigS Alpha [a:Alpha]Beta)-> Alpha*Beta:= +[c] Cases c of (existS a b)=>(a,b) end. + +End A. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v new file mode 100644 index 00000000..284695f4 --- /dev/null +++ b/test-suite/success/Case12.v @@ -0,0 +1,60 @@ +(* This example was proposed by Cuihtlauac ALVARADO *) + +Require PolyList. + +Fixpoint mult2 [n:nat] : nat := +Cases n of +| O => O +| (S n) => (S (S (mult2 n))) +end. + +Inductive list : nat -> Set := +| nil : (list O) +| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))). + +Type +[P:((n:nat)(list n)->Prop); + f:(P O nil); + f0:((n:nat; l:(list (mult2 n))) + (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))] + Fix F + {F [n:nat; l:(list n)] : (P n l) := + <P>Cases l of + nil => f + | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0)) + end}. + +Inductive list' : nat -> Set := +| nil' : (list' O) +| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))). + +Fixpoint length [n; l:(list' n)] : nat := + Cases l of + nil' => O + | (cons' _ m l0) => (S (length m l0)) + end. + +Type +[P:((n:nat)(list' n)->Prop); + f:(P O nil'); + f0:((n:nat) + [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))] + Fix F + {F [n:nat; l:(list' n)] : (P n l) := + <P> + Cases l of + nil' => f + | (cons' n0 m l0) => (f0 n0 l0 (F m l0)) + end}. + +(* Check on-the-fly insertion of let-in patterns for compatibility *) + +Inductive list'' : nat -> Set := +| nil'' : (list'' O) +| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p). + +Check Fix length { length [n; l:(list'' n)] : nat := + Cases l of + nil'' => O + | (cons'' n l0) => (S (length (mult2 n) l0)) + end }. diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v new file mode 100644 index 00000000..71c9191d --- /dev/null +++ b/test-suite/success/Case13.v @@ -0,0 +1,33 @@ +(* Check coercions in patterns *) + +Inductive I : Set := + C1 : nat -> I +| C2 : I -> I. + +Coercion C1 : nat >-> I. + +(* Coercion at the root of pattern *) +Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end. + +(* Coercion not at the root of pattern *) +Check [x]Cases x of (C2 O) => O | _ => O end. + +(* Unification and coercions inside patterns *) +Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end. + +(* Coercion up to delta-conversion, and unification *) +Coercion somenat := (Some nat). +Check [x]Cases x of None => O | O => O | (S n) => n end. + +(* Coercions with parameters *) +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Inductive I' : nat -> Set := + C1' : (n:nat) (listn n) -> (I' n) +| C2' : (n:nat) (I' n) -> (I' n). + +Coercion C1' : listn >-> I'. +Check [x:(I' O)]Cases x of (C2' _ _) => O | niln => O | _ => O end. +Check [x:(I' O)]Cases x of (C2' _ niln) => O | _ => O end. diff --git a/test-suite/success/Case14.v b/test-suite/success/Case14.v new file mode 100644 index 00000000..edecee79 --- /dev/null +++ b/test-suite/success/Case14.v @@ -0,0 +1,16 @@ +(* Test of inference of elimination predicate for "if" *) +(* submitted by Robert R Schneck *) + +Axiom bad : false = true. + +Definition try1 : False := + <[b:bool][_:false=b](if b then False else True)> + Cases bad of refl_equal => I end. + +Definition try2 : False := + <[b:bool][_:false=b]((if b then False else True)::Prop)> + Cases bad of refl_equal => I end. + +Definition try3 : False := + <[b:bool][_:false=b](([b':bool] if b' then False else True) b)> + Cases bad of refl_equal => I end. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v new file mode 100644 index 00000000..22944520 --- /dev/null +++ b/test-suite/success/Case15.v @@ -0,0 +1,48 @@ +(* Check compilation of multiple pattern-matching on terms non + apparently of inductive type *) + +(* Check that the non dependency in y is OK both in V7 and V8 *) +Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of + | O y z' => (or_introl ? (z'=z') (refl_equal ? O)) + | _ y O => (or_intror ?? (refl_equal ? O)) + | x y _ => (or_introl ?? (refl_equal ? x)) + end). + +(* Suggested by Pierre Letouzey (PR#207) *) +Inductive Boite : Set := + boite : (b:bool)(if b then nat else nat*nat)->Boite. + +Definition test := [B:Boite]<nat>Cases B of + (boite true n) => n +| (boite false (n,m)) => (plus n m) +end. + +(* Check lazyness of compilation ... future work +Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. + +Check [x] + Cases x of + (c (true as y) (true as x)) => (if x then y else true) + | (c false O) => true | _ => false + end. + +Check [x] + Cases x of + (c true true) => true + | (c false O) => true + | _ => false + end. + +(* Devrait produire ceci mais trouver le type intermediaire est coton ! *) +Check + [x:I] + Cases x of + (c b y) => + (<[b:bool](if b then bool else nat)->bool>if b + then [y](if y then true else false) + else [y]Cases y of + O => true + | (S _) => false + end y) + end. +*) diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v new file mode 100644 index 00000000..3f142fae --- /dev/null +++ b/test-suite/success/Case16.v @@ -0,0 +1,9 @@ +(**********************************************************************) +(* Test dependencies in constructors *) +(**********************************************************************) + +Check [x : {b:bool|if b then True else False}] + <[x]let (b,_) = x in if b then True else False>Cases x of + | (exist true y) => y + | (exist false z) => z + end. diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v new file mode 100644 index 00000000..07d64958 --- /dev/null +++ b/test-suite/success/Case17.v @@ -0,0 +1,45 @@ +(* Check the synthesis of predicate from a cast in case of matching of + the first component (here [list bool]) of a dependent type (here [sigS]) + (Simplification of an example from file parsing2.v of the Coq'Art + exercises) *) + +Require Import PolyList. + +Variable parse_rel : (list bool) -> (list bool) -> nat -> Prop. + +Variables l0:(list bool); rec:(l' : (list bool)) + (le (length l') (S (length l0))) -> + {l'' : (list bool) & + {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + + {(l'' : (list bool))(t : nat)~ (parse_rel l' l'' t)}. + +Axiom HHH : (A:Prop)A. + +Check (Cases (rec l0 (HHH ?)) of + | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) + | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => + (inright ? ? (HHH ?)) + | (inleft (existS _ _)) => (inright ? ? (HHH ?)) + | (inright Hnp) => (inright ? ? (HHH ?)) + end :: + {l'' : (list bool) & + {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). + +(* The same but with relative links to l0 and rec *) + +Check [l0:(list bool);rec:(l' : (list bool)) + (le (length l') (S (length l0))) -> + {l'' : (list bool) & + {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel l' l'' t)}] + (Cases (rec l0 (HHH ?)) of + | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) + | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => + (inright ? ? (HHH ?)) + | (inleft (existS _ _)) => (inright ? ? (HHH ?)) + | (inright Hnp) => (inright ? ? (HHH ?)) + end :: + {l'' : (list bool) & + {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + + {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). diff --git a/test-suite/success/Case2.v b/test-suite/success/Case2.v new file mode 100644 index 00000000..0aa7b5be --- /dev/null +++ b/test-suite/success/Case2.v @@ -0,0 +1,11 @@ +(* ============================================== *) +(* To test compilation of dependent case *) +(* Nested patterns *) +(* ============================================== *) + +Type <[n:nat]n=n>Cases O of + O => (refl_equal nat O) + | m => (refl_equal nat m) +end. + + diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v new file mode 100644 index 00000000..fe49cdf9 --- /dev/null +++ b/test-suite/success/Case5.v @@ -0,0 +1,14 @@ + +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v new file mode 100644 index 00000000..a262251e --- /dev/null +++ b/test-suite/success/Case6.v @@ -0,0 +1,19 @@ +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +[m:nat] + <[n,m:nat] n=m \/ ~n=m>Cases n m of + O O => (or_introl ? ~O=O (refl_equal ? O)) + + | O (S x) => (or_intror O=(S x) ? (discr_r x)) + + | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) + + | ((S x) as N) ((S y) as M) => + <N=M\/~N=M>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h)) + | (or_intror h) => (or_intror N=M ? (ff x y h)) + end + end. diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v new file mode 100644 index 00000000..6e2aea48 --- /dev/null +++ b/test-suite/success/Case7.v @@ -0,0 +1,16 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Inductive Empty [A:Set] : (List A)-> Prop := + intro_Empty: (Empty A (Nil A)). + +Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)). + + +Type +[A:Set] +[l:(List A)] + <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of + Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A)) + | ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y)) + end. diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v new file mode 100644 index 00000000..a5d07405 --- /dev/null +++ b/test-suite/success/Case9.v @@ -0,0 +1,55 @@ +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Inductive eqlong : (List nat)-> (List nat)-> Prop := + eql_cons : (n,m:nat)(x,y:(List nat)) + (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) +| eql_nil : (eqlong (Nil nat) (Nil nat)). + + +Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). +Parameter V2 : (a:nat)(x:(List nat)) + (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). +Parameter V3 : (a:nat)(x:(List nat)) + (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). +Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) + (eqlong (Cons nat a x)(Cons nat b y)) + \/ ~(eqlong (Cons nat a x) (Cons nat b y)). + +Parameter nff : (n,m:nat)(x,y:(List nat)) + ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)). +Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)). +Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)). + +Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) := +[y:(List nat)] + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of + Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) + + | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) + + | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) + + | ((Cons a x) as L1) ((Cons b y) as L2) => + <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of + (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) + | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + end + end. + + +Type + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of + Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) + + | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) + + | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) + + | ((Cons a x) as L1) ((Cons b y) as L2) => + <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of + (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) + | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + end + end. + diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v new file mode 100644 index 00000000..b5f0e730 --- /dev/null +++ b/test-suite/success/CaseAlias.v @@ -0,0 +1,21 @@ +(* This has been a bug reported by Y. Bertot *) +Inductive expr : Set := + b: expr -> expr -> expr + | u: expr -> expr + | a: expr + | var: nat -> expr . + +Fixpoint f [t : expr] : expr := + Cases t of + | (b t1 t2) => (b (f t1) (f t2)) + | a => a + | x => (b t a) + end. + +Fixpoint f2 [t : expr] : expr := + Cases t of + | (b t1 t2) => (b (f2 t1) (f2 t2)) + | a => a + | x => (b x a) + end. + diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v new file mode 100644 index 00000000..6ccd669a --- /dev/null +++ b/test-suite/success/Cases.v @@ -0,0 +1,1597 @@ +(****************************************************************************) +(* Pattern-matching when non inductive terms occur *) + +(* Dependent form of annotation *) +Type <[n:nat]nat>Cases O eq of O x => O | (S x) y => x end. +Type <[_,_:nat]nat>Cases O eq O of O x y => O | (S x) y z => x end. + +(* Non dependent form of annotation *) +Type <nat>Cases O eq of O x => O | (S x) y => x end. + +(* Combining dependencies and non inductive arguments *) +Type [A:Set][a:A][H:O=O]<[x][H]H==H>Cases H a of _ _ => (refl_eqT ? H) end. + +(* Interaction with coercions *) +Parameter bool2nat : bool -> nat. +Coercion bool2nat : bool >-> nat. +Check [x](Cases x of O => true | (S _) => O end :: nat). + +(****************************************************************************) +(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) + +Inductive IFExpr : Set := + Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. + +Inductive List [A:Set] :Set := + Nil:(List A) | Cons:A->(List A)->(List A). + +Inductive listn : nat-> Set := + niln : (listn O) +| consn : (n:nat)nat->(listn n) -> (listn (S n)). + +Inductive Listn [A:Set] : nat-> Set := + Niln : (Listn A O) +| Consn : (n:nat)nat->(Listn A n) -> (Listn A (S n)). + +Inductive Le : nat->nat->Set := + LeO: (n:nat)(Le O n) +| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)). + +Inductive LE [n:nat] : nat->Set := + LE_n : (LE n n) | LE_S : (m:nat)(LE n m)->(LE n (S m)). + +Require Bool. + + + +Inductive PropForm : Set := + Fvar : nat -> PropForm + | Or : PropForm -> PropForm -> PropForm . + +Section testIFExpr. +Definition Assign:= nat->bool. +Parameter Prop_sem : Assign -> PropForm -> bool. + +Type [A:Assign][F:PropForm] + <bool>Cases F of + (Fvar n) => (A n) + | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G)) + end. + +Type [A:Assign][H:PropForm] + <bool>Cases H of + (Fvar n) => (A n) + | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G)) + end. +End testIFExpr. + + + +Type [x:nat]<nat>Cases x of O => O | x => x end. + +Section testlist. +Parameter A:Set. +Inductive list : Set := nil : list | cons : A->list->list. +Parameter inf: A->A->Prop. + + +Definition list_Lowert2 := + [a:A][l:list](<Prop>Cases l of nil => True + | (cons b l) =>(inf a b) end). + +Definition titi := + [a:A][l:list](<list>Cases l of nil => l + | (cons b l) => l end). +Reset list. +End testlist. + + +(* To test translation *) +(* ------------------- *) + + +Type <nat>Cases O of O => O | _ => O end. + +Type <nat>Cases O of + (O as b) => b + | (S O) => O + | (S (S x)) => x end. + +Type Cases O of + (O as b) => b + | (S O) => O + | (S (S x)) => x end. + + +Type [x:nat]<nat>Cases x of + (O as b) => b + | (S x) => x end. + +Type [x:nat]Cases x of + (O as b) => b + | (S x) => x end. + +Type <nat>Cases O of + (O as b) => b + | (S x) => x end. + +Type <nat>Cases O of + x => x + end. + +Type Cases O of + x => x + end. + +Type <nat>Cases O of + O => O + | ((S x) as b) => b + end. + +Type [x:nat]<nat>Cases x of + O => O + | ((S x) as b) => b + end. + +Type [x:nat] Cases x of + O => O + | ((S x) as b) => b + end. + + +Type <nat>Cases O of + O => O + | (S x) => O + end. + + +Type <nat*nat>Cases O of + O => (O,O) + | (S x) => (x,O) + end. + +Type Cases O of + O => (O,O) + | (S x) => (x,O) + end. + +Type <nat->nat>Cases O of + O => [n:nat]O + | (S x) => [n:nat]O + end. + +Type Cases O of + O => [n:nat]O + | (S x) => [n:nat]O + end. + + +Type <nat->nat>Cases O of + O => [n:nat]O + | (S x) => [n:nat](plus x n) + end. + +Type Cases O of + O => [n:nat]O + | (S x) => [n:nat](plus x n) + end. + + +Type <nat>Cases O of + O => O + | ((S x) as b) => (plus b x) + end. + +Type <nat>Cases O of + O => O + | ((S (x as a)) as b) => (plus b a) + end. +Type Cases O of + O => O + | ((S (x as a)) as b) => (plus b a) + end. + + +Type Cases O of + O => O + | _ => O + end. + +Type <nat>Cases O of + O => O + | x => x + end. + +Type <nat>Cases O (S O) of + x y => (plus x y) + end. + +Type Cases O (S O) of + x y => (plus x y) + end. + +Type <nat>Cases O (S O) of + O y => y + | (S x) y => (plus x y) + end. + +Type Cases O (S O) of + O y => y + | (S x) y => (plus x y) + end. + + +Type <nat>Cases O (S O) of + O x => x + | (S y) O => y + | x y => (plus x y) + end. + + + + +Type Cases O (S O) of + O x => (plus x O) + | (S y) O => (plus y O) + | x y => (plus x y) + end. + +Type + <nat>Cases O (S O) of + O x => (plus x O) + | (S y) O => (plus y O) + | x y => (plus x y) + end. + + +Type + <nat>Cases O (S O) of + O x => x + | ((S x) as b) (S y) => (plus (plus b x) y) + | x y => (plus x y) + end. + + +Type Cases O (S O) of + O x => x + | ((S x) as b) (S y) => (plus (plus b x) y) + | x y => (plus x y) + end. + + +Type [l:(List nat)]<(List nat)>Cases l of + Nil => (Nil nat) + | (Cons a l) => l + end. + +Type [l:(List nat)] Cases l of + Nil => (Nil nat) + | (Cons a l) => l + end. + +Type <nat>Cases (Nil nat) of + Nil =>O + | (Cons a l) => (S a) + end. +Type Cases (Nil nat) of + Nil =>O + | (Cons a l) => (S a) + end. + +Type <(List nat)>Cases (Nil nat) of + (Cons a l) => l + | x => x + end. + +Type Cases (Nil nat) of + (Cons a l) => l + | x => x + end. + +Type <(List nat)>Cases (Nil nat) of + Nil => (Nil nat) + | (Cons a l) => l + end. + +Type Cases (Nil nat) of + Nil => (Nil nat) + | (Cons a l) => l + end. + + +Type + <nat>Cases O of + O => O + | (S x) => <nat>Cases (Nil nat) of + Nil => x + | (Cons a l) => (plus x a) + end + end. + +Type + Cases O of + O => O + | (S x) => Cases (Nil nat) of + Nil => x + | (Cons a l) => (plus x a) + end + end. + +Type + [y:nat]Cases y of + O => O + | (S x) => Cases (Nil nat) of + Nil => x + | (Cons a l) => (plus x a) + end + end. + + +Type + <nat>Cases O (Nil nat) of + O x => O + | (S x) Nil => x + | (S x) (Cons a l) => (plus x a) + end. + + + +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of + niln => O + | x => O + end. + +Type [n:nat][l:(listn n)] + Cases l of + niln => O + | x => O + end. + + +Type <[_:nat]nat>Cases niln of + niln => O + | x => O + end. + +Type Cases niln of + niln => O + | x => O + end. + + +Type <[_:nat]nat>Cases niln of + niln => O + | (consn n a l) => a + end. +Type Cases niln of niln => O + | (consn n a l) => a + end. + + +Type <[n:nat][_:(listn n)]nat>Cases niln of + (consn m _ niln) => m + | _ => (S O) end. + + + +Type [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of + O niln => O + | y x => O + end. + +Type <[_:nat]nat>Cases O niln of + O niln => O + | y x => O + end. + + +Type <[_:nat]nat>Cases niln O of + niln O => O + | y x => O + end. + +Type Cases niln O of + niln O => O + | y x => O + end. + +Type <[_:nat][_:nat]nat>Cases niln niln of + niln niln => O + | x y => O + end. + +Type Cases niln niln of + niln niln => O + | x y => O + end. + +Type <[_,_,_:nat]nat>Cases niln niln niln of + niln niln niln => O + | x y z => O + end. + + +Type Cases niln niln niln of + niln niln niln => O + | x y z => O + end. + + + +Type <[_:nat]nat>Cases (niln) of + niln => O + | (consn n a l) => O + end. + +Type Cases (niln) of + niln => O + | (consn n a l) => O + end. + + +Type <[_:nat][_:nat]nat>Cases niln niln of + niln niln => O + | niln (consn n a l) => n + | (consn n a l) x => a + end. + + +Type Cases niln niln of + niln niln => O + | niln (consn n a l) => n + | (consn n a l) x => a + end. + + +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of + niln => O + | x => O + end. + +Type [c:nat;s:bool] + <[_:nat;_:bool]nat>Cases c s of + | O _ => O + | _ _ => c + end. + +Type [c:nat;s:bool] + <[_:nat;_:bool]nat>Cases c s of + | O _ => O + | (S _) _ => c + end. + + +(* Rows of pattern variables: some tricky cases *) +Axiom P:nat->Prop; f:(n:nat)(P n). + +Type [i:nat] + <[_:bool;n:nat](P n)>Cases true i of + | true k => (f k) + | _ k => (f k) + end. + +Type [i:nat] + <[n:nat;_:bool](P n)>Cases i true of + | k true => (f k) + | k _ => (f k) + end. + +(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe + * it has to synthtize the predicate on O (which he can't) + *) +Type <[n]Cases n of O => bool | (S _) => nat end>Cases O of + O => true + | (S _) => O + end. + +Type [n:nat][l:(listn n)]Cases l of + niln => O + | x => O + end. + +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + + +Type [n:nat][l:(listn n)]Cases l of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + + + +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + +Type [n:nat][l:(listn n)]Cases l of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + + +Type [A:Set][n:nat][l:(Listn A n)]<[_:nat]nat>Cases l of + Niln => O + | (Consn n a Niln) => O + | (Consn n a (Consn m b l)) => (plus n m) + end. + +Type [A:Set][n:nat][l:(Listn A n)]Cases l of + Niln => O + | (Consn n a Niln) => O + | (Consn n a (Consn m b l)) => (plus n m) + end. + +(* +Type [A:Set][n:nat][l:(Listn A n)] + <[_:nat](Listn A O)>Cases l of + (Niln as b) => b + | (Consn n a (Niln as b))=> (Niln A) + | (Consn n a (Consn m b l)) => (Niln A) + end. + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + (Niln as b) => b + | (Consn n a (Niln as b))=> (Niln A) + | (Consn n a (Consn m b l)) => (Niln A) + end. +*) +(******** This example rises an error unconstrained_variables! +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + (Niln as b) => (Consn A O O b) + | ((Consn n a Niln) as L) => L + | (Consn n a _) => (Consn A O O (Niln A)) + end. +**********) + +(* To test tratement of as-patterns in depth *) +Type [A:Set] [l:(List A)] + Cases l of + (Nil as b) => (Nil A) + | ((Cons a Nil) as L) => L + | ((Cons a (Cons b m)) as L) => L + end. + + +Type [n:nat][l:(listn n)] + <[_:nat](listn n)>Cases l of + niln => l + | (consn n a c) => l + end. +Type [n:nat][l:(listn n)] + Cases l of + niln => l + | (consn n a c) => l + end. + + +Type [n:nat][l:(listn n)] + <[_:nat](listn n)>Cases l of + (niln as b) => l + | _ => l + end. + + +Type [n:nat][l:(listn n)] + Cases l of + (niln as b) => l + | _ => l + end. + +Type [n:nat][l:(listn n)] + <[_:nat](listn n)>Cases l of + (niln as b) => l + | x => l + end. + + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + (Niln as b) => l + | _ => l + end. + +Type [A:Set][n:nat][l:(Listn A n)] + <[_:nat](Listn A n)>Cases l of + Niln => l + | (Consn n a Niln) => l + | (Consn n a (Consn m b c)) => l + end. + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + Niln => l + | (Consn n a Niln) => l + | (Consn n a (Consn m b c)) => l + end. + +Type [A:Set][n:nat][l:(Listn A n)] + <[_:nat](Listn A n)>Cases l of + (Niln as b) => l + | (Consn n a (Niln as b)) => l + | (Consn n a (Consn m b _)) => l + end. + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + (Niln as b) => l + | (Consn n a (Niln as b)) => l + | (Consn n a (Consn m b _)) => l + end. + + +Type <[_:nat]nat>Cases (niln) of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + + +Type Cases (niln) of + niln => O + | (consn n a niln) => O + | (consn n a (consn m b l)) => (plus n m) + end. + +Type <[_,_:nat]nat>Cases (LeO O) of + (LeO x) => x + | (LeS n m h) => (plus n m) + end. + + +Type Cases (LeO O) of + (LeO x) => x + | (LeS n m h) => (plus n m) + end. + +Type [n:nat][l:(Listn nat n)] + <[_:nat]nat>Cases l of + Niln => O + | (Consn n a l) => O + end. + + +Type [n:nat][l:(Listn nat n)] + Cases l of + Niln => O + | (Consn n a l) => O + end. + + +Type Cases (Niln nat) of + Niln => O + | (Consn n a l) => O + end. + +Type <[_:nat]nat>Cases (LE_n O) of + LE_n => O + | (LE_S m h) => O + end. + + +Type Cases (LE_n O) of + LE_n => O + | (LE_S m h) => O + end. + + + +Type Cases (LE_n O) of + LE_n => O + | (LE_S m h) => O + end. + + + +Type <[_:nat]nat>Cases (niln ) of + niln => O + | (consn n a niln) => n + | (consn n a (consn m b l)) => (plus n m) + end. + +Type Cases (niln ) of + niln => O + | (consn n a niln) => n + | (consn n a (consn m b l)) => (plus n m) + end. + + +Type <[_:nat]nat>Cases (Niln nat) of + Niln => O + | (Consn n a Niln) => n + | (Consn n a (Consn m b l)) => (plus n m) + end. + +Type Cases (Niln nat) of + Niln => O + | (Consn n a Niln) => n + | (Consn n a (Consn m b l)) => (plus n m) + end. + + +Type <[_,_:nat]nat>Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) => (plus n x) + end. + + +Type Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) => (plus n x) + end. + + +Type <[_,_:nat]nat>Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) => m + end. + +Type Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) => m + end. + + +Type [n,m:nat][h:(Le n m)] + <[_,_:nat]nat>Cases h of + (LeO x) => x + | x => O + end. + +Type [n,m:nat][h:(Le n m)] + Cases h of + (LeO x) => x + | x => O + end. + + +Type [n,m:nat][h:(Le n m)] + <[_,_:nat]nat>Cases h of + (LeS n m h) => n + | x => O + end. + + +Type [n,m:nat][h:(Le n m)] + Cases h of + (LeS n m h) => n + | x => O + end. + + +Type [n,m:nat][h:(Le n m)] + <[_,_:nat]nat*nat>Cases h of + (LeO n) => (O,n) + |(LeS n m _) => ((S n),(S m)) + end. + + +Type [n,m:nat][h:(Le n m)] + Cases h of + (LeO n) => (O,n) + |(LeS n m _) => ((S n),(S m)) + end. + + +Fixpoint F [n,m:nat; h:(Le n m)] : (Le n (S m)) := + <[n,m:nat](Le n (S m))>Cases h of + (LeO m') => (LeO (S m')) + | (LeS n' m' h') => (LeS n' (S m') (F n' m' h')) + end. + +Reset F. + +Fixpoint F [n,m:nat; h:(Le n m)] :(Le n (S m)) := + <[n,m:nat](Le n (S m))>Cases h of + (LeS n m h) => (LeS n (S m) (F n m h)) + | (LeO m) => (LeO (S m)) + end. + +(* Rend la longueur de la liste *) +Definition length1:= [n:nat] [l:(listn n)] + <[_:nat]nat>Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + +Reset length1. +Definition length1:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S O) + | _ => O + end. + + +Definition length2:= [n:nat] [l:(listn n)] + <[_:nat]nat>Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S n) + | _ => O + end. + +Reset length2. + +Definition length2:= [n:nat] [l:(listn n)] + Cases l of + (consn n _ (consn m _ _)) => (S (S m)) + |(consn n _ _) => (S n) + | _ => O + end. + +Definition length3 := +[n:nat][l:(listn n)] + <[_:nat]nat>Cases l of + (consn n _ (consn m _ l)) => (S n) + |(consn n _ _) => (S O) + | _ => O + end. + + +Reset length3. + +Definition length3 := +[n:nat][l:(listn n)] + Cases l of + (consn n _ (consn m _ l)) => (S n) + |(consn n _ _) => (S O) + | _ => O + end. + + +Type <[_,_:nat]nat>Cases (LeO O) of + (LeS n m h) =>(plus n m) + | x => O + end. +Type Cases (LeO O) of + (LeS n m h) =>(plus n m) + | x => O + end. + +Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) + end. + + +Type [n,m:nat][h:(Le n m)]Cases h of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) + end. + +Type <[_,_:nat]nat>Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) + end. + +Type Cases (LeO O) of + (LeO x) => x + | (LeS n m (LeO x)) => (plus x m) + | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) + end. + + +Type <[_:nat]nat>Cases (LE_n O) of + LE_n => O + | (LE_S m LE_n) => (plus O m) + | (LE_S m (LE_S y h)) => (plus O m) + end. + + +Type Cases (LE_n O) of + LE_n => O + | (LE_S m LE_n) => (plus O m) + | (LE_S m (LE_S y h)) => (plus O m) + end. + + +Type [n,m:nat][h:(Le n m)] Cases h of + x => x + end. + +Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of + (LeO n) => n + | x => O + end. +Type [n,m:nat][h:(Le n m)] Cases h of + (LeO n) => n + | x => O + end. + + +Type [n:nat]<[_:nat]nat->nat>Cases niln of + niln => [_:nat]O + | (consn n a niln) => [_:nat]O + | (consn n a (consn m b l)) => [_:nat](plus n m) + end. + + +Type [n:nat] Cases niln of + niln => [_:nat]O + | (consn n a niln) => [_:nat]O + | (consn n a (consn m b l)) => [_:nat](plus n m) + end. + +Type [A:Set][n:nat][l:(Listn A n)] + <[_:nat]nat->nat>Cases l of + Niln => [_:nat]O + | (Consn n a Niln) => [_:nat] n + | (Consn n a (Consn m b l)) => [_:nat](plus n m) + end. + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + Niln => [_:nat]O + | (Consn n a Niln) => [_:nat] n + | (Consn n a (Consn m b l)) => [_:nat](plus n m) + end. + +(* Alsos tests for multiple _ patterns *) +Type [A:Set][n:nat][l:(Listn A n)] + <[n:nat](Listn A n)>Cases l of + (Niln as b) => b + | ((Consn _ _ _ ) as b)=> b + end. + +(** Horrible error message! + +Type [A:Set][n:nat][l:(Listn A n)] + Cases l of + (Niln as b) => b + | ((Consn _ _ _ ) as b)=> b + end. +******) + +Type <[n:nat](listn n)>Cases niln of + (niln as b) => b + | ((consn _ _ _ ) as b)=> b + end. + + +Type <[n:nat](listn n)>Cases niln of + (niln as b) => b + | x => x + end. + +Type [n,m:nat][h:(LE n m)]<[_:nat]nat->nat>Cases h of + LE_n => [_:nat]n + | (LE_S m LE_n) => [_:nat](plus n m) + | (LE_S m (LE_S y h)) => [_:nat](plus m y ) + end. +Type [n,m:nat][h:(LE n m)]Cases h of + LE_n => [_:nat]n + | (LE_S m LE_n) => [_:nat](plus n m) + | (LE_S m (LE_S y h)) => [_:nat](plus m y ) + end. + + +Type [n,m:nat][h:(LE n m)] + <[_:nat]nat>Cases h of + LE_n => n + | (LE_S m LE_n ) => (plus n m) + | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y) + | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y')) + end. + + + +Type [n,m:nat][h:(LE n m)] + Cases h of + LE_n => n + | (LE_S m LE_n ) => (plus n m) + | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y) + | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y')) + end. + + +Type [n,m:nat][h:(LE n m)]<[_:nat]nat>Cases h of + LE_n => n + | (LE_S m LE_n) => (plus n m) + | (LE_S m (LE_S y h)) => (plus (plus n m) y) + end. + + +Type [n,m:nat][h:(LE n m)]Cases h of + LE_n => n + | (LE_S m LE_n) => (plus n m) + | (LE_S m (LE_S y h)) => (plus (plus n m) y) + end. + +Type [n,m:nat] + <[_,_:nat]nat>Cases (LeO O) of + (LeS n m h) =>(plus n m) + | x => O + end. + +Type [n,m:nat] + Cases (LeO O) of + (LeS n m h) =>(plus n m) + | x => O + end. + +Parameter test : (n:nat){(le O n)}+{False}. +Type [n:nat]<nat>Cases (test n) of + (left _) => O + | _ => O end. + + +Type [n:nat] <nat> Cases (test n) of + (left _) => O + | _ => O end. + +Type [n:nat]Cases (test n) of + (left _) => O + | _ => O end. + +Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. +Type <nat>Cases (compare O O) of + (* k<i *) (inleft (left _)) => O + | (* k=i *) (inleft _) => O + | (* k>i *) (inright _) => O end. + +Type Cases (compare O O) of + (* k<i *) (inleft (left _)) => O + | (* k=i *) (inleft _) => O + | (* k>i *) (inright _) => O end. + + + +CoInductive SStream [A:Set] : (nat->A->Prop)->Type := +scons : + (P:nat->A->Prop)(a:A)(P O a)->(SStream A [n:nat](P (S n)))->(SStream A P). +Parameter B : Set. + +Type + [P:nat->B->Prop][x:(SStream B P)]<[_:nat->B->Prop]B>Cases x of + (scons _ a _ _) => a end. + + +Type + [P:nat->B->Prop][x:(SStream B P)] Cases x of + (scons _ a _ _) => a end. + +Type <nat*nat>Cases (O,O) of (x,y) => ((S x),(S y)) end. +Type <nat*nat>Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. +Type <nat*nat>Cases (O,O) of (pair x y) => ((S x),(S y)) end. + +Type Cases (O,O) of (x,y) => ((S x),(S y)) end. +Type Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. +Type Cases (O,O) of (pair x y) => ((S x),(S y)) end. + + + +Parameter concat : (A:Set)(List A) ->(List A) ->(List A). + +Type <(List nat)>Cases (Nil nat) (Nil nat) of + (Nil as b) x => (concat nat b x) + | ((Cons _ _) as d) (Nil as c) => (concat nat d c) + | _ _ => (Nil nat) + end. +Type Cases (Nil nat) (Nil nat) of + (Nil as b) x => (concat nat b x) + | ((Cons _ _) as d) (Nil as c) => (concat nat d c) + | _ _ => (Nil nat) + end. + + +Inductive redexes : Set := + VAR : nat -> redexes + | Fun : redexes -> redexes + | Ap : bool -> redexes -> redexes -> redexes. + +Fixpoint regular [U:redexes] : Prop := <Prop>Cases U of + (VAR n) => True +| (Fun V) => (regular V) +| (Ap true ((Fun _) as V) W) => (regular V) /\ (regular W) +| (Ap true _ W) => False +| (Ap false V W) => (regular V) /\ (regular W) +end. + + +Type [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end. + +Reset concat. +Parameter concat :(n:nat) (listn n) -> (m:nat) (listn m)-> (listn (plus n m)). +Type [n:nat][l:(listn n)][m:nat][l':(listn m)] + <[n,_:nat](listn (plus n m))>Cases l l' of + niln x => x + | (consn n a l'') x =>(consn (plus n m) a (concat n l'' m x)) + end. + +Type [x,y,z:nat] + [H:x=y] + [H0:y=z]<[_:nat]x=z>Cases H of refl_equal => + <[n:nat]x=n>Cases H0 of refl_equal => H + end + end. + +Type [h:False]<False>Cases h of end. + +Type [h:False]<True>Cases h of end. + +Definition is_zero := [n:nat]Cases n of O => True | _ => False end. + +Type [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end. + +Definition disc : (n:nat)O=(S n)->False := + [n:nat][h:O=(S n)] + <[n:nat](is_zero n)>Cases h of refl_equal => I end. + +Definition nlength3 := [n:nat] [l: (listn n)] + Cases l of + niln => O + | (consn O _ _) => (S O) + | (consn (S n) _ _) => (S (S n)) + end. + +(* == Testing strategy elimintation predicate synthesis == *) +Section titi. +Variable h:False. +Type Cases O of + O => O + | _ => (Except h) + end. +End titi. + +Type Cases niln of + (consn _ a niln) => a + | (consn n _ x) => O + | niln => O + end. + + + +Inductive wsort : Set := ws : wsort | wt : wsort. +Inductive TS : wsort->Set := + id :(TS ws) +| lift:(TS ws)->(TS ws). + +Type [b:wsort][M:(TS b)][N:(TS b)] + Cases M N of + (lift M1) id => False + | _ _ => True + end. + + + +(* ===================================================================== *) +(* To test pattern matching over a non-dependent inductive type, but *) +(* having constructors with some arguments that depend on others *) +(* I.e. to test manipulation of elimination predicate *) +(* ===================================================================== *) + + +Parameter LTERM : nat -> Set. +Mutual Inductive TERM : Type := + var : TERM + | oper : (op:nat) (LTERM op) -> TERM. + +Parameter t1, t2:TERM. + +Type Cases t1 t2 of + var var => True + + | (oper op1 l1) (oper op2 l2) => False + | _ _ => False + end. +Reset LTERM. + + + +Require Peano_dec. +Parameter n:nat. +Definition eq_prf := (EXT m | n=m). +Parameter p:eq_prf . + +Type Cases p of + (exT_intro c eqc) => + Cases (eq_nat_dec c n) of + (right _) => (refl_equal ? n) + |(left y) (* c=n*) => (refl_equal ? n) + end + end. + + +Parameter ordre_total : nat->nat->Prop. + +Parameter N_cla:(N:nat){N=O}+{N=(S O)}+{(ge N (S (S O)))}. + +Parameter exist_U2:(N:nat)(ge N (S (S O)))-> + {n:nat|(m:nat)(lt O m)/\(le m N) + /\(ordre_total n m) + /\(lt O n)/\(lt n N)}. + +Type [N:nat](Cases (N_cla N) of + (inright H)=>(Cases (exist_U2 N H) of + (exist a b)=>a + end) + | _ => O + end). + + + +(* ============================================== *) +(* To test compilation of dependent case *) +(* Nested patterns *) +(* ============================================== *) + +(* == To test that terms named with AS are correctly absolutized before + substitution in rhs == *) + +Type [n:nat]<[n:nat]nat>Cases (n) of + O => O + | (S O) => O + | ((S (S n1)) as N) => N + end. + +(* ========= *) + +Type <[n:nat][_:(listn n)]Prop>Cases niln of + niln => True + | (consn (S O) _ _) => False + | _ => True end. + +Type <[n:nat][_:(listn n)]Prop>Cases niln of + niln => True + | (consn (S (S O)) _ _) => False + | _ => True end. + + +Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of + (LeO _) => O + | (LeS (S x) _ _) => x + | _ => (S O) end. + +Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of + (LeO _) => O + | (LeS (S x) (S y) _) => x + | _ => (S O) end. + +Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of + (LeO _) => O + | (LeS ((S x) as b) (S y) _) => b + | _ => (S O) end. + + + +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S x) => (or_intror (S x)=O ? (discr_l x)) + end. + + +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +[m:nat] + <[n,m:nat] n=m \/ ~n=m>Cases n m of + O O => (or_introl ? ~O=O (refl_equal ? O)) + + | O (S x) => (or_intror O=(S x) ? (discr_r x)) + + | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) + + | (S x) (S y) => + <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h)) + | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) + end + end. + +Reset eqdec. + +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of + O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of + O => (or_introl ? ~O=O (refl_equal nat O)) + |(S x) => (or_intror O=(S x) ? (discr_r x)) + end + | (S x) => [m:nat] + <[m:nat](S x)=m\/~(S x)=m>Cases m of + O => (or_intror (S x)=O ? (discr_l x)) + | (S y) => + <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h)) + | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) + end + end + end. + + +Inductive empty : (n:nat)(listn n)-> Prop := + intro_empty: (empty O niln). + +Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + end. + +Reset ff. +Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). +Parameter discr_r : (n:nat) ~(O=(S n)). +Parameter discr_l : (n:nat) ~((S n)=O). + +Type +[n:nat] + <[n:nat]n=O\/~n=O>Cases n of + O => (or_introl ? ~O=O (refl_equal ? O)) + | (S x) => (or_intror (S x)=O ? (discr_l x)) + end. + + +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +[m:nat] + <[n,m:nat] n=m \/ ~n=m>Cases n m of + O O => (or_introl ? ~O=O (refl_equal ? O)) + + | O (S x) => (or_intror O=(S x) ? (discr_r x)) + + | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) + + | (S x) (S y) => + <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h)) + | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) + end + end. +Reset eqdec. + +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of + O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of + O => (or_introl ? ~O=O (refl_equal nat O)) + |(S x) => (or_intror O=(S x) ? (discr_r x)) + end + | (S x) => [m:nat] + <[m:nat](S x)=m\/~(S x)=m>Cases m of + O => (or_intror (S x)=O ? (discr_l x)) + | (S y) => + <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h)) + | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) + end + end + end. + + +(* ================================================== *) +(* Pour tester parametres *) +(* ================================================== *) + + +Inductive Empty [A:Set] : (List A)-> Prop := + intro_Empty: (Empty A (Nil A)). + +Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)). + + +Type + <[l:(List nat)](Empty nat l) \/ ~(Empty nat l)>Cases (Nil nat) of + Nil => (or_introl ? ~(Empty nat (Nil nat)) (intro_Empty nat)) + | (Cons a y) => (or_intror (Empty nat (Cons nat a y)) ? + (inv_Empty nat a y)) + end. + + +(* ================================================== *) +(* Sur les listes *) +(* ================================================== *) + + +Inductive empty : (n:nat)(listn n)-> Prop := + intro_empty: (empty O niln). + +Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). + +Type +[n:nat] [l:(listn n)] + <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of + niln => (or_introl ? ~(empty O niln) intro_empty) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + end. + +(* ===================================== *) +(* Test parametros: *) +(* ===================================== *) + +Inductive eqlong : (List nat)-> (List nat)-> Prop := + eql_cons : (n,m:nat)(x,y:(List nat)) + (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) +| eql_nil : (eqlong (Nil nat) (Nil nat)). + + +Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). +Parameter V2 : (a:nat)(x:(List nat)) + (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). +Parameter V3 : (a:nat)(x:(List nat)) + (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). +Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) + (eqlong (Cons nat a x)(Cons nat b y)) + \/ ~(eqlong (Cons nat a x) (Cons nat b y)). + +Type + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of + Nil Nil => V1 + | Nil (Cons a x) => (V2 a x) + | (Cons a x) Nil => (V3 a x) + | (Cons a x) (Cons b y) => (V4 a x b y) + end. + + +Type +[x,y:(List nat)] + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of + Nil Nil => V1 + | Nil (Cons a x) => (V2 a x) + | (Cons a x) Nil => (V3 a x) + | (Cons a x) (Cons b y) => (V4 a x b y) + end. + + +(* ===================================== *) + +Inductive Eqlong : (n:nat) (listn n)-> (m:nat) (listn m)-> Prop := + Eql_cons : (n,m:nat )(x:(listn n))(y:(listn m)) (a,b:nat) + (Eqlong n x m y) + ->(Eqlong (S n) (consn n a x) (S m) (consn m b y)) +| Eql_niln : (Eqlong O niln O niln). + + +Parameter W1 : (Eqlong O niln O niln)\/ ~(Eqlong O niln O niln). +Parameter W2 : (n,a:nat)(x:(listn n)) + (Eqlong O niln (S n)(consn n a x)) \/ ~(Eqlong O niln (S n) (consn n a x)). +Parameter W3 : (n,a:nat)(x:(listn n)) + (Eqlong (S n) (consn n a x) O niln) \/ ~(Eqlong (S n) (consn n a x) O niln). +Parameter W4 : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) + (Eqlong (S n)(consn n a x) (S m) (consn m b y)) + \/ ~(Eqlong (S n)(consn n a x) (S m) (consn m b y)). + +Type + <[n:nat][x:(listn n)][m:nat][y:(listn m)] + (Eqlong n x m y)\/~(Eqlong n x m y)>Cases niln niln of + niln niln => W1 + | niln (consn n a x) => (W2 n a x) + | (consn n a x) niln => (W3 n a x) + | (consn n a x) (consn m b y) => (W4 n a x m b y) + end. + + +Type +[n,m:nat][x:(listn n)][y:(listn m)] + <[n:nat][x:(listn n)][m:nat][y:(listn m)] + (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of + niln niln => W1 + | niln (consn n a x) => (W2 n a x) + | (consn n a x) niln => (W3 n a x) + | (consn n a x) (consn m b y) => (W4 n a x m b y) + end. + + +Parameter Inv_r : (n,a:nat)(x:(listn n)) ~(Eqlong O niln (S n) (consn n a x)). +Parameter Inv_l : (n,a:nat)(x:(listn n)) ~(Eqlong (S n) (consn n a x) O niln). +Parameter Nff : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) + ~(Eqlong n x m y) + -> ~(Eqlong (S n) (consn n a x) (S m) (consn m b y)). + + + +Fixpoint Eqlongdec [n:nat; x:(listn n)] : (m:nat)(y:(listn m)) + (Eqlong n x m y)\/~(Eqlong n x m y) +:= [m:nat][y:(listn m)] + <[n:nat][x:(listn n)][m:nat][y:(listn m)] + (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of + niln niln => (or_introl ? ~(Eqlong O niln O niln) Eql_niln) + + | niln ((consn n a x) as L) => + (or_intror (Eqlong O niln (S n) L) ? (Inv_r n a x)) + + | ((consn n a x) as L) niln => + (or_intror (Eqlong (S n) L O niln) ? (Inv_l n a x)) + + + | ((consn n a x) as L1) ((consn m b y) as L2) => + <(Eqlong (S n) L1 (S m) L2) \/~(Eqlong (S n) L1 (S m) L2)> + Cases (Eqlongdec n x m y) of + (or_introl h) => + (or_introl ? ~(Eqlong (S n) L1 (S m) L2)(Eql_cons n m x y a b h)) + | (or_intror h) => + (or_intror (Eqlong (S n) L1 (S m) L2) ? (Nff n a x m b y h)) + end + end. + +(* ============================================== *) +(* To test compilation of dependent case *) +(* Multiple Patterns *) +(* ============================================== *) +Inductive skel: Type := + PROP: skel + | PROD: skel->skel->skel. + +Parameter Can : skel -> Type. +Parameter default_can : (s:skel) (Can s). + +Type [s1,s2:skel] +[s1,s2:skel]<[s1:skel][_:skel](Can s1)>Cases s1 s2 of + PROP PROP => (default_can PROP) +| (PROD x y) PROP => (default_can (PROD x y)) +| (PROD x y) _ => (default_can (PROD x y)) +| PROP _ => (default_can PROP) +end. + +(* to test bindings in nested Cases *) +(* ================================ *) +Inductive Pair : Set := + pnil : Pair | + pcons : Pair -> Pair -> Pair. + +Type [p,q:Pair]Cases p of + (pcons _ x) => + Cases q of + (pcons _ (pcons _ x)) => True + | _ => False + end +| _ => False +end. + + +Type [p,q:Pair]Cases p of + (pcons _ x) => + Cases q of + (pcons _ (pcons _ x)) => + Cases q of + (pcons _ (pcons _ (pcons _ x))) => x + | _ => pnil + end + | _ => pnil + end +| _ => pnil +end. + +Type + [n:nat] + [l:(listn (S n))] + <[z:nat](listn (pred z))>Cases l of + niln => niln + | (consn n _ l) => + <[m:nat](listn m)>Cases l of + niln => niln + | b => b + end + end. + + + +(* Test de la syntaxe avec nombres *) +Require Arith. +Type [n]Cases n of (2) => true | _ => false end. + +Require ZArith. +Type [n]Cases n of `0` => true | _ => false end. diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v new file mode 100644 index 00000000..0256280c --- /dev/null +++ b/test-suite/success/CasesDep.v @@ -0,0 +1,405 @@ +(* Check forward dependencies *) + +Check [P:nat->Prop][Q][A:(P O)->Q][B:(n:nat)(P (S n))->Q][x] + <[_]Q>Cases x of + | (exist O H) => (A H) + | (exist (S n) H) => (B n H) + end. + +(* Check dependencies in anonymous arguments (from FTA/listn.v) *) + +Inductive listn [A:Set] : nat->Set := + niln: (listn A O) +| consn: (a:A)(n:nat)(listn A n)->(listn A (S n)). + +Section Folding. +Variables B, C : Set. +Variable g : B -> C -> C. +Variable c : C. + +Fixpoint foldrn [n:nat; bs:(listn B n)] : C := + Cases bs of niln => c + | (consn b _ tl) => (g b (foldrn ? tl)) + end. +End Folding. + +(* -------------------------------------------------------------------- *) +(* Example to test patterns matching on dependent families *) +(* This exemple extracted from the developement done by Nacira Chabane *) +(* (equipe Paris 6) *) +(* -------------------------------------------------------------------- *) + + +Require Prelude. +Require Logic_Type. + +Section Orderings. + Variable U: Type. + + Definition Relation := U -> U -> Prop. + + Variable R: Relation. + + Definition Reflexive : Prop := (x: U) (R x x). + + Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + + Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + + Definition Antisymmetric : Prop := + (x,y: U) (R x y) -> (R y x) -> x==y. + + Definition contains : Relation -> Relation -> Prop := + [R,R': Relation] (x,y: U) (R' x y) -> (R x y). + Definition same_relation : Relation -> Relation -> Prop := + [R,R': Relation] (contains R R') /\ (contains R' R). +Inductive Equivalence : Prop := + Build_Equivalence: + Reflexive -> Transitive -> Symmetric -> Equivalence. + + Inductive PER : Prop := + Build_PER: Symmetric -> Transitive -> PER. + +End Orderings. + +(***** Setoid *******) + +Inductive Setoid : Type + := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid. + +Definition elem := [A:Setoid] let (S,R,e)=A in S. + +Grammar constr constr1 := + elem [ "|" constr0($s) "|"] -> [ (elem $s) ]. + +Definition equal := [A:Setoid] + <[s:Setoid](Relation |s|)>let (S,R,e)=A in R. + +Grammar constr constr1 := + equal [ constr0($c) "=" "%" "S" constr0($c2) ] -> + [ (equal ? $c $c2) ]. + + +Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)). +Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)). +Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)). +Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)). + +Section Maps. +Variables A,B: Setoid. + +Definition Map_law := [f:|A| -> |B|] + (x,y:|A|) x =%S y -> (f x) =%S (f y). + +Inductive Map : Type := + Build_Map : (f:|A| -> |B|)(p:(Map_law f))Map. + +Definition explicit_ap := [m:Map] <|A| -> |B|>Match m with + [f:?][p:?]f end. + +Axiom pres : (m:Map)(Map_law (explicit_ap m)). + +Definition ext := [f,g:Map] + (x:|A|) (explicit_ap f x) =%S (explicit_ap g x). + +Axiom Equiv_map_eq : (Equivalence Map ext). + +Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq). + +End Maps. + +Notation ap := (explicit_ap ? ?). + +Grammar constr constr8 := + map_setoid [ constr7($c1) "=>" constr8($c2) ] + -> [ (Map_setoid $c1 $c2) ]. + + +Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)). + + +(***** posint ******) + +Inductive posint : Type + := Z : posint | Suc : posint -> posint. + +Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y). +Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m). + +(* The predecessor function *) + +Definition pred : posint->posint + := [n:posint](<posint>Case n of (* Z *) Z + (* Suc u *) [u:posint]u end). + +Axiom pred_Sucn : (m:posint) m==(pred (Suc m)). +Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m. +Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)). + + +Definition IsSuc : posint->Prop + := [n:posint](<Prop>Case n of (* Z *) False + (* Suc p *) [p:posint]True end). +Definition IsZero :posint->Prop := + [n:posint]<Prop>Match n with + True + [p:posint][H:Prop]False end. + +Axiom Z_Suc : (n:posint) ~(Z==(Suc n)). +Axiom Suc_Z: (n:posint) ~(Suc n)==Z. +Axiom n_Sucn : (n:posint) ~(n==(Suc n)). +Axiom Sucn_n : (n:posint) ~(Suc n)==n. +Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a). + + +(******* Dsetoid *****) + +Definition Decidable :=[A:Type][R:(Relation A)] + (x,y:A)(R x y) \/ ~(R x y). + + +Record DSetoid : Type := +{Set_of : Setoid; + prf_decid : (Decidable |Set_of| (equal Set_of))}. + +(* example de Dsetoide d'entiers *) + + +Axiom eqT_equiv : (Equivalence posint (eqT posint)). +Axiom Eq_posint_deci : (Decidable posint (eqT posint)). + +(* Dsetoide des posint*) + +Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv). + +Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci). + + + +(**************************************) + + +(* Definition des signatures *) +(* une signature est un ensemble d'operateurs muni + de l'arite de chaque operateur *) + + +Section Sig. + +Record Signature :Type := +{Sigma : DSetoid; + Arity : (Map (Set_of Sigma) (Set_of Dposint))}. + +Variable S:Signature. + + + +Variable Var : DSetoid. + +Mutual Inductive TERM : Type := + var : |(Set_of Var)| -> TERM + | oper : (op: |(Set_of (Sigma S))| ) (LTERM (ap (Arity S) op)) -> TERM +with + LTERM : posint -> Type := + nil : (LTERM Z) + | cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)). + + + +(* -------------------------------------------------------------------- *) +(* Examples *) +(* -------------------------------------------------------------------- *) + + +Parameter t1,t2: TERM. + +Type + Cases t1 t2 of + | (var v1) (var v2) => True + | (oper op1 l1) (oper op2 l2) => False + | _ _ => False + end. + + + +Parameter n2:posint. +Parameter l1, l2:(LTERM n2). + +Type + Cases l1 l2 of + nil nil => True + | (cons v m y) nil => False + | _ _ => False +end. + + +Type Cases l1 l2 of + nil nil => True + | (cons u n x) (cons v m y) =>False + | _ _ => False +end. + + + +Definition equalT [t1:TERM]:TERM->Prop := +[t2:TERM] + Cases t1 t2 of + (var v1) (var v2) => True + | (oper op1 l1) (oper op2 l2) => False + | _ _ => False + end. + +Definition EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] + Cases l1 l2 of + nil nil => True + | (cons t1 n1' l1') (cons t2 n2' l2') => False + | _ _ => False +end. + + +Reset equalT. +(* ------------------------------------------------------------------*) +(* Initial exemple (without patterns) *) +(*-------------------------------------------------------------------*) + +Fixpoint equalT [t1:TERM]:TERM->Prop := +<TERM->Prop>Case t1 of + (*var*) [v1:|(Set_of Var)|][t2:TERM] + <Prop>Case t2 of + (*var*)[v2:|(Set_of Var)|] (v1 =%S v2) + (*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False + end + (*oper*)[op1:|(Set_of (Sigma S))|] + [l1:(LTERM (ap (Arity S) op1))][t2:TERM] + <Prop>Case t2 of + (*var*)[v2:|(Set_of Var)|]False + (*oper*)[op2:|(Set_of (Sigma S))|] + [l2:(LTERM (ap (Arity S) op2))] + ((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of + (*nil*) [n2:posint][l2:(LTERM n2)] + <[_:posint]Prop>Case l2 of + (*nil*)True + (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False + end + (*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')] + [n2:posint][l2:(LTERM n2)] + <[_:posint]Prop>Case l2 of + (*nil*) False + (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')] + ((equalT t1 t2) /\ (EqListT n1' l1' n2' l2')) + end +end. + + +(* ---------------------------------------------------------------- *) +(* Version with simple patterns *) +(* ---------------------------------------------------------------- *) +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +Cases t1 of + (var v1) => [t2:TERM] + Cases t2 of + (var v2) => (v1 =%S v2) + | (oper op2 _) =>False + end +| (oper op1 l1) => [t2:TERM] + Cases t2 of + (var _) => False + | (oper op2 l2) => (op1=%S op2) + /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of + nil => [n2:posint][l2:(LTERM n2)] + Cases l2 of + nil => True + | _ => False + end +| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)] + Cases l2 of + nil =>False + | (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + end +end. + + +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +Cases t1 of + (var v1) => [t2:TERM] + Cases t2 of + (var v2) => (v1 =%S v2) + | (oper op2 _) =>False + end +| (oper op1 l1) => [t2:TERM] + Cases t2 of + (var _) => False + | (oper op2 l2) => (op1=%S op2) + /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] +Cases l1 of + nil => + Cases l2 of + nil => True + | _ => False + end +| (cons t1 n1' l1') => Cases l2 of + nil =>False + | (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + end +end. + +(* ---------------------------------------------------------------- *) +(* Version with multiple patterns *) +(* ---------------------------------------------------------------- *) +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +[t2:TERM] + Cases t1 t2 of + (var v1) (var v2) => (v1 =%S v2) + + | (oper op1 l1) (oper op2 l2) => + (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + + | _ _ => False + end + +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] + Cases l1 l2 of + nil nil => True + | (cons t1 n1' l1') (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + | _ _ => False +end. + + +(* ------------------------------------------------------------------ *) + +End Sig. + +(* Exemple soumis par Bruno *) + +Definition bProp [b:bool] : Prop := + if b then True else False. + +Definition f0 [F:False;ty:bool]: (bProp ty) := + <[_:bool][ty:bool](bProp ty)>Cases ty ty of + true true => I + | _ false => F + | _ true => I + end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v new file mode 100644 index 00000000..5d183528 --- /dev/null +++ b/test-suite/success/Check.v @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Compiling the theories allows to test parsing and typing but not printing *) +(* This file tests that pretty-printing does not fail *) +(* Test of exact output is not specified *) + +Check O. +Check S. +Check nat. diff --git a/test-suite/success/Conjecture.v b/test-suite/success/Conjecture.v new file mode 100644 index 00000000..6db5859b --- /dev/null +++ b/test-suite/success/Conjecture.v @@ -0,0 +1,13 @@ +(* Check keywords Conjecture and Admitted are recognized *) + +Conjecture c : (n:nat)n=O. + +Check c. + +Theorem d : (n:nat)n=O. +Proof. + NewInduction n. + Reflexivity. + Assert H:False. + 2:NewDestruct H. +Admitted. diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v new file mode 100644 index 00000000..73907bc4 --- /dev/null +++ b/test-suite/success/DHyp.v @@ -0,0 +1,14 @@ +V7only [ +HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ]. + +Lemma lem1 : ~(le (S O) O). +Intro H. +DHyp H. +Qed. + +HintDestruct Conclusion h2 (le O ?) 3 [Constructor]. + +Lemma lem2 : (le O O). +DConcl. +Qed. +]. diff --git a/test-suite/success/Decompose.v b/test-suite/success/Decompose.v new file mode 100644 index 00000000..21a3ab5d --- /dev/null +++ b/test-suite/success/Decompose.v @@ -0,0 +1,7 @@ +(* This was a Decompose bug reported by Randy Pollack (29 Mar 2000) *) + +Goal (O=O/\((x:nat)(x=x)->(x=x)/\((y:nat)y=y->y=y)))-> True. +Intro H. +Decompose [and] H. (* Was failing *) + +Abort. diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v new file mode 100644 index 00000000..fdd929bb --- /dev/null +++ b/test-suite/success/Destruct.v @@ -0,0 +1,13 @@ +(* Submitted by Robert Schneck *) + +Parameter A,B,C,D : Prop. +Axiom X : A->B->C/\D. + +Lemma foo : A->B->C. +Proof. +Intros. +NewDestruct X. (* Should find axiom X and should handle arguments of X *) +Assumption. +Assumption. +Assumption. +Qed. diff --git a/test-suite/success/DiscrR.v b/test-suite/success/DiscrR.v new file mode 100644 index 00000000..5d12098f --- /dev/null +++ b/test-suite/success/DiscrR.v @@ -0,0 +1,41 @@ +Require Reals. +Require DiscrR. + +Lemma ex0: ``1<>0``. +Proof. + DiscrR. +Save. + +Lemma ex1: ``0<>2``. +Proof. + DiscrR. +Save. +Lemma ex2: ``4<>3``. +Proof. + DiscrR. +Save. + +Lemma ex3: ``3<>5``. +Proof. + DiscrR. +Save. + +Lemma ex4: ``-1<>0``. +Proof. + DiscrR. +Save. + +Lemma ex5: ``-2<>-3``. +Proof. + DiscrR. +Save. + +Lemma ex6: ``8<>-3``. +Proof. + DiscrR. +Save. + +Lemma ex7: ``-8<>3``. +Proof. + DiscrR. +Save. diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v new file mode 100644 index 00000000..39d2f4bb --- /dev/null +++ b/test-suite/success/Discriminate.v @@ -0,0 +1,11 @@ +(* Check the behaviour of Discriminate *) + +(* Check that Discriminate tries Intro until *) + +Lemma l1 : O=(S O)->False. +Discriminate 1. +Qed. + +Lemma l2 : (H:O=(S O))H==H. +Discriminate H. +Qed. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v new file mode 100644 index 00000000..c203b739 --- /dev/null +++ b/test-suite/success/Field.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: Field.v,v 1.1.16.1 2004/07/16 19:30:58 herbelin Exp $ *) + +(**** Tests of Field with real numbers ****) + +Require Reals. + +(* Example 1 *) +Goal (eps:R)``eps*1/(2+2)+eps*1/(2+2) == eps*1/2``. +Proof. + Intros. + Field. +Abort. + +(* Example 2 *) +Goal (f,g:(R->R); x0,x1:R) + ``((f x1)-(f x0))*1/(x1-x0)+((g x1)-(g x0))*1/(x1-x0) == ((f x1)+ + (g x1)-((f x0)+(g x0)))*1/(x1-x0)``. +Proof. + Intros. + Field. +Abort. + +(* Example 3 *) +Goal (a,b:R)``1/(a*b)*1/1/b == 1/a``. +Proof. + Intros. + Field. +Abort. + +(* Example 4 *) +Goal (a,b:R)``a <> 0``->``b <> 0``->``1/(a*b)/1/b == 1/a``. +Proof. + Intros. + Field. +Abort. + +(* Example 5 *) +Goal (a:R)``1 == 1*1/a*a``. +Proof. + Intros. + Field. +Abort. + +(* Example 6 *) +Goal (a,b:R)``b == b*/a*a``. +Proof. + Intros. + Field. +Abort. + +(* Example 7 *) +Goal (a,b:R)``b == b*1/a*a``. +Proof. + Intros. + Field. +Abort. + +(* Example 8 *) +Goal (x,y:R)``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``. +Proof. + Intros. + Field. +Abort. diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v new file mode 100644 index 00000000..f1f7ae08 --- /dev/null +++ b/test-suite/success/Fourier.v @@ -0,0 +1,16 @@ +Require Rfunctions. +Require Fourier. + +Lemma l1: + (x, y, z : R) + ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``. +Intros; SplitAbsolu; Fourier. +Qed. + +Lemma l2: + (x, y : R) + ``x < (Rabsolu y)`` -> + ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` -> ``(Rabsolu x) <= 1``. +Intros. +SplitAbsolu; Fourier. +Qed. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v new file mode 100644 index 00000000..819da259 --- /dev/null +++ b/test-suite/success/Funind.v @@ -0,0 +1,440 @@ + +Definition iszero [n:nat] : bool := Cases n of + | O => true + | _ => false + end. + +Functional Scheme iszer_ind := Induction for iszero. + +Lemma toto : (n:nat) n = 0 -> (iszero n) = true. +Intros x eg. +Functional Induction iszero x; Simpl. +Trivial. +Subst x. +Inversion H_eq_. +Qed. + +(* We can even reuse the proof as a scheme: *) + +Functional Scheme toto_ind := Induction for iszero. + + + + + +Definition ftest [n, m:nat] : nat := + Cases n of + | O => Cases m of + | O => 0 + | _ => 1 + end + | (S p) => 0 + end. + +Functional Scheme ftest_ind := Induction for ftest. + +Lemma test1 : (n,m:nat) (le (ftest n m) 2). +Intros n m. +Functional Induction ftest n m;Auto. +Save. + + +Lemma test11 : (m:nat) (le (ftest 0 m) 2). +Intros m. +Functional Induction ftest 0 m. +Auto. +Auto. +Qed. + + +Definition lamfix := +[m:nat ] +(Fix trivfun {trivfun [n:nat] : nat := Cases n of + | O => m + | (S p) => (trivfun p) + end}). + +(* Parameter v1 v2 : nat. *) + +Lemma lamfix_lem : (v1,v2:nat) (lamfix v1 v2) = v1. +Intros v1 v2. +Functional Induction lamfix v1 v2. +Trivial. +Assumption. +Defined. + + + +(* polymorphic function *) +Require PolyList. + +Functional Scheme app_ind := Induction for app. + +Lemma appnil : (A:Set)(l,l':(list A)) l'=(nil A) -> l = (app l l'). +Intros A l l'. +Functional Induction app A l l';Intuition. +Rewrite <- H1;Trivial. +Save. + + + + + +Require Export Arith. + + +Fixpoint trivfun [n:nat] : nat := + Cases n of + | O => 0 + | (S m) => (trivfun m) + end. + + +(* essaie de parametre variables non locaux:*) + +Parameter varessai : nat. + +Lemma first_try : (trivfun varessai) = 0. +Functional Induction trivfun varessai. +Trivial. +Simpl. +Assumption. +Defined. + + +Functional Scheme triv_ind := Induction for trivfun. + +Lemma bisrepetita : (n':nat) (trivfun n') = 0. +Intros n'. +Functional Induction trivfun n'. +Trivial. +Simpl . +Assumption. +Qed. + + + + + + + +Fixpoint iseven [n:nat] : bool := + Cases n of + | O => true + | (S (S m)) => (iseven m) + | _ => false + end. + +Fixpoint funex [n:nat] : nat := + Cases (iseven n) of + | true => n + | false => Cases n of + | O => 0 + | (S r) => (funex r) + end + end. + +Fixpoint nat_equal_bool [n:nat] : nat -> bool := +[m:nat] + Cases n of + | O => Cases m of + | O => true + | _ => false + end + | (S p) => Cases m of + | O => false + | (S q) => (nat_equal_bool p q) + end + end. + + +Require Export Div2. + +Lemma div2_inf : (n:nat) (le (div2 n) n). +Intros n. +Functional Induction div2 n. +Auto. +Auto. + +Apply le_S. +Apply le_n_S. +Exact H. +Qed. + +(* reuse this lemma as a scheme:*) + +Functional Scheme div2_ind := Induction for div2_inf. + +Fixpoint nested_lam [n:nat] : nat -> nat := + Cases n of + | O => [m:nat ] 0 + | (S n') => [m:nat ] (plus m (nested_lam n' m)) + end. + +Functional Scheme nested_lam_ind := Induction for nested_lam. + +Lemma nest : (n, m:nat) (nested_lam n m) = (mult n m). +Intros n m. +Functional Induction nested_lam n m; Auto. +Qed. + +Lemma nest2 : (n, m:nat) (nested_lam n m) = (mult n m). +Intros n m. Pattern n m . +Apply nested_lam_ind; Simpl ; Intros; Auto. +Qed. + + +Fixpoint essai [x : nat] : nat * nat -> nat := + [p : nat * nat] ( Case p of [n, m : ?] Cases n of + O => O + | (S q) => + Cases x of + O => (S O) + | (S r) => (S (essai r (q, m))) + end + end end ). + +Lemma essai_essai: + (x : nat) + (p : nat * nat) ( Case p of [n, m : ?] (lt O n) -> (lt O (essai x p)) end ). +Intros x p. +(Functional Induction essai x p); Intros. +Inversion H. +Simpl; Try Abstract ( Auto with arith ). +Simpl; Try Abstract ( Auto with arith ). +Qed. + + +Fixpoint plus_x_not_five'' [n : nat] : nat -> nat := + [m : nat] let x = (nat_equal_bool m (S (S (S (S (S O)))))) in + let y = O in + Cases n of + O => y + | (S q) => + let recapp = (plus_x_not_five'' q m) in + Cases x of true => (S recapp) | false => (S recapp) end + end. + +Lemma notplusfive'': + (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five'' x y) = x. +Intros a b. +Unfold plus_x_not_five''. +(Functional Induction plus_x_not_five'' a b); Intros hyp; Simpl; Auto. +Qed. + +Lemma iseq_eq: (n, m : nat) n = m -> (nat_equal_bool n m) = true. +Intros n m. +Unfold nat_equal_bool. +(Functional Induction nat_equal_bool n m); Simpl; Intros hyp; Auto. +Inversion hyp. +Inversion hyp. +Qed. + +Lemma iseq_eq': (n, m : nat) (nat_equal_bool n m) = true -> n = m. +Intros n m. +Unfold nat_equal_bool. +(Functional Induction nat_equal_bool n m); Simpl; Intros eg; Auto. +Inversion eg. +Inversion eg. +Qed. + + +Inductive istrue : bool -> Prop := + istrue0: (istrue true) . + +Lemma inf_x_plusxy': (x, y : nat) (le x (plus x y)). +Intros n m. +(Functional Induction plus n m); Intros. +Auto with arith. +Auto with arith. +Qed. + + +Lemma inf_x_plusxy'': (x : nat) (le x (plus x O)). +Intros n. +Unfold plus. +(Functional Induction plus n O); Intros. +Auto with arith. +Apply le_n_S. +Assumption. +Qed. + +Lemma inf_x_plusxy''': (x : nat) (le x (plus O x)). +Intros n. +(Functional Induction plus O n); Intros;Auto with arith. +Qed. + +Fixpoint mod2 [n : nat] : nat := + Cases n of O => O + | (S (S m)) => (S (mod2 m)) + | _ => O end. + +Lemma princ_mod2: (n : nat) (le (mod2 n) n). +Intros n. +(Functional Induction mod2 n); Simpl; Auto with arith. +Qed. + +Definition isfour : nat -> bool := + [n : nat] Cases n of (S (S (S (S O)))) => true | _ => false end. + +Definition isononeorfour : nat -> bool := + [n : nat] Cases n of (S O) => true + | (S (S (S (S O)))) => true + | _ => false end. + +Lemma toto'': (n : nat) (istrue (isfour n)) -> (istrue (isononeorfour n)). +Intros n. +(Functional Induction isononeorfour n); Intros istr; Simpl; Inversion istr. +Apply istrue0. +Qed. + +Lemma toto': (n, m : nat) n = (S (S (S (S O)))) -> (istrue (isononeorfour n)). +Intros n. +(Functional Induction isononeorfour n); Intros m istr; Inversion istr. +Apply istrue0. +Qed. + +Definition ftest4 : nat -> nat -> nat := + [n, m : nat] Cases n of + O => + Cases m of O => O | (S q) => (S O) end + | (S p) => + Cases m of O => O | (S r) => (S O) end + end. + +Lemma test4: (n, m : nat) (le (ftest n m) (S (S O))). +Intros n m. +(Functional Induction ftest n m); Auto with arith. +Qed. + +Lemma test4': (n, m : nat) (le (ftest4 (S n) m) (S (S O))). +Intros n m. +(Functional Induction ftest4 (S n) m). +Auto with arith. +Auto with arith. +Qed. + +Definition ftest44 : nat * nat -> nat -> nat -> nat := + [x : nat * nat] + [n, m : nat] + ( Case x of [p, q : ?] Cases n of + O => + Cases m of O => O | (S q) => (S O) end + | (S p) => + Cases m of O => O | (S r) => (S O) end + end end ). + +Lemma test44: + (pq : nat * nat) (n, m, o, r, s : nat) (le (ftest44 pq n (S m)) (S (S O))). +Intros pq n m o r s. +(Functional Induction ftest44 pq n (S m)). +Auto with arith. +Auto with arith. +Auto with arith. +Auto with arith. +Qed. + +Fixpoint ftest2 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => + Cases m of O => O | (S q) => O end + | (S p) => (ftest2 p m) + end. + +Lemma test2: (n, m : nat) (le (ftest2 n m) (S (S O))). +Intros n m. +(Functional Induction ftest2 n m) ; Simpl; Intros; Auto. +Qed. + +Fixpoint ftest3 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => O + | (S p) => + Cases m of O => (ftest3 p O) | (S r) => O end + end. + +Lemma test3: (n, m : nat) (le (ftest3 n m) (S (S O))). +Intros n m. +(Functional Induction ftest3 n m). +Intros. +Auto. +Intros. +Auto. +Intros. +Simpl. +Auto. +Qed. + +Fixpoint ftest5 [n : nat] : nat -> nat := + [m : nat] Cases n of + O => O + | (S p) => + Cases m of O => (ftest5 p O) | (S r) => (ftest5 p r) end + end. + +Lemma test5: (n, m : nat) (le (ftest5 n m) (S (S O))). +Intros n m. +(Functional Induction ftest5 n m). +Intros. +Auto. +Intros. +Auto. +Intros. +Simpl. +Auto. +Qed. + +Definition ftest7 : (n : nat) nat := + [n : nat] Cases (ftest5 n O) of O => O | (S r) => O end. + +Lemma essai7: + (Hrec : (n : nat) (ftest5 n O) = O -> (le (ftest7 n) (S (S O)))) + (Hrec0 : (n, r : nat) (ftest5 n O) = (S r) -> (le (ftest7 n) (S (S O)))) + (n : nat) (le (ftest7 n) (S (S O))). +Intros hyp1 hyp2 n. +Unfold ftest7. +(Functional Induction ftest7 n); Auto. +Qed. + +Fixpoint ftest6 [n : nat] : nat -> nat := + [m : nat] + Cases n of + O => O + | (S p) => + Cases (ftest5 p O) of O => (ftest6 p O) | (S r) => (ftest6 p r) end + end. + + +Lemma princ6: + ((n, m : nat) n = O -> (le (ftest6 O m) (S (S O)))) -> + ((n, m, p : nat) + (le (ftest6 p O) (S (S O))) -> + (ftest5 p O) = O -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> + ((n, m, p, r : nat) + (le (ftest6 p r) (S (S O))) -> + (ftest5 p O) = (S r) -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> + (x, y : nat) (le (ftest6 x y) (S (S O))). +Intros hyp1 hyp2 hyp3 n m. +Generalize hyp1 hyp2 hyp3. +Clear hyp1 hyp2 hyp3. +(Functional Induction ftest6 n m);Auto. +Qed. + +Lemma essai6: (n, m : nat) (le (ftest6 n m) (S (S O))). +Intros n m. +Unfold ftest6. +(Functional Induction ftest6 n m); Simpl; Auto. +Qed. + + + + + + + + + + + + + diff --git a/test-suite/success/Generalize.v b/test-suite/success/Generalize.v new file mode 100644 index 00000000..0dc73991 --- /dev/null +++ b/test-suite/success/Generalize.v @@ -0,0 +1,7 @@ +(* Check Generalize Dependent *) + +Lemma l1 : [a:=O;b:=a](c:b=b;d:(True->b=b))d=d. +Intros. +Generalize Dependent a. +Intros a b c d. +Abort. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v new file mode 100644 index 00000000..f32753e0 --- /dev/null +++ b/test-suite/success/Hints.v @@ -0,0 +1,48 @@ +(* Checks syntax of Hints commands *) +(* Checks that qualified names are accepted *) + +(* New-style syntax *) +Hint h1 : core arith := Resolve Logic.refl_equal. +Hint h2 := Immediate Logic.trans_equal. +Hint h3 : core := Unfold Logic.sym_equal. +Hint h4 : foo bar := Constructors Logic.eq. +Hint h5 : foo bar := Extern 3 (eq ? ? ?) Apply Logic.refl_equal. + +(* Old-style syntax *) +Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal. +Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo. +Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal. +Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo. +Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal. +Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo. + +(* What's this stranged syntax ? *) +HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ]. +HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ]. +HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ]. + +(* Checks that local names are accepted *) +Section A. + Remark Refl : (A:Set)(x:A)x=x. + Proof refl_equal. + Definition Sym := sym_equal. + Local Trans := trans_equal. + + Hint h1 : foo := Resolve Refl. + Hint h2 : bar := Resolve Sym. + Hint h3 : foo2 := Resolve Trans. + + Hint h2 := Immediate Refl. + Hint h2 := Immediate Sym. + Hint h2 := Immediate Trans. + + Hint h3 := Unfold Refl. + Hint h3 := Unfold Sym. + Hint h3 := Unfold Trans. + + Hints Resolve Sym Trans Refl. + Hints Immediate Sym Trans Refl. + Hints Unfold Sym Trans Refl. + +End A. + diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v new file mode 100644 index 00000000..87431a75 --- /dev/null +++ b/test-suite/success/Inductive.v @@ -0,0 +1,34 @@ +(* Check local definitions in context of inductive types *) +Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set := + I : (z:E)(A C D x y z). + +Check + [C,D:Prop; E:=C; F:=D; x,y:(E ->F); + P:((c:C)(A C D x y c) ->Type); + f:((z:C)(P z (I C D x y z))); + y0:C; a:(A C D x y y0)] + <[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end. + +Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }. + +Check + [C,D:Set; E:=C; F:=D; x,y:(E ->F); + P:((B C D x y) ->Type); + f:((p0,q0:C)(P (Build_B C D x y p0 q0))); + b:(B C D x y)] + <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end. + +(* Check implicit parameters of inductive types (submitted by Pierre + Casteran and also implicit in #338) *) + +Set Implicit Arguments. + +CoInductive LList [A:Set] : Set := + | LNil : (LList A) + | LCons : A -> (LList A) -> (LList A). + +Implicits LNil [1]. + +Inductive Finite [A:Set] : (LList A) -> Prop := + | Finite_LNil : (Finite LNil) + | Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)). diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v new file mode 100644 index 00000000..fd80cec6 --- /dev/null +++ b/test-suite/success/Injection.v @@ -0,0 +1,34 @@ +(* Check the behaviour of Injection *) + +(* Check that Injection tries Intro until *) + +Lemma l1 : (x:nat)(S x)=(S (S x))->False. +Injection 1. +Apply n_Sn. +Qed. + +Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False. +Injection H. +Intros. +Apply (n_Sn x H0). +Qed. + +(* Check that no tuple needs to be built *) +Lemma l3 : (x,y:nat) + (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))= + (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y))) + -> x=y. +Intros x y H. +Injection H. +Exact [H]H. +Qed. + +(* Check that a tuple is built (actually the same as the initial one) *) +Lemma l4 : (p1,p2:{O=O}+{O=O}) + (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2) + ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2). +Intros. +Injection H. +Exact [H]H. +Qed. + diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v new file mode 100644 index 00000000..a9e4a843 --- /dev/null +++ b/test-suite/success/Inversion.v @@ -0,0 +1,85 @@ +Axiom magic:False. + +(* Submitted by Dachuan Yu (bug #220) *) +Fixpoint T[n:nat] : Type := + Cases n of + | O => (nat -> Prop) + | (S n') => (T n') + end. +Inductive R : (n:nat)(T n) -> nat -> Prop := + | RO : (Psi:(T O); l:nat) + (Psi l) -> (R O Psi l) + | RS : (n:nat; Psi:(T (S n)); l:nat) + (R n Psi l) -> (R (S n) Psi l). +Definition Psi00 : (nat -> Prop) := [n:nat] False. +Definition Psi0 : (T O) := Psi00. +Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). +Inversion 1. +Abort. + +(* Submitted by Pierre Casteran (bug #540) *) + +Set Implicit Arguments. +Parameter rule: Set -> Type. + +Inductive extension [I:Set]:Type := + NL : (extension I) +|add_rule : (rule I) -> (extension I) -> (extension I). + + +Inductive in_extension [I :Set;r: (rule I)] : (extension I) -> Type := + in_first : (e:?)(in_extension r (add_rule r e)) +|in_rest : (e,r':?)(in_extension r e) -> (in_extension r (add_rule r' e)). + +Implicits NL [1]. + +Inductive super_extension [I:Set;e :(extension I)] : (extension I) -> Type := + super_NL : (super_extension e NL) +| super_add : (r:?)(e': (extension I)) + (in_extension r e) -> + (super_extension e e') -> + (super_extension e (add_rule r e')). + + + +Lemma super_def : (I :Set)(e1, e2: (extension I)) + (super_extension e2 e1) -> + (ru:?) + (in_extension ru e1) -> + (in_extension ru e2). +Proof. + Induction 1. + Inversion 1; Auto. + Elim magic. +Qed. + +(* Example from Norbert Schirmer on Coq-Club, Sep 2000 *) + +Unset Implicit Arguments. +Definition Q[n,m:nat;prf:(le n m)]:=True. +Goal (n,m:nat;H:(le (S n) m))(Q (S n) m H)==True. +Intros. +Dependent Inversion_clear H. +Elim magic. +Elim magic. +Qed. + +(* Submitted by Boris Yakobowski (bug #529) *) +(* Check that Inversion does not fail due to unnormalized evars *) + +Set Implicit Arguments. +Require Import Bvector. + +Inductive I : nat -> Set := +| C1 : (I (S O)) +| C2 : (k,i:nat)(vector (I i) k) -> (I i). + +Inductive SI : (k:nat)(I k) -> (vector nat k) -> nat -> Prop := +| SC2 : (k,i,vf:nat) (v:(vector (I i) k))(xi:(vector nat i))(SI (C2 v) xi vf). + +Theorem SUnique : (k:nat)(f:(I k))(c:(vector nat k)) +(v,v':?) (SI f c v) -> (SI f c v') -> v=v'. +Proof. +NewInduction 1. +Intros H ; Inversion H. +Admitted. diff --git a/test-suite/success/LetIn.v b/test-suite/success/LetIn.v new file mode 100644 index 00000000..0e0b4435 --- /dev/null +++ b/test-suite/success/LetIn.v @@ -0,0 +1,11 @@ +(* Simple let-in's *) +Definition l1 := [P := O]P. +Definition l2 := [P := nat]P. +Definition l3 := [P := True]P. +Definition l4 := [P := Prop]P. +Definition l5 := [P := Type]P. + +(* Check casting of let-in *) +Definition l6 := [P := O : nat]P. +Definition l7 := [P := True : Prop]P. +Definition l8 := [P := True : Type]P. diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v new file mode 100644 index 00000000..d89ee3be --- /dev/null +++ b/test-suite/success/MatchFail.v @@ -0,0 +1,28 @@ +Require Export ZArith. +Require Export ZArithRing. + +(* Cette tactique a pour objectif de remplacer toute instance + de (POS (xI e)) ou de (POS (xO e)) par + 2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus + à même d'être utilisées par Ring, lorsque ces expressions contiennent + des variables de type positive. *) +Tactic Definition compute_POS := + (Match Context With + | [|- [(POS (xI ?1))]] -> Let v = ?1 In + (Match v With + | [xH] -> + (Fail 1) + |_-> + Rewrite (POS_xI v)) + | [ |- [(POS (xO ?1))]] -> Let v = ?1 In + Match v With + |[xH]-> + (Fail 1) + |[?]-> + Rewrite (POS_xO v)). + +Goal (x:positive)(POS (xI (xI x)))=`4*(POS x)+3`. +Intros. +Repeat compute_POS. +Ring. +Qed. diff --git a/test-suite/success/Mod_ltac.v b/test-suite/success/Mod_ltac.v new file mode 100644 index 00000000..1a9f6fc5 --- /dev/null +++ b/test-suite/success/Mod_ltac.v @@ -0,0 +1,20 @@ +(* Submitted by Houda Anoun *) + +Module toto. +Tactic Definition titi:=Auto. +End toto. + +Module ti. +Import toto. +Tactic Definition equal:= +Match Context With +[ |- ?1=?1]-> titi +| [ |- ?]-> Idtac. + +End ti. + +Import ti. +Definition simple:(a:nat) a=a. +Intro. +equal. +Qed. diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v new file mode 100644 index 00000000..098de3cf --- /dev/null +++ b/test-suite/success/Mod_params.v @@ -0,0 +1,78 @@ +(* Syntax test - all possible kinds of module parameters *) + +Module Type SIG. +End SIG. + +Module Type FSIG[X:SIG]. +End FSIG. + +Module F[X:SIG]. +End F. + +Module Q. +End Q. + +(* +#trace Nametab.push;; +#trace Nametab.push_short_name;; +#trace Nametab.freeze;; +#trace Nametab.unfreeze;; +#trace Nametab.exists_cci;; +*) + +Module M. +Reset M. +Module M[X:SIG]. +Reset M. +Module M[X,Y:SIG]. +Reset M. +Module M[X:SIG;Y:SIG]. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]. +Reset M. +Module M[X:SIG][Y:SIG]. +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]. +Reset M. +Module M:SIG. +Reset M. +Module M[X:SIG]:SIG. +Reset M. +Module M[X,Y:SIG]:SIG. +Reset M. +Module M[X:SIG;Y:SIG]:SIG. +Reset M. +Module M[X,Y:SIG;Z1,Z:SIG]:SIG. +Reset M. +Module M[X:SIG][Y:SIG]:SIG. +Reset M. +Module M[X,Y:SIG][Z1,Z:SIG]:SIG. +Reset M. +Module M:=(F Q). +Reset M. +Module M[X:FSIG]:=(X Q). +Reset M. +Module M[X,Y:FSIG]:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z). +Reset M. +Module M:SIG:=(F Q). +Reset M. +Module M[X:FSIG]:SIG:=(X Q). +Reset M. +Module M[X,Y:FSIG]:SIG:=(X Q). +Reset M. +Module M[X:FSIG;Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z). +Reset M. +Module M[X:FSIG][Y:SIG]:SIG:=(X Y). +Reset M. +Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z). +Reset M. diff --git a/test-suite/success/Mod_strengthen.v b/test-suite/success/Mod_strengthen.v new file mode 100644 index 00000000..a472e698 --- /dev/null +++ b/test-suite/success/Mod_strengthen.v @@ -0,0 +1,64 @@ +Module Type Sub. + Axiom Refl1 : (x:nat)(x=x). + Axiom Refl2 : (x:nat)(x=x). + Axiom Refl3 : (x:nat)(x=x). + Inductive T : Set := A : T. +End Sub. + +Module Type Main. + Declare Module M:Sub. +End Main. + + +Module A <: Main. + Module M <: Sub. + Lemma Refl1 : (x:nat) x=x. + Intros;Reflexivity. + Qed. + Axiom Refl2 : (x:nat) x=x. + Lemma Refl3 : (x:nat) x=x. + Intros;Reflexivity. + Defined. + Inductive T : Set := A : T. + End M. +End A. + + + +(* first test *) + +Module F[S:Sub]. + Module M:=S. +End F. + +Module B <: Main with Module M:=A.M := F A.M. + + + +(* second test *) + +Lemma r1 : (A.M.Refl1 == B.M.Refl1). +Proof. + Reflexivity. +Qed. + +Lemma r2 : (A.M.Refl2 == B.M.Refl2). +Proof. + Reflexivity. +Qed. + +Lemma r3 : (A.M.Refl3 == B.M.Refl3). +Proof. + Reflexivity. +Qed. + +Lemma t : (A.M.T == B.M.T). +Proof. + Reflexivity. +Qed. + +Lemma a : (A.M.A == B.M.A). +Proof. + Reflexivity. +Qed. + diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v new file mode 100644 index 00000000..6a1eeccc --- /dev/null +++ b/test-suite/success/NatRing.v @@ -0,0 +1,10 @@ +Require ArithRing. + +Lemma l1 : (S (S O))=(plus (S O) (S O)). +NatRing. +Qed. + +Lemma l2 : (x:nat)(S (S x))=(plus (S O) (S x)). +Intro. +NatRing. +Qed.
\ No newline at end of file diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v new file mode 100644 index 00000000..c324919f --- /dev/null +++ b/test-suite/success/Omega.v @@ -0,0 +1,89 @@ + +Require Omega. + +(* Submitted by Xavier Urbain 18 Jan 2002 *) + +Lemma lem1 : (x,y:Z) + `-5 < x < 5` -> + `-5 < y` -> + `-5 < x+y+5`. +Proof. +Intros x y. +Omega. +Qed. + +(* Proposed by Pierre Crégut *) + +Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`. +Intro. +Omega. +Qed. + +(* Proposed by Jean-Christophe Filliâtre *) + +Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`. +Proof. +Intros. +Omega. +Qed. + +(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) +(* internal variable and a section variable (June 2001) *) + +Section A. +Variable x,y : Z. +Hypothesis H : `x > y`. +Lemma lem4 : `x > y`. +Omega. +Qed. +End A. + +(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *) +(* May 2002 *) + +Section B. +Variables R1,R2,S1,S2,H,S:Z. +Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`. +Hypothesis J:`R1 < 0`->`S2 = S1-1`. +Hypothesis K:`R1 >= 0`->`R2 = R1`. +Hypothesis L:`R1 >= 0`->`S2 = S1`. +Hypothesis M:`H <= 2*S`. +Hypothesis N:`S < H`. +Lemma lem5 : `H > 0`. +Omega. +Qed. +End B. + +(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) +Lemma lem6: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`. +Intros. +Omega. +Qed. + +(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) +Require Omega. +Section C. +Parameter g:(m:nat)~m=O->Prop. +Parameter f:(m:nat)(H:~m=O)(g m H). +Variable n:nat. +Variable ap_n:~n=O. +Local delta:=(f n ap_n). +Lemma lem7 : n=n. +Omega. +Qed. +End C. + +(* Problem of dependencies *) +Require Omega. +Lemma lem8 : (H:O=O->O=O) H=H -> O=O. +Intros; Omega. +Qed. + +(* Bug that what caused by the use of intro_using in Omega *) +Require Omega. +Lemma lem9 : (p,q:nat) + ~((le p q)/\(lt p q)\/(le q p)/\(lt p q)) + -> (lt p p)\/(le p p). +Intros; Omega. +Qed. + diff --git a/test-suite/success/PPFix.v8 b/test-suite/success/PPFix.v8 new file mode 100644 index 00000000..1ecbae3a --- /dev/null +++ b/test-suite/success/PPFix.v8 @@ -0,0 +1,8 @@ + +(* To test PP of fixpoints *) +Require Import Arith. +Check fix a(n: nat): n<5 -> nat := + match n return n<5 -> nat with + | 0 => fun _ => 0 + | S n => fun h => S (a n (lt_S_n _ _ (lt_S _ _ h))) + end. diff --git a/test-suite/success/Print.v b/test-suite/success/Print.v new file mode 100644 index 00000000..4554a843 --- /dev/null +++ b/test-suite/success/Print.v @@ -0,0 +1,20 @@ +Print Tables. +Print ML Path. +Print ML Modules. +Print LoadPath. +Print Graph. +Print Coercions. +Print Classes. +Print nat. +Print Proof O. +Print All. +Print Grammar constr constr. +Inspect 10. + +Section A. +Coercion f := [x]True : nat -> Prop. +Print Coercion Paths nat SORTCLASS. + +Print Section A. +Print. + diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v new file mode 100644 index 00000000..7f5cd800 --- /dev/null +++ b/test-suite/success/Projection.v @@ -0,0 +1,45 @@ +Structure S : Type := + {Dom : Type; + Op : Dom -> Dom -> Dom}. + +Check [s:S](Dom s). +Check [s:S](Op s). +Check [s:S;a,b:(Dom s)](Op s a b). + +(* v8 +Check fun s:S => s.(Dom). +Check fun s:S => s.(Op). +Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b. +*) + +Set Implicit Arguments. +Unset Strict Implicits. + +Structure S' [A:Set] : Type := + {Dom' : Type; + Op' : A -> Dom' -> Dom'}. + +Check [s:(S' nat)](Dom' s). +Check [s:(S' nat)](Op' 2!s). +Check [s:(S' nat)](!Op' nat s). +Check [s:(S' nat);a:nat;b:(Dom' s)](Op' a b). +Check [s:(S' nat);a:nat;b:(Dom' s)](!Op' nat s a b). + +(* v8 +Check fun s:S' => s.(Dom'). +Check fun s:S' => s.(Op'). +Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b. +Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b. + +Set Implicit Arguments. +Unset Strict Implicits. + +Structure S' (A:Set) : Type := + {Dom' : Type; + Op' : A -> Dom' -> Dom'}. + +Check fun s:S' nat => s.(Dom'). +Check fun s:S' nat => s.(Op'). +Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => _.(@Op' nat) a b. +Check fun (s:S' nat) (a:nat) (b:s.(Dom')) => s.(Op') a b. +*) diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v new file mode 100644 index 00000000..f3a13634 --- /dev/null +++ b/test-suite/success/Record.v @@ -0,0 +1,3 @@ +(* Nijmegen expects redefinition of sorts *) +Definition CProp := Prop. +Record test : CProp := { n:nat }. diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v new file mode 100644 index 00000000..eaa0690c --- /dev/null +++ b/test-suite/success/Reg.v @@ -0,0 +1,136 @@ +Require Reals. + +Axiom y : R->R. +Axiom d_y : (derivable y). +Axiom n_y : (x:R)``(y x)<>0``. +Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1. + +Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0). +Assert H := d_y. +Assert H0 := n_y. +Reg. +Qed. + +Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``). +Reg. +Qed. + +Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``). +Reg. +Qed. + +Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0). +Reg. +Qed. + +Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``). +Reg. +Qed. + +Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``). +Reg. +Qed. + +Lemma essai6 : (derivable [x:R]``(cos (x+3))``). +Reg. +Qed. + +Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1). +Reg. +Apply Rlt_R0_R1. +Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption. +Qed. + +Lemma essai8 : (derivable_pt [x:R]``(sqrt ((Rsqr x)+(sin x)+1))`` R0). +Reg. +Rewrite sin_0. +Rewrite Rsqr_O. +Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring]. +Qed. + +Lemma essai9 : (derivable_pt (plus_fct id sin) R1). +Reg. +Qed. + +Lemma essai10 : (derivable_pt [x:R]``x+2`` R0). +Reg. +Qed. + +Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1. +Reg. +Qed. + +Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``). +Reg. +Qed. + +Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``. +Reg. +Qed. + +Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``). +Reg. +Qed. + +Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``. +Reg. +Qed. + +Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0). +Reg. +Qed. + +Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``. +Reg. +Rewrite cos_0. +Reflexivity. +Qed. + +Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``). +Assert H := d_y. +Reg. +Qed. + +Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``. +Assert H := dy_0. +Assert H0 := d_y. +Reg. +Qed. + +Axiom z:R->R. +Axiom d_z: (derivable z). + +Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0). +Reg. +Apply d_y. +Apply d_z. +Qed. + +Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1. +Assert H := dy_0. +Reg. +Abort. + +Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``). +Assert H := d_y. +Reg. +Apply n_y. +Apply d_z. +Qed. + +(* Pour tester la continuite de sqrt en 0 *) +Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1). +Reg. +Left; Apply Rlt_R0_R1. +Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity. +Qed. + +Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``). +Reg. +Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``. +Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1]. +Unfold Rsqr; Ring. +Red; Intro; Cut ``0<x*x+1``. +Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0). +Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1]. +Qed. diff --git a/test-suite/success/Remark.v b/test-suite/success/Remark.v new file mode 100644 index 00000000..2dd6a211 --- /dev/null +++ b/test-suite/success/Remark.v @@ -0,0 +1,12 @@ +(* Test obsolete, Remark est maintenant global +Section A. +Section B. +Section C. +Remark t : True. Proof I. +End C. +Locate C.t. +End B. +Locate B.C.t. +End A. +Locate A.B.C.t. +*) diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v new file mode 100644 index 00000000..edb20a81 --- /dev/null +++ b/test-suite/success/Rename.v @@ -0,0 +1,5 @@ +Goal (n:nat)(n=O)->(n=O). +Intros. +Rename n into p. +NewInduction p; Auto. +Qed. diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v new file mode 100644 index 00000000..654808fc --- /dev/null +++ b/test-suite/success/Require.v @@ -0,0 +1,3 @@ +Require Coq.Arith.Plus. +Read Module Coq.Arith.Minus. +Locate Library Coq.Arith.Minus. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v new file mode 100644 index 00000000..55d8343e --- /dev/null +++ b/test-suite/success/Scopes.v @@ -0,0 +1,8 @@ +(* Check exportation of Argument Scopes even without import of modules *) + +Require Import ZArith. + +Module A. +Definition opp := Zopp. +End A. +Check (A.opp 3). diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v new file mode 100644 index 00000000..41aa77ef --- /dev/null +++ b/test-suite/success/Simplify_eq.v @@ -0,0 +1,13 @@ +(* Check the behaviour of Simplify_eq *) + +(* Check that Simplify_eq tries Intro until *) + +Lemma l1 : O=(S O)->False. +Simplify_eq 1. +Qed. + +Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False. +Simplify_eq H. +Intros. +Apply (n_Sn x H0). +Qed. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v new file mode 100644 index 00000000..883a82ab --- /dev/null +++ b/test-suite/success/Tauto.v @@ -0,0 +1,240 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: Tauto.v,v 1.10.8.1 2004/07/16 19:30:59 herbelin Exp $ *) + +(**** Tactics Tauto and Intuition ****) + +(**** Tauto: + Tactic for automating proof in Intuionnistic Propositional Calculus, based on + the contraction-free LJT* of Dickhoff ****) + +(**** Intuition: + Simplifications of goals, based on LJT* calcul ****) + +(**** Examples of intuitionistic tautologies ****) +Parameter A,B,C,D,E,F:Prop. +Parameter even:nat -> Prop. +Parameter P:nat -> Prop. + +Lemma Ex_Wallen:(A->(B/\C)) -> ((A->B)\/(A->C)). +Proof. + Tauto. +Save. + +Lemma Ex_Klenne:~(~(A \/ ~A)). +Proof. + Tauto. +Save. + +Lemma Ex_Klenne':(n:nat)(~(~((even n) \/ ~(even n)))). +Proof. + Tauto. +Save. + +Lemma Ex_Klenne'':~(~(((n:nat)(even n)) \/ ~((m:nat)(even m)))). +Proof. + Tauto. +Save. + +Lemma tauto:((x:nat)(P x)) -> ((y:nat)(P y)). +Proof. + Tauto. +Save. + +Lemma tauto1:(A -> A). +Proof. + Tauto. +Save. + +Lemma tauto2:(A -> B -> C) -> (A -> B) -> A -> C. +Proof. + Tauto. +Save. + +Lemma a:(x0: (A \/ B))(x1:(B /\ C))(A -> B). +Proof. + Tauto. +Save. + +Lemma a2:((A -> (B /\ C)) -> ((A -> B) \/ (A -> C))). +Proof. + Tauto. +Save. + +Lemma a4:(~A -> ~A). +Proof. + Tauto. +Save. + +Lemma e2:~(~(A \/ ~A)). +Proof. + Tauto. +Save. + +Lemma e4:~(~((A \/ B) -> (A \/ B))). +Proof. + Tauto. +Save. + +Lemma y0:(x0:A)(x1: ~A)(x2:(A -> B))(x3:(A \/ B))(x4:(A /\ B))(A -> False). +Proof. + Tauto. +Save. + +Lemma y1:(x0:((A /\ B) /\ C))B. +Proof. + Tauto. +Save. + +Lemma y2:(x0:A)(x1:B)(C \/ B). +Proof. + Tauto. +Save. + +Lemma y3:(x0:(A /\ B))(B /\ A). +Proof. + Tauto. +Save. + +Lemma y5:(x0:(A \/ B))(B \/ A). +Proof. + Tauto. +Save. + +Lemma y6:(x0:(A -> B))(x1:A) B. +Proof. + Tauto. +Save. + +Lemma y7:(x0 : ((A /\ B) -> C))(x1 : B)(x2 : A) C. +Proof. + Tauto. +Save. + +Lemma y8:(x0 : ((A \/ B) -> C))(x1 : A) C. +Proof. + Tauto. +Save. + +Lemma y9:(x0 : ((A \/ B) -> C))(x1 : B) C. +Proof. + Tauto. +Save. + +Lemma y10:(x0 : ((A -> B) -> C))(x1 : B) C. +Proof. + Tauto. +Save. + +(* This example took much time with the old version of Tauto *) +Lemma critical_example0:(~~B->B)->(A->B)->~~A->B. +Proof. + Tauto. +Save. + +(* Same remark as previously *) +Lemma critical_example1:(~~B->B)->(~B->~A)->~~A->B. +Proof. + Tauto. +Save. + +(* This example took very much time (about 3mn on a PIII 450MHz in bytecode) + with the old Tauto. Now, it's immediate (less than 1s). *) +Lemma critical_example2:(~A<->B)->(~B<->A)->(~~A<->A). +Proof. + Tauto. +Save. + +(* This example was a bug *) +Lemma old_bug0:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F. +Proof. + Tauto. +Save. + +(* Another bug *) +Lemma old_bug1:((A->B->False)->False) -> (B->False) -> False. +Proof. + Tauto. +Save. + +(* A bug again *) +Lemma old_bug2: + ((((C->False)->A)->((B->False)->A)->False)->False) -> + (((C->B->False)->False)->False) -> + ~A->A. +Proof. + Tauto. +Save. + +(* A bug from CNF form *) +Lemma old_bug3: + ((~A\/B)/\(~B\/B)/\(~A\/~B)/\(~B\/~B)->False)->~((A->B)->B)->False. +Proof. + Tauto. +Save. + +(* sometimes, the behaviour of Tauto depends on the order of the hyps *) +Lemma old_bug3bis: + ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False. +Proof. + Tauto. +Save. + +(* A bug found by Freek Wiedijk <freek@cs.kun.nl> *) +Lemma new_bug: + ((A<->B)->(B<->C)) -> + ((B<->C)->(C<->A)) -> + ((C<->A)->(A<->B)) -> + (A<->B). +Proof. + Tauto. +Save. + + +(* A private club has the following rules : + * + * . rule 1 : Every non-scottish member wears red socks + * . rule 2 : Every member wears a kilt or doesn't wear red socks + * . rule 3 : The married members don't go out on sunday + * . rule 4 : A member goes out on sunday if and only if he is scottish + * . rule 5 : Every member who wears a kilt is scottish and married + * . rule 6 : Every scottish member wears a kilt + * + * Actually, no one can be accepted ! + *) + +Section club. + +Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop. + +Hypothesis rule1 : ~Scottish -> RedSocks. +Hypothesis rule2 : WearKilt \/ ~RedSocks. +Hypothesis rule3 : Married -> ~GoOutSunday. +Hypothesis rule4 : GoOutSunday <-> Scottish. +Hypothesis rule5 : WearKilt -> (Scottish /\ Married). +Hypothesis rule6 : Scottish -> WearKilt. + +Lemma NoMember : False. +Tauto. +Save. + +End club. + +(**** Use of Intuition ****) +Lemma intu0:(((x:nat)(P x)) /\ B) -> + (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)). +Proof. + Intuition. +Save. + +Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Proof. + Intuition. +Save. + diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v new file mode 100644 index 00000000..05cab1e6 --- /dev/null +++ b/test-suite/success/Try.v @@ -0,0 +1,8 @@ +(* To shorten interactive scripts, it is better that Try catches + non-existent names in Unfold [cf bug #263] *) + +Lemma lem1 : True. +Try (Unfold i_dont_exist). +Trivial. +Qed. + diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v new file mode 100644 index 00000000..4d898da9 --- /dev/null +++ b/test-suite/success/cc.v @@ -0,0 +1,83 @@ + +Theorem t1: (A:Set)(a:A)(f:A->A) + (f a)=a->(f (f a))=a. +Intros. +Congruence. +Save. + +Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A) + a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))-> + (g a b)=a. +Intros. +Congruence. +Save. + +(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *) + +Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N) + (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s o)))))))))))))))=o-> + (s (s (s (s (s (s (s (s (s (s o))))))))))=o-> + (s (s (s (s (s (s o))))))=o-> + o=(s o). +Intros. +Congruence. +Save. + +(* Examples that fail due to dependencies *) + +(* yields transitivity problem *) + +Theorem dep:(A:Set)(P:A->Set)(f,g:(x:A)(P x))(x,y:A) + (e:x=y)(e0:(f y)=(g y))(f x)=(g x). +Intros;Dependent Rewrite -> e;Exact e0. +Save. + +(* yields congruence problem *) + +Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B) + (f A true)=(f B true). +Intros;Rewrite e;Reflexivity. +Save. + + +(* example that Congruence. can solve + (dependent function applied to the same argument)*) + +Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x). Intros. +Congruence. +Save. + +(* Examples with injection rule *) + +Theorem inj1 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d. +Intros. +Split;Congruence. +Save. + +Theorem inj2 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))-> + (Some ? (f c))=(Some ? (f d))->c=d. +Intros. +Congruence. +Save. + +(* Examples with discrimination rule *) + +Theorem discr1 : true=false->False. +Intros. +Congruence. +Save. + +Theorem discr2 : (Some ? true)=(Some ? false)->False. +Intros. +Congruence. +Save. + +(* example with Congruence.Solve (requires CCSolve.v)*) + +Require CCSolve. + +Theorem t4 : (A:Set; P:(A->Prop); a,b,c,d:A)a=b->c=d-> + (P a)->((P b)->(P c))->(P d). +Intros. +CCsolve. +Save. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v new file mode 100644 index 00000000..98b613ba --- /dev/null +++ b/test-suite/success/coercions.v @@ -0,0 +1,11 @@ +(* Interaction between coercions and casts *) +(* Example provided by Eduardo Gimenez *) + +Parameter Z,S:Set. + +Parameter f: S -> Z. +Coercion f: S >-> Z. + +Parameter g : Z -> Z. + +Check [s](g (s::S)). diff --git a/test-suite/success/coqbugs0181.v b/test-suite/success/coqbugs0181.v new file mode 100644 index 00000000..21f906a6 --- /dev/null +++ b/test-suite/success/coqbugs0181.v @@ -0,0 +1,7 @@ + +(* test the strength of pretyping unification *) + +Require PolyList. +Definition listn := [A,n] {l:(list A)|(length l)=n}. +Definition make_ln [A,n;l:(list A); h:([l](length l)=n l)] := + (exist ?? l h). diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v new file mode 100644 index 00000000..97f7ccf0 --- /dev/null +++ b/test-suite/success/eauto.v @@ -0,0 +1,49 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Require PolyList. + +Parameter in_list : (list nat*nat)->nat->Prop. +Definition not_in_list : (list nat*nat)->nat->Prop + := [l,n]~(in_list l n). + +(* Hints Unfold not_in_list. *) + +Axiom lem1 : (l1,l2:(list nat*nat))(n:nat) + (not_in_list (app l1 l2) n)->(not_in_list l1 n). + +Axiom lem2 : (l1,l2:(list nat*nat))(n:nat) + (not_in_list (app l1 l2) n)->(not_in_list l2 n). + +Axiom lem3 : (l:(list nat*nat))(n,p,q:nat) + (not_in_list (cons (p,q) l) n)->(not_in_list l n). + +Axiom lem4 : (l1,l2:(list nat*nat))(n:nat) + (not_in_list l1 n)->(not_in_list l2 n)->(not_in_list (app l1 l2) n). + +Hints Resolve lem1 lem2 lem3 lem4: essai. + +Goal (l:(list nat*nat))(n,p,q:nat) + (not_in_list (cons (p,q) l) n)->(not_in_list l n). +Intros. +EAuto with essai. +Save. + +(* Example from Nicolas Magaud on coq-club - Jul 2000 *) + +Definition Nat: Set := nat. +Parameter S':Nat ->Nat. +Parameter plus':Nat -> Nat ->Nat. + +Lemma simpl_plus_l_rr1: + ((n0:Nat) ((m, p:Nat) (plus' n0 m)=(plus' n0 p) ->m=p) -> + (m, p:Nat) (S' (plus' n0 m))=(S' (plus' n0 p)) ->m=p) -> + (n:Nat) ((m, p:Nat) (plus' n m)=(plus' n p) ->m=p) -> + (m, p:Nat) (S' (plus' n m))=(S' (plus' n p)) ->m=p. +Intros. +EAuto. (* does EApply H *) +Qed. diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v new file mode 100644 index 00000000..f826df9a --- /dev/null +++ b/test-suite/success/eqdecide.v @@ -0,0 +1,29 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Inductive T : Set := A: T | B :T->T. + +Lemma lem1 : (x,y:T){x=y}+{~x=y}. +Decide Equality. +Qed. + +Lemma lem2 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Decide Equality x y. +Qed. + +Lemma lem3 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Decide Equality y x. +Qed. + +Lemma lem4 : (x,y:T){x=y}+{~x=y}. +Intros x y. +Compare x y; Auto. +Qed. + diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v new file mode 100644 index 00000000..a7b6d6d8 --- /dev/null +++ b/test-suite/success/evars.v @@ -0,0 +1,23 @@ +(* The "?" of cons and eq should be inferred *) +Variable list:Set -> Set. +Variable cons:(T:Set) T -> (list T) -> (list T). +Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). + +(* Examples provided by Eduardo Gimenez *) + +Definition c [A;Q:(nat*A->Prop)->Prop;P] := + (Q [p:nat*A]let (i,v) = p in (P i v)). + +(* What does this test ? *) +Require PolyList. +Definition list_forall_bool [A:Set][p:A->bool][l:(list A)] : bool := + (fold_right ([a][r]if (p a) then r else false) true l). + +(* Checks that solvable ? in the lambda prefix of the definition are harmless*) +Parameter A1,A2,F,B,C : Set. +Parameter f : F -> A1 -> B. +Definition f1 [frm0,a1]: B := (f frm0 a1). + +(* Checks that solvable ? in the type part of the definition are harmless *) +Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1). + diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v new file mode 100644 index 00000000..374029bb --- /dev/null +++ b/test-suite/success/fix.v @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Ancien bug signale par Laurent Thery sur la condition de garde *) + +Require Import Bool. +Require Import ZArith. + +Definition rNat := positive. + +Inductive rBoolOp: Set := + rAnd: rBoolOp + | rEq: rBoolOp . + +Definition rlt: rNat -> rNat ->Prop := [a, b:rNat](compare a b EGAL)=INFERIEUR. + +Definition rltDec: (m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}. +Intros n m; Generalize (compare_convert_INFERIEUR n m); + Generalize (compare_convert_SUPERIEUR n m); + Generalize (compare_convert_EGAL n m); Case (compare n m EGAL). +Intros H' H'0 H'1; Right; Right; Auto. +Intros H' H'0 H'1; Left; Unfold rlt. +Apply convert_compare_INFERIEUR; Auto. +Intros H' H'0 H'1; Right; Left; Unfold rlt. +Apply convert_compare_INFERIEUR; Auto. +Apply H'0; Auto. +Defined. + + +Definition rmax: rNat -> rNat ->rNat. +Intros n m; Case (rltDec n m); Intros Rlt0. +Exact m. +Exact n. +Defined. + +Inductive rExpr: Set := + rV: rNat ->rExpr + | rN: rExpr ->rExpr + | rNode: rBoolOp -> rExpr -> rExpr ->rExpr . + +Fixpoint maxVar[e:rExpr]: rNat := + Cases e of + (rV n) => n + | (rN p) => (maxVar p) + | (rNode n p q) => (rmax (maxVar p) (maxVar q)) + end. + diff --git a/test-suite/success/if.v b/test-suite/success/if.v new file mode 100644 index 00000000..85cd1f11 --- /dev/null +++ b/test-suite/success/if.v @@ -0,0 +1,5 @@ +(* The synthesis of the elimination predicate may fail if algebric *) +(* universes are not cautiously treated *) + +Check [b:bool]if b then Type else nat. + diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v new file mode 100644 index 00000000..c597f9bf --- /dev/null +++ b/test-suite/success/implicit.v @@ -0,0 +1,31 @@ +(* Implicit on section variables *) + +Set Implicit Arguments. + +(* Example submitted by David Nowak *) + +Section Spec. +Variable A:Set. +Variable op : (A:Set)A->A->Set. +Infix 6 "#" op V8only (at level 70). +Check (x:A)(x # x). + +(* Example submitted by Christine *) +Record stack : Type := {type : Set; elt : type; + empty : type -> bool; proof : (empty elt)=true }. + +Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack. + +End Spec. + +(* Example submitted by Frédéric (interesting in v8 syntax) *) + +Parameter f : nat -> nat * nat. +Notation lhs := fst. +Check [x](lhs ? ? (f x)). +Check [x](!lhs ? ? (f x)). +Notation "'rhs'" := snd. +Check [x](rhs ? ? (f x)). +(* V8 seulement +Check (fun x => @ rhs ? ? (f x)). +*) diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v new file mode 100644 index 00000000..d031691d --- /dev/null +++ b/test-suite/success/import_lib.v @@ -0,0 +1,202 @@ +Definition le_trans:=O. + + +Module Test_Read. + Module M. + Read Module Le. (* Reading without importing *) + + Check Le.le_trans. + + Lemma th0 : le_trans = O. + Reflexivity. + Qed. + End M. + + Check Le.le_trans. + + Lemma th0 : le_trans = O. + Reflexivity. + Qed. + + Import M. + + Lemma th1 : le_trans = O. + Reflexivity. + Qed. +End Test_Read. + + +(****************************************************************) + +Definition le_decide := (S O). (* from Arith/Compare *) +Definition min := O. (* from Arith/Min *) + +Module Test_Require. + + Module M. + Require Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th4 : min = O. + Reflexivity. + Qed. + +End Test_Require. + +(****************************************************************) + +Module Test_Import. + Module M. + Import Compare. (* Imports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + (* Checks that Compare and List are loaded *) + Check Compare.le_decide. + Check Min.min. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + (* It should still be the case after Import M *) + Import M. + + Lemma th3 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th4 : min = O. + Reflexivity. + Qed. +End Test_Import. + +(************************************************************************) + +Module Test_Export. + Module M. + Export Compare. (* Exports Min as well *) + + Lemma th1 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th2 : min = Min.min. + Reflexivity. + Qed. + + End M. + + + (* Checks that Compare and List are _not_ imported *) + Lemma th1 : le_decide = (S O). + Reflexivity. + Qed. + + Lemma th2 : min = O. + Reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : le_decide = Compare.le_decide. + Reflexivity. + Qed. + + Lemma th4 : min = Min.min. + Reflexivity. + Qed. +End Test_Export. + + +(************************************************************************) + +Module Test_Require_Export. + + Definition mult_sym:=(S O). (* from Arith/Mult *) + Definition plus_sym:=O. (* from Arith/Plus *) + + Module M. + Require Export Mult. (* Exports Plus as well *) + + Lemma th1 : mult_sym = Mult.mult_sym. + Reflexivity. + Qed. + + Lemma th2 : plus_sym = Plus.plus_sym. + Reflexivity. + Qed. + + End M. + + + (* Checks that Mult and Plus are _not_ imported *) + Lemma th1 : mult_sym = (S O). + Reflexivity. + Qed. + + Lemma th2 : plus_sym = O. + Reflexivity. + Qed. + + + (* After Import M they should be imported as well *) + + Import M. + + Lemma th3 : mult_sym = Mult.mult_sym. + Reflexivity. + Qed. + + Lemma th4 : plus_sym = Plus.plus_sym. + Reflexivity. + Qed. + +End Test_Require_Export. diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v new file mode 100644 index 00000000..b4a8af46 --- /dev/null +++ b/test-suite/success/import_mod.v @@ -0,0 +1,75 @@ + +Definition p:=O. +Definition m:=O. + +Module Test_Import. + Module P. + Definition p:=(S O). + End P. + + Module M. + Import P. + Definition m:=p. + End M. + + Module N. + Import M. + + Lemma th0 : p=O. + Reflexivity. + Qed. + + End N. + + + (* M and P should be closed *) + Lemma th1 : m=O /\ p=O. + Split; Reflexivity. + Qed. + + + Import N. + + (* M and P should still be closed *) + Lemma th2 : m=O /\ p=O. + Split; Reflexivity. + Qed. +End Test_Import. + + +(********************************************************************) + + +Module Test_Export. + Module P. + Definition p:=(S O). + End P. + + Module M. + Export P. + Definition m:=p. + End M. + + Module N. + Export M. + + Lemma th0 : p=(S O). + Reflexivity. + Qed. + + End N. + + + (* M and P should be closed *) + Lemma th1 : m=O /\ p=O. + Split; Reflexivity. + Qed. + + + Import N. + + (* M and P should now be opened *) + Lemma th2 : m=(S O) /\ p=(S O). + Split; Reflexivity. + Qed. +End Test_Export. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v new file mode 100644 index 00000000..a391b804 --- /dev/null +++ b/test-suite/success/inds_type_sec.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +Section S. +Inductive T [U:Type] : Type := c : U -> (T U). +End S. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v new file mode 100644 index 00000000..9ae498d2 --- /dev/null +++ b/test-suite/success/induct.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Teste des definitions inductives imbriquees *) + +Require PolyList. + +Inductive X : Set := + cons1 : (list X)->X. + +Inductive Y : Set := + cons2 : (list Y*Y)->Y. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v new file mode 100644 index 00000000..55aa110d --- /dev/null +++ b/test-suite/success/ltac.v @@ -0,0 +1,70 @@ +(* The tactic language *) + +(* Submitted by Pierre Crégut *) +(* Checks substitution of x *) +Tactic Definition f x := Unfold x; Idtac. + +Lemma lem1 : (plus O O) = O. +f plus. +Reflexivity. +Qed. + +(* Submitted by Pierre Crégut *) +(* Check syntactic correctness *) +Recursive Tactic Definition F x := Idtac; (G x) +And G y := Idtac; (F y). + +(* Check that Match Context keeps a closure *) +Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a. + +Lemma lem2 : True. +U. +Qed. + +(* Check that Match giving non-tactic arguments are evaluated at Let-time *) + +Tactic Definition B := + Let y = (Match Context With [ z:? |- ? ] -> z) In + Intro H1; Exact y. + +Lemma lem3 : True -> False -> True -> False. +Intros H H0. +B. (* y is H0 if at let-time, H1 otherwise *) +Qed. + +(* Checks the matching order of hypotheses *) +Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x. +Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x. + +Lemma lem4 : (True->False) -> (False->False) -> False. +Intros H H0. +Z. (* Apply H0 *) +Y. (* Apply H *) +Exact I. +Qed. + +(* Check backtracking *) +Lemma back1 : (0)=(1)->(0)=(0)->(1)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +Lemma back2 : (0)=(0)->(0)=(1)->(1)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +Lemma back3 : (0)=(0)->(1)=(1)->(0)=(1)->(0)=(0). +Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Qed. + +(* Check context binding *) +Tactic Definition sym t := Match t With [C[?1=?2]] -> Inst C[?1=?2]. + +Lemma sym : ~(0)=(1)->~(1)=(0). +Intro H. +Let t = (sym (Check H)) In Assert t. +Exact H. +Intro H1. +Apply H. +Symmetry. +Assumption. +Qed. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v new file mode 100644 index 00000000..e932f50c --- /dev/null +++ b/test-suite/success/mutual_ind.v @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Definition mutuellement inductive et dependante *) + +Require Export PolyList. + + Record signature : Type := { + sort : Set; + sort_beq : sort->sort->bool; + sort_beq_refl : (f:sort)true=(sort_beq f f); + sort_beq_eq : (f1,f2:sort)true=(sort_beq f1 f2)->f1=f2; + fsym :> Set; + fsym_type : fsym->(list sort)*sort; + fsym_beq : fsym->fsym->bool; + fsym_beq_refl : (f:fsym)true=(fsym_beq f f); + fsym_beq_eq : (f1,f2:fsym)true=(fsym_beq f1 f2)->f1=f2 + }. + + + Variable F : signature. + + Definition vsym := (sort F)*nat. + + Definition vsym_sort := (fst (sort F) nat). + Definition vsym_nat := (snd (sort F) nat). + + + Mutual Inductive term : (sort F)->Set := + | term_var : (v:vsym)(term (vsym_sort v)) + | term_app : (f:F)(list_term (Fst (fsym_type F f))) + ->(term (Snd (fsym_type F f))) + with list_term : (list (sort F)) -> Set := + | term_nil : (list_term (nil (sort F))) + | term_cons : (s:(sort F);l:(list (sort F))) + (term s)->(list_term l)->(list_term (cons s l)). + diff --git a/test-suite/success/options.v b/test-suite/success/options.v new file mode 100644 index 00000000..9e9af4fa --- /dev/null +++ b/test-suite/success/options.v @@ -0,0 +1,34 @@ +(* Check that the syntax for options works *) +Set Implicit Arguments. +Unset Implicit Arguments. +Test Implicit Arguments. + +Set Printing Coercions. +Unset Printing Coercions. +Test Printing Coercions. + +Set Silent. +Unset Silent. +Test Silent. + +Set Printing Depth 100. +Print Table Printing Depth. + +Parameter i : bool -> nat. +Coercion i : bool >-> nat. +Set Printing Coercion i. +Unset Printing Coercion i. +Test Printing Coercion i. + +Print Table Printing Let. +Print Table Printing If. +Remove Printing Let sig. +Remove Printing If bool. + +Unset Printing Synth. +Set Printing Synth. +Test Printing Synth. + +Unset Printing Wildcard. +Set Printing Wildcard. +Test Printing Wildcard. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v new file mode 100644 index 00000000..ad4eed5a --- /dev/null +++ b/test-suite/success/refine.v @@ -0,0 +1,30 @@ + +(* Refine and let-in's *) + +Goal (EX x:nat | x=O). +Refine let y = (plus O O) in ?. +Exists y; Auto. +Save test1. + +Goal (EX x:nat | x=O). +Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?). +Auto. +Save test2. + +Goal nat. +Refine let y = O in (plus O ?). +Exact (S O). +Save test3. + +(* Example submitted by Yves on coqdev *) + +Require PolyList. + +Goal (l:(list nat))l=l. +Proof. +Refine [l]<[l]l=l> + Cases l of + | nil => ? + | (cons O l0) => ? + | (cons (S _) l0) => ? + end. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v new file mode 100644 index 00000000..2d2b2af8 --- /dev/null +++ b/test-suite/success/setoid_test.v @@ -0,0 +1,104 @@ +Require Setoid. + +Parameter A : Set. + +Axiom eq_dec : (a,b :A) {a=b}+{~a=b}. + +Inductive set : Set := +|Empty : set +|Add : A -> set -> set. + +Fixpoint In [a:A; s:set] : Prop := +Cases s of +|Empty => False +|(Add b s') => a=b \/ (In a s') +end. + +Definition same [s,t:set] : Prop := +(a:A) (In a s) <-> (In a t). + +Lemma setoid_set : (Setoid_Theory set same). + +Unfold same; Split. +Red; Auto. + +Red. +Intros. +Elim (H a); Auto. + +Intros. +Elim (H a); Elim (H0 a). +Split; Auto. +Save. + +Add Setoid set same setoid_set. + +Add Morphism In : In_ext. +Unfold same; Intros a s t H; Elim (H a); Auto. +Save. + +Lemma add_aux : (s,t:set) (same s t) -> + (a,b:A)(In a (Add b s)) -> (In a (Add b t)). +Unfold same; Induction 2; Intros. +Rewrite H1. +Simpl; Left; Reflexivity. + +Elim (H a). +Intros. +Simpl; Right. +Apply (H2 H1). +Save. + +Add Morphism Add : Add_ext. +Split; Apply add_aux. +Assumption. + +Rewrite H. +Apply Seq_refl. +Exact setoid_set. +Save. + +Fixpoint remove [a:A; s:set] : set := +Cases s of +|Empty => Empty +|(Add b t) => Cases (eq_dec a b) of + |(left _) => (remove a t) + |(right _) => (Add b (remove a t)) + end +end. + +Lemma in_rem_not : (a:A)(s:set) ~(In a (remove a (Add a Empty))). + +Intros. +Setoid_replace (remove a (Add a Empty)) with Empty. +Unfold same. +Split. +Simpl. +Intro H; Elim H. + +Simpl. +Case (eq_dec a a). +Intros e ff; Elim ff. + +Intros; Absurd a=a; Trivial. + +Auto. +Save. + +Parameter P :set -> Prop. +Parameter P_ext : (s,t:set) (same s t) -> (P s) -> (P t). + +Add Morphism P : P_extt. +Exact P_ext. +Save. + +Lemma test_rewrite : (a:A)(s,t:set)(same s t) -> (P (Add a s)) -> (P (Add a t)). +Intros. +Rewrite <- H. +Rewrite H. +Setoid_rewrite <- H. +Setoid_rewrite H. +Setoid_rewrite <- H. +Trivial. +Save. + diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v new file mode 100644 index 00000000..de75dfce --- /dev/null +++ b/test-suite/success/unfold.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Test le Hint Unfold sur des var locales *) + +Section toto. +Local EQ:=eq. +Goal (EQ nat O O). +Hints Unfold EQ. +Auto. +Save. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v new file mode 100644 index 00000000..0a4b284f --- /dev/null +++ b/test-suite/success/univers.v @@ -0,0 +1,19 @@ +(* This requires cumulativity *) + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +Lemma lem1 : (True->Type1)->Type2. +Intro H. +Apply H. +Exact I. +Qed. + +Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). +Auto. +Qed. + +Lemma lem3 : (P:Prop)P. +Intro P ; Pattern P. +Apply lem2. +Abort. diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v new file mode 100644 index 00000000..f752c5bc --- /dev/null +++ b/test-suite/tactics/TestRefine.v @@ -0,0 +1,203 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Petit bench vite fait, mal fait *) + +Require Refine. + + +(************************************************************************) + +Lemma essai : (x:nat)x=x. + +Refine (([x0:nat]Cases x0 of + O => ? + | (S p) => ? + end) :: (x:nat)x=x). (* x0=x0 et x0=x0 *) + +Restart. + +Refine [x0:nat]<[n:nat]n=n>Case x0 of ? [p:nat]? end. (* OK *) + +Restart. + +Refine [x0:nat]<[n:nat]n=n>Cases x0 of O => ? | (S p) => ? end. (* OK *) + +Restart. + +(** +Refine [x0:nat]Cases x0 of O => ? | (S p) => ? end. (* cannot be executed *) +**) + +Abort. + + +(************************************************************************) + +Lemma T : nat. + +Refine (S ?). + +Abort. + + +(************************************************************************) + +Lemma essai2 : (x:nat)x=x. + +Refine Fix f{f/1 : (x:nat)x=x := [x:nat]? }. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Case x of ? [p:nat]? end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat]n=n>Cases x of O => ? | (S p) => ? end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Case x of + ? + [p:nat](f_equal nat nat S p p ?) end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Cases x of + O => ? + | (S p) =>(f_equal nat nat S p p ?) end}. + +Abort. + + +(************************************************************************) + +Lemma essai : nat. + +Parameter f : nat*nat -> nat -> nat. + +Refine (f ? ([x:nat](? :: nat) O)). + +Restart. + +Refine (f ? O). + +Abort. + + +(************************************************************************) + +Parameter P : nat -> Prop. + +Lemma essai : { x:nat | x=(S O) }. + +Refine (exist nat ? (S O) ?). (* ECHEC *) + +Restart. + +(* mais si on contraint par le but alors ca marche : *) +(* Remarque : on peut toujours faire ça *) +Refine ((exist nat ? (S O) ?) :: { x:nat | x=(S O) }). + +Restart. + +Refine (exist nat [x:nat](x=(S O)) (S O) ?). + +Abort. + + +(************************************************************************) + +Lemma essai : (n:nat){ x:nat | x=(S n) }. + +Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end. + +Restart. + +Refine (([n:nat]Case n of ? [p:nat]? end) :: (n:nat){ x:nat | x=(S n) }). + +Restart. + +Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end. + +Restart. + +Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := + [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end}. + +Restart. + +Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := + [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end}. + +Exists (S O). Trivial. +Elim (f0 p). +Refine [x:nat][h:x=(S p)](exist nat [x:nat]x=(S (S p)) (S x) ?). +Rewrite h. Auto. +Save. + + + +(* Quelques essais de recurrence bien fondée *) + +Require Wf. +Require Wf_nat. + +Lemma essai_wf : nat->nat. + +Refine [x:nat](well_founded_induction + nat + lt ? + [_:nat]nat->nat + [phi0:nat][w:(phi:nat)(lt phi phi0)->nat->nat](w x ?) + x x). +Exact lt_wf. + +Abort. + + +Require Compare_dec. +Require Lt. + +Lemma fibo : nat -> nat. +Refine (well_founded_induction + nat + lt ? + [_:nat]nat + [x0:nat][fib:(x:nat)(lt x x0)->nat] + Cases (zerop x0) of + (left _) => (S O) + | (right h1) => Cases (zerop (pred x0)) of + (left _) => (S O) + | (right h2) => (plus (fib (pred x0) ?) + (fib (pred (pred x0)) ?)) + end + end). +(********* +Refine (well_founded_induction + nat + lt ? + [_:nat]nat + [x0:nat][fib:(x:nat)(lt x x0)->nat] + Cases x0 of + O => (S O) + | (S O) => (S O) + | (S (S p)) => (plus (fib (pred x0) ?) + (fib (pred (pred x0)) ?)) + end). +***********) +Exact lt_wf. +Auto. +Apply lt_trans with m:=(pred x0); Auto. +Save. + + |