From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- test-suite/Makefile | 60 ++- test-suite/bench/lists-100.v | 2 +- test-suite/bench/lists_100.v | 2 +- test-suite/bugs/closed/2105.v | 2 + test-suite/bugs/closed/shouldfail/2406.v | 3 + test-suite/bugs/closed/shouldfail/2586.v | 5 + test-suite/bugs/closed/shouldsucceed/1416.v | 7 +- test-suite/bugs/closed/shouldsucceed/1507.v | 1 - test-suite/bugs/closed/shouldsucceed/1834.v | 174 +++++++ test-suite/bugs/closed/shouldsucceed/1912.v | 6 + test-suite/bugs/closed/shouldsucceed/1962.v | 55 +++ test-suite/bugs/closed/shouldsucceed/2127.v | 3 - test-suite/bugs/closed/shouldsucceed/2141.v | 14 + test-suite/bugs/closed/shouldsucceed/2181.v | 3 + test-suite/bugs/closed/shouldsucceed/2304.v | 4 + test-suite/bugs/closed/shouldsucceed/2307.v | 3 + test-suite/bugs/closed/shouldsucceed/2320.v | 14 + test-suite/bugs/closed/shouldsucceed/2342.v | 8 + test-suite/bugs/closed/shouldsucceed/2362.v | 38 ++ test-suite/bugs/closed/shouldsucceed/2378.v | 608 ++++++++++++++++++++++++ test-suite/bugs/closed/shouldsucceed/2388.v | 6 + test-suite/bugs/closed/shouldsucceed/2393.v | 13 + test-suite/bugs/closed/shouldsucceed/2404.v | 46 ++ test-suite/bugs/closed/shouldsucceed/2456.v | 53 +++ test-suite/bugs/closed/shouldsucceed/2473.v | 39 ++ test-suite/bugs/closed/shouldsucceed/2603.v | 18 + test-suite/bugs/closed/shouldsucceed/2613.v | 17 + test-suite/bugs/closed/shouldsucceed/2615.v | 14 + test-suite/bugs/closed/shouldsucceed/2616.v | 7 + test-suite/bugs/closed/shouldsucceed/2640.v | 17 + test-suite/bugs/opened/shouldnotfail/2310.v | 17 + test-suite/complexity/Notations.v | 10 + test-suite/complexity/evar_instance.v | 78 +++ test-suite/complexity/guard.v | 30 ++ test-suite/complexity/patternmatching.v | 8 + test-suite/complexity/ring2.v | 4 +- test-suite/csdp.cache | Bin 44878 -> 76555 bytes test-suite/failure/Tauto.v | 2 +- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/inductive4.v | 15 + test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/failure/universes2.v | 4 - test-suite/ide/undo.v | 5 +- test-suite/ide/undo001.fake | 10 + test-suite/ide/undo002.fake | 10 + test-suite/ide/undo003.fake | 8 + test-suite/ide/undo004.fake | 14 + test-suite/ide/undo005.fake | 15 + test-suite/ide/undo006.fake | 14 + test-suite/ide/undo007.fake | 17 + test-suite/ide/undo008.fake | 18 + test-suite/ide/undo009.fake | 20 + test-suite/ide/undo010.fake | 28 ++ test-suite/ide/undo011.fake | 32 ++ test-suite/ide/undo012.fake | 26 + test-suite/ide/undo013.fake | 31 ++ test-suite/ide/undo014.fake | 26 + test-suite/ide/undo015.fake | 29 ++ test-suite/ide/undo016.fake | 34 ++ test-suite/ide/undo017.fake | 13 + test-suite/ide/undo018.fake | 13 + test-suite/ide/undo019.fake | 14 + test-suite/ideal-features/Apply.v | 2 +- test-suite/ideal-features/Case8.v | 36 -- test-suite/micromega/csdp.cache | Bin 44878 -> 0 bytes test-suite/misc/berardi_test.v | 4 +- test-suite/misc/deps/deps.out | 2 +- test-suite/misc/universes/universes.v | 2 + test-suite/modules/errors.v | 70 +++ test-suite/output/Arguments.out | 93 ++++ test-suite/output/Arguments.v | 40 ++ test-suite/output/ArgumentsScope.out | 5 + test-suite/output/Arguments_renaming.out | 108 +++++ test-suite/output/Arguments_renaming.v | 54 +++ test-suite/output/Errors.out | 2 + test-suite/output/Errors.v | 9 + test-suite/output/Existentials.out | 4 +- test-suite/output/Fixpoint.out | 15 +- test-suite/output/Fixpoint.v | 8 +- test-suite/output/Implicit.out | 2 + test-suite/output/Implicit.v | 17 +- test-suite/output/InitSyntax.out | 2 +- test-suite/output/Notations.out | 16 +- test-suite/output/Notations.v | 8 + test-suite/output/Notations2.out | 25 +- test-suite/output/Notations2.v | 26 +- test-suite/output/NumbersSyntax.out | 14 +- test-suite/output/PrintInfos.out | 129 +++++ test-suite/output/PrintInfos.v | 41 ++ test-suite/output/Record.out | 16 + test-suite/output/Record.v | 21 + test-suite/output/Search.out | 6 + test-suite/output/SearchPattern.out | 8 +- test-suite/output/Tactics.out | 10 +- test-suite/output/Tactics.v | 13 +- test-suite/output/ZSyntax.out | 8 +- test-suite/output/ZSyntax.v | 8 +- test-suite/output/inference.out | 6 + test-suite/output/inference.v | 14 + test-suite/output/rewrite-2172.out | 2 + test-suite/output/rewrite-2172.v | 21 + test-suite/success/AdvancedCanonicalStructure.v | 18 +- test-suite/success/CaseAlias.v | 70 +++ test-suite/success/Cases.v | 83 ++-- test-suite/success/CasesDep.v | 54 +++ test-suite/success/Check.v | 2 +- test-suite/success/Discriminate.v | 6 + test-suite/success/Field.v | 4 +- test-suite/success/Hints.v | 2 +- test-suite/success/Inductive.v | 29 ++ test-suite/success/Inversion.v | 15 +- test-suite/success/LegacyField.v | 4 +- test-suite/success/Notations.v | 27 ++ test-suite/success/Nsatz.v | 574 +++++++++++++++------- test-suite/success/PCase.v | 66 +++ test-suite/success/PrintSortedUniverses.v | 2 + test-suite/success/ProgramWf.v | 6 + test-suite/success/RecTutorial.v | 98 ++-- test-suite/success/Scheme.v | 4 + test-suite/success/Tauto.v | 4 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/apply.v | 34 +- test-suite/success/auto.v | 26 + test-suite/success/autorewrite.v | 29 ++ test-suite/success/autorewritein.v | 23 - test-suite/success/bullet.v | 5 + test-suite/success/change.v | 8 + test-suite/success/coercions.v | 8 + test-suite/success/conv_pbs.v | 5 + test-suite/success/destruct.v | 19 + test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 9 +- test-suite/success/eta.v | 19 + test-suite/success/evars.v | 71 +++ test-suite/success/extraction.v | 4 +- test-suite/success/fix.v | 5 +- test-suite/success/implicit.v | 17 + test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 25 +- test-suite/success/ltac.v | 27 ++ test-suite/success/mutual_ind.v | 2 +- test-suite/success/polymorphism.v | 2 +- test-suite/success/proof_using.v | 61 +++ test-suite/success/remember.v | 8 + test-suite/success/rewrite.v | 21 + test-suite/success/searchabout.v | 60 +++ test-suite/success/setoid_test.v | 35 ++ test-suite/success/simpl_tuning.v | 149 ++++++ test-suite/success/telescope_canonical.v | 12 + test-suite/success/unfold.v | 2 +- test-suite/success/unification.v | 50 +- test-suite/success/universes-coercion.v | 22 + test-suite/typeclasses/NewSetoid.v | 4 +- 158 files changed, 4047 insertions(+), 457 deletions(-) create mode 100644 test-suite/bugs/closed/2105.v create mode 100644 test-suite/bugs/closed/shouldfail/2406.v create mode 100644 test-suite/bugs/closed/shouldfail/2586.v create mode 100644 test-suite/bugs/closed/shouldsucceed/1834.v create mode 100644 test-suite/bugs/closed/shouldsucceed/1912.v create mode 100644 test-suite/bugs/closed/shouldsucceed/1962.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2141.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2181.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2304.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2307.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2320.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2342.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2362.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2378.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2393.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2404.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2456.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2473.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2603.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2613.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2615.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2616.v create mode 100644 test-suite/bugs/closed/shouldsucceed/2640.v create mode 100644 test-suite/bugs/opened/shouldnotfail/2310.v create mode 100644 test-suite/complexity/Notations.v create mode 100644 test-suite/complexity/evar_instance.v create mode 100644 test-suite/complexity/guard.v create mode 100644 test-suite/complexity/patternmatching.v create mode 100644 test-suite/failure/inductive4.v delete mode 100644 test-suite/failure/universes2.v create mode 100644 test-suite/ide/undo001.fake create mode 100644 test-suite/ide/undo002.fake create mode 100644 test-suite/ide/undo003.fake create mode 100644 test-suite/ide/undo004.fake create mode 100644 test-suite/ide/undo005.fake create mode 100644 test-suite/ide/undo006.fake create mode 100644 test-suite/ide/undo007.fake create mode 100644 test-suite/ide/undo008.fake create mode 100644 test-suite/ide/undo009.fake create mode 100644 test-suite/ide/undo010.fake create mode 100644 test-suite/ide/undo011.fake create mode 100644 test-suite/ide/undo012.fake create mode 100644 test-suite/ide/undo013.fake create mode 100644 test-suite/ide/undo014.fake create mode 100644 test-suite/ide/undo015.fake create mode 100644 test-suite/ide/undo016.fake create mode 100644 test-suite/ide/undo017.fake create mode 100644 test-suite/ide/undo018.fake create mode 100644 test-suite/ide/undo019.fake delete mode 100644 test-suite/ideal-features/Case8.v delete mode 100644 test-suite/micromega/csdp.cache create mode 100644 test-suite/misc/universes/universes.v create mode 100644 test-suite/modules/errors.v create mode 100644 test-suite/output/Arguments.out create mode 100644 test-suite/output/Arguments.v create mode 100644 test-suite/output/Arguments_renaming.out create mode 100644 test-suite/output/Arguments_renaming.v create mode 100644 test-suite/output/Errors.out create mode 100644 test-suite/output/Errors.v create mode 100644 test-suite/output/PrintInfos.out create mode 100644 test-suite/output/PrintInfos.v create mode 100644 test-suite/output/Record.out create mode 100644 test-suite/output/Record.v create mode 100644 test-suite/output/inference.out create mode 100644 test-suite/output/inference.v create mode 100644 test-suite/output/rewrite-2172.out create mode 100644 test-suite/output/rewrite-2172.v create mode 100644 test-suite/success/PCase.v create mode 100644 test-suite/success/PrintSortedUniverses.v create mode 100644 test-suite/success/Scheme.v create mode 100644 test-suite/success/auto.v create mode 100644 test-suite/success/autorewrite.v delete mode 100644 test-suite/success/autorewritein.v create mode 100644 test-suite/success/bullet.v create mode 100644 test-suite/success/eta.v create mode 100644 test-suite/success/proof_using.v create mode 100644 test-suite/success/remember.v create mode 100644 test-suite/success/searchabout.v create mode 100644 test-suite/success/simpl_tuning.v create mode 100644 test-suite/success/telescope_canonical.v create mode 100644 test-suite/success/universes-coercion.v (limited to 'test-suite') diff --git a/test-suite/Makefile b/test-suite/Makefile index 98bab43b..cd5886f8 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -75,7 +75,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ interactive micromega $(COMPLEXITY) modules # All subsystems -SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs +SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide ####################################################################### # Phony targets @@ -94,12 +94,9 @@ clean: rm -f trace lia.cache $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.log>" $(HIDE)find . \( \ - -name '*.stamp' -o -name '*.vo' -o -name '*.v.log' \ + -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ \) -print0 | xargs -0 rm -f -distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f - ####################################################################### # Per-subsystem targets ####################################################################### @@ -115,7 +112,7 @@ $(foreach S,$(VSUBSYSTEMS),$(eval $(call mkstamp,$(S)))) # Summary ####################################################################### -summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 tail -q -n1 | sort -g +summary_dir = echo $(1); find $(2) -name '*.log' -print0 | xargs -0 -n 1 tail -n1 | sort -g .PHONY: summary summary.log @@ -131,6 +128,7 @@ summary: $(call summary_dir, "Miscellaneous tests", misc); \ $(call summary_dir, "Complexity tests", complexity); \ $(call summary_dir, "Module tests", modules); \ + $(call summary_dir, "IDE tests", ide); \ nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \ nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \ nb_tests=`expr $$nb_success + $$nb_failure`; \ @@ -271,7 +269,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v | grep -v "Welcome to Coq" \ | grep -v "Skipping rcfile loading" \ > $$tmpoutput; \ - diff $$tmpoutput $*.out 2>&1; R=$$?; times; \ + diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -354,7 +352,7 @@ $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik. # Miscellaneous tests ####################################################################### -misc: misc/xml.log misc/deps-order.log +misc: misc/xml.log misc/deps-order.log misc/universes.log # Test xml compilation xml: misc/xml.log @@ -371,7 +369,7 @@ misc/xml.log: else \ echo $(log_success); \ echo " misc/xml...apparently ok"; \ - fi; rm -r misc/xml; \ + fi; rm -rf misc/xml; \ } > "$@" # Check that both coqdep and coqtop/coqc takes the later -I/-R @@ -386,7 +384,7 @@ misc/deps-order.log: tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ $(coqdep) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 \ | head -n 1 > $$tmpoutput; \ - diff $$tmpoutput misc/deps/deps.out 2>&1; R=$$?; times; \ + diff -u misc/deps/deps.out $$tmpoutput 2>&1; R=$$?; times; \ $(bincoqc) -I misc/deps/lib -as lib misc/deps/lib/foo.v 2>&1; \ $(bincoqc) -I misc/deps/lib -as lib -R misc/deps/client client misc/deps/client/foo.v 2>&1; \ $(coqtop) -I misc/deps/lib -as lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1; \ @@ -400,3 +398,45 @@ misc/deps-order.log: fi; \ rm $$tmpoutput; \ } > "$@" + +# Sort universes for the whole standard library +EXPECTED_UNIVERSES := 3 +universes: misc/universes.log +misc/universes.log: misc/universes/all_stdlib.v + @echo "TEST misc/universes" + $(HIDE){ \ + $(bincoqc) -I misc/universes misc/universes/all_stdlib 2>&1; \ + $(bincoqc) -I misc/universes misc/universes/universes 2>&1; \ + mv universes.txt misc/universes; \ + N=`awk '{print $$3}' misc/universes/universes.txt | sort -u | wc -l`; \ + times; \ + if [ "$$N" -eq $(EXPECTED_UNIVERSES) ]; then \ + echo $(log_success); \ + echo " misc/universes...Ok ($(EXPECTED_UNIVERSES) universes)"; \ + else \ + echo $(log_failure); \ + echo " misc/universes...Error! ($$N/$(EXPECTED_UNIVERSES) universes)"; \ + fi; \ + } > "$@" + +misc/universes/all_stdlib.v: + cd .. && $(MAKE) test-suite/$@ + + +# IDE : some tests of backtracking for coqtop -ideslave + +ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) + +%.fake.log : %.fake + @echo "TEST $<" + $(HIDE){ \ + echo $(call log_intro,$<); \ + $(BIN)fake_ide "$(BIN)coqtop -boot" < $< 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + else \ + echo $(log_failure); \ + echo " $<...Error!"; \ + fi; \ + } > "$@" diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 490de2a6..3d145d96 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* x) (at level 20). +Definition crash_the_rooster f := ’. diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v new file mode 100644 index 00000000..6111a641 --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/2586.v @@ -0,0 +1,5 @@ +Require Import Setoid SetoidClass Program. + +Goal forall `(Setoid nat) x y, x == y -> S x == S y. + intros. + clsubst H0. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v index da67d9b0..ee092005 100644 --- a/test-suite/bugs/closed/shouldsucceed/1416.v +++ b/test-suite/bugs/closed/shouldsucceed/1416.v @@ -1,3 +1,8 @@ +(* In 8.1 autorewrite used to raised an anomaly here *) +(* After resolution of the bug, autorewrite succeeded *) +(* From forthcoming 8.4, autorewrite is forbidden to instantiate *) +(* evars, so the new test just checks it is not an anomaly *) + Set Implicit Arguments. Record Place (Env A: Type) : Type := { @@ -22,6 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A), Proof. intros Env A e p; eapply ex_intro. autorewrite with placeeq. (* Here is the bug *) - auto. -Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v index ea72ba89..f2ab9100 100644 --- a/test-suite/bugs/closed/shouldsucceed/1507.v +++ b/test-suite/bugs/closed/shouldsucceed/1507.v @@ -2,7 +2,6 @@ Implementing reals a la Stolzenberg Danko Ilik, March 2007 - svn revision: $Id: 1507.v 12337 2009-09-17 15:58:14Z glondu $ XField.v -- (unfinished) axiomatisation of the theories of real and rational intervals. diff --git a/test-suite/bugs/closed/shouldsucceed/1834.v b/test-suite/bugs/closed/shouldsucceed/1834.v new file mode 100644 index 00000000..947d15f0 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1834.v @@ -0,0 +1,174 @@ +(* This tests rather deep nesting of abstracted terms *) + +(* This used to fail before Nov 2011 because of a de Bruijn indice bug + in extract_predicate. + + Note: use of eq_ok allows shorten notations but was not in the + original example +*) + +Scheme eq_rec_dep := Induction for eq Sort Type. + +Section Teq. + +Variable P0: Type. +Variable P1: forall (y0:P0), Type. +Variable P2: forall y0 (y1:P1 y0), Type. +Variable P3: forall y0 y1 (y2:P2 y0 y1), Type. +Variable P4: forall y0 y1 y2 (y3:P3 y0 y1 y2), Type. +Variable P5: forall y0 y1 y2 y3 (y4:P4 y0 y1 y2 y3), Type. + +Variable x0:P0. + +Inductive eq0 : P0 -> Prop := + refl0: eq0 x0. + +Definition eq_0 y0 := x0 = y0. + +Variable x1:P1 x0. + +Inductive eq1 : forall y0, P1 y0 -> Prop := + refl1: eq1 x0 x1. + +Definition S0_0 y0 (e0:eq_0 y0) := + eq_rec_dep P0 x0 (fun y0 e0 => P1 y0) x1 y0 e0. + +Definition eq_ok0 y0 y1 (E: eq_0 y0) := S0_0 y0 E = y1. + +Definition eq_1 y0 y1 := + {E0:eq_0 y0 | eq_ok0 y0 y1 E0}. + +Variable x2:P2 x0 x1. + +Inductive eq2 : +forall y0 y1, P2 y0 y1 -> Prop := +refl2: eq2 x0 x1 x2. + +Definition S1_0 y0 (e0:eq_0 y0) := +eq_rec_dep P0 x0 (fun y0 e0 => P2 y0 (S0_0 y0 e0)) x2 y0 e0. + +Definition S1_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := + eq_rec_dep (P1 y0) (S0_0 y0 e0) (fun y1 e1 => P2 y0 y1) + (S1_0 y0 e0) + y1 e1. + +Definition eq_ok1 y0 y1 y2 (E: eq_1 y0 y1) := + match E with exist e0 e1 => S1_1 y0 y1 e0 e1 = y2 end. + +Definition eq_2 y0 y1 y2 := + {E1:eq_1 y0 y1 | eq_ok1 y0 y1 y2 E1}. + +Variable x3:P3 x0 x1 x2. + +Inductive eq3 : +forall y0 y1 y2, P3 y0 y1 y2 -> Prop := +refl3: eq3 x0 x1 x2 x3. + +Definition S2_0 y0 (e0:eq_0 y0) := +eq_rec_dep P0 x0 (fun y0 e0 => P3 y0 (S0_0 y0 e0) (S1_0 y0 e0)) x3 y0 e0. + +Definition S2_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := + eq_rec_dep (P1 y0) (S0_0 y0 e0) + (fun y1 e1 => P3 y0 y1 (S1_1 y0 y1 e0 e1)) + (S2_0 y0 e0) + y1 e1. + +Definition S2_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) := + eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) + (fun y2 e2 => P3 y0 y1 y2) + (S2_1 y0 y1 e0 e1) + y2 e2. + +Definition eq_ok2 y0 y1 y2 y3 (E: eq_2 y0 y1 y2) : Prop := + match E with exist (exist e0 e1) e2 => + S2_2 y0 y1 y2 e0 e1 e2 = y3 end. + +Definition eq_3 y0 y1 y2 y3 := + {E2: eq_2 y0 y1 y2 | eq_ok2 y0 y1 y2 y3 E2}. + +Variable x4:P4 x0 x1 x2 x3. + +Inductive eq4 : +forall y0 y1 y2 y3, P4 y0 y1 y2 y3 -> Prop := +refl4: eq4 x0 x1 x2 x3 x4. + +Definition S3_0 y0 (e0:eq_0 y0) := +eq_rec_dep P0 x0 (fun y0 e0 => P4 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0)) + x4 y0 e0. + +Definition S3_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := + eq_rec_dep (P1 y0) (S0_0 y0 e0) + (fun y1 e1 => P4 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1)) + (S3_0 y0 e0) + y1 e1. + +Definition S3_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) := + eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) + (fun y2 e2 => P4 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2)) + (S3_1 y0 y1 e0 e1) + y2 e2. + +Definition S3_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):= + eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2) + (fun y3 e3 => P4 y0 y1 y2 y3) + (S3_2 y0 y1 y2 e0 e1 e2) + y3 e3. + +Definition eq_ok3 y0 y1 y2 y3 y4 (E: eq_3 y0 y1 y2 y3) : Prop := + match E with exist (exist (exist e0 e1) e2) e3 => + S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4 end. + +Definition eq_4 y0 y1 y2 y3 y4 := + {E3: eq_3 y0 y1 y2 y3 | eq_ok3 y0 y1 y2 y3 y4 E3}. + +Variable x5:P5 x0 x1 x2 x3 x4. + +Inductive eq5 : +forall y0 y1 y2 y3 y4, P5 y0 y1 y2 y3 y4 -> Prop := +refl5: eq5 x0 x1 x2 x3 x4 x5. + +Definition S4_0 y0 (e0:eq_0 y0) := +eq_rec_dep P0 x0 +(fun y0 e0 => P5 y0 (S0_0 y0 e0) (S1_0 y0 e0) (S2_0 y0 e0) (S3_0 y0 e0)) + x5 y0 e0. + +Definition S4_1 y0 y1 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) := + eq_rec_dep (P1 y0) (S0_0 y0 e0) + (fun y1 e1 => P5 y0 y1 (S1_1 y0 y1 e0 e1) (S2_1 y0 y1 e0 e1) (S3_1 y0 y1 e0 +e1)) + (S4_0 y0 e0) + y1 e1. + +Definition S4_2 y0 y1 y2 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) := + eq_rec_dep (P2 y0 y1) (S1_1 y0 y1 e0 e1) + (fun y2 e2 => P5 y0 y1 y2 (S2_2 y0 y1 y2 e0 e1 e2) (S3_2 y0 y1 y2 e0 e1 e2)) + (S4_1 y0 y1 e0 e1) + y2 e2. + +Definition S4_3 y0 y1 y2 y3 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3):= + eq_rec_dep (P3 y0 y1 y2) (S2_2 y0 y1 y2 e0 e1 e2) + (fun y3 e3 => P5 y0 y1 y2 y3 (S3_3 y0 y1 y2 y3 e0 e1 e2 e3)) + (S4_2 y0 y1 y2 e0 e1 e2) + y3 e3. + +Definition S4_4 y0 y1 y2 y3 y4 (e0:eq_0 y0) (e1:S0_0 y0 e0 = y1) + (e2:S1_1 y0 y1 e0 e1 = y2) (e3:S2_2 y0 y1 y2 e0 e1 e2 = y3) + (e4:S3_3 y0 y1 y2 y3 e0 e1 e2 e3 = y4) := + eq_rec_dep (P4 y0 y1 y2 y3) (S3_3 y0 y1 y2 y3 e0 e1 e2 e3) + (fun y4 e4 => P5 y0 y1 y2 y3 y4) + (S4_3 y0 y1 y2 y3 e0 e1 e2 e3) + y4 e4. + +Definition eq_ok4 y0 y1 y2 y3 y4 y5 (E: eq_4 y0 y1 y2 y3 y4) : Prop := + match E with exist (exist (exist (exist e0 e1) e2) e3) e4 => + S4_4 y0 y1 y2 y3 y4 e0 e1 e2 e3 e4 = y5 end. + +Definition eq_5 y0 y1 y2 y3 y4 y5 := + {E4: eq_4 y0 y1 y2 y3 y4 | eq_ok4 y0 y1 y2 y3 y4 y5 E4 }. + +End Teq. diff --git a/test-suite/bugs/closed/shouldsucceed/1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v new file mode 100644 index 00000000..987a5417 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1912.v @@ -0,0 +1,6 @@ +Require Import ZArith. + +Goal forall x, Z.succ (Z.pred x) = x. +intros x. +omega. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1962.v b/test-suite/bugs/closed/shouldsucceed/1962.v new file mode 100644 index 00000000..a6b0fee5 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1962.v @@ -0,0 +1,55 @@ +(* Bug 1962.v + +Bonjour, + +J'ai un exemple de lemme que j'arrivais à prouver avec fsetdec avec la 8.2beta3 +avec la beta4 et la version svn 11447 branche 8.2 çà diverge. + +Voici l'exemple en question, l'exmple test2 marche bien dans les deux version, +test en revanche pose probleme: + +*) + +Require Export FSets. + +(** This module takes a decidable type and +build finite sets of this type, tactics and defs *) + +Module BuildFSets (DecPoints: UsualDecidableType). + +Module Export FiniteSetsOfPoints := FSetWeakList.Make DecPoints. +Module Export FiniteSetsOfPointsProperties := + WProperties FiniteSetsOfPoints. +Module Export Dec := WDecide FiniteSetsOfPoints. +Module Export FM := Dec.F. + +Definition set_of_points := t. +Definition Point := DecPoints.t. + +Definition couple(x y :Point) : set_of_points := +add x (add y empty). + +Definition triple(x y t :Point): set_of_points := +add x (add y (add t empty)). + +Lemma test : forall P A B C A' B' C', +Equal +(union (singleton P) (union (triple A B C) (triple A' B' C'))) +(union (triple P B B') (union (couple P A) (triple C A' C'))). +Proof. +intros. +unfold triple, couple. +Time fsetdec. (* works in 8.2 beta 3, not in beta 4 and final 8.2 *) + (* appears to works again in 8.3 and trunk, take 4-6 seconds *) +Qed. + +Lemma test2 : forall A B C, +Equal + (union (singleton C) (couple A B)) (triple A B C). +Proof. +intros. +unfold triple, couple. +Time fsetdec. +Qed. + +End BuildFSets. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v index 20ea4603..0fc854b6 100644 --- a/test-suite/bugs/closed/shouldsucceed/2127.v +++ b/test-suite/bugs/closed/shouldsucceed/2127.v @@ -6,6 +6,3 @@ Module A. Hint Rewrite sym_equal using apply refl_equal : foo. End A. - - - diff --git a/test-suite/bugs/closed/shouldsucceed/2141.v b/test-suite/bugs/closed/shouldsucceed/2141.v new file mode 100644 index 00000000..941ae530 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2141.v @@ -0,0 +1,14 @@ +Require Import FSetList. +Require Import OrderedTypeEx. + +Module NatSet := FSetList.Make (Nat_as_OT). +Recursive Extraction NatSet.fold. + +Module FSetHide (X : FSetInterface.S). + Include X. +End FSetHide. + +Module NatSet' := FSetHide NatSet. +Recursive Extraction NatSet'.fold. + +(* Extraction "test2141.ml" NatSet'.fold. *) \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2181.v b/test-suite/bugs/closed/shouldsucceed/2181.v new file mode 100644 index 00000000..62820d86 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2181.v @@ -0,0 +1,3 @@ +Class C. +Parameter P: C -> Prop. +Fail Record R: Type := { _: C; u: P _ }. diff --git a/test-suite/bugs/closed/shouldsucceed/2304.v b/test-suite/bugs/closed/shouldsucceed/2304.v new file mode 100644 index 00000000..1ac2702b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2304.v @@ -0,0 +1,4 @@ +(* This used to fail with an anomaly NotASort at some time *) +Class A (O: Type): Type := a: O -> Type. +Fail Goal forall (x: a tt), @a x = @a x. + diff --git a/test-suite/bugs/closed/shouldsucceed/2307.v b/test-suite/bugs/closed/shouldsucceed/2307.v new file mode 100644 index 00000000..7c049495 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2307.v @@ -0,0 +1,3 @@ +Inductive V: nat -> Type := VS n: V (S n). +Definition f (e: V 1): nat := match e with VS 0 => 3 end. + diff --git a/test-suite/bugs/closed/shouldsucceed/2320.v b/test-suite/bugs/closed/shouldsucceed/2320.v new file mode 100644 index 00000000..facb9ecf --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2320.v @@ -0,0 +1,14 @@ +(* Managing metavariables in the return clause of a match *) + +(* This was working in 8.1 but is failing in 8.2 and 8.3. It works in + trunk thanks to the new proof engine. It could probably made to work in + 8.2 and 8.3 if a return predicate of the form "dummy 0" instead of + (or in addition to) a sophisticated predicate of the form + "as x in dummy y return match y with 0 => ?P | _ => ID end" *) + +Inductive dummy : nat -> Prop := constr : dummy 0. + +Lemma failure : forall (x : dummy 0), x = constr. +Proof. +intros x. +refine (match x with constr => _ end). diff --git a/test-suite/bugs/closed/shouldsucceed/2342.v b/test-suite/bugs/closed/shouldsucceed/2342.v new file mode 100644 index 00000000..094e5466 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2342.v @@ -0,0 +1,8 @@ +(* Checking that the type inference algoithme does not commit to an + equality over sorts when only a subtyping constraint is around *) + +Parameter A : Set. +Parameter B : A -> Set. +Parameter F : Set -> Prop. +Check (F (forall x, B x)). + diff --git a/test-suite/bugs/closed/shouldsucceed/2362.v b/test-suite/bugs/closed/shouldsucceed/2362.v new file mode 100644 index 00000000..febb9c7b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2362.v @@ -0,0 +1,38 @@ +Set Implicit Arguments. + +Class Pointed (M:Type -> Type) := +{ + creturn: forall {A: Type}, A -> M A +}. + +Unset Implicit Arguments. +Inductive FPair (A B:Type) (neutral: B) : Type:= + fpair : forall (a:A) (b:B), FPair A B neutral. +Implicit Arguments fpair [[A] [B] [neutral]]. + +Set Implicit Arguments. + +Notation "( x ,> y )" := (fpair x y) (at level 0). + +Instance Pointed_FPair B neutral: + Pointed (fun A => FPair A B neutral) := + { creturn := fun A (a:A) => (a,> neutral) }. +Definition blah_fail (x:bool) : FPair bool nat O := + creturn x. +Set Printing All. Print blah_fail. + +Definition blah_explicit (x:bool) : FPair bool nat O := + @creturn _ (Pointed_FPair _ ) _ x. + +Print blah_explicit. + + +Instance Pointed_FPair_mono: + Pointed (fun A => FPair A nat 0) := + { creturn := fun A (a:A) => (a,> 0) }. + + +Definition blah (x:bool) : FPair bool nat O := + creturn x. + + diff --git a/test-suite/bugs/closed/shouldsucceed/2378.v b/test-suite/bugs/closed/shouldsucceed/2378.v new file mode 100644 index 00000000..7deec64d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2378.v @@ -0,0 +1,608 @@ +(* test with Coq 8.3rc1 *) + +Require Import Program. + +Inductive Unit: Set := unit: Unit. + +Definition eq_dec T := forall x y:T, {x=y}+{x<>y}. + +Section TTS_TASM. + +Variable Time: Set. +Variable Zero: Time. +Variable tle: Time -> Time -> Prop. +Variable tlt: Time -> Time -> Prop. +Variable tadd: Time -> Time -> Time. +Variable tsub: Time -> Time -> Time. +Variable tmin: Time -> Time -> Time. +Notation "t1 @<= t2" := (tle t1 t2) (at level 70, no associativity). +Notation "t1 @< t2" := (tlt t1 t2) (at level 70, no associativity). +Notation "t1 @+ t2" := (tadd t1 t2) (at level 50, left associativity). +Notation "t1 @- t2" := (tsub t1 t2) (at level 50, left associativity). +Notation "t1 @<= t2 @<= t3" := ((tle t1 t2) /\ (tle t2 t3)) (at level 70, t2 at next level). +Notation "t1 @<= t2 @< t3" := ((tle t1 t2) /\ (tlt t2 t3)) (at level 70, t2 at next level). + +Variable tzerop: forall n, (n = Zero) + {Zero @< n}. +Variable tlt_eq_gt_dec: forall x y, {x @< y} + {x=y} + {y @< x}. +Variable tle_plus_l: forall n m, n @<= n @+ m. +Variable tle_lt_eq_dec: forall n m, n @<= m -> {n @< m} + {n = m}. + +Variable tzerop_zero: tzerop Zero = inleft (Zero @< Zero) (@eq_refl _ Zero). +Variable tplus_n_O: forall n, n @+ Zero = n. +Variable tlt_le_weak: forall n m, n @< m -> n @<= m. +Variable tlt_irrefl: forall n, ~ n @< n. +Variable tplus_nlt: forall n m, ~n @+ m @< n. +Variable tle_n: forall n, n @<= n. +Variable tplus_lt_compat_l: forall n m p, n @< m -> p @+ n @< p @+ m. +Variable tlt_trans: forall n m p, n @< m -> m @< p -> n @< p. +Variable tle_lt_trans: forall n m p, n @<= m -> m @< p -> n @< p. +Variable tlt_le_trans: forall n m p, n @< m -> m @<= p -> n @< p. +Variable tle_refl: forall n, n @<= n. +Variable tplus_le_0: forall n m, n @+ m @<= n -> m = Zero. +Variable Time_eq_dec: eq_dec Time. + +(*************************************************************) + +Section PropLogic. +Variable Predicate: Type. + +Inductive LP: Type := + LPPred: Predicate -> LP +| LPAnd: LP -> LP -> LP +| LPNot: LP -> LP. + +Variable State: Type. +Variable Sat: State -> Predicate -> Prop. + +Fixpoint lpSat st f: Prop := + match f with + LPPred p => Sat st p + | LPAnd f1 f2 => lpSat st f1 /\ lpSat st f2 + | LPNot f1 => ~lpSat st f1 + end. +End PropLogic. + +Implicit Arguments lpSat. + +Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 := + match f with + LPPred p => p2lp p + | LPAnd f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2) + | LPNot f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1) + end. +Implicit Arguments LPTransfo. + +Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := + LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f. + +Section TTS. + +Variable State: Type. + +Record TTS: Type := mkTTS { + Init: State -> Prop; + Delay: State -> Time -> State -> Prop; + Next: State -> State -> Prop; + Predicate: Type; + Satisfy: State -> Predicate -> Prop +}. + +Definition TTSIndexedProduct Ind (tts: Ind -> TTS): TTS := mkTTS + (fun st => forall i, Init (tts i) st) + (fun st d st' => forall i, Delay (tts i) st d st') + (fun st st' => forall i, Next (tts i) st st') + { i: Ind & Predicate (tts i) } + (fun st p => Satisfy (tts (projT1 p)) st (projT2 p)). + +End TTS. + +Section SIMU_F. + +Variables StateA StateC: Type. + +Record mapping: Type := mkMapping { + mState: Type; + mInit: StateC -> mState; + mNext: mState -> StateC -> mState; + mDelay: mState -> StateC -> Time -> mState; + mabs: mState -> StateC -> StateA +}. + +Variable m: mapping. + +Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuPrf { + inv: (mState m) -> StateC -> Prop; + invInit: forall st, Init _ c st -> inv (mInit m st) st; + invDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> inv (mDelay m ex1 st1 d) st2; + invNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> inv (mNext m ex1 st1) st2; + simuInit: forall st, Init _ c st -> Init _ a (mabs m (mInit m st) st); + simuDelay: forall ex1 st1 st2 d, Delay _ c st1 d st2 -> inv ex1 st1 -> + Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2); + simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 -> + Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2); + simuPred: forall ext st, inv ext st -> + (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) +}. + +Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)), + lpSat (Sat i) st f + <-> + lpSat + (fun (st : State) (p : {i : Ind & Pred i}) => Sat (projT1 p) st (projT2 p)) st + (addIndex Ind _ i f). +Proof. + induction f; simpl; intros; split; intros; intuition. +Qed. + +Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))): + {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) := + fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)). + +Implicit Arguments trProd. +Require Import Setoid. + +Theorem satTrProd: + forall State Ind Pred (tts: Ind -> TTS State) + (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}), + lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p)) + <-> + lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p). +Proof. + unfold trProd, TTSIndexedProduct; simpl; intros. + rewrite (satProd State Ind (fun i => Predicate State (tts i)) + (fun i => Satisfy _ (tts i))); tauto. +Qed. + +Theorem simuProd: + forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) + (tra: forall i, (Pred i) -> LP (Predicate _ (tta i))) + (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))), + (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> + simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc) + (trProd Pred tta tra) (trProd Pred ttc trc). +Proof. + intros. + apply simuPrf with (fun ex st => forall i, inv _ _ (ttc i) (tra i) (trc i) (X i) ex st); simpl; intros; auto. + eapply invInit; eauto. + eapply invDelay; eauto. + eapply invNext; eauto. + eapply simuInit; eauto. + eapply simuDelay; eauto. + eapply simuNext; eauto. + split; simpl; intros. + generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro. + rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1. + rewrite (satTrProd StateC Ind Pred ttc trc); apply H0. + + generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro. + rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1. + rewrite (satTrProd StateA Ind Pred tta tra); apply H0. +Qed. + +End SIMU_F. + +Section TRANSFO. + +Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predicate _ a)) (trc: Pred -> LP (Predicate _ c)): Type := simuEquivPrf { + simuLR: simu StateA StateC m1 Pred a c tra trc; + simuRL: simu StateC StateA m2 Pred c a trc tra +}. + +Theorem simu_equivProd: + forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) + (tra: forall i, (Pred i) -> LP (Predicate _ (tta i))) + (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))), + (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> + simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc) + (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc). +Proof. + intros; split; intros. + apply simuProd; intro. + elim (X i); auto. + apply simuProd; intro. + elim (X i); auto. +Qed. + +Record RTLanguage: Type := mkRTLanguage { + Syntax: Type; + DynamicState: Syntax -> Type; + Semantic: forall (mdl:Syntax), TTS (DynamicState mdl); + MdlPredicate: Syntax -> Type; + MdlPredicateDefinition: forall mdl, MdlPredicate mdl -> LP (Predicate _ (Semantic mdl)) +}. + +Record Transformation (l1 l2: RTLanguage): Type := mkTransformation { + Tmodel: Syntax l1 -> Syntax l2; + Tl1l2: forall mdl, mapping (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)); + Tl2l1: forall mdl, mapping (DynamicState l2 (Tmodel mdl)) (DynamicState l1 mdl); + Tpred: forall mdl, MdlPredicate l1 mdl -> LP (MdlPredicate l2 (Tmodel mdl)); + Tsim: forall mdl, simu_equiv (DynamicState l1 mdl) (DynamicState l2 (Tmodel mdl)) (Tl1l2 mdl) (Tl2l1 mdl) + (MdlPredicate l1 mdl) (Semantic l1 mdl) (Semantic l2 (Tmodel mdl)) + (MdlPredicateDefinition l1 mdl) + (fun p => LPTransfo (MdlPredicateDefinition l2 (Tmodel mdl)) (Tpred mdl p)) +}. + +Section Product. + +Record PSyntax (L: RTLanguage): Type := mkPSyntax { + pIndex: Type; + pIsEmpty: pIndex + {pIndex -> False}; + pState: Type; + pComponents: pIndex -> Syntax L; + pIsShared: forall i, DynamicState L (pComponents i) = pState +}. + +Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & MdlPredicate L (pComponents L sys i)}. + +(* product with shared state *) + +Definition PLanguage (L: RTLanguage): RTLanguage := + mkRTLanguage + (PSyntax L) + (pState L) + (fun mdl => TTSIndexedProduct (pState L mdl) (pIndex L mdl) + (fun i => match pIsShared L mdl i in (_ = y) return TTS y with + eq_refl => Semantic L (pComponents L mdl i) + end)) + (pPredicate L) + (fun mdl => trProd _ _ _ _ + (fun i pi => match pIsShared L mdl i as e in (_ = y) return + (LP (Predicate y + match e in (_ = y0) return (TTS y0) with + | eq_refl => Semantic L (pComponents L mdl i) + end)) + with + | eq_refl => MdlPredicateDefinition L (pComponents L mdl i) pi + end)). + +Inductive Empty: Type :=. + +Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf { +sameState: forall mdl i j, + DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) = + DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j)); +sameMState: forall mdl i j, + mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl i)) = + mState _ _ (Tl1l2 _ _ tr (pComponents l1 mdl j)); +sameM12: forall mdl i j, + Tl1l2 _ _ tr (pComponents l1 mdl i) = + match sym_eq (sameState mdl i j) in _=y return mapping _ y with + eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with + eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with + eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j) + end + end + end; +sameM21: forall mdl i j, + Tl2l1 l1 l2 tr (pComponents l1 mdl i) = + match + sym_eq (sameState mdl i j) in (_ = y) + return (mapping y (DynamicState l1 (pComponents l1 mdl i))) + with eq_refl => + match + sym_eq (pIsShared l1 mdl i) in (_ = y) + return + (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y) + with + | eq_refl => + match + pIsShared l1 mdl j in (_ = y) + return + (mapping + (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j))) y) + with + | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl j) + end + end +end +}. + +Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl := + mkPSyntax l2 (pIndex l1 mdl) + (pIsEmpty l1 mdl) + (match pIsEmpty l1 mdl return Type with + inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) + |inright h => pState l1 mdl + end) + (fun i => Tmodel l1 l2 tr (pComponents l1 mdl i)) + (fun i => match pIsEmpty l1 mdl as y return + (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) = + match y with + | inleft i0 => + DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i0)) + | inright _ => pState l1 mdl + end) + with + inleft j => sameState l1 l2 tr h mdl i j + | inright h => match h i with end + end). + +Definition compSemantic l mdl i := + match pIsShared l mdl i in (_=y) return TTS y with + eq_refl => Semantic l (pComponents l mdl i) + end. + +Definition compSemanticEq l mdl i s (e: DynamicState l (pComponents l mdl i) = s) := + match e in (_=y) return TTS y with + eq_refl => Semantic l (pComponents l mdl i) + end. + +Definition Pmap12 l1 l2 tr (h: isSharedTransfo l1 l2 tr) (mdl : PSyntax l1) := +match + pIsEmpty l1 mdl as s + return + (mapping (pState l1 mdl) + match s with + | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) + | inright _ => pState l1 mdl + end) +with +| inleft p => + match + pIsShared l1 mdl p in (_ = y) + return + (mapping y (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p)))) + with + | eq_refl => Tl1l2 l1 l2 tr (pComponents l1 mdl p) + end +| inright _ => + mkMapping (pState l1 mdl) (pState l1 mdl) Unit + (fun _ : pState l1 mdl => unit) + (fun (_ : Unit) (_ : pState l1 mdl) => unit) + (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit) + (fun (_ : Unit) (X : pState l1 mdl) => X) +end. + +Definition Pmap21 l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl := +match + pIsEmpty l1 mdl as s + return + (mapping + match s with + | inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) + | inright _ => pState l1 mdl + end (pState l1 mdl)) +with +| inleft p => + match + pIsShared l1 mdl p in (_ = y) + return + (mapping (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) y) + with + | eq_refl => Tl2l1 l1 l2 tr (pComponents l1 mdl p) + end +| inright _ => + mkMapping (pState l1 mdl) (pState l1 mdl) Unit + (fun _ : pState l1 mdl => unit) + (fun (_ : Unit) (_ : pState l1 mdl) => unit) + (fun (_ : Unit) (_ : pState l1 mdl) (_ : Time) => unit) + (fun (_ : Unit) (X : pState l1 mdl) => X) +end. + +Definition PTpred l1 l2 tr (h : isSharedTransfo l1 l2 tr) mdl (pp : pPredicate l1 mdl): + LP (MdlPredicate (PLanguage l2) (PTransfoSyntax l1 l2 tr h mdl)) := +match pIsEmpty l1 mdl with +| inleft _ => + let (x, p) := pp in + addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x + (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x)) + (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p)) +| inright f => match f (projS1 pp) with end +end. + +Lemma simu_eqA: + forall A1 A2 C m P sa sc tta ttc (h: A2=A1), + simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) + P (match h in (_=y) return TTS y with eq_refl => sa end) + sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end) + ttc -> + simu A2 C m P sa sc tta ttc. +admit. +Qed. + +Lemma simu_eqC: + forall A C1 C2 m P sa sc tta ttc (h: C2=C1), + simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) + P sa (match h in (_=y) return TTS y with eq_refl => sc end) + tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end) + -> + simu A C2 m P sa sc tta ttc. +admit. +Qed. + +Lemma simu_eqA1: + forall A1 A2 C m P sa sc tta ttc (h: A1=A2), + simu A1 C m + P + (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc + (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc + -> + simu A2 C (match h in (_=y) return mapping _ C with eq_refl => m end) P sa sc tta ttc. +admit. +Qed. + +Lemma simu_eqA2: + forall A1 A2 C m P sa sc tta ttc (h: A1=A2), + simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end) + P + sa sc tta ttc + -> + simu A2 C m P + (match h in (_=y) return TTS y with eq_refl => sa end) sc + (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end) + ttc. +admit. +Qed. + +Lemma simu_eqC2: + forall A C1 C2 m P sa sc tta ttc (h: C1=C2), + simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end) + P + sa sc tta ttc + -> + simu A C2 m P + sa (match h in (_=y) return TTS y with eq_refl => sc end) + tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end). +admit. +Qed. + +Lemma simu_eqM: + forall A C m1 m2 P sa sc tta ttc (h: m1=m2), + simu A C m1 P sa sc tta ttc + -> + simu A C m2 P sa sc tta ttc. +admit. +Qed. + +Lemma LPTransfo_trans: + forall Pred1 Pred2 Pred3 (tr1: Pred1 -> LP Pred2) (tr2: Pred2 -> LP Pred3) f, + LPTransfo tr2 (LPTransfo tr1 f) = LPTransfo (fun x => LPTransfo tr2 (tr1 x)) f. +Proof. + admit. +Qed. + +Lemma LPTransfo_addIndex: + forall Ind Pred tr1 x (tr2: forall i, Pred i -> LP (tr1 i)) (p: LP (Pred x)), + addIndex Ind tr1 x (LPTransfo (tr2 x) p) = + LPTransfo + (fun p0 : {i : Ind & Pred i} => + addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))) + (addIndex Ind Pred x p). +Proof. + unfold addIndex; intros. + rewrite LPTransfo_trans. + rewrite LPTransfo_trans. + simpl. + auto. +Qed. + +Record tr_compat I0 I1 tr := compatPrf { + and_compat: forall p1 p2, tr (LPAnd I0 p1 p2) = LPAnd I1 (tr p1) (tr p2); + not_compat: forall p, tr (LPNot I0 p) = LPNot I1 (tr p) +}. + +Lemma LPTransfo_addIndex_tr: + forall Ind Pred tr0 tr1 x (tr2: forall i, Pred i -> LP (tr0 i)) (tr3: forall i, LP (tr0 i) -> LP (tr1 i)) (p: LP (Pred x)), + (forall x, tr_compat (tr0 x) (tr1 x) (tr3 x)) -> + addIndex Ind tr1 x (tr3 x (LPTransfo (tr2 x) p)) = + LPTransfo + (fun p0 : {i : Ind & Pred i} => + addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))) + (addIndex Ind Pred x p). +Proof. + unfold addIndex; simpl; intros. + rewrite LPTransfo_trans; simpl. + rewrite <- LPTransfo_trans. + f_equal. + induction p; simpl; intros; auto. + rewrite (and_compat _ _ _ (H x)). + rewrite <- IHp1, <- IHp2; auto. + rewrite <- IHp. + rewrite (not_compat _ _ _ (H x)); auto. +Qed. + +Require Export Coq.Logic.FunctionalExtensionality. +Print PLanguage. +Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): +Transformation (PLanguage l1) (PLanguage l2) := + mkTransformation (PLanguage l1) (PLanguage l2) + (PTransfoSyntax l1 l2 tr h) + (Pmap12 l1 l2 tr h) + (Pmap21 l1 l2 tr h) + (PTpred l1 l2 tr h) + (fun mdl => simu_equivProd + (pState l1 mdl) + (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) + (Pmap12 l1 l2 tr h mdl) + (Pmap21 l1 l2 tr h mdl) + (pIndex l1 mdl) + (fun i => MdlPredicate l1 (pComponents l1 mdl i)) + (compSemantic l1 mdl) + (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl)) + _ + _ + _ + ). + +Next Obligation. + unfold compSemantic, PTransfoSyntax; simpl. + case (pIsEmpty l1 mdl); simpl; intros. + unfold pPredicate; simpl. + unfold pPredicate in X; simpl in X. + case (sameState l1 l2 tr h mdl i p). + apply (LPTransfo (MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))). + apply (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl i))). + apply (LPPred _ X). + + apply False_rect; apply (f i). +Defined. + +Next Obligation. + split; intros. + unfold Pmap12; simpl. + unfold PTransfo_obligation_1; simpl. + unfold compSemantic; simpl. + unfold eq_ind, eq_rect, f_equal; simpl. + case (pIsEmpty l1 mdl); intros. + apply simu_eqA2. + apply simu_eqC2. + apply simu_eqM with (Tl1l2 l1 l2 tr (pComponents l1 mdl i)). + apply sameM12. + apply (simuLR _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro. + + apply False_rect; apply (f i). + + unfold Pmap21; simpl. + unfold PTransfo_obligation_1; simpl. + unfold compSemantic; simpl. + unfold eq_ind, eq_rect, f_equal; simpl. + case (pIsEmpty l1 mdl); intros. + apply simu_eqC2. + apply simu_eqA2. + apply simu_eqM with (Tl2l1 l1 l2 tr (pComponents l1 mdl i)). + apply sameM21. + apply (simuRL _ _ _ _ _ _ _ _ _ (Tsim l1 l2 tr (pComponents l1 mdl i))); intro. + + apply False_rect; apply (f i). +Qed. + +Next Obligation. + unfold trProd; simpl. + unfold PTransfo_obligation_1; simpl. + unfold compSemantic; simpl. + unfold eq_ind, eq_rect, f_equal; simpl. + apply functional_extensionality; intro. + case x; clear x; intros. + unfold PTpred; simpl. + case (pIsEmpty l1 mdl); simpl; intros. + set (tr0 i := + Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) + (Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)))). + set (tr1 i := + Predicate (DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl p))) + match sameState l1 l2 tr h mdl i p in (_ = y) return (TTS y) with + | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) + end). + set (tr2 x := MdlPredicateDefinition l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))). + set (Pred x := MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl x))). + set (tr3 x f := match + sameState l1 l2 tr h mdl x p as e in (_ = y) + return + (LP + (Predicate y + match e in (_ = y0) return (TTS y0) with + | eq_refl => Semantic l2 (Tmodel l1 l2 tr (pComponents l1 mdl x)) + end)) + with + | eq_refl => f + end). + apply (LPTransfo_addIndex_tr _ Pred tr0 tr1 x tr2 tr3 + (Tpred l1 l2 tr (pComponents l1 mdl x) m)). + unfold tr0, tr1, tr3; intros; split; simpl; intros; auto. + case (sameState l1 l2 tr h mdl x0 p); auto. + case (sameState l1 l2 tr h mdl x0 p); auto. + + apply False_rect; apply (f x). +Qed. + +End Product. diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v index 8cc43ee6..c7926711 100644 --- a/test-suite/bugs/closed/shouldsucceed/2388.v +++ b/test-suite/bugs/closed/shouldsucceed/2388.v @@ -2,3 +2,9 @@ Fail Parameters (A:Prop) (a:A A). +(* This is a variant (reported as part of bug #2347) *) + +Require Import EquivDec. +Fail Program Instance bool_eq_eqdec : EqDec bool eq := + {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. + diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v new file mode 100644 index 00000000..fb4f9261 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2393.v @@ -0,0 +1,13 @@ +Require Import Program. + +Inductive T := MkT. + +Definition sizeOf (t : T) : nat + := match t with + | MkT => 1 + end. +Variable vect : nat -> Type. +Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T + := match t with + | MkT => MkT + end. diff --git a/test-suite/bugs/closed/shouldsucceed/2404.v b/test-suite/bugs/closed/shouldsucceed/2404.v new file mode 100644 index 00000000..fe8eba54 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2404.v @@ -0,0 +1,46 @@ +(* Check that dependencies in the indices of the type of the terms to + match are taken into account and correctly generalized *) + +Require Import Relations.Relation_Definitions. +Require Import Basics. + +Record Base := mkBase + {(* Primitives *) + World : Set + (* Names are real, links are theoretical *) + ; Name : World -> Set + + ; wweak : World -> World -> Prop + + ; exportw : forall a b : World, (wweak a b) -> (Name b) -> option (Name a) +}. + +Section Derived. + Variable base : Base. + Definition bWorld := World base. + Definition bName := Name base. + Definition bexportw := exportw base. + Definition bwweak := wweak base. + + Implicit Arguments bexportw [a b]. + +Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type := + starReflS : forall a, RstarSetProof T a a +| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k. + +Implicit Arguments starTransS [I T i j k]. + +Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))). + +Definition bwweakFlip (b a : bWorld) : Prop := (bwweak a b). +Definition Rweak : forall a b : bWorld, Type := RstarInv bwweak. + +Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) := + match aRWb,y with + | starReflS a, y' => Some y' + | starTransS i j k jWk jRWi, y' => + match (bexportw jWk y) with + | Some x => exportRweak jRWi x + | None => None + end + end. diff --git a/test-suite/bugs/closed/shouldsucceed/2456.v b/test-suite/bugs/closed/shouldsucceed/2456.v new file mode 100644 index 00000000..56f046c4 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2456.v @@ -0,0 +1,53 @@ + +Require Import Equality. + +Parameter Patch : nat -> nat -> Set. + +Inductive Catch (from to : nat) : Type + := MkCatch : forall (p : Patch from to), + Catch from to. +Implicit Arguments MkCatch [from to]. + +Inductive CatchCommute5 + : forall {from mid1 mid2 to : nat}, + Catch from mid1 + -> Catch mid1 to + -> Catch from mid2 + -> Catch mid2 to + -> Prop + := MkCatchCommute5 : + forall {from mid1 mid2 to : nat} + (p : Patch from mid1) + (q : Patch mid1 to) + (q' : Patch from mid2) + (p' : Patch mid2 to), + CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). + +Inductive CatchCommute {from mid1 mid2 to : nat} + (p : Catch from mid1) + (q : Catch mid1 to) + (q' : Catch from mid2) + (p' : Catch mid2 to) + : Prop + := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), + CatchCommute p q q' p'. +Notation "<< p , q >> <~> << q' , p' >>" + := (CatchCommute p q q' p') + (at level 60, no associativity). + +Lemma CatchCommuteUnique2 : + forall {from mid mid' to : nat} + {p : Catch from mid} {q : Catch mid to} + {q' : Catch from mid'} {p' : Catch mid' to} + {q'' : Catch from mid'} {p'' : Catch mid' to} + (commute1 : <> <~> <>) + (commute2 : <> <~> <>), + (p' = p'') /\ (q' = q''). +Proof with auto. +intros. +set (X := commute2). +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails generalizing X. +Admitted. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2473.v b/test-suite/bugs/closed/shouldsucceed/2473.v new file mode 100644 index 00000000..4c302512 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2473.v @@ -0,0 +1,39 @@ + +Require Import Relations Program Setoid Morphisms. + +Section S1. + Variable R: nat -> relation bool. + Instance HR1: forall n, Transitive (R n). Admitted. + Instance HR2: forall n, Symmetric (R n). Admitted. + Hypothesis H: forall n a, R n (andb a a) a. + Goal forall n a b, R n b a. + intros. + (* rewrite <- H. *) (* Anomaly: Evar ?.. was not declared. Please report. *) + (* idem with setoid_rewrite *) +(* assert (HR2' := HR2 n). *) + rewrite <- H. (* ok *) + admit. + Qed. +End S1. + +Section S2. + Variable R: nat -> relation bool. + Instance HR: forall n, Equivalence (R n). Admitted. + Hypothesis H: forall n a, R n (andb a a) a. + Goal forall n a b, R n a b. + intros. rewrite <- H. admit. + Qed. +End S2. + +(* the parametrised relation is required to get the problem *) +Section S3. + Variable R: relation bool. + Instance HR1': Transitive R. Admitted. + Instance HR2': Symmetric R. Admitted. + Hypothesis H: forall a, R (andb a a) a. + Goal forall a b, R b a. + intros. + rewrite <- H. (* ok *) + admit. + Qed. +End S3. \ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v new file mode 100644 index 00000000..a556b9bf --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2603.v @@ -0,0 +1,18 @@ +Module Type T. +End T. + +Declare Module K : T. + +Module Type L. +Declare Module E : T. +End L. + +Module M1 : L with Module E:=K. +Module E := K. +Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *) +End M1. + +Module M2 : L with Module E:=K. +Inductive t := E. +Fail Module E := K. (* Used to be accepted *) +Fail End M2. (* Used to be accepted *) diff --git a/test-suite/bugs/closed/shouldsucceed/2613.v b/test-suite/bugs/closed/shouldsucceed/2613.v new file mode 100644 index 00000000..4f0470b1 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2613.v @@ -0,0 +1,17 @@ +(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *) + +Require Import ZArith. +Require Recdef. + +Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}. + +Locate eq_sym. (* Constant Coq.Init.Logic.eq_sym *) + +Function loop (n: nat) {measure (fun x => x) n} : bool := + if nat_eq_dec n 0 then false else loop (pred n). +Proof. + admit. +Defined. + +Check eq_sym eq_refl : 0=0. + diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v new file mode 100644 index 00000000..54e1a07c --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2615.v @@ -0,0 +1,14 @@ +(* This failed with an anomaly in pre-8.4 because of let-in not + properly taken into account in the test for unification pattern *) + +Inductive foo : forall A, A -> Prop := +| foo_intro : forall A x, foo A x. +Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x). +Fail induction 1. + +(* Whether these examples should succeed with a non-dependent return predicate + or fail because there is well-typed return predicate dependent in f + is questionable. As of 25 oct 2011, they succeed *) +refine (fun p => match p with _ => _ end). +Undo. +refine (fun p => match p with foo_intro _ _ => _ end). diff --git a/test-suite/bugs/closed/shouldsucceed/2616.v b/test-suite/bugs/closed/shouldsucceed/2616.v new file mode 100644 index 00000000..8758e32d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2616.v @@ -0,0 +1,7 @@ +(* Testing ill-typed rewrite which used to succeed in 8.3 *) +Goal + forall (N : nat -> Prop) (g : nat -> sig N) (IN : forall a : sig N, a = g 0), + N 0 -> False. +Proof. +intros. +Fail rewrite IN in H. diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v new file mode 100644 index 00000000..da0cc68a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2640.v @@ -0,0 +1,17 @@ +(* Testing consistency of globalization and interpretation in some + extreme cases *) + +Section sect. + + (* Simplification of the initial example *) + Hypothesis Other: True. + + Lemma C2 : True. + proof. + Fail have True using Other. + Abort. + + (* Variant of the same problem *) + Lemma C2 : True. + Fail clear; Other. + Abort. diff --git a/test-suite/bugs/opened/shouldnotfail/2310.v b/test-suite/bugs/opened/shouldnotfail/2310.v new file mode 100644 index 00000000..8d1a5149 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/2310.v @@ -0,0 +1,17 @@ +(* Dependent higher-order hole in "refine" (simplified version) *) + +Set Implicit Arguments. + +Inductive Nest t := Cons : Nest (prod t t) -> Nest t. + +Definition cast A x y Heq P H := @eq_rect A x P H y Heq. + +Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. + +(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta. + It raises a regular error in 8.3 and almost succeeds with the new + proof engine: there are two solutions to a unification problem + (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either + leave P as subgoal or choose itself one solution *) + +intros. refine (Cons (cast H _ y)). diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v new file mode 100644 index 00000000..02a3c252 --- /dev/null +++ b/test-suite/complexity/Notations.v @@ -0,0 +1,10 @@ +(* Last line should not loop, even in the presence of eta-expansion in the *) +(* printing mechanism *) +(* Expected time < 1.00s *) + +Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at + level 0, y at level 0,format "'[hv' 'bind' x <- y ; '/' z ']'"). + +Definition f (g : (nat -> nat) -> nat) := g (fun x => 0). + +Time Check (fun g => f g). diff --git a/test-suite/complexity/evar_instance.v b/test-suite/complexity/evar_instance.v new file mode 100644 index 00000000..97a66c95 --- /dev/null +++ b/test-suite/complexity/evar_instance.v @@ -0,0 +1,78 @@ +(* Checks behavior of unification with respect to the size of evar instances *) +(* Expected time < 2.00s *) + +(* Note that the exact example chosen is not important as soon as it + involves a few of each part of the unification algorithme (and especially + evar-evar unification and evar-term instantiation) *) + +(* In 8.2, the example was in O(n^3) in the number of section variables; + From current commit it is in O(n^2) *) + +(* For the record: with coqtop.byte on a Dual Core 2: + + Nb of extra T i m e + variables 8.1 8.2 8.3beta current + 800 1.6s 188s 185s 1.6s + 400 0.5s 24s 24s 0.43s + 200 0.17s 3s 3.2s 0.12s + 100 0.06s 0.5s 0.48s 0.04s + 50 0.02s 0.08s 0.08s 0.016s + n 12*a*n^2 a*n^3 a*n^3 8*a*n^2 +*) + +Set Implicit Arguments. +Parameter t:Set->Set. +Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'. +Parameter avl: forall elt : Set, t elt -> Prop. +Parameter bst: forall elt : Set, t elt -> Prop. +Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + avl m -> avl (map f m). +Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + bst m -> bst (map f m). +Record bbst (elt:Set) : Set := + Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}. +Definition t' := bbst. +Section B. + +Variables + a b c d e f g h i j k m n o p q r s u v w x y z + a0 b0 c0 d0 e0 f0 g0 h0 i0 j0 k0 m0 n0 o0 p0 q0 r0 s0 u0 v0 w0 x0 y0 z0 + a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 k1 m1 n1 o1 p1 q1 r1 s1 u1 v1 w1 x1 y1 z1 + a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 k2 m2 n2 o2 p2 q2 r2 s2 u2 v2 w2 x2 y2 z2 + a3 b3 c3 d3 e3 f3 g3 h3 i3 j3 k3 m3 n3 o3 p3 q3 r3 s3 u3 v3 w3 x3 y3 z3 + a4 b4 c4 d4 e4 f4 g4 h4 i4 j4 k4 m4 n4 o4 p4 q4 r4 s4 u4 v4 w4 x4 y4 z4 + a5 b5 c5 d5 e5 f5 g5 h5 i5 j5 k5 m5 n5 o5 p5 q5 r5 s5 u5 v5 w5 x5 y5 z5 + a6 b6 c6 d6 e6 f6 g6 h6 i6 j6 k6 m6 n6 o6 p6 q6 r6 s6 u6 v6 w6 x6 y6 z6 + + a7 b7 c7 d7 e7 f7 g7 h7 i7 j7 k7 m7 n7 o7 p7 q7 r7 s7 u7 v7 w7 x7 y7 z7 + a8 b8 c8 d8 e8 f8 g8 h8 i8 j8 k8 m8 n8 o8 p8 q8 r8 s8 u8 v8 w8 x8 y8 z8 + a9 b9 c9 d9 e9 f9 g9 h9 i9 j9 k9 m9 n9 o9 p9 q9 r9 s9 u9 v9 w9 x9 y9 z9 + aA bA cA dA eA fA gA hA iA jA kA mA nA oA pA qA rA sA uA vA wA xA yA zA + aB bB cB dB eB fB gB hB iB jB kB mB nB oB pB qB rB sB uB vB wB xB yB zB + aC bC cC dC eC fC gC hC iC jC kC mC nC oC pC qC rC sC uC vC wC xC yC zC + aD bD cD dD eD fD gD hD iD jD kD mD nD oD pD qD rD sD uD vD wD xD yD zD + aE bE cE dE eE fE gE hE iE jE kE mE nE oE pE qE rE sE uE vE wE xE yE zE + + aF bF cF dF eF fF gF hF iF jF kF mF nF oF pF qF rF sF uF vF wF xF yF zF + aG bG cG dG eG fG gG hG iG jG kG mG nG oG pG qG rG sG uG vG wG xG yG zG + aH bH cH dH eH fH gH hH iH jH kH mH nH oH pH qH rH sH uH vH wH xH yH zH + aI bI cI dI eI fI gI hI iI jI kI mI nI oI pI qI rI sI uI vI wI xI yI zI + aJ bJ cJ dJ eJ fJ gJ hJ iJ jJ kJ mJ nJ oJ pJ qJ rJ sJ uJ vJ wJ xJ yJ zJ + aK bK cK dK eK fK gK hK iK jK kK mK nK oK pK qK rK sK uK vK wK xK yK zK + aL bL cL dL eL fL gL hL iL jL kL mL nL oL pL qL rL sL uL vL wL xL yL zL + aM bM cM dM eM fM gM hM iM jM kM mM nM oM pM qM rM sM uM vM wM xM yM zM + + aN bN cN dN eN fN gN hN iN jN kN mN nN oN pN qN rN sN uN vN wN xN yN zN + aO bO cO dO eO fO gO hO iO jO kO mO nO oO pO qO rO sO uO vO wO xO yO zO + aP bP cP dP eP fP gP hP iP jP kP mP nP oP pP qP rP sP uP vP wP xP yP zP + aQ bQ cQ dQ eQ fQ gQ hQ iQ jQ kQ mQ nQ oQ pQ qQ rQ sQ uQ vQ wQ xQ yQ zQ + aR bR cR dR eR fR gR hR iR jR kR mR nR oR pR qR rR sR uR vR wR xR yR zR + aS bS cS dS eS fS gS hS iS jS kS mS nS oS pS qS rS sS uS vS wS xS yS zS + aT bT cT dT eT fT gT hT iT jT kT mT nT oT pT qT rT sT uT vT wT xT yT zT + aU bU cU dU eU fU gU hU iU jU kU mU nU oU pU qU rU sU uU vU wU xU yU zU + + : nat . + +Variables elt elt': Set. +Timeout 5 Time Definition map' f (m:t' elt) : t' elt' := + Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v new file mode 100644 index 00000000..ceb7835a --- /dev/null +++ b/test-suite/complexity/guard.v @@ -0,0 +1,30 @@ +(* Examples to check that the guard condition does not evaluate + irrelevant subterms *) +(* Expected time < 1.00s *) +Require Import Bool. + +Fixpoint slow n := + match n with + | 0 => true + | S k => andb (slow k) (slow k) + end. + +Timeout 5 Time Fixpoint F n := + match n with + | 0 => 0 + | S k => + if slow 100 then F k else 0 + end. + +Fixpoint slow2 n := + match n with + | 0 => 0 + | S k => slow2 k + slow2 k + end. + +Timeout 5 Time Fixpoint F' n := + match n with + | 0 => 0 + | S k => + if slow2 100 then F' k else 0 + end. diff --git a/test-suite/complexity/patternmatching.v b/test-suite/complexity/patternmatching.v new file mode 100644 index 00000000..7b628136 --- /dev/null +++ b/test-suite/complexity/patternmatching.v @@ -0,0 +1,8 @@ +(* This example checks the efficiency of pattern-matching compilation on simple cases *) +(* Expected time < 1.00s *) + +Time Definition a400 n := match n with + S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) => x +| _ => 0 +end. + diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index ab57afdb..6945edc8 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -11,7 +11,7 @@ match x with | 0%Z => x | Zpos y' => Zpos (x' + y') | Zneg y' => - match (x' ?= y')%positive Eq with + match (x' ?= y')%positive with | Eq => 0%Z | Lt => Zneg (y' - x') | Gt => Zpos (x' - y') @@ -21,7 +21,7 @@ match x with match y with | 0%Z => x | Zpos y' => - match (x' ?= y')%positive Eq with + match (x' ?= y')%positive with | Eq => 0%Z | Lt => Zpos (y' - x') | Gt => Zneg (x' - y') diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache index 645de69c..297ac255 100644 Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 96e66a0d..a08c5154 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Y -> prod X Y. +Definition B : Prop := let F := prod True in F Prop. (* Aie! *) +Definition p2b (P:Prop) : B := pair True Prop I P. +Definition b2p (b:B) : Prop := match b with pair _ P => P end. +Lemma L1 : forall A : Prop, b2p (p2b A) -> A. +Proof (fun A x => x). +Lemma L2 : forall A : Prop, A -> b2p (p2b A). +Proof (fun A x => x). +Check Hurkens.paradox B p2b b2p L1 L2. + diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index c02661e0..e9fbe969 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* T. -Check (K (forall T : Type, T -> T) K). diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index d5e9ee5e..ea392055 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -3,8 +3,8 @@ (* Undoing arbitrary commands, as first step *) -Theorem a : O=O. -Ltac f x := x. +Theorem a : O=O. (* 2 *) +Ltac f x := x. (* 1 * 3 *) assert True by trivial. trivial. Qed. @@ -79,6 +79,7 @@ Definition q := O. Definition r := O. (* Bug 2082 : Follow the numbers *) +(* Broken due to proof engine rewriting *) Variable A : Prop. Variable B : Prop. diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake new file mode 100644 index 00000000..bbaea7e7 --- /dev/null +++ b/test-suite/ide/undo001.fake @@ -0,0 +1,10 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Simple backtrack by 1 between two global definitions +# +INTERP Definition foo := 0. +INTERP Definition bar := 1. +REWIND 1 +INTERPRAW Check foo. +INTERPRAW Fail Check bar. diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake new file mode 100644 index 00000000..b855b6ea --- /dev/null +++ b/test-suite/ide/undo002.fake @@ -0,0 +1,10 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Simple backtrack by 2 before two global definitions +# +INTERP Definition foo := 0. +INTERP Definition bar := 1. +REWIND 2 +INTERPRAW Fail Check foo. +INTERPRAW Fail Check bar. diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake new file mode 100644 index 00000000..4c72e8dc --- /dev/null +++ b/test-suite/ide/undo003.fake @@ -0,0 +1,8 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Simple backtrack by 0 should be a no-op +# +INTERP Definition foo := 0. +REWIND 0 +INTERPRAW Check foo. diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake new file mode 100644 index 00000000..c2ddfb8c --- /dev/null +++ b/test-suite/ide/undo004.fake @@ -0,0 +1,14 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing arbitrary commands, as first step +# +INTERP Theorem a : O=O. +INTERP Ltac f x := x. +REWIND 1 +# +INTERP Ltac f x := x. +# <\replay> +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake new file mode 100644 index 00000000..525b9f2a --- /dev/null +++ b/test-suite/ide/undo005.fake @@ -0,0 +1,15 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing arbitrary commands, as non-first step +# +INTERP Theorem b : O=O. +INTERP assert True by trivial. +INTERP Ltac g x := x. +# +REWIND 1 +# <\replay> +INTERP Ltac g x := x. +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake new file mode 100644 index 00000000..ed88bef5 --- /dev/null +++ b/test-suite/ide/undo006.fake @@ -0,0 +1,14 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, as first step +# Was bugged in 8.1 +# +INTERP Theorem c : O=O. +INTERP Inductive T : Type := I. +REWIND 1 +# +INTERP Inductive T : Type := I. +# <\replay> +INTERP trivial. +INTERP Qed. diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake new file mode 100644 index 00000000..87c06dbb --- /dev/null +++ b/test-suite/ide/undo007.fake @@ -0,0 +1,17 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, as first step +# new in 8.2 +# +INTERP Theorem d : O=O. +INTERP Definition e := O. +INTERP Definition f := O. +REWIND 1 +# +INTERP Definition f := O. +# <\replay> +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. +INTERPRAW Check e. diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake new file mode 100644 index 00000000..1c46c1e8 --- /dev/null +++ b/test-suite/ide/undo008.fake @@ -0,0 +1,18 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, as non-first step +# new in 8.2 +# +INTERP Theorem h : O=O. +INTERP assert True by trivial. +INTERP Definition i := O. +INTERP Definition j := O. +REWIND 1 +# +INTERP Definition j := O. +# <\replay> +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. +INTERPRAW Check i. diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake new file mode 100644 index 00000000..47c77d23 --- /dev/null +++ b/test-suite/ide/undo009.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, interleaved with proof steps +# new in 8.2 *) +# +INTERP Theorem k : O=O. +INTERP assert True by trivial. +INTERP Definition l := O. +INTERP assert True by trivial. +INTERP Definition m := O. +REWIND 3 +# +INTERP Definition l := O. +INTERP assert True by trivial. +INTERP Definition m := O. +# <\replay> +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake new file mode 100644 index 00000000..4fe9df98 --- /dev/null +++ b/test-suite/ide/undo010.fake @@ -0,0 +1,28 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Undoing declarations, interleaved with proof steps and commands *) +# new in 8.2 *) +# +INTERP Theorem n : O=O. +INTERP assert True by trivial. +INTERP Definition o := O. +INTERP Ltac h x := x. +INTERP assert True by trivial. +INTERP Focus. +INTERP Definition p := O. +REWIND 1 +REWIND 1 +REWIND 1 +REWIND 1 +REWIND 1 +# +INTERP Definition o := O. +INTERP Ltac h x := x. +INTERP assert True by trivial. +INTERP Focus. +INTERP Definition p := O. +# +INTERP assert True by trivial. +INTERP trivial. +INTERP Qed. diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake new file mode 100644 index 00000000..cc85a764 --- /dev/null +++ b/test-suite/ide/undo011.fake @@ -0,0 +1,32 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Bug 2082 +# Broken due to proof engine rewriting +# +INTERP Variable A : Prop. +INTERP Variable B : Prop. +INTERP Axiom OR : A \/ B. +INTERP Lemma MyLemma2 : True. +INTERP proof. +INTERP per cases of (A \/ B) by OR. +INTERP suppose A. +INTERP then (1 = 1). +INTERP then H1 : thesis. +INTERP thus thesis by H1. +INTERP suppose B. +REWIND 1 +# +INTERP suppose B. +# +REWIND 2 +# +INTERP thus thesis by H1. +INTERP suppose B. +# +INTERP then (1 = 1). +INTERP then H2 : thesis. +INTERP thus thesis by H2. +INTERP end cases. +INTERP end proof. +INTERP Qed. diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake new file mode 100644 index 00000000..f9b29ca1 --- /dev/null +++ b/test-suite/ide/undo012.fake @@ -0,0 +1,26 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# First, undoing the whole +# +INTERP Lemma aa : True -> True /\ True. +INTERP intro H. +INTERP split. +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +INTERP Qed. +INTERP apply H. +INTERP Qed. +REWIND 1 +# We should now be just before aa, without opened proofs +INTERPRAW Fail idtac. +INTERPRAW Fail Check aa. +INTERPRAW Fail Check bb. +INTERPRAW Fail Check cc. diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake new file mode 100644 index 00000000..3b1c61e6 --- /dev/null +++ b/test-suite/ide/undo013.fake @@ -0,0 +1,31 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# Second, trigger the full undo of an inner proof +# +INTERP Lemma aa : True -> True /\ True. +INTERP intro H. +INTERP split. +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +INTERP Qed. +INTERP apply H. +REWIND 2 +# We should now be just before "Lemma cc" +# +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +INTERP Qed. +INTERP apply H. +# +INTERP Qed. +INTERPRAW Fail idtac. +INTERPRAW Check (aa,bb,cc). diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake new file mode 100644 index 00000000..5224b504 --- /dev/null +++ b/test-suite/ide/undo014.fake @@ -0,0 +1,26 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# Third, undo inside an inner proof +# +INTERP Lemma aa : True -> True /\ True. +INTERP intro H. +INTERP split. +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +REWIND 1 +# +INTERP destruct H. +# +INTERP Qed. +INTERP apply H. +INTERP Qed. +INTERPRAW Fail idtac. +INTERPRAW Check (aa,bb,cc). diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake new file mode 100644 index 00000000..32e46ec9 --- /dev/null +++ b/test-suite/ide/undo015.fake @@ -0,0 +1,29 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# Fourth, undo from an inner proof to a above proof +# +INTERP Lemma aa : True -> True /\ True. +INTERP intro H. +INTERP split. +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +REWIND 4 +# +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +# +INTERP Qed. +INTERP apply H. +INTERP Qed. +INTERPRAW Fail idtac. +INTERPRAW Check (aa,bb,cc). diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake new file mode 100644 index 00000000..2a6e512c --- /dev/null +++ b/test-suite/ide/undo016.fake @@ -0,0 +1,34 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Test backtracking in presence of nested proofs +# Fifth, undo from an inner proof to a previous inner proof +# +INTERP Lemma aa : True -> True /\ True. +INTERP intro H. +INTERP split. +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +REWIND 6 +# We should be just before "Lemma bb" +# +INTERP Lemma bb : False -> False. +INTERP intro H. +INTERP apply H. +INTERP Qed. +INTERP apply H. +INTERP Lemma cc : False -> True. +INTERP intro H. +INTERP destruct H. +# +INTERP Qed. +INTERP apply H. +INTERP Qed. +INTERPRAW Fail idtac. +INTERPRAW Check (aa,bb,cc). diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake new file mode 100644 index 00000000..232360e9 --- /dev/null +++ b/test-suite/ide/undo017.fake @@ -0,0 +1,13 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# bug #2569 : Undoing inside modules +# +INTERP Module M. +INTERP Definition x := 0. +INTERP End M. +REWIND 1 +# +INTERP End M. +# +INTERPRAW Check M.x. diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake new file mode 100644 index 00000000..ef0945ab --- /dev/null +++ b/test-suite/ide/undo018.fake @@ -0,0 +1,13 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# bug #2569 : Undoing inside section +# +INTERP Section M. +INTERP Definition x := 0. +INTERP End M. +REWIND 1 +# +INTERP End M. +# +INTERPRAW Check x. diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake new file mode 100644 index 00000000..70e70d7e --- /dev/null +++ b/test-suite/ide/undo019.fake @@ -0,0 +1,14 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# bug #2569 : Undoing a focused subproof +# +INTERP Goal True. +INTERP { +INTERP exact I. +INTERP } +REWIND 1 +# +INTERP } +# +INTERP Qed. diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index db52af2f..8b36f44b 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Set := - | niln : listn 0 - | consn : forall n : nat, nat -> listn n -> listn (S n). - -Inductive empty : forall n : nat, listn n -> Prop := - intro_empty : empty 0 niln. - -Parameter - inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l). - -Type - (fun (n : nat) (l : listn n) => - match l in (listn n) return (empty n l \/ ~ empty n l) with - | niln => or_introl (~ empty 0 niln) intro_empty - | consn n O y as b => or_intror (empty (S n) b) (inv_empty n 0 y) - | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) - end). - - -Type - (fun (n : nat) (l : listn n) => - match l in (listn n) return (empty n l \/ ~ empty n l) with - | niln => or_introl (~ empty 0 niln) intro_empty - | consn n O y => or_intror (empty (S n) (consn n 0 y)) (inv_empty n 0 y) - | consn n a y => or_intror (empty (S n) (consn n a y)) (inv_empty n a y) - end). - - - -Type - (fun (n : nat) (l : listn n) => - match l in (listn n) return (empty n l \/ ~ empty n l) with - | niln => or_introl (~ empty 0 niln) intro_empty - | consn O a y as b => or_intror (empty 1 b) (inv_empty 0 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/micromega/csdp.cache b/test-suite/micromega/csdp.cache deleted file mode 100644 index 645de69c..00000000 Binary files a/test-suite/micromega/csdp.cache and /dev/null differ diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v index da54166a..2b388687 100644 --- a/test-suite/misc/berardi_test.v +++ b/test-suite/misc/berardi_test.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop := CA : nat -> TA 0. End SA. +Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA. + +Module Type SA. Inductive TA := CA : nat -> TA. End SA. +Module MA : SA. Inductive TA := CA : bool -> TA. Fail End MA. + +Module Type SA. Inductive TA := CA : nat -> TA. End SA. +Module MA : SA. Inductive TA := CA : bool -> nat -> TA. Fail End MA. + +Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2. +Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2. + +Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3. +Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3. + +Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4. +Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4. + +Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5. +Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5. + +Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6. +Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6. + +Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7. +Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7. + +Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8. +Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8. + +Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9. +Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9. + +Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10. +Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10. + +Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11. +Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11. + +(* Basic mismatches *) +Module Type SB. Inductive TB := CB : nat -> TB. End SB. +Module MB : SB. Module Type TB. End TB. Fail End MB. + +Module Type SC. Module Type TC. End TC. End SC. +Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC. + +Module Type SD. Module TD. End TD. End SD. +Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD. + +Module Type SE. Definition DE := nat. End SE. +Module ME : SE. Definition DE := bool. Fail End ME. + +Module Type SF. Parameter DF : nat. End SF. +Module MF : SF. Definition DF := bool. Fail End MF. + +(* Needs a type constraint in module type *) +Module Type SG. Definition DG := Type. End SG. +Module MG : SG. Definition DG := Type : Type. Fail End MG. + +(* Should work *) +Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7. +Module MA7 : SA7. Inductive TA7 (B:Type):= CA7 : B -> TA7 B. End MA7. + +Module Type SA11. Record TA11 (B:Type):= { CA11 : B }. End SA11. +Module MA11 : SA11. Record TA11 (A:Type):= { CA11 : A }. End MA11. + +Module Type SE. Parameter DE : Type. End SE. +Module ME : SE. Definition DE := Type : Type. End ME. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out new file mode 100644 index 00000000..139f9e99 --- /dev/null +++ b/test-suite/output/Arguments.out @@ -0,0 +1,93 @@ +minus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +The simpl tactic unfolds minus avoiding to expose match constructs +minus is transparent +Expands to: Constant Coq.Init.Peano.minus +minus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +The simpl tactic unfolds minus when applied to 1 argument + avoiding to expose match constructs +minus is transparent +Expands to: Constant Coq.Init.Peano.minus +minus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +The simpl tactic unfolds minus + when the 1st argument evaluates to a constructor and + when applied to 1 argument avoiding to expose match constructs +minus is transparent +Expands to: Constant Coq.Init.Peano.minus +minus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +The simpl tactic unfolds minus + when the 1st and 2nd arguments evaluate to a constructor and + when applied to 2 arguments +minus is transparent +Expands to: Constant Coq.Init.Peano.minus +minus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +The simpl tactic unfolds minus + when the 1st and 2nd arguments evaluate to a constructor +minus is transparent +Expands to: Constant Coq.Init.Peano.minus +pf : +forall D1 C1 : Type, +(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 + +Arguments D2, C2 are implicit +Arguments D1, C1 are implicit and maximally inserted +Argument scopes are [foo_scope type_scope _ _ _ _ _] +The simpl tactic never unfolds pf +pf is transparent +Expands to: Constant Top.pf +fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C + +Arguments A, B, C are implicit and maximally inserted +Argument scopes are [type_scope type_scope type_scope _ _ _] +The simpl tactic unfolds fcomp when applied to 6 arguments +fcomp is transparent +Expands to: Constant Top.fcomp +volatile : nat -> nat + +Argument scope is [nat_scope] +The simpl tactic always unfolds volatile +volatile is transparent +Expands to: Constant Top.volatile +f : T1 -> T2 -> nat -> unit -> nat -> nat + +Argument scopes are [_ _ nat_scope _ nat_scope] +f is transparent +Expands to: Constant Top.S1.S2.f +f : T1 -> T2 -> nat -> unit -> nat -> nat + +Argument scopes are [_ _ nat_scope _ nat_scope] +The simpl tactic unfolds f + when the 3rd, 4th and 5th arguments evaluate to a constructor +f is transparent +Expands to: Constant Top.S1.S2.f +f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +Argument T2 is implicit +Argument scopes are [type_scope _ _ nat_scope _ nat_scope] +The simpl tactic unfolds f + when the 4th, 5th and 6th arguments evaluate to a constructor +f is transparent +Expands to: Constant Top.S1.f +f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +Arguments T1, T2 are implicit +Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] +The simpl tactic unfolds f + when the 5th, 6th and 7th arguments evaluate to a constructor +f is transparent +Expands to: Constant Top.f +f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat + +The simpl tactic unfolds f + when the 5th, 6th and 7th arguments evaluate to a constructor +f is transparent +Expands to: Constant Top.f diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v new file mode 100644 index 00000000..3a94f19a --- /dev/null +++ b/test-suite/output/Arguments.v @@ -0,0 +1,40 @@ +Arguments minus n m : simpl nomatch. +About minus. +Arguments minus n / m : simpl nomatch. +About minus. +Arguments minus !n / m : simpl nomatch. +About minus. +Arguments minus !n !m /. +About minus. +Arguments minus !n !m. +About minus. +Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := + fun x => (f (fst x), g (snd x)). +Delimit Scope foo_scope with F. +Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. +About pf. +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). +Arguments fcomp {_ _ _}%type_scope f g x /. +About fcomp. +Definition volatile := fun x : nat => x. +Arguments volatile /. +About volatile. +Set Implicit Arguments. +Section S1. +Variable T1 : Type. +Section S2. +Variable T2 : Type. +Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat := + match n, m with + | 0,_ => 0 + | S _, 0 => n + | S n', S m' => f x y n' v m' end. +About f. +Global Arguments f x y !n !v !m. +About f. +End S2. +About f. +End S1. +About f. +Arguments f : clear implicits and scopes. +About f. diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 6643c142..756e8ede 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -21,6 +21,11 @@ negb : bool -> bool Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead +Warning: Arguments Scope is deprecated; use Arguments instead a : bool -> bool Expands to: Variable a diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out new file mode 100644 index 00000000..e443115c --- /dev/null +++ b/test-suite/output/Arguments_renaming.out @@ -0,0 +1,108 @@ +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. +@eq_refl + : forall (B : Type) (y : B), y = y +eq_refl + : forall x : nat, x = x +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq_refl: Arguments are renamed to B, y +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments B, y are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument B is implicit +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +eq_refl : forall (A : Type) (x : A), x = x + +Arguments are renamed to B, y +When applied to no arguments: + Arguments B, y are implicit and maximally inserted +When applied to 1 argument: + Argument B is implicit +Argument scopes are [type_scope _] +Expands to: Constructor Coq.Init.Logic.eq_refl +Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x + +For myrefl: Arguments are renamed to C, x, _ +For myrefl: Argument C is implicit and maximally inserted +For myEq: Argument scopes are [type_scope _ _] +For myrefl: Argument scopes are [type_scope _ _] +myrefl : forall (B : Type) (x : A), B -> myEq B x x + +Arguments are renamed to C, x, _ +Argument C is implicit and maximally inserted +Argument scopes are [type_scope _ _] +Expands to: Constructor Top.Test1.myrefl +myplus = +fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S n' => S (myplus T t n' m) + end + : forall T : Type, T -> nat -> nat -> nat + +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +myplus : forall T : Type, T -> nat -> nat -> nat + +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +The simpl tactic unfolds myplus + when the 2nd and 3rd arguments evaluate to a constructor +myplus is transparent +Expands to: Constant Top.Test1.myplus +myplus + : forall Z : Type, Z -> nat -> nat -> nat +Inductive myEq (A B : Type) (x : A) : A -> Prop := + myrefl : B -> myEq A B x x + +For myrefl: Arguments are renamed to A, C, x, _ +For myrefl: Argument C is implicit and maximally inserted +For myEq: Argument scopes are [type_scope type_scope _ _] +For myrefl: Argument scopes are [type_scope type_scope _ _] +myrefl : forall (A B : Type) (x : A), B -> myEq A B x x + +Arguments are renamed to A, C, x, _ +Argument C is implicit and maximally inserted +Argument scopes are [type_scope type_scope _ _] +Expands to: Constructor Top.myrefl +myrefl + : forall (A C : Type) (x : A), C -> myEq A C x x +myplus = +fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S n' => S (myplus T t n' m) + end + : forall T : Type, T -> nat -> nat -> nat + +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +myplus : forall T : Type, T -> nat -> nat -> nat + +Arguments are renamed to Z, t, n, m +Argument Z is implicit and maximally inserted +Argument scopes are [type_scope _ nat_scope nat_scope] +The simpl tactic unfolds myplus + when the 2nd and 3rd arguments evaluate to a constructor +myplus is transparent +Expands to: Constant Top.myplus +myplus + : forall Z : Type, Z -> nat -> nat -> nat +The command has indeed failed with message: +=> Error: All arguments lists must declare the same names. +The command has indeed failed with message: +=> Error: The following arguments are not declared: x. +The command has indeed failed with message: +=> Error: Arguments names must be distinct. +The command has indeed failed with message: +=> Error: Argument z cannot be declared implicit. +The command has indeed failed with message: +=> Error: Extra argument y. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v new file mode 100644 index 00000000..b133e733 --- /dev/null +++ b/test-suite/output/Arguments_renaming.v @@ -0,0 +1,54 @@ +Fail Arguments eq_refl {B y}, [B] y. +Fail Arguments identity T _ _. +Arguments eq_refl A x. +Arguments eq_refl {B y}, [B] y : rename. + +Check @eq_refl. +Check (eq_refl (B := nat)). +Print eq_refl. +About eq_refl. + +Goal 3 = 3. +apply @eq_refl with (B := nat). +Undo. +apply @eq_refl with (y := 3). +Undo. +pose (y := nat). +apply (@eq_refl y) with (y0 := 3). +Qed. + +Section Test1. + +Variable A : Type. + +Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x. + +Global Arguments myrefl {C} x _ : rename. +Print myrefl. +About myrefl. + +Fixpoint myplus T (t : T) (n m : nat) {struct n} := + match n with O => m | S n' => S (myplus T t n' m) end. + +Global Arguments myplus {Z} !t !n m : rename. + +Print myplus. +About myplus. +Check @myplus. + +End Test1. +Print myrefl. +About myrefl. +Check myrefl. + +Print myplus. +About myplus. +Check @myplus. + +Fail Arguments eq_refl {F g}, [H] k. +Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F F}, [F] F. +Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x z y. + + diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out new file mode 100644 index 00000000..f61b7ecf --- /dev/null +++ b/test-suite/output/Errors.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +=> Error: The field t is missing in Top.M. diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v new file mode 100644 index 00000000..75763f3b --- /dev/null +++ b/test-suite/output/Errors.v @@ -0,0 +1,9 @@ +(* Test error messages *) + +(* Test non-regression of bug fixed in r13486 (bad printer for module names) *) + +Module Type S. +Parameter t:Type. +End S. +Module M : S. +Fail End M. diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index ca79ba69..2f756cbb 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1 +1,3 @@ -Existential 1 = ?9 : [n : nat m : nat |- nat] +Existential 1 = ?10 : [q : nat n : nat m : nat |- n = ?9] +Existential 2 = ?9 : [n : nat m : nat |- nat] +Existential 3 = ?7 : [p : nat q := S p : nat n : nat m : nat |- ?9 = m] diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index c69d31f4..a13ae462 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -9,17 +9,4 @@ let fix f (m : nat) : nat := match m with | S m' => f m' end in f 0 : nat -fix even_pos_odd_pos 2 - with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1). - intros. - destruct H. - omega. - - apply odd_pos_even_pos in H. - omega. - - intros. - destruct H. - apply even_pos_odd_pos in H. - omega. - +Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index af5f05f6..8afa50ba 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -25,6 +25,11 @@ Inductive even: Z -> Prop := with odd: Z -> Prop := | odd_succ: forall n, even (n - 1) -> odd n. +(* Check printing of fix *) +Ltac f id1 id2 := fix id1 2 with (id2 n (H:odd n) {struct H} : n >= 1). +Print Ltac f. + +(* Incidentally check use of fix in proofs *) Lemma even_pos_odd_pos: forall n, even n -> n >= 0. Proof. fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). @@ -37,5 +42,6 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1). destruct H. apply even_pos_odd_pos in H. omega. -Show Script. Qed. + + diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index ecfe8505..3b65003c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -11,3 +11,5 @@ map id (1 :: nil) : list nat map id' (1 :: nil) : list nat +map (id'' (A:=nat)) (1 :: nil) + : list nat diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index 4c6f2b5d..7c9b89f9 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -18,6 +18,9 @@ Definition d2 x := d1 (y:=x). Print d2. +Set Strict Implicit. +Unset Implicit Arguments. + (* Check maximal insertion of implicit *) Require Import List. @@ -33,6 +36,18 @@ Check map id (1::nil). Definition id' (A:Type) (x:A) := x. -Implicit Arguments id' [[A]]. +Arguments id' {A} x. Check map id' (1::nil). + +Unset Maximal Implicit Insertion. +Unset Implicit Arguments. + +(* Check explicit insertion of last non-maximal trailing implicit to ensure *) +(* correct arity of partiol applications *) + +Set Implicit Arguments. +Definition id'' (A:Type) (x:A) := x. + +Check map (@id'' nat) (1::nil). + diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 9299e010..55017469 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> sig2 P Q + exist2 : forall x : A, P x -> Q x -> {x | P x & Q x} For sig2: Argument A is implicit For exist2: Argument A is implicit diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 215d9b68..ada524f1 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -2,10 +2,10 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true : nat -Defining 'proj1' as keyword +Identifier 'proj1' now a keyword fun e : nat * nat => proj1 e : nat * nat -> nat -Defining 'decomp' as keyword +Identifier 'decomp' now a keyword decomp (true, true) as t, u in (t, u) : bool * bool !(0 = 0) @@ -28,18 +28,18 @@ forall n n0 : nat, ###(n = n0) : list nat (1; 2, 4) : nat * nat * nat -Defining 'ifzero' as keyword +Identifier 'ifzero' now a keyword ifzero 3 : bool -Defining 'pred' as keyword +Identifier 'pred' now a keyword pred 3 : nat fun n : nat => pred n : nat -> nat fun n : nat => pred n : nat -> nat -Defining 'ifn' as keyword -Defining 'is' as keyword +Identifier 'ifn' now a keyword +Identifier 'is' now a keyword fun x : nat => ifn x is succ n then n else 0 : nat -> nat 1- @@ -80,7 +80,7 @@ Nil : forall A : Type, list A NIL:list nat : list nat -Defining 'I' as keyword +Identifier 'I' now a keyword (false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] @@ -120,3 +120,5 @@ fun x : option Z => match x with | NONE3 => 0 end : option Z -> Z +s + : s diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b8f8f48f..4a2c411e 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -245,3 +245,11 @@ Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. Notation SOME3 := @Some. Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). + +(* Check correct matching of "Type" in notations. Of course the + notation denotes a term that will be reinterpreted with a different + universe than the actual one; but it would be the same anyway + without a notation *) + +Notation s := Type. +Check s. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 6731d505..47741e43 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -10,10 +10,19 @@ end : nat let '(a, _, _) := (2, 3, 4) in a : nat +fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 + : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 : Prop +let a := 0 in +∃ x y : nat, +let b := 1 in +let c := b in +let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d + : Prop ∀ n p : nat, n + p = 0 : Prop +Identifier 'λ' now a keyword λ n p : nat, n + p = 0 : nat -> nat -> Prop λ (A : Type) (n p : A), n = p @@ -22,6 +31,18 @@ let '(a, _, _) := (2, 3, 4) in a : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -Defining 'let'' as keyword -let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +Identifier 'let'' now a keyword +let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat +λ (f : nat -> nat) (x : nat), f(x) + S(x) + : (nat -> nat) -> nat -> nat +Notation plus2 n := (S (S n)) +λ n : list(nat), +match n with +| nil => 2 +| 0 :: _ => 2 +| list1 => 0 +| 1 :: _ :: _ => 2 +| plus2 _ :: _ => 2 +end + : list(nat) -> nat diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 57d8ebbc..e902a3c2 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -25,19 +25,25 @@ Remove Printing Let prod. Check match (0,0,0) with (x,y,z) => x+y+z end. Check let '(a,b,c) := ((2,3),4) in a. +(* Test notation for anonymous functions up to eta-expansion *) + +Check fun P:nat->nat->Prop => fun x:nat => ex (P x). + (* Test notations with binders *) -Notation "∃ x .. y , P":= - (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200). +Notation "∃ x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..)) + (x binder, y binder, at level 200, right associativity). Check (∃ n p, n+p=0). +Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d. + Notation "∀ x .. y , P":= (forall x, .. (forall y, P) ..) (x binder, at level 200, right associativity). Check (∀ n p, n+p=0). -Notation "'λ' x .. y , P":= (fun x, .. (fun y, P) ..) +Notation "'λ' x .. y , P":= (fun x => .. (fun y => P) ..) (y binder, at level 200, right associativity). Check (λ n p, n+p=0). @@ -53,7 +59,19 @@ Notation "'let'' f x .. y := t 'in' u":= (f ident, x closed binder, y closed binder, at level 200, right associativity). -Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2. +Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. + +(* In practice, only the printing rule is used here *) +(* Note: does not work for pattern *) +Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Check fun f x => f x + S x. + +Open Scope list_scope. +Notation list1 := (1::nil)%list. +Notation plus2 n := (S (S n)). +(* plus2 was not correctly printed in the two following tests in 8.3pl1 *) +Print plus2. +Check fun n => match n with list1 => 0 | _ => 2 end. (* This one is not fully satisfactory because binders in the same type are re-factorized and parentheses are needed even for atomic binder diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out index b2a44fb7..b2677b6a 100644 --- a/test-suite/output/NumbersSyntax.out +++ b/test-suite/output/NumbersSyntax.out @@ -13,19 +13,19 @@ I31 = 710436486 : int31 2 - : BigN.t_ + : BigN.t' 1000000000000000000 - : BigN.t_ + : BigN.t' 2 + 2 - : BigN.t_ + : bigN 2 + 2 - : BigN.t_ + : bigN = 4 - : BigN.t_ + : bigN = 37151199385380486 - : BigN.t_ + : bigN = 1267650600228229401496703205376 - : BigN.t_ + : bigN 2 : BigZ.t_ -1000000000000000000 diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out new file mode 100644 index 00000000..40c786ab --- /dev/null +++ b/test-suite/output/PrintInfos.out @@ -0,0 +1,129 @@ +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P + +Argument A is implicit +Argument scopes are [type_scope _ _ _] +Expands to: Constructor Coq.Init.Specif.existT +Inductive sigT (A : Type) (P : A -> Type) : Type := + existT : forall x : A, P x -> sigT P + +For sigT: Argument A is implicit +For existT: Argument A is implicit +For sigT: Argument scopes are [type_scope type_scope] +For existT: Argument scopes are [type_scope _ _ _] +existT : forall (A : Type) (P : A -> Type) (x : A), P x -> sigT P + +Argument A is implicit +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +eq_refl : forall (A : Type) (x : A), x = x + +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit +Argument scopes are [type_scope _] +Expands to: Constructor Coq.Init.Logic.eq_refl +eq_refl : forall (A : Type) (x : A), x = x + +When applied to no arguments: + Arguments A, x are implicit and maximally inserted +When applied to 1 argument: + Argument A is implicit +plus = +fix plus (n m : nat) : nat := match n with + | 0 => m + | S p => S (plus p m) + end + : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +plus : nat -> nat -> nat + +Argument scopes are [nat_scope nat_scope] +plus is transparent +Expands to: Constant Coq.Init.Peano.plus +plus : nat -> nat -> nat + +plus_n_O : forall n : nat, n = n + 0 + +Argument scope is [nat_scope] +plus_n_O is opaque +Expands to: Constant Coq.Init.Peano.plus_n_O +Warning: Implicit Arguments is deprecated; use Arguments instead +Inductive le (n : nat) : nat -> Prop := + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + +For le_S: Argument m is implicit +For le_S: Argument n is implicit and maximally inserted +For le: Argument scopes are [nat_scope nat_scope] +For le_n: Argument scope is [nat_scope] +For le_S: Argument scopes are [nat_scope nat_scope _] +Inductive le (n : nat) : nat -> Prop := + le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m + +For le_S: Argument m is implicit +For le_S: Argument n is implicit and maximally inserted +For le: Argument scopes are [nat_scope nat_scope] +For le_n: Argument scope is [nat_scope] +For le_S: Argument scopes are [nat_scope nat_scope _] +comparison : Set + +Expands to: Inductive Coq.Init.Datatypes.comparison +Inductive comparison : Set := + Eq : comparison | Lt : comparison | Gt : comparison +Warning: Implicit Arguments is deprecated; use Arguments instead +bar : foo + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Expands to: Constant Top.bar +*** [ bar : foo ] + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +bar : foo + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Expands to: Constant Top.bar +*** [ bar : foo ] + +Expanded type for implicit arguments +bar : forall x : nat, x = 0 + +Argument x is implicit and maximally inserted +Module Coq.Init.Peano +Notation existS2 := existT2 +Expands to: Notation Coq.Init.Specif.existS2 +Warning: Implicit Arguments is deprecated; use Arguments instead +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit and maximally inserted +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] +Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x + +For eq: Argument A is implicit and maximally inserted +For eq_refl, when applied to no arguments: + Arguments A, x are implicit and maximally inserted +For eq_refl, when applied to 1 argument: + Argument A is implicit and maximally inserted +For eq: Argument scopes are [type_scope _ _] +For eq_refl: Argument scopes are [type_scope _] diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v new file mode 100644 index 00000000..deeb1f65 --- /dev/null +++ b/test-suite/output/PrintInfos.v @@ -0,0 +1,41 @@ +About existT. +Print existT. +Print Implicit existT. + +Print eq_refl. +About eq_refl. +Print Implicit eq_refl. + +Print plus. +About plus. +Print Implicit plus. + +About plus_n_O. + +Implicit Arguments le_S [[n] m]. +Print le_S. + +Arguments le_S {n} [m] _. (* Test new syntax *) +Print le_S. + +About comparison. +Print comparison. + +Definition foo := forall x, x = 0. +Parameter bar : foo. +Implicit Arguments bar [x]. +About bar. +Print bar. + +Arguments bar [x]. (* Test new syntax *) +About bar. +Print bar. + +About Peano. (* Module *) +About existS2. (* Notation *) + +Implicit Arguments eq_refl [[A] [x]] [[A]]. +Print eq_refl. + +Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *) +Print eq_refl. diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out new file mode 100644 index 00000000..36d643a4 --- /dev/null +++ b/test-suite/output/Record.out @@ -0,0 +1,16 @@ +{| field := 5 |} + : test +{| field := 5 |} + : test +{| field_r := 5 |} + : test_r +build_c 5 + : test_c +build 5 + : test +build 5 + : test +{| field_r := 5 |} + : test_r +build_c 5 + : test_c diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v new file mode 100644 index 00000000..6aa3df98 --- /dev/null +++ b/test-suite/output/Record.v @@ -0,0 +1,21 @@ +Record test := build { field : nat }. +Record test_r := build_r { field_r : nat }. +Record test_c := build_c { field_c : nat }. + +Add Printing Constructor test_c. +Add Printing Record test_r. + +Set Printing Records. + +Check build 5. +Check {| field := 5 |}. + +Check build_r 5. +Check build_c 5. + +Unset Printing Records. + +Check build 5. +Check {| field := 5 |}. +Check build_r 5. +Check build_c 5. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 154d9cdd..5d8f98ed 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,5 +1,7 @@ le_S: forall n m : nat, n <= m -> n <= S m le_n: forall n : nat, n <= n +le_pred: forall n m : nat, n <= m -> pred n <= pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool true: bool xorb: bool -> bool -> bool @@ -14,5 +16,9 @@ plus_Sn_m: forall n m : nat, S n + m = S (n + m) plus_O_n: forall n : nat, 0 + n = n mult_n_Sm: forall n m : nat, n * m + n = n * S m mult_n_O: forall n : nat, 0 = n * 0 +min_r: forall n m : nat, m <= n -> min n m = m +min_l: forall n m : nat, n <= m -> min n m = n +max_r: forall n m : nat, n <= m -> max n m = m +max_l: forall n m : nat, m <= n -> max n m = n eq_add_S: forall n m : nat, S n = S m -> n = m eq_S: forall x y : nat, x = y -> S x = S y diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index c87eaadc..9106a4e3 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -11,16 +11,20 @@ pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat +min: nat -> nat -> nat +max: nat -> nat -> nat length: forall A : Type, list A -> nat S: nat -> nat pred: nat -> nat plus: nat -> nat -> nat mult: nat -> nat -> nat minus: nat -> nat -> nat +min: nat -> nat -> nat +max: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m le_n: forall n : nat, n <= n -eq_refl: forall (A : Type) (x : A), x = x identity_refl: forall (A : Type) (a : A), identity a a +eq_refl: forall (A : Type) (x : A), x = x iff_refl: forall A : Prop, A <-> A -conj: forall A B : Prop, A -> B -> A /\ B pair: forall A B : Type, A -> B -> A * B +conj: forall A B : Prop, A -> B -> A /\ B diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index ac5eedc1..9949658c 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1,6 +1,4 @@ -intro H; split; [ a H | e H ]. - -intros; match goal with - | |- context [if ?X then _ else _] => case X - end; trivial. - +Ltac f H := split; [ a H | e H ] +Ltac g := match goal with + | |- context [if ?X then _ else _] => case X + end diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 8fa91994..a7c497cf 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -3,16 +3,11 @@ Tactic Notation "a" constr(x) := apply x. Tactic Notation "e" constr(x) := exact x. -Lemma test : True -> True /\ True. -intro H; split; [a H|e H]. -Show Script. -Qed. +Ltac f H := split; [a H|e H]. +Print Ltac f. (* Test printing of match context *) (* Used to fail after translator removal (see bug #1070) *) -Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O. -Proof. -intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial. -Show Script. -Qed. +Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end. +Print Ltac g. diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out index f23198b0..1b7a2903 100644 --- a/test-suite/output/ZSyntax.out +++ b/test-suite/output/ZSyntax.out @@ -16,11 +16,11 @@ fun x : positive => (- Zpos x~0)%Z : positive -> Z fun x : positive => (- Zpos x~0 + 0)%Z : positive -> Z -(Z_of_nat 0 + 1)%Z +(Z.of_nat 0 + 1)%Z : Z -(0 + Z_of_nat (0 + 0))%Z +(0 + Z.of_nat (0 + 0))%Z : Z -Z_of_nat 0 = 0%Z +Z.of_nat 0 = 0%Z : Prop -(0 + Z_of_nat 11)%Z +(0 + Z.of_nat 11)%Z : Z diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v index 289a1e3f..d3640cae 100644 --- a/test-suite/output/ZSyntax.v +++ b/test-suite/output/ZSyntax.v @@ -8,10 +8,10 @@ Check (fun x : positive => Zneg (xO x)). Check (fun x : positive => (Zpos (xO x) + 0)%Z). Check (fun x : positive => (- Zpos (xO x))%Z). Check (fun x : positive => (- Zpos (xO x) + 0)%Z). -Check (Z_of_nat 0 + 1)%Z. -Check (0 + Z_of_nat (0 + 0))%Z. -Check (Z_of_nat 0 = 0%Z). +Check (Z.of_nat 0 + 1)%Z. +Check (0 + Z.of_nat (0 + 0))%Z. +Check (Z.of_nat 0 = 0%Z). (* Submitted by Pierre Casteran *) Require Import Arith. -Check (0 + Z_of_nat 11)%Z. +Check (0 + Z.of_nat 11)%Z. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out new file mode 100644 index 00000000..bca3b361 --- /dev/null +++ b/test-suite/output/inference.out @@ -0,0 +1,6 @@ +P = +fun e : option L => match e with + | Some cl => Some cl + | None => None + end + : option L -> option L diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v new file mode 100644 index 00000000..968ea71a --- /dev/null +++ b/test-suite/output/inference.v @@ -0,0 +1,14 @@ +(* Check that types are not uselessly unfolded *) + +(* Check here that P returns something of type "option L" and not + "option (list nat)" *) + +Definition L := list nat. + +Definition P (e:option L) := + match e with + | None => None + | Some cl => Some cl + end. + +Print P. diff --git a/test-suite/output/rewrite-2172.out b/test-suite/output/rewrite-2172.out new file mode 100644 index 00000000..30385072 --- /dev/null +++ b/test-suite/output/rewrite-2172.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +=> Error: Unable to find an instance for the variable E. diff --git a/test-suite/output/rewrite-2172.v b/test-suite/output/rewrite-2172.v new file mode 100644 index 00000000..212b1c12 --- /dev/null +++ b/test-suite/output/rewrite-2172.v @@ -0,0 +1,21 @@ +(* This checks an error message as reported in bug #2172 *) + +Axiom axiom : forall (E F : nat), E = F. +Lemma test : forall (E F : nat), E = F. +Proof. + intros. +(* This used to raise the following non understandable error message: + + Error: Unable to find an instance for the variable x + + The reason this error was that rewrite generated the proof + + "eq_ind ?A ?x ?P ? ?y (axiom ?E ?F)" + + and the equation ?x=?E was solved in the way ?E:=?x leaving ?x + unresolved. A stupid hack for solve this consisted in ordering + meta=meta equations the other way round (with most recent evars + instantiated first - since they are assumed to come first from the + user in rewrite/induction/destruct calls). +*) + Fail rewrite <- axiom. diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index b533db6e..97cf316c 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -79,19 +79,17 @@ Record interp_pair :Type := link: abs = interp repr }. Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) . -proof. -let a:interp_pair,b:interp_pair. -reconsider thesis as (a * b = interp a * interp b). -thus thesis by (link a),(link b). -end proof. +Proof. +intros a b. +change (a * b = interp a * interp b). +rewrite (link a), (link b); reflexivity. Qed. Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b). -proof. -let a:interp_pair,b:interp_pair. -reconsider thesis as ((a -> b) = (interp a -> interp b)). -thus thesis using rewrite (link a);rewrite (link b);reflexivity. -end proof. +Proof. +intros a b. +change ((a -> b) = (interp a -> interp b)). +rewrite (link a), (link b); reflexivity. Qed. Canonical Structure ProdCan (a b:interp_pair) := diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v index 32d85779..a9249086 100644 --- a/test-suite/success/CaseAlias.v +++ b/test-suite/success/CaseAlias.v @@ -1,3 +1,4 @@ +(*********************************************) (* This has been a bug reported by Y. Bertot *) Inductive expr : Set := | b : expr -> expr -> expr @@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr := | x => b x a end. +(*********************************************) +(* Test expansion of aliases *) +(* Originally taken from NMake_gen.v *) + + Local Notation SizePlus n := (S (S (S (S (S (S n)))))). + Local Notation Size := (SizePlus O). + + Parameter zn2z : Type -> Type. + Parameter w0 : Type. + Fixpoint word (w : Type) (n : nat) {struct n} : Type := + match n with + | 0 => w + | S n0 => zn2z (word w n0) + end. + + Definition w1 := zn2z w0. + Definition w2 := zn2z w1. + Definition w3 := zn2z w2. + Definition w4 := zn2z w3. + Definition w5 := zn2z w4. + Definition w6 := zn2z w5. + + Definition dom_t n := match n with + | 0 => w0 + | 1 => w1 + | 2 => w2 + | 3 => w3 + | 4 => w4 + | 5 => w5 + | 6 => w6 + | SizePlus n => word w6 n + end. +Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n). + +(* This used to fail because of a bug in expansion of SizePlus wrongly + reusing n as an alias for the subpattern *) +Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) := + match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S n') as n => plus_t n + | _ as n => + fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S (S m')) as m => plus_t n m + | _ => fun x => x + end + end. + +(* Test (useless) intermediate alias *) +Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) := + match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with + | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n'' + | _ as n => + fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S (S m')) as m => plus_t n m + | _ => fun x => x + end + end. + +(*****************************************************************************) +(* Check that alias expansion behaves consistently from versions to versions *) + +Definition g m := + match pred m with + | 0 => 0 + | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *) + end. + +Goal forall m, g m = match pred m with 0 => 0 | S n => S n end. +intro; reflexivity. +Abort. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index e63972ce..745529bf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -543,7 +543,7 @@ Type 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) + * it has to synthesize the predicate on O (which he can't) *) Type match 0 as n return match n with @@ -611,31 +611,52 @@ Type | Consn n a (Consn m b l) => 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 was deactivated in Cristina's code + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A O with + | Niln as b => b + | Consn n a (Niln as b) => (Niln A) + | Consn n a (Consn m b l) => (Niln A) + end). +*) + +(* This one is (still) failing: too weak unification + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l with + | Niln as b => b + | Consn n a (Niln as b) => (Niln A) + | Consn n a (Consn m b l) => (Niln A) + end). +*) + +(* This one is failing: alias L not chosen of the right type + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A (S 0) with + | 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). *) -(******** 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. + +(******** This example (still) failed + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A (S 0) with + | 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 *) +(* To test treatment of as-patterns in depth *) Type (fun (A : Set) (l : List A) => match l with @@ -1064,7 +1085,7 @@ Type | Consn n a (Consn m b l) => fun _ : nat => n + m end). -(* Alsos tests for multiple _ patterns *) +(* Also tests for multiple _ patterns *) Type (fun (A : Set) (n : nat) (l : Listn A n) => match l in (Listn _ n) return (Listn A n) with @@ -1072,14 +1093,14 @@ Type | Consn _ _ _ as b => b end). -(** Horrible error message! +(** This one was said to raised once an "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 + (fun (A:Set) (n:nat) (l:Listn A n) => + match l with + | Niln as b => b + | Consn _ _ _ as b => b + end). Type match niln in (listn n) return (listn n) with diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 29721843..d3b7cf3f 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := end. End Folding. +(** Testing post-processing of nested dependencies *) + +Check fun x:{x|x=0}*nat+nat => match x with + | inl ((exist 0 eq_refl),0) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + + (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *) + (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) + +Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with + | exist2 (x,y) eq_refl I => None + end. + +Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with + | inl (exist (exist2 (x,y) eq_refl I) I) => None + | _ => Some 0 + end. + (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) @@ -506,3 +540,23 @@ Definition test (s:step E E) := | Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. + +(* Testing regression of bug 2454 ("get" used not be type-checkable when + defined with its type constraint) *) + +Inductive K : nat -> Type := KC : forall (p q:nat), K p. + +Definition get : K O -> nat := fun x => match x with KC p q => q end. + +(* Checking correct order of substitution of realargs *) +(* (was broken from revision 14664 to 14669) *) +(* Example extracted from contrib CoLoR *) + +Inductive EQ : nat -> nat -> Prop := R x y : EQ x y. + +Check fun e t (d1 d2:EQ e t) => + match d1 in EQ e1 t1, d2 in EQ e2 t2 return + (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0 + with + | R _ _, R _ _ => fun _ _ => eq_refl + end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index d5b94ab4..47180ef6 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* fun H => apply H. (* Checks that local names are accepted *) Section A. Remark Refl : forall (A : Set) (x : A), x = x. - Proof. exact refl_equal. Defined. + Proof. exact @refl_equal. Defined. Definition Sym := sym_equal. Let Trans := trans_equal. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 203fbbb7..da5dd5e4 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -54,6 +54,15 @@ Check | Build_B x0 x1 => f x0 x1 end). +(* Check inductive types with local definitions (constructors) *) + +Inductive I1 : Set := C1 (_:I1) (_:=0). + +Check (fun x:I1 => + match x with + | C1 i n => (i,n) + end). + (* Check implicit parameters of inductive types (submitted by Pierre Casteran and also implicit in #338) *) @@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}. Definition F (p:P) := (PA p) -> (PB p). Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F. + +(* Check that test for binders capturing implicit arguments is not stronger + than needed (problem raised by Cedric Auger) *) + +Set Implicit Arguments. +Inductive bool_comp2 (b: bool): bool -> Prop := +| Opp2: forall q, (match b return Prop with + | true => match q return Prop with + true => False | + false => True end + | false => match q return Prop with + true => True | + false => False end end) -> bool_comp2 b q. + +(* This one is still to be made acceptable... + +Set Implicit Arguments. +Inductive I A : A->Prop := C a : (forall A, A) -> I a. + + *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 5091b44c..b068f729 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -73,15 +73,15 @@ Require Import Bvector. Inductive I : nat -> Set := | C1 : I 1 - | C2 : forall k i : nat, vector (I i) k -> I i. + | C2 : forall k i : nat, Vector.t (I i) k -> I i. -Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop := +Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop := SC2 : - forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i), + forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i), SI (C2 v) xi vf. Theorem SUnique : - forall (k : nat) (f : I k) (c : vector nat k) v v', + forall (k : nat) (f : I k) (c : Vector.t nat k) v v', SI f c v -> SI f c v' -> v = v'. Proof. induction 1. @@ -129,3 +129,10 @@ Proof. an inconsistent state that disturbed "inversion" *) intros. inversion H. Abort. + +(* Bug #2314 (simplified): check that errors do not show as anomalies *) + +Goal True -> True. +intro. +Fail inversion H using False. +Fail inversion foo using True_ind. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v index 53bcc63a..df4da431 100644 --- a/test-suite/success/LegacyField.v +++ b/test-suite/success/LegacyField.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match x with R x y => (x,y) end). Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. + +(* Check well-scoping of alpha-renaming of private binders *) +(* see bug #2248 (thanks to Marc Lasson) *) + +Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P). +Check (fun p => {q,r| q + r = p}). + +(* Check that declarations of empty levels are correctly backtracked *) + +Section B. +Notation "*" := 5 (at level 0) : nat_scope. +Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope. +End B. + +(* Should succeed *) +Definition n := 5 * 5. + +(* Check that lonely notations (here FOO) do not modify the visibility + of scoped interpretations (bug #2634 fixed in r14819) *) + +Notation "x ++++ y" := (mult x y) (at level 40). +Notation "x ++++ y" := (plus x y) : A_scope. +Open Scope A_scope. +Notation "'FOO' x" := (S x) (at level 40). +Goal (2 ++++ 3) = 5. +reflexivity. +Abort. diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 518d22e9..d316e4a0 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,51 +1,27 @@ -Require Import Nsatz ZArith Reals List Ring_polynom. +(* compile en user 3m39.915s sur cachalot *) +Require Import Nsatz. (* Example with a generic domain *) -Variable A: Type. -Variable Ad: Domain A. +Section test. -Definition Ari : Ring A:= (@domain_ring A Ad). -Existing Instance Ari. - -Existing Instance ring_setoid. -Existing Instance ring_plus_comp. -Existing Instance ring_mult_comp. -Existing Instance ring_sub_comp. -Existing Instance ring_opp_comp. - -Add Ring Ar: (@ring_ring A (@domain_ring A Ad)). - -Instance zero_ring2 : Zero A := {zero := ring0}. -Instance one_ring2 : One A := {one := ring1}. -Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}. -Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}. -Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}. -Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}. - -Infix "==" := ring_eq (at level 70, no associativity). - -Ltac nsatzA := simpl; unfold Ari; nsatz_domain. - -Goal forall x y:A, x == y -> x+0 == y*1+0. -nsatzA. -Qed. +Context {A:Type}`{Aid:Integral_domain A}. Lemma example3 : forall x y z, x+y+z==0 -> x*y+x*z+y*z==0-> - x*y*z==0 -> x*x*x==0. + x*y*z==0 -> x^3%Z==0. Proof. -Time nsatzA. -Admitted. +Time nsatz. +Qed. Lemma example4 : forall x y z u, x+y+z+u==0 -> x*y+x*z+x*u+y*z+y*u+z*u==0-> x*y*z+x*y*u+x*z*u+y*z*u==0-> - x*y*z*u==0 -> x*x*x*x==0. + x*y*z*u==0 -> x^4%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Lemma example5 : forall x y z u v, @@ -53,15 +29,17 @@ Lemma example5 : forall x y z u v, x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0-> x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0-> x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 -> - x*y*z*u*v==0 -> x*x*x*x*x ==0. + x*y*z*u*v==0 -> x^5%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z. nsatz. Qed. +Require Import Reals. + Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R. nsatz. Qed. @@ -70,85 +48,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R. nsatz. Qed. -Section Examples. - -Delimit Scope PE_scope with PE. -Infix "+" := PEadd : PE_scope. -Infix "*" := PEmul : PE_scope. -Infix "-" := PEsub : PE_scope. -Infix "^" := PEpow : PE_scope. -Notation "[ n ]" := (@PEc Z n) (at level 0). - -Open Scope R_scope. - -Lemma example1 : forall x y, - x+y=0 -> - x*y=0 -> - x^2=0. -Proof. - nsatz. -Qed. - -Lemma example2 : forall x, x^2=0 -> x=0. -Proof. - nsatz. -Qed. - -(* -Notation X := (PEX Z 3). -Notation Y := (PEX Z 2). -Notation Z_ := (PEX Z 1). -*) -Lemma example3b : forall x y z, - x+y+z=0 -> - x*y+x*z+y*z=0-> - x*y*z=0 -> x^3=0. -Proof. -Time nsatz. -Qed. - -(* -Notation X := (PEX Z 4). -Notation Y := (PEX Z 3). -Notation Z_ := (PEX Z 2). -Notation U := (PEX Z 1). -*) -Lemma example4b : forall x y z u, - x+y+z+u=0 -> - x*y+x*z+x*u+y*z+y*u+z*u=0-> - x*y*z+x*y*u+x*z*u+y*z*u=0-> - x*y*z*u=0 -> x^4=0. -Proof. -Time nsatz. -Qed. - -(* -Notation x_ := (PEX Z 5). -Notation y_ := (PEX Z 4). -Notation z_ := (PEX Z 3). -Notation u_ := (PEX Z 2). -Notation v_ := (PEX Z 1). -Notation "x :: y" := (List.cons x y) -(at level 60, right associativity, format "'[hv' x :: '/' y ']'"). -Notation "x :: y" := (List.app x y) -(at level 60, right associativity, format "x :: y"). -*) - -Lemma example5b : forall x y z u v, - x+y+z+u+v=0 -> - x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> - x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> - x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> - x*y*z*u*v=0 -> x^5=0. -Proof. -Time nsatz. -Qed. - -End Examples. +End test. Section Geometry. +(* See the interactive pictures of Laurent Théry + on http://www-sop.inria.fr/marelle/CertiGeo/ + and research paper on + https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr +*) -Open Scope R_scope. +Require Import List. +Require Import Reals. Record point:Type:={ X:R; @@ -170,60 +80,122 @@ Definition equal2(A B:point):= (X A)=(X B) /\ (Y A)=(Y B). Definition equal3(A B:point):= - ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0. + ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0. Definition nequal2(A B:point):= (X A)<>(X B) \/ (Y A)<>(Y B). Definition nequal3(A B:point):= - not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0). + not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0). Definition middle(A B I:point):= - 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B). + 2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B). Definition distance2(A B:point):= - (X B - X A)^2 + (Y B - Y A)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z. (* AB = CD *) Definition samedistance2(A B C D:point):= - (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z. Definition determinant(A O B:point):= (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O). Definition scalarproduct(A O B:point):= (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O). Definition norm2(A O B:point):= - ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2). - - -Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)). -intuition. -Qed. - -Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C). -intuition. + ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z). + +Definition equaldistance(A B C D:point):= + ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z = + ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z. + +Definition equaltangente(A B C D E F:point):= + let s1:= determinant A B C in + let c1:= scalarproduct A B C in + let s2:= determinant D E F in + let c2:= scalarproduct D E F in + s1 * c2 = s2 * c1. + +Ltac cnf2 f := + match f with + | ?A \/ (?B /\ ?C) => + let c1 := cnf2 (A\/B) in + let c2 := cnf2 (A\/C) in constr:(c1/\c2) + | (?B /\ ?C) \/ ?A => + let c1 := cnf2 (B\/A) in + let c2 := cnf2 (C\/A) in constr:(c1/\c2) + | (?A \/ ?B) \/ ?C => + let c1 := cnf2 (B\/C) in cnf2 (A \/ c1) + | _ => f + end +with cnf f := + match f with + | ?A \/ ?B => + let c1 := cnf A in + let c2 := cnf B in + cnf2 (c1 \/ c2) + | ?A /\ ?B => + let c1 := cnf A in + let c2 := cnf B in + constr:(c1 /\ c2) + | _ => f + end. + +Ltac scnf := + match goal with + | |- ?f => let c := cnf f in + assert c;[repeat split| tauto] + end. + +Ltac disj_to_pol f := + match f with + | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p) + | ?a = ?b => constr:(a - b) + end. + +Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y. +nsatz. Qed. -Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d). -intros. -assert ( (a-b = 0) \/ (c-d = 0)). -apply Rmult_integral. -trivial. -destruct H0. -left; nsatz. -right; nsatz. -Qed. +Ltac fastnsatz:= + try trivial; try apply fastnsatz1; try trivial; nsatz. + +Ltac proof_pol_disj := + match goal with + | |- ?g => let p := disj_to_pol g in + let h := fresh "hp" in + assert (h:p = 0); + [idtac| + prod_disj h p] + | _ => idtac + end +with prod_disj h p := + match goal with + | |- ?a = ?b \/ ?g => + match p with + | ?q * ?p1 => + let h0 := fresh "hp" in + let h1 := fresh "hp" in + let h2 := fresh "hp" in + assert (h0:a - b = 0 \/ p1 = 0); + [apply Rmult_integral; exact h| + destruct h0 as [h1|h2]; + [left; fastnsatz| + right; prod_disj h2 p1]] + end + | _ => fastnsatz + end. -Ltac geo_unfold := - unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal; - unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; - unfold middle; unfold samedistance2; - unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2. +(* +Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a. +intros. scnf; proof_pol_disj . +admit.*) -Ltac geo_end := - repeat ( - repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end); - repeat (apply a1 || apply a2 || apply a3); - repeat split). +Ltac geo_unfold := + unfold collinear, parallel, notparallel, orthogonal, + equal2, equal3, nequal2, nequal3, + middle, samedistance2, + determinant, scalarproduct, norm2, distance2, + equaltangente, determinant, scalarproduct, equaldistance. Ltac geo_rewrite_hyps:= repeat (match goal with @@ -231,14 +203,41 @@ Ltac geo_rewrite_hyps:= | h:Y _ = _ |- _ => rewrite h in *; clear h end). +Ltac geo_split_hyps:= + repeat (match goal with + | h:_ /\ _ |- _ => destruct h + end). + Ltac geo_begin:= geo_unfold; intros; geo_rewrite_hyps; - geo_end. + geo_split_hyps; + scnf; proof_pol_disj. (* Examples *) +Lemma medians: forall A B C A1 B1 C1 H:point, + middle B C A1 -> + middle A C B1 -> + middle A B C1 -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ collinear A B C. +Proof. geo_begin. +idtac "Medians". + Time nsatz. +(*Finished transaction in 2. secs (2.69359u,0.s) +*) Qed. + +Lemma Pythagore: forall A B C:point, + orthogonal A B A C -> + distance2 A C + distance2 A B = distance2 B C. +Proof. geo_begin. +idtac "Pythagore". +Time nsatz. +(*Finished transaction in 0. secs (0.354946u,0.s) +*) Qed. Lemma Thales: forall O A B C D:point, collinear O A C -> collinear O B D -> @@ -246,9 +245,268 @@ Lemma Thales: forall O A B C D:point, (distance2 O B * distance2 O C = distance2 O D * distance2 O A /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B) \/ collinear O A B. -repeat geo_begin. +geo_begin. +idtac "Thales". +Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*) +Time nsatz. +Qed. + +Lemma segments_of_chords: forall A B C D M O:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> + collinear C D M -> + (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D) + \/ parallel A B C D. +Proof. +geo_begin. +idtac "segments_of_chords". +Time nsatz. +(*Finished transaction in 3. secs (2.704589u,0.s) +*) Qed. + + +Lemma isoceles: forall A B C:point, + equaltangente A B C B C A -> + distance2 A B = distance2 A C + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed. + +Lemma minh: forall A B C D O E H I:point, + X A = 0 -> Y A = 0 -> Y O = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal A C B D -> + collinear A C E -> + collinear B D E -> + collinear A B H -> + orthogonal E H A B -> + collinear C D I -> + middle C D I -> + collinear H E I + \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z + * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0 + \/ parallel A C B D. +Proof. geo_begin. +idtac "minh". +Time nsatz with radicalmax :=1%N strategy:=1%Z + parameters:=(X O::X B::X C::nil) + variables:= (@nil R). +(*Finished transaction in 13. secs (10.102464u,0.s) +*) +Qed. + +Lemma Pappus: forall A B C A1 B1 C1 P Q S:point, + X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 -> + collinear A1 B1 C1 -> + collinear A B1 P -> collinear A1 B P -> + collinear A C1 Q -> collinear A1 C Q -> + collinear B C1 S -> collinear B1 C S -> + collinear P Q S + \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1) + \/ (X A1 = X C) \/ (X C = X B1) + \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C. +Proof. +geo_begin. +idtac "Pappus". +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) + variables:= (X B + :: X A1 + :: Y A1 + :: X B1 + :: Y B1 + :: X C + :: Y C1 + :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). +(*Finished transaction in 8. secs (7.795815u,0.000999999999999s) +*) +Qed. + +Lemma Simson: forall A B C O D E F G:point, + X A = 0 -> Y A = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal E D B C -> + collinear B C E -> + orthogonal F D A C -> + collinear A C F -> + orthogonal G D A B -> + collinear A B G -> + collinear E F G + \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0 + \/ equal3 B A + \/ equal3 A C \/ (X C - X B)^2%Z = 0 + \/ equal3 B C. +Proof. +geo_begin. +idtac "Simson". +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::Y B::X C::Y C::Y D::nil) + variables:= (@nil R). (* compute -[X Y]. *) +(*Finished transaction in 8. secs (7.550852u,0.s) +*) +Qed. + +Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point, + (* H1 intersection of bisections *) + middle B C A1 -> orthogonal H1 A1 B C -> + middle A C B1 -> orthogonal H1 B1 A C -> + (* H2 intersection of medians *) + collinear A A1 H2 -> collinear B B1 H2 -> + (* H3 intersection of altitudes *) + collinear B C A2 -> orthogonal A A2 B C -> + collinear A C B2 -> orthogonal B B2 A C -> + collinear A A1 H3 -> collinear B B1 H3 -> + collinear H1 H2 H3 + \/ collinear A B C. +Proof. geo_begin. +idtac "threepoints". +Time nsatz. +(*Finished transaction in 7. secs (6.282045u,0.s) +*) Qed. + +Lemma Feuerbach: forall A B C A1 B1 C1 O A2 B2 C2 O2:point, + forall r r2:R, + X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0-> + middle A B C1 -> middle B C A1 -> middle C A B1 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + collinear A B C2 -> orthogonal A B O2 C2 -> + collinear B C A2 -> orthogonal B C O2 A2 -> + collinear A C B2 -> orthogonal A C O2 B2 -> + distance2 O2 A2 = distance2 O2 B2 -> + distance2 O2 A2 = distance2 O2 C2 -> + r^2%Z = distance2 O A1 -> + r2^2%Z = distance2 O2 A2 -> + distance2 O O2 = (r + r2)^2%Z + \/ distance2 O O2 = (r - r2)^2%Z + \/ collinear A B C. +Proof. geo_begin. +idtac "Feuerbach". +Time nsatz. +(*Finished transaction in 21. secs (19.021109u,0.s)*) +Qed. + + + + +Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point, + middle A B C1 -> middle B C A1 -> middle C A B1 -> + orthogonal A B C C2 -> collinear A B C2 -> + orthogonal B C A A2 -> collinear B C A2 -> + orthogonal A C B B2 -> collinear A C B2 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + (distance2 O A2 = distance2 O A1 + /\distance2 O B2 = distance2 O A1 + /\distance2 O C2 = distance2 O A1) + \/ collinear A B C. +Proof. geo_begin. +idtac "Euler_circle 3 goals". +Time nsatz. +(*Finished transaction in 13. secs (11.208296u,0.124981s)*) +Time nsatz. +(*Finished transaction in 10. secs (8.846655u,0.s)*) +Time nsatz. +(*Finished transaction in 11. secs (9.186603u,0.s)*) +Qed. + + + +Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, + X S = 0 -> Y S = 0 -> Y A = 0 -> + collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> + collinear B1 C1 P -> collinear B C P -> + collinear A1 C1 Q -> collinear A C Q -> + collinear A1 B1 R -> collinear A B R -> + collinear P Q R + \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 + \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. +Proof. +geo_begin. +idtac "Desargues". +Time +let lv := rev (X A + :: X B + :: Y B + :: X C + :: Y C + :: Y A1 :: X A1 + :: Y B1 + :: Y C1 + :: X R + :: Y R + :: X Q + :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) +Qed. + +Lemma chords: forall O A B C D M:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> collinear C D M -> + scalarproduct A M B = scalarproduct C M D + \/ parallel A B C D. +Proof. geo_begin. +idtac "chords". + Time nsatz. +(*Finished transaction in 4. secs (3.959398u,0.s)*) +Qed. + +Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> + (distance2 D B) * (distance2 E C) * (distance2 F A) = + (distance2 D C) * (distance2 E A) * (distance2 F B) + \/ collinear A B C. +Proof. geo_begin. +idtac "Ceva". Time nsatz. +(*Finished transaction in 105. secs (104.121171u,0.474928s)*) +Qed. + +Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> + equaltangente A B M M B C -> + equaltangente B C M M C A + \/ equal3 A B. +Proof. geo_begin. +idtac "bissectrices". Time nsatz. +(*Finished transaction in 2. secs (1.937705u,0.s)*) +Qed. + +Lemma bisections: forall A B C A1 B1 C1 H:point, + middle B C A1 -> orthogonal H A1 B C -> + middle A C B1 -> orthogonal H B1 A C -> + middle A B C1 -> + orthogonal H C1 A B + \/ collinear A B C. +Proof. geo_begin. +idtac "bisections". +Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*) +Qed. + +Lemma altitudes: forall A B C A1 B1 C1 H:point, + collinear B C A1 -> orthogonal A A1 B C -> + collinear A C B1 -> orthogonal B B1 A C -> + collinear A B C1 -> orthogonal C C1 A B -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ equal2 A B + \/ collinear A B C. +Proof. geo_begin. +idtac "altitudes". +Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*) +Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*) Qed. Lemma hauteurs:forall A B C A1 B1 C1 H:point, @@ -261,26 +519,16 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, \/ collinear A B C. geo_begin. - -(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*) -(*Finished transaction in 3. secs (2.363641u,0.s)*) -(*Time nsatz_domainR. trop long! *) +idtac "hauteurs". Time let lv := constr:(Y A1 - :: X A1 - :: Y B1 - :: X B1 - :: Y A0 - :: Y B - :: X B - :: X A0 - :: X H - :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in - nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi; - discrR. -(* Finished transaction in 6. secs (5.579152u,0.001s) *) + :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C + :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in +nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) + variables := lv. +(*Finished transaction in 5. secs (4.360337u,0.008999s)*) Qed. + End Geometry. diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v new file mode 100644 index 00000000..67d680ba --- /dev/null +++ b/test-suite/success/PCase.v @@ -0,0 +1,66 @@ + +(** Some tests of patterns containing matchs ending with joker branches. + Cf. the new form of the [constr_pattern] constructor [PCase] + in [pretyping/pattern.ml] *) + +(* A universal match matcher *) + +Ltac kill_match := + match goal with + |- context [ match ?x with _ => _ end ] => destruct x + end. + +(* A match matcher restricted to a given type : nat *) + +Ltac kill_match_nat := + match goal with + |- context [ match ?x in nat with _ => _ end ] => destruct x + end. + +(* Another way to restrict to a given type : give a branch *) + +Ltac kill_match_nat2 := + match goal with + |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x + end. + +(* This should act only on empty match *) + +Ltac kill_match_empty := + match goal with + |- context [ match ?x with end ] => destruct x + end. + +Lemma test1 (b:bool) : if b then True else O=O. +Proof. + Fail kill_match_nat. + Fail kill_match_nat2. + Fail kill_match_empty. + kill_match. exact I. exact eq_refl. +Qed. + +Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + Fail kill_match_empty. + kill_match_nat. exact I. exact eq_refl. +Qed. + +Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + kill_match_nat2. exact I. exact eq_refl. +Qed. + +Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + kill_match. exact I. exact eq_refl. +Qed. + +Lemma test3a (f:False) : match f return Prop with end. +Proof. + kill_match_empty. +Qed. + +Lemma test3b (f:False) : match f return Prop with end. +Proof. + kill_match. +Qed. diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v new file mode 100644 index 00000000..81326580 --- /dev/null +++ b/test-suite/success/PrintSortedUniverses.v @@ -0,0 +1,2 @@ +Require Reals. +Print Sorted Universes. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 81bdbc29..00a13aed 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -1,3 +1,9 @@ +(* Before loading Program, check non-anomaly on missing library Program *) + +Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end. + +(* Then we test Program properly speaking *) + Require Import Arith Program. Require Import ZArith Zwf. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index d4e6a82e..2602c7e3 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -55,13 +55,13 @@ Check (cons 3 (cons 2 nil)). Require Import Bvector. -Print vector. +Print Vector.t. -Check (Vnil nat). +Check (Vector.nil nat). -Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)). +Check (fun (A:Set)(a:A)=> Vector.cons _ a _ (Vector.nil _)). -Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))). +Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))). @@ -315,16 +315,16 @@ Proof. Qed. Definition Vtail_total - (A : Set) (n : nat) (v : vector A n) : vector A (pred n):= -match v in (vector _ n0) return (vector A (pred n0)) with -| Vnil => Vnil A -| Vcons _ n0 v0 => v0 + (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):= +match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with +| Vector.nil => Vector.nil A +| Vector.cons _ n0 v0 => v0 end. -Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n). +Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n). case v. simpl. - exact (Vnil A). + exact (Vector.nil A). simpl. auto. Defined. @@ -543,7 +543,7 @@ Inductive ex_Set (P : Set -> Prop) : Type := Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop := c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p). -Goal (comes_from_the_left _ _ (or_introl True I)). +Goal (comes_from_the_left _ _ (or_introl True I)). split. Qed. @@ -966,37 +966,37 @@ let rec div_aux x y = | Right -> div_aux (minus x y) y) *) -Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A. Proof. intros A v;inversion v. Abort. (* - Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), + Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A. Toplevel input, characters 40281-40287 -> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A. +> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A. > ^^^^^^ Error: In environment A : Set n : nat -v : vector A n +v : Vector.t A n e : n = 0 -The term "Vnil A" has type "vector A 0" while it is expected to have type - "vector A n" +The term "Vnil A" has type "Vector.t A 0" while it is expected to have type + "Vector.t A n" *) Require Import JMeq. -Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), - n= 0 -> JMeq v (Vnil A). +Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), + n= 0 -> JMeq v (Vector.nil A). Proof. destruct v. auto. intro; discriminate. Qed. -Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A. +Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A. Proof. intros a v;apply JMeq_eq. apply vector0_is_vnil_aux. @@ -1004,56 +1004,56 @@ Proof. Qed. -Implicit Arguments Vcons [A n]. -Implicit Arguments Vnil [A]. -Implicit Arguments Vhead [A n]. -Implicit Arguments Vtail [A n]. +Implicit Arguments Vector.cons [A n]. +Implicit Arguments Vector.nil [A]. +Implicit Arguments Vector.hd [A n]. +Implicit Arguments Vector.tl [A n]. -Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n. +Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. destruct n; intro v. - exact Vnil. - exact (Vcons (Vhead v) (Vtail v)). + exact Vector.nil. + exact (Vector.cons (Vector.hd v) (Vector.tl v)). Defined. -Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)). +Eval simpl in (fun (A:Set)(v:Vector.t A 0) => (Vid _ _ v)). -Eval simpl in (fun (A:Set)(v:vector A 0) => v). +Eval simpl in (fun (A:Set)(v:Vector.t A 0) => v). -Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v). +Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v). Proof. destruct v. reflexivity. reflexivity. Defined. -Theorem zero_nil : forall A (v:vector A 0), v = Vnil. +Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil. Proof. intros. - change (Vnil (A:=A)) with (Vid _ 0 v). + change (Vector.nil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined. Theorem decomp : - forall (A : Set) (n : nat) (v : vector A (S n)), - v = Vcons (Vhead v) (Vtail v). + forall (A : Set) (n : nat) (v : Vector.t A (S n)), + v = Vector.cons (Vector.hd v) (Vector.tl v). Proof. intros. - change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v). + change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v). apply Vid_eq. Defined. Definition vector_double_rect : - forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type), - P 0 Vnil Vnil -> - (forall n (v1 v2 : vector A n) a b, P n v1 v2 -> - P (S n) (Vcons a v1) (Vcons b v2)) -> - forall n (v1 v2 : vector A n), P n v1 v2. + forall (A:Set) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type), + P 0 Vector.nil Vector.nil -> + (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 -> + P (S n) (Vector.cons a v1) (Vector.cons b v2)) -> + forall n (v1 v2 : Vector.t A n), P n v1 v2. induction n. intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2). auto. @@ -1063,24 +1063,24 @@ Defined. Require Import Bool. -Definition bitwise_or n v1 v2 : vector bool n := - vector_double_rect bool (fun n v1 v2 => vector bool n) - Vnil - (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2. +Definition bitwise_or n v1 v2 : Vector.t bool n := + vector_double_rect bool (fun n v1 v2 => Vector.t bool n) + Vector.nil + (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2. -Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v} +Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} : option A := match n,v with - _ , Vnil => None - | 0 , Vcons b _ _ => Some b - | S n', Vcons _ p' v' => vector_nth A n' p' v' + _ , Vector.nil => None + | 0 , Vector.cons b _ _ => Some b + | S n', Vector.cons _ p' v' => vector_nth A n' p' v' end. Implicit Arguments vector_nth [A p]. -Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b, +Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, vector_nth i v1 = Some a -> vector_nth i v2 = Some b -> vector_nth i (bitwise_or _ v1 v2) = Some (orb a b). diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v new file mode 100644 index 00000000..dd5aa81d --- /dev/null +++ b/test-suite/success/Scheme.v @@ -0,0 +1,4 @@ +(* This failed in 8.3pl2 *) + +Scheme Induction for eq Sort Prop. +Check eq_ind_dep. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 324d340a..c4e67677 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* ... in hyp" is correctly instantiated by Ltac *) + +Goal (True <-> False) -> True -> False. +intros Heq H. +match goal with [ H : True |- _ ] => apply -> Heq in H end. +Abort. + (* Test coercion below product and on non meta-free terms in with bindings *) (* Cf wishes #1408 from E. Makarov *) @@ -326,13 +333,12 @@ exact (refl_equal 4). Qed. (* From 12612, descent in conjunctions is more powerful *) -(* The following, which was failing badly in bug 1980, is now accepted - (even if somehow surprising) *) +(* The following, which was failing badly in bug 1980, is now + properly rejected, as descend in conjunctions builds an + ill-formed elimination from Prop to Type. *) Goal True. -eapply ex_intro. -instantiate (2:=fun _ :True => True). -instantiate (1:=I). +Fail eapply ex_intro. exact I. Qed. @@ -391,3 +397,21 @@ intro x; apply x. *) + +Section A. + +Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1), + identity (f t11) (f t12). + +Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X), + identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x'). + +Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X, + forall g : Y -> X, + let gf := (fun x : X => g (f x)) : X -> X in + identity (map Y X g (f x) (f x')) (map X X gf x x'). +intros. +apply mapfuncomp. +Abort. + +End A. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v new file mode 100644 index 00000000..9b691e25 --- /dev/null +++ b/test-suite/success/auto.v @@ -0,0 +1,26 @@ +(* Wish #2154 by E. van der Weegen *) + +(* auto was not using f_equal-style lemmas with metavariables occuring + only in the type of an evar of the concl, but not directly in the + concl itself *) + +Parameters + (F: Prop -> Prop) + (G: forall T, (T -> Prop) -> Type) + (L: forall A (P: A -> Prop), G A P -> forall x, F (P x)) + (Q: unit -> Prop). + +Hint Resolve L. + +Goal G unit Q -> F (Q tt). + intro. + auto. +Qed. + +(* Test implicit arguments in "using" clause *) + +Goal forall n:nat, nat * nat. +auto using (pair O). +Undo. +eauto using (pair O). +Qed. diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v new file mode 100644 index 00000000..5e9064f8 --- /dev/null +++ b/test-suite/success/autorewrite.v @@ -0,0 +1,29 @@ +Variable Ack : nat -> nat -> nat. + +Axiom Ack0 : forall m : nat, Ack 0 m = S m. +Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. +Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + +Hint Rewrite Ack0 Ack1 Ack2 : base0. + +Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. +Proof. + intros. + autorewrite with base0 in H using try (apply H; reflexivity). +Qed. + +Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. +Proof. + intros. + autorewrite with base0 in *. + apply H;reflexivity. +Qed. + +(* Check autorewrite does not solve existing evars *) +(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) + +Hint Rewrite <- plus_n_O : base1. +Goal forall y, exists x, y+x = y. +eexists. autorewrite with base1. +Fail reflexivity. + diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewritein.v deleted file mode 100644 index 68f2f7ce..00000000 --- a/test-suite/success/autorewritein.v +++ /dev/null @@ -1,23 +0,0 @@ -Variable Ack : nat -> nat -> nat. - -Axiom Ack0 : forall m : nat, Ack 0 m = S m. -Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. -Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). - -Hint Rewrite Ack0 Ack1 Ack2 : base0. - -Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. -Proof. - intros. - autorewrite with base0 in H using try (apply H; reflexivity). -Qed. - -Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. -Proof. - intros. - autorewrite with base0 in *. - apply H;reflexivity. -Qed. - - - diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v new file mode 100644 index 00000000..1099f3e1 --- /dev/null +++ b/test-suite/success/bullet.v @@ -0,0 +1,5 @@ +Goal True /\ True. +split. +- exact I. +- exact I. +Qed. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 5ac6ce82..c65cf303 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *. change 3 at 1 with (1+2) in H, H|-. change 3 in |- * at 1. *) + +(* Test that pretyping checks allowed elimination sorts *) + +Goal True. +Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x). +Fail change True with + match ex_intro _ True (eq_refl True) with ex_intro x _ => x end. +Abort. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 908b5f77..001beae7 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -81,3 +81,11 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True). Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x. +(* Check that coercions are made visible only when modules are imported *) + +Module A. + Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B. + Fail Check S true. +End A. +Import A. +Fail Check S true. diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v index f6ebacae..05d2c98f 100644 --- a/test-suite/success/conv_pbs.v +++ b/test-suite/success/conv_pbs.v @@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A} (ProofForallL x t (subst_formula (remove_assoc _ x rho) A) (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _))))) end. + + +(* A simple example that raised an uncaught exception at some point *) + +Fail Check fun x => @eq_refl x <: true = true. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 8013e1d3..fc40ea96 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -74,3 +74,22 @@ destruct H. destruct H0. reflexivity. Qed. + +(* These did not work before 8.4 *) + +Goal (exists x, x=0) -> True. +destruct 1 as (_,_); exact I. +Abort. + +Goal (exists x, x=0 /\ True) -> True. +destruct 1 as (_,(_,H)); exact H. +Abort. + +Goal (exists x, x=0 /\ True) -> True. +destruct 1 as (_,(_,x)); exact x. +Abort. + +Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. +intros. +destruct (g _). (* This was failing in at least r14571 *) +Abort. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 1862ad10..a94d8b1d 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* y}. intros x y. - decide equality x y. -Qed. - -Lemma lem3 : forall x y : T, {x = y} + {x <> y}. -intros x y. - decide equality y x. + decide equality. Qed. Lemma lem4 : forall x y : T, {x = y} + {x <> y}. diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v new file mode 100644 index 00000000..08078012 --- /dev/null +++ b/test-suite/success/eta.v @@ -0,0 +1,19 @@ +(* Kernel test (head term is a constant) *) +Check (fun a : S = S => a : S = fun x => S x). + +(* Kernel test (head term is a variable) *) +Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x). + +(* Test type inference (head term is syntactically rigid) *) +Check (fun (a : list = list) => a : list = fun A => _ A). + +(* Test type inference (head term is a variable) *) +(* This one is still to be done... +Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x). +*) + +(* Test tactic unification *) +Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S. +intro H; apply H. +Qed. + diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 6423ad14..2f1ec757 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -238,3 +238,74 @@ eapply f_equal with (* should fail because ill-typed *) end) in H || injection H. Abort. + +(* A legitimate simple eapply that was failing in coq <= 8.3. + Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars + on 30/9/2010 +*) + +Lemma simple_eapply_was_failing : + (forall f:nat->nat, exists g, f = g) -> True. +Proof. + assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto. + intros. + eapply modusponens. + simple eapply H. + (* error message with V8.3 : + Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *) +Abort. + +(* Regression test *) + +Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0. + +(* This example revealed an incorrect evar restriction at some time + around October 2011 *) + +Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a). +intros. +refine ((fun H => conj (proj1 H) (proj2 H)) _). +Abort. + +(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *) +(* r14753 after the restrictions made on detecting Miller's pattern in the *) +(* presence of alias, only the second-order unification procedure was *) +(* able to solve this problem but it was deactivated for 8.4 in r14219 *) + +Definition k0 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) o := + match o with (* note: match introduces an alias! *) + | Some a => e _ (j a) + | None => O + end. + +Definition k1 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a). + +Definition k2 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b). + +(* Other examples about aliases involved in pattern unification *) + +Definition k3 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b). + +Definition k4 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b). + +Definition k5 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b). + +Definition k6 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b). + +Definition k7 + (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b). diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 4fec6e7f..3f8a3bc4 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* I2. +Check C2 eq_refl. + +Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := + | C3 : I3 a (n:=0). + +(* Check global implicit declaration over ref not in section *) + +Section D. Global Arguments eq [A] _ _. End D. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 7626ecc4..234c4223 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (forall y x, ?u = 0) => + assert (forall x y:nat, u = u) + end. + +Goal True. +f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)). +reflexivity. +f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)). +reflexivity. +f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *) +|| exact I. +Qed. + (* Test regular failure when clear/intro breaks soundness of the interpretation of terms in current environment *) @@ -275,3 +298,7 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check that this returns an error and not an anomaly (see r13667) *) + +Fail Local Tactic Notation "myintro" := intro. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 41aa3b3e..fcadd150 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop), P nat 0 -> P nat 0. +intros. +Fail remember nat as X. +Fail remember nat as X in H. (* This line used to succeed in 8.3 *) +Fail remember nat as X in |- *. +Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 3bce52fe..08c406be 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -108,3 +108,24 @@ intros. rewrite (H _). reflexivity. Qed. + +(* Example of rewriting of a degenerated pattern using the right-most + argument of the goal. This is sometimes used in contribs, even if + ad hoc. Here, we have the extra requirement that checking types + needs delta-conversion *) + +Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p). +Definition P := (nat * nat)%type. +Goal forall x:P, x = x. +intros. rewrite s. +Abort. + +(* Test second-order unification and failure of pattern-unification *) + +Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False. +intros. +(* The next line used to succeed between June and November 2011 *) +(* causing ill-typed rewriting *) +Fail rewrite H in H0. +Abort. + diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v new file mode 100644 index 00000000..d9ade314 --- /dev/null +++ b/test-suite/success/searchabout.v @@ -0,0 +1,60 @@ + +(** Test of the different syntaxes of SearchAbout, in particular + with and without the [ ... ] delimiters *) + +SearchAbout plus. +SearchAbout plus mult. +SearchAbout "plus_n". +SearchAbout plus "plus_n". +SearchAbout "*". +SearchAbout "*" "+". + +SearchAbout plus inside Peano. +SearchAbout plus mult inside Peano. +SearchAbout "plus_n" inside Peano. +SearchAbout plus "plus_n" inside Peano. +SearchAbout "*" inside Peano. +SearchAbout "*" "+" inside Peano. + +SearchAbout plus outside Peano Logic. +SearchAbout plus mult outside Peano Logic. +SearchAbout "plus_n" outside Peano Logic. +SearchAbout plus "plus_n" outside Peano Logic. +SearchAbout "*" outside Peano Logic. +SearchAbout "*" "+" outside Peano Logic. + +SearchAbout -"*" "+" outside Logic. +SearchAbout -"*"%nat "+"%nat outside Logic. + +SearchAbout [plus]. +SearchAbout [plus mult]. +SearchAbout ["plus_n"]. +SearchAbout [plus "plus_n"]. +SearchAbout ["*"]. +SearchAbout ["*" "+"]. + +SearchAbout [plus] inside Peano. +SearchAbout [plus mult] inside Peano. +SearchAbout ["plus_n"] inside Peano. +SearchAbout [plus "plus_n"] inside Peano. +SearchAbout ["*"] inside Peano. +SearchAbout ["*" "+"] inside Peano. + +SearchAbout [plus] outside Peano Logic. +SearchAbout [plus mult] outside Peano Logic. +SearchAbout ["plus_n"] outside Peano Logic. +SearchAbout [plus "plus_n"] outside Peano Logic. +SearchAbout ["*"] outside Peano Logic. +SearchAbout ["*" "+"] outside Peano Logic. + +SearchAbout [-"*" "+"] outside Logic. +SearchAbout [-"*"%nat "+"%nat] outside Logic. + + +(** The example in the Reference Manual *) + +Require Import ZArith. + +SearchAbout Zmult Zplus "distr". +SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. +SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 033b3f48..19693d70 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -130,3 +130,38 @@ intros f0 Q H. setoid_rewrite H. tauto. Qed. + +(** Check proper refreshing of the lemma application for multiple + different instances in a single setoid rewrite. *) + +Section mult. + Context (fold : forall {A} {B}, (A -> B) -> A -> B). + Context (add : forall A, A -> A). + Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)). + Context (ab : forall B, A -> B). + Context (anat : forall A, nat -> A). + +Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). +Proof. intros. + setoid_rewrite fold_lemma. + change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)). +Abort. + +End mult. + +(** Current semantics for rewriting with typeclass constraints in the lemma + does not fix the instance at the first unification, use [at], or simply rewrite for + this semantics. *) + +Require Import Arith. + +Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}. +Instance: Foo nat. admit. Defined. +Instance: Foo bool. admit. Defined. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort. + diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v new file mode 100644 index 00000000..d4191b93 --- /dev/null +++ b/test-suite/success/simpl_tuning.v @@ -0,0 +1,149 @@ +(* as it is dynamically inferred by simpl *) +Arguments minus !n / m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end. +Abort. + +(* we avoid exposing a match *) +Arguments minus n m : simpl nomatch. + +Lemma foo x : minus 0 x = 0. +simpl. +match goal with |- (0 = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* we unfold as soon as we have 1 args, but we avoid exposing a match *) +Arguments minus n / m : simpl nomatch. + +Lemma foo : minus 0 = fun x => 0. +simpl. +match goal with |- minus 0 = _ => idtac end. +Abort. +(* This does not work as one may expect. The point is that simpl is implemented + as "strong (whd_simpl_state)" and after unfolding minus you have + (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes + a match, that of course "strong" would reduce away but at that stage + we don't know, and reducing by hand under the lambda is against whd *) + +(* extra tuning for the usual heuristic *) +Arguments minus !n / m : simpl nomatch. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* full control *) +Arguments minus !n !m /. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* omitting /, that being immediately after the last ! is irrelevant *) +Arguments minus !n !m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := + fun x => (f (fst x), g (snd x)). + +Delimit Scope foo_scope with F. +Notation "@@" := nat (only parsing) : foo_scope. +Notation "@@" := (fun x => x) (only parsing). + +Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. + +Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x. +Abort. + +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). + +(* fcomp is unfolded if applied to 6 args *) +Arguments fcomp {A B C}%type f g x /. + +Notation "f \o g" := (fcomp f g) (at level 50). + +Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x). +simpl. +match goal with |- (pf (f \o g) h x = _) => idtac end. +case x; intros x1 x2. +simpl. +match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end. +unfold pf; simpl. +match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. +Abort. + +Definition volatile := fun x : nat => x. +Arguments volatile /. + +Lemma foo : volatile = volatile. +simpl. +match goal with |- (fun _ => _) = _ => idtac end. +Abort. + +Set Implicit Arguments. + +Section S1. + +Variable T1 : Type. + +Section S2. + +Variable T2 : Type. + +Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat := + match n, m with + | 0,_ => 0 + | S _, 0 => n + | S n', S m' => f x y n' v m' end. + +Global Arguments f x y !n !v !m. + +Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S2. + +Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S1. + +Arguments f : clear implicits and scopes. + diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v new file mode 100644 index 00000000..8a607c93 --- /dev/null +++ b/test-suite/success/telescope_canonical.v @@ -0,0 +1,12 @@ +Structure Inner := mkI { is :> Type }. +Structure Outer := mkO { os :> Inner }. + +Canonical Structure natInner := mkI nat. +Canonical Structure natOuter := mkO natInner. + +Definition hidden_nat := nat. + +Axiom P : forall S : Outer, is (os S) -> Prop. + +Lemma foo (n : hidden_nat) : P _ n. +Admitted. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 66c4e080..5649e2f7 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop), (forall f, P (f x)) -> P (x+x). +Proof. +intros x P H; apply H. +Qed. (* Example submitted for Zenon *) @@ -90,12 +96,14 @@ intros. apply H. Qed. +(* Feature deactivated in commit 14189 (see commit log) (* Test instanciation of evars by unification *) Goal (forall x, 0 + x = 0 -> True) -> True. intros; eapply H. rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *) Abort. +*) (* Check handling of identity equation between evars *) (* The example failed to pass until revision 10623 *) @@ -135,4 +143,44 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) -> forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f. Proof. intros. - rewrite H. + rewrite H with (f:=f0). +Abort. + +(* Three tests provided by Dan Grayson as part of a custom patch he + made for a more powerful "destruct" for handling Voevodsky's + Univalent Foundations. The test checks if second-order matching in + tactic unification is able to guess by itself on which dependent + terms to abstract so that the elimination predicate is well-typed *) + +Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) : + identity (fxe x) (fxe x). +Proof. destruct (fxe x). apply identity_refl. Defined. + +(* a harder example *) + +Definition UU := Type . +Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t. +Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0. +Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1. +Proof. intros t. exact t. Defined. + +Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k). +Proof. + destruct k. + apply idpath. +Defined. + +(* an example with two constructors *) + +Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := +| newfoo1 : foo' x0 x0 +| newfoo2 : foo' x0 x0 . +Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} : + foo' x0 x1 -> foo' x0 x1. +Proof. intros t. exact t. Defined. +Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k). +Proof. + destruct k. + apply idpath. + apply idpath. +Defined. diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v new file mode 100644 index 00000000..d7504340 --- /dev/null +++ b/test-suite/success/universes-coercion.v @@ -0,0 +1,22 @@ +(* This example used to emphasize the absence of LEGO-style universe + polymorphism; Matthieu's improvements of typing on 2011/3/11 now + makes (apparently) that Amokrane's automatic eta-expansion in the + coercion mechanism works; this makes its illustration as a "weakness" + of universe polymorphism obsolete (example submitted by Randy Pollack). + + Note that this example is not an evidence that the current + non-kernel eta-expansion behavior is the most expected one. +*) + +Parameter K : forall T : Type, T -> T. +Check (K (forall T : Type, T -> T) K). + +(* + note that the inferred term is + "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))" + which is not eta-equivalent to + "(K (forall T : Type, T -> T) K" + because the eta-expansion of the latter + "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)" + assuming K of type "forall T (* u2 *) : Type, T -> T" +*) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index cc40ae07..3fdcce6f 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*