summaryrefslogtreecommitdiff
path: root/test-suite/failure
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/failure
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/failure')
-rw-r--r--test-suite/failure/circular_subtyping1.v7
-rw-r--r--test-suite/failure/circular_subtyping2.v8
-rw-r--r--test-suite/failure/fixpoint2.v6
-rw-r--r--test-suite/failure/guard.v10
-rw-r--r--test-suite/failure/rewrite_in_hyp2.v8
-rw-r--r--test-suite/failure/subtyping.v21
-rw-r--r--test-suite/failure/subtyping2.v245
-rw-r--r--test-suite/failure/univ_include.v30
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.
+
+