Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

8 files changed, 335 insertions, 0 deletions

diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v
new file mode 100644
index 00000000..0b3a8688
--- /dev/null
+++ b/test-suite/failure/circular_subtyping1.v
@@ -0,0 +1,7 @@
+(* subtyping verification in presence of  pseudo-circularity*)
+Module Type S. End S.
+Module Type T. Declare Module M:S. End T.
+
+Module N:S. End N.
+Module NN <: T. Module M:=N. End NN.
+Module P <: T with Module M:=NN := NN.
diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v
new file mode 100644
index 00000000..3bacdc65
--- /dev/null
+++ b/test-suite/failure/circular_subtyping2.v
@@ -0,0 +1,8 @@
+(*subtyping verification in presence of  pseudo-circularity at functor application *)
+Module Type S. End S.
+Module Type T. Declare Module M:S. End T.
+Module N:S. End N.
+
+Module F (X:S) (Y:T with Module M:=X). End F.
+
+Module G := F N N.
\ No newline at end of file
diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v
new file mode 100644
index 00000000..d2f02ea1
--- /dev/null
+++ b/test-suite/failure/fixpoint2.v
@@ -0,0 +1,6 @@
+(* Check Guard in proofs *)
+
+Goal nat->nat.
+fix f 1.
+intro n; apply f; assumption.
+Guarded.
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
new file mode 100644
index 00000000..46208c29
--- /dev/null
+++ b/test-suite/failure/guard.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Fixpoint F (n:nat) : False := F (match F n with end).
+
diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v
new file mode 100644
index 00000000..a32037a2
--- /dev/null
+++ b/test-suite/failure/rewrite_in_hyp2.v
@@ -0,0 +1,8 @@
+(* Until revision 10221, rewriting in hypotheses of the form 
+   "(fun x => phi(x)) t" with "t" not rewritable used to behave as a
+   beta-normalization tactic instead of raising the expected message
+   "nothing to rewrite" *)
+
+Goal forall b, S b = O -> (fun a => 0 = (S a)) b -> True.
+  intros b H H0.
+  rewrite H in H0.
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
new file mode 100644
index 00000000..35fd2036
--- /dev/null
+++ b/test-suite/failure/subtyping.v
@@ -0,0 +1,21 @@
+(* A variant of bug #1302 that must fail *)
+
+Module Type T.
+
+ Parameter A : Type.
+
+ Inductive L : Prop := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End T.
+
+Module TT : T. 
+
+ Parameter A : Type.
+
+ Inductive L : Type := 
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End TT.
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
new file mode 100644
index 00000000..0a75ae45
--- /dev/null
+++ b/test-suite/failure/subtyping2.v
@@ -0,0 +1,245 @@
+(* Check that no constraints on inductive types disappear at subtyping *)
+
+Module Type S.
+
+Record A0 : Type :=  (* Type_i' *)
+  i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *)
+
+Variable i0' : forall X0 : Type, (X0 -> X0 -> Prop) -> A0.
+
+End S.
+
+Module M.
+
+Record A0 : Type :=  (* Type_i' *)
+  i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *)
+
+Definition i0' := i0 : forall X0 : Type, (X0 -> X0 -> Prop) -> A0.
+
+End M.
+
+(* The rest of this file formalizes Burali-Forti paradox *)
+(* (if the constraint between i0' and A0 is lost, the proof goes through) *)
+
+  Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop :=
+      ACC_intro :
+        forall x : A, (forall y : A, R y x -> ACC A R y) -> ACC A R x.
+
+  Lemma ACC_nonreflexive :
+   forall (A : Type) (R : A -> A -> Prop) (x : A),
+   ACC A R x -> R x x -> False.
+simple induction 1; intros.
+exact (H1 x0 H2 H2).
+Qed.
+
+  Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x.
+
+
+Section Inverse_Image.
+
+  Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B).
+
+  Definition Rof (x y : A) : Prop := R (f x) (f y).
+
+  Remark ACC_lemma :
+   forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x.
+    simple induction 1; intros.
+    constructor; intros.
+    apply (H1 (f y0)); trivial.
+    elim H2 using eq_ind_r; trivial.
+    Qed.
+
+  Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x.
+    intros; apply (ACC_lemma (f x)); trivial.
+    Qed.
+
+  Lemma WF_inverse_image : WF B R -> WF A Rof.
+    red in |- *; intros; apply ACC_inverse_image; auto.
+    Qed.
+
+End Inverse_Image.
+
+Section Burali_Forti_Paradox.
+
+  Definition morphism (A : Type) (R : A -> A -> Prop) 
+    (B : Type) (S : B -> B -> Prop) (f : A -> B) :=
+    forall x y : A, R x y -> S (f x) (f y).
+
+  (* The hypothesis of the paradox:
+     assumes there exists an universal system of notations, i.e:
+      - A type A0
+      - An injection i0 from relations on any type into A0
+      - The proof that i0 is injective modulo morphism 
+   *)
+  Variable A0 : Type.                     (* Type_i *)
+  Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
+  Hypothesis
+    inj :
+      forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+        (R2 : X2 -> X2 -> Prop),
+      i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
+
+  (* Embedding of x in y: x and y are images of 2 well founded relations
+     R1 and R2, the ordinal of R2 being strictly greater than that of R1.
+   *)
+  Record emb (x y : A0) : Prop := 
+    {X1 : Type;
+     R1 : X1 -> X1 -> Prop;
+     eqx : x = i0 X1 R1;
+     X2 : Type;
+     R2 : X2 -> X2 -> Prop;
+     eqy : y = i0 X2 R2;
+     W2 : WF X2 R2;
+     f : X1 -> X2;
+     fmorph : morphism X1 R1 X2 R2 f;
+     maj : X2;
+     majf : forall z : X1, R2 (f z) maj}.
+
+
+  Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z.
+intros.
+case H; intros.
+case H0; intros.
+generalize eqx0; clear eqx0.
+elim eqy using eq_ind_r; intro.
+case (inj _ _ _ _ eqx0); intros.
+exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
+red in |- *; auto.
+Defined.
+
+
+  Lemma ACC_emb :
+   forall (X : Type) (R : X -> X -> Prop) (x : X),
+   ACC X R x ->
+   forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X),
+   morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S).
+simple induction 1; intros.
+constructor; intros.
+case H4; intros.
+elim eqx using eq_ind_r.
+case (inj X2 R2 Y S).
+apply sym_eq; assumption.
+
+intros.
+apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
+ try red in |- *; auto.
+Defined.
+
+  (* The embedding relation is well founded *)
+  Lemma WF_emb : WF A0 emb.
+constructor; intros.
+case H; intros.
+elim eqx using eq_ind_r.
+apply ACC_emb with (X := X2) (R := R2) (x := maj) (f := f); trivial.
+Defined.
+
+
+  (* The following definition enforces Type_j >= Type_i *)
+  Definition Omega : A0 := i0 A0 emb.
+
+
+Section Subsets.
+
+  Variable a : A0.
+
+  (* We define the type of elements of A0 smaller than a w.r.t embedding.
+     The Record is in Type, but it is possible to avoid such structure. *)
+  Record sub : Type :=  {witness : A0; emb_wit : emb witness a}.
+
+  (* F is its image through i0 *)
+  Definition F : A0 := i0 sub (Rof _ _ emb witness).
+
+  (* F is embedded in Omega:
+     - the witness projection is a morphism
+     - a is an upper bound because emb_wit proves that witness is
+       smaller than a.
+   *)
+  Lemma F_emb_Omega : emb F Omega.
+exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
+exact WF_emb.
+
+red in |- *; trivial.
+
+exact emb_wit.
+Defined.
+
+End Subsets.
+
+
+  Definition fsub (a b : A0) (H : emb a b) (x : sub a) : 
+    sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
+
+  (* F is a morphism: a < b => F(a) < F(b)
+      - the morphism from F(a) to F(b) is fsub above
+      - the upper bound is a, which is in F(b) since a < b
+   *)
+  Lemma F_morphism : morphism A0 emb A0 emb F.
+red in |- *; intros.
+exists
+ (sub x)
+   (Rof _ _ emb (witness x))
+   (sub y)
+   (Rof _ _ emb (witness y))
+   (fsub x y H)
+   (Build_sub _ x H); trivial.
+apply WF_inverse_image.
+exact WF_emb.
+
+unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+trivial.
+
+unfold Rof, fsub in |- *; simpl in |- *; intros.
+apply emb_wit.
+Defined.
+
+
+  (* Omega is embedded in itself:
+     - F is a morphism
+     - Omega is an upper bound of the image of F
+   *)
+  Lemma Omega_refl : emb Omega Omega.
+exists A0 emb A0 emb F Omega; trivial.
+exact WF_emb.
+
+exact F_morphism.
+
+exact F_emb_Omega.
+Defined.
+
+  (* The paradox is that Omega cannot be embedded in itself, since
+     the embedding relation is well founded.
+   *)
+  Theorem Burali_Forti : False.
+apply ACC_nonreflexive with A0 emb Omega.
+apply WF_emb.
+
+exact Omega_refl.
+
+Defined.
+
+End Burali_Forti_Paradox.
+
+Import M.
+
+  (* Note: this proof uses a large elimination of A0. *)
+  Lemma inj :
+   forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
+     (R2 : X2 -> X2 -> Prop),
+   i0' X1 R1 = i0' X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
+intros.
+change
+  match i0' X1 R1, i0' X2 R2 with
+  | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
+  end in |- *.
+case H; simpl in |- *.
+exists (fun x : X1 => x).
+red in |- *; trivial.
+Defined.
+
+(* The following command raises 'Error: Universe Inconsistency'.
+   To allow large elimination of A0, i0 must not be a large constructor.
+   Hence, the constraint Type_j' < Type_i' is added, which is incompatible
+   with the constraint j >= i in the paradox.
+*)
+
+  Definition Paradox : False := Burali_Forti A0 i0' inj.
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
new file mode 100644
index 00000000..4be70d88
--- /dev/null
+++ b/test-suite/failure/univ_include.v
@@ -0,0 +1,30 @@
+Definition T := Type.
+Definition U := Type.
+
+Module Type MT. 
+  Parameter t : T.
+End MT. 
+
+Module Type MU.
+  Parameter t : U.
+End MU.
+
+Module F (E : MT).
+  Definition elt :T := E.t.
+End F.
+
+Module G (E : MU).
+  Include F E.
+Print Universes. (* U <= T *)
+End G.
+Print Universes. (* Check if constraint is lost *)
+
+Module Mt.
+  Definition t := T.
+End Mt.
+
+Module P := G Mt. (* should yield Universe inconsistency *)
+(* ... otherwise the following command will show that T has type T! *)
+Eval cbv delta [P.elt Mt.t] in P.elt.
+
+