summaryrefslogtreecommitdiff
path: root/test-suite/bugs
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs')
-rw-r--r--test-suite/bugs/closed/2105.v2
-rw-r--r--test-suite/bugs/closed/shouldfail/2406.v3
-rw-r--r--test-suite/bugs/closed/shouldfail/2586.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1416.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v1
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1834.v174
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1912.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1962.v55
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2127.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2141.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2181.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2304.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2307.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2320.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2342.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2362.v38
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2378.v608
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2388.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2393.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2404.v46
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2456.v53
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2473.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2603.v18
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2613.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2615.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2616.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2640.v17
-rw-r--r--test-suite/bugs/opened/shouldnotfail/2310.v17
28 files changed, 1189 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/2105.v b/test-suite/bugs/closed/2105.v
new file mode 100644
index 00000000..46a416fd
--- /dev/null
+++ b/test-suite/bugs/closed/2105.v
@@ -0,0 +1,2 @@
+
+Definition id (T:Type) := Eval vm_compute in T.
diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v
new file mode 100644
index 00000000..112ea2bb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2406.v
@@ -0,0 +1,3 @@
+(* Check correct handling of unsupported notations *)
+Notation "'’'" := (fun x => 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 : <<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..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)).