diff options
author | 2013-05-08 18:01:07 +0200 | |
---|---|---|
committer | 2013-05-08 18:01:07 +0200 | |
commit | 095eac936751bab72e3c6bbdfa3ede51f7198721 (patch) | |
tree | 44cf2859ba6b8486f056efaaf7ee6c2d855f2aae /test-suite/bugs/closed/shouldsucceed | |
parent | 4e6d6dab2ef2de6c1ad7972fc981e55a4fde7ae3 (diff) | |
parent | 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 (diff) |
Merge branch 'experimental/master'
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
42 files changed, 1409 insertions, 13 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index 495a16bc..ee9e2504 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -26,13 +26,13 @@ Program Fixpoint union | t1,Leaf => t1 | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then - if (Z_eq_dec h2 1) + if (Z.eq_dec h2 1) then add v2 s else let (l2', r2') := split v1 u in join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else - if (Z_eq_dec h1 1) + if (Z.eq_dec h1 1) then add v1 s else let (l1', r1') := split v2 u in 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/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 718b0e86..fb2f0ca9 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with | I x => match y with - | I y => if (Z_eq_dec x y) then in_left else in_right + | I y => if (Z.eq_dec x y) then in_left else in_right | S ys => in_right end | S xs => 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/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v index 5627612f..17eeb352 100644 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -1,6 +1,6 @@ Require Import ZArith. -Definition zeq := Z_eq_dec. +Definition zeq := Z.eq_dec. Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A := fun y => if zeq x y then v else s y. 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/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v index 72396d49..d5837619 100644 --- a/test-suite/bugs/closed/shouldsucceed/1935.v +++ b/test-suite/bugs/closed/shouldsucceed/1935.v @@ -13,7 +13,7 @@ Qed. Require Import ZArith. -Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt. +Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt. Lemma f_refl'' : forall n , f'' true n n. Proof. 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..142ada26 100644 --- a/test-suite/bugs/closed/shouldsucceed/2127.v +++ b/test-suite/bugs/closed/shouldsucceed/2127.v @@ -1,11 +1,8 @@ -(* Check that "apply refl_equal" is not exported as an interactive +(* Check that "apply eq_refl" is not exported as an interactive tactic but as a statically globalized one *) (* (this is a simplification of the original bug report) *) Module A. -Hint Rewrite sym_equal using apply refl_equal : foo. +Hint Rewrite eq_sym using apply eq_refl : 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 : <<p, q>> <~> <<q', p'>>) + (commute2 : <<p, q>> <~> <<q'', p''>>), + (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..371bfdc5 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2603.v @@ -0,0 +1,33 @@ +(** Namespace of module vs. namescope of definitions/constructors/... + +As noticed by A. Appel in bug #2603, module names and definition +names used to be in the same namespace. But conflict with names +of constructors (or 2nd mutual inductive...) used to not be checked +enough, leading to stange situations. + +- In 8.3pl3 we introduced checks that forbid uniformly the following + situations. + +- For 8.4 we finally managed to make module names and other names + live in two separate namespace, hence allowing all of the following + situations. +*) + +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. +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. +Module E := K. (* Used to be accepted *) +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/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v new file mode 100644 index 00000000..759cd3dd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2629.v @@ -0,0 +1,22 @@ +Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}. + +Class sepalg (t: Type) {JOIN: Join t} : Type := + SepAlg { + join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z'; + join_assoc: forall {a b c d e}, join a b d -> join d c e -> + {f : t & join b c f /\ join a f e}; + join_com: forall {a b c}, join a b c -> join b a c; + join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2; + + unit_for : t -> t -> Prop := fun e a => join e a a; + join_ex_units: forall a, {e : t & unit_for e a} +}. + +Definition joins {A} `{Join A} (a b : A) : Prop := + exists c, join a b c. + +Lemma join_joins {A} `{sepalg A}: forall {a b c}, + join a b c -> joins a b. +Proof. + firstorder. +Qed. 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/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v new file mode 100644 index 00000000..74c8fa34 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2668.v @@ -0,0 +1,6 @@ +Require Import MSetPositive. +Require Import MSetProperties. + +Module Pos := MSetPositive.PositiveSet. +Module PPPP := MSetProperties.WPropertiesOn(Pos). +Print Module PPPP.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v new file mode 100644 index 00000000..f22a8ccc --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2732.v @@ -0,0 +1,19 @@ +(* Check correct behavior of add_primitive_tactic in TACEXTEND *) + +(* Added also the case of eauto and congruence *) + +Ltac thus H := solve [H]. + +Lemma test: forall n : nat, n <= n. +Proof. + intro. + thus firstorder. + Undo. + thus eauto. +Qed. + +Lemma test2: false = true -> False. +Proof. + intro. + thus congruence. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v new file mode 100644 index 00000000..fd7bd3bd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2733.v @@ -0,0 +1,26 @@ +Definition goodid : forall {A} (x: A), A := fun A x => x. +Definition wrongid : forall A (x: A), A := fun {A} x => x. + +Inductive ty := N | B. + +Inductive alt_list : ty -> ty -> Type := + | nil {k} : alt_list k k + | Ncons {k} : nat -> alt_list B k -> alt_list N k + | Bcons {k} : bool -> alt_list N k -> alt_list B k. + +Definition trullynul k {k'} (l : alt_list k k') := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + +Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> +alt_list t1 t3 := + match l with + | nil _ => fun _ l2 => P l2 + | Ncons _ n l1 => fun _ l2 => Ncons n (app (@P) l1 l2) + | Bcons _ b l1 => fun _ l2 => Bcons b (app (@P) l1 l2) + end. + +Check (fun {t t'} (l: alt_list t t') => + app trullynul (goodid l) (wrongid _ nil)). diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v new file mode 100644 index 00000000..826361be --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2734.v @@ -0,0 +1,15 @@ +Require Import Arith List. +Require Import OrderedTypeEx. + +Module Adr. + Include Nat_as_OT. + Definition nat2t (i: nat) : t := i. +End Adr. + +Inductive expr := Const: Adr.t -> expr. + +Inductive control := Go: expr -> control. + +Definition program := (Adr.t * (control))%type. + +Fail Definition myprog : program := (Adr.nat2t 0, Go (Adr.nat2t 0) ).
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v new file mode 100644 index 00000000..fc580f10 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2750.v @@ -0,0 +1,23 @@ + +Module Type ModWithRecord. + + Record foo : Type := + { A : nat + ; B : nat + }. +End ModWithRecord. + +Module Test_ModWithRecord (M : ModWithRecord). + + Definition test1 : M.foo := + {| M.A := 0 + ; M.B := 2 + |}. + + Module B := M. + + Definition test2 : M.foo := + {| M.A := 0 + ; M.B := 2 + |}. +End Test_ModWithRecord.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v new file mode 100644 index 00000000..08dff992 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2817.v @@ -0,0 +1,9 @@ +(** Occur-check for Meta (up to application of already known instances) *) + +Goal forall (f: nat -> nat -> Prop) (x:bool) + (H: forall (u: nat), f u u -> True) + (H0: forall x0, f (if x then x0 else x0) x0), +False. + +intros. +Fail apply H in H0. (* should fail without exhausting the stack *) diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v new file mode 100644 index 00000000..a948b75e --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2836.v @@ -0,0 +1,39 @@ +(* Check that possible instantiation made during evar materialization + are taken into account and do not raise Not_found *) + +Set Implicit Arguments. + +Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := { + Object :> _ := obj; + + Identity' : forall o, Morphism o o; + Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' +}. + +Section SpecializedCategoryInterface. + Variable obj : Type. + Variable mor : obj -> obj -> Type. + Variable C : @SpecializedCategory obj mor. + + Definition Morphism (s d : C) := mor s d. + Definition Identity (o : C) : Morphism o o := C.(Identity') o. + Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) : +Morphism s d' := C.(Compose') s d d' m m0. +End SpecializedCategoryInterface. + +Section ProductCategory. + Variable objC : Type. + Variable morC : objC -> objC -> Type. + Variable objD : Type. + Variable morD : objD -> objD -> Type. + Variable C : SpecializedCategory morC. + Variable D : SpecializedCategory morD. + +(* Should fail nicely *) +Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d +=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type). +Fail refine {| + Identity' := (fun o => (Identity (fst o), Identity (snd o))); + Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd +m2) (snd m1))) + |}. diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v new file mode 100644 index 00000000..21e92ae2 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2928.v @@ -0,0 +1,11 @@ +Class Equiv A := equiv: A -> A -> Prop. +Infix "=" := equiv : type_scope. + +Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z. + +Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }. + +Class SemiLattice A op `{Equiv A} := + { semilattice_sg :>> SemiGroup A op + ; redundant : Associative op + }. diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v new file mode 100644 index 00000000..15598352 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2983.v @@ -0,0 +1,8 @@ +Module Type ModA. +End ModA. +Module Type ModB(A : ModA). +End ModB. +Module Foo(A : ModA)(B : ModB A). +End Foo. + +Print Module Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v new file mode 100644 index 00000000..ba3acd08 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2995.v @@ -0,0 +1,9 @@ +Module Type Interface. + Parameter error: nat. +End Interface. + +Module Implementation <: Interface. + Definition t := bool. + Definition error: t := false. +Fail End Implementation. +(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v new file mode 100644 index 00000000..27de34ed --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3000.v @@ -0,0 +1,2 @@ +Inductive t (t':Type) : Type := A | B. +Definition d := match t with _ => 1 end. (* used to fail on list_chop *) diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v new file mode 100644 index 00000000..896b1958 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3004.v @@ -0,0 +1,7 @@ +Set Implicit Arguments. +Unset Strict Implicit. +Parameter (M : nat -> Type). +Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2). + +Definition foo (s : list {n : nat & M n}) := + let exT := existT in mp (fun x => projT1 x) s. diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v new file mode 100644 index 00000000..3f3a979a --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/3008.v @@ -0,0 +1,29 @@ +Module Type Intf1. +Parameter T : Type. +Inductive a := A. +End Intf1. + +Module Impl1 <: Intf1. +Definition T := unit. +Inductive a := A. +End Impl1. + +Module Type Intf2 + (Impl1 : Intf1). +Parameter x : Impl1.A=Impl1.A -> Impl1.T. +End Intf2. + +Module Type Intf3 + (Impl1 : Intf1) + (Impl2 : Intf2(Impl1)). +End Intf3. + +Fail Module Toto + (Impl1' : Intf1) + (Impl2 : Intf2(Impl1')) + (Impl3 : Intf3(Impl1)(Impl2)). +(* A UserError is expected here, not an uncaught Not_found *) + +(* NB : the Inductive above and the A=A weren't in the initial test, + they are here only to force an access to the environment + (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file |