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/bugs/closed/shouldsucceed/1962.v | 55 +++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 test-suite/bugs/closed/shouldsucceed/1962.v (limited to 'test-suite/bugs/closed/shouldsucceed/1962.v') 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 -- cgit v1.2.3