From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- test-suite/failure/Case5.v | 2 +- test-suite/failure/Case9.v | 2 +- test-suite/failure/ImportedCoercion.v | 7 +++++++ test-suite/failure/Sections.v | 4 ++++ test-suite/failure/evar1.v | 3 +++ test-suite/failure/evarlemma.v | 3 +++ test-suite/failure/fixpoint3.v | 13 ++++++++++++ test-suite/failure/fixpoint4.v | 19 ++++++++++++++++++ test-suite/failure/guard.v | 2 +- test-suite/failure/inductive3.v | 2 +- test-suite/failure/proofirrelevance.v | 2 +- test-suite/failure/rewrite_in_hyp2.v | 2 +- test-suite/failure/subtyping.v | 6 +++--- test-suite/failure/subtyping2.v | 8 ++++---- test-suite/failure/univ_include.v | 4 ++-- test-suite/failure/universes-buraliforti-redef.v | 8 ++++---- test-suite/failure/universes-buraliforti.v | 8 ++++---- test-suite/failure/universes3.v | 25 ++++++++++++++++++++++++ 18 files changed, 97 insertions(+), 23 deletions(-) create mode 100644 test-suite/failure/ImportedCoercion.v create mode 100644 test-suite/failure/Sections.v create mode 100644 test-suite/failure/evar1.v create mode 100644 test-suite/failure/evarlemma.v create mode 100644 test-suite/failure/fixpoint3.v create mode 100644 test-suite/failure/fixpoint4.v create mode 100644 test-suite/failure/universes3.v (limited to 'test-suite/failure') diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v index 29996fd4..494443f1 100644 --- a/test-suite/failure/Case5.v +++ b/test-suite/failure/Case5.v @@ -1,7 +1,7 @@ Inductive MS : Set := | X : MS -> MS | Y : MS -> MS. - + Type (fun p : MS => match p return nat with | X x => 0 end). diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v index a3b99f63..d63c4940 100644 --- a/test-suite/failure/Case9.v +++ b/test-suite/failure/Case9.v @@ -1,7 +1,7 @@ Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. Type match compare 0 0 return nat with - + (* k 0 (* k=i *) | left _ _ _ => 0 (* k>i *) | right _ _ _ => 0 diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v new file mode 100644 index 00000000..0a69b851 --- /dev/null +++ b/test-suite/failure/ImportedCoercion.v @@ -0,0 +1,7 @@ +(* Test visibility of coercions *) + +Require Import make_local. + +(* Local coercion must not be used *) + +Check (0 = true). diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v new file mode 100644 index 00000000..9b3b35c1 --- /dev/null +++ b/test-suite/failure/Sections.v @@ -0,0 +1,4 @@ +Module A. +Section B. +End A. +End A. diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v new file mode 100644 index 00000000..1a4e42a8 --- /dev/null +++ b/test-suite/failure/evar1.v @@ -0,0 +1,3 @@ +(* This used to succeed by producing an ill-typed term in v8.2 *) + +Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A). diff --git a/test-suite/failure/evarlemma.v b/test-suite/failure/evarlemma.v new file mode 100644 index 00000000..ea753e79 --- /dev/null +++ b/test-suite/failure/evarlemma.v @@ -0,0 +1,3 @@ +(* Check success of inference of evars in the context of lemmas *) + +Lemma foo x : True. diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v new file mode 100644 index 00000000..42f06916 --- /dev/null +++ b/test-suite/failure/fixpoint3.v @@ -0,0 +1,13 @@ +(* Check that arguments of impredicative types are not considered + subterms for the guard condition (an example by Thierry Coquand) *) + +Inductive I : Prop := +| C: (forall P:Prop, P->P) -> I. + +Definition i0 := C (fun _ x => x). + +Definition Paradox : False := + (fix ni i : False := + match i with + | C f => ni (f _ i) + end) i0. diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v new file mode 100644 index 00000000..fd956373 --- /dev/null +++ b/test-suite/failure/fixpoint4.v @@ -0,0 +1,19 @@ +(* Check that arguments of impredicative types are not considered + subterms even through commutative cuts on functional arguments + (example prepared by Bruno) *) + +Inductive IMP : Prop := + CIMP : (forall A:Prop, A->A) -> IMP +| LIMP : (nat->IMP)->IMP. + +Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))). + +Definition Paradox : False := + (fix F y o {struct o} : False := + match y with + | tt => fun f => + match f 0 with + | CIMP h => F y (h _ o) + | _ => F y (f 0) + end + end match o with LIMP f => f | _ => fun _ => o end) tt i0. diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 7e07a905..75e51138 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -18,4 +18,4 @@ Definition f := let h := f in (* h = Rel 4 *) fix F (n:nat) : nat := h F S n. (* here Rel 4 = g *) - + diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v index e5a4e1b6..cf035edf 100644 --- a/test-suite/failure/inductive3.v +++ b/test-suite/failure/inductive3.v @@ -1,4 +1,4 @@ -(* Check that the nested inductive types positivity check avoids recursively +(* Check that the nested inductive types positivity check avoids recursively non uniform parameters (at least if these parameters break positivity) *) Inductive t (A:Type) : Type := c : t (A -> A) -> t A. diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index eedf2612..93e159e8 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,5 +1,5 @@ (* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic + of inductive types), but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v index a32037a2..1533966e 100644 --- a/test-suite/failure/rewrite_in_hyp2.v +++ b/test-suite/failure/rewrite_in_hyp2.v @@ -1,4 +1,4 @@ -(* Until revision 10221, rewriting in hypotheses of the form +(* 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" *) diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v index 35fd2036..127da851 100644 --- a/test-suite/failure/subtyping.v +++ b/test-suite/failure/subtyping.v @@ -4,17 +4,17 @@ Module Type T. Parameter A : Type. - Inductive L : Prop := + Inductive L : Prop := | L0 | L1 : (A -> Prop) -> L. End T. -Module TT : T. +Module TT : T. Parameter A : Type. - Inductive L : Type := + Inductive L : Type := | L0 | L1 : (A -> Prop) -> L. diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v index 0a75ae45..addd3b45 100644 --- a/test-suite/failure/subtyping2.v +++ b/test-suite/failure/subtyping2.v @@ -61,7 +61,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + 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). @@ -69,7 +69,7 @@ Section Burali_Forti_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 + - 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 *) @@ -82,7 +82,7 @@ Section Burali_Forti_Paradox. (* 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 := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -166,7 +166,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + 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) diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v index 4be70d88..56f04f9d 100644 --- a/test-suite/failure/univ_include.v +++ b/test-suite/failure/univ_include.v @@ -1,9 +1,9 @@ Definition T := Type. Definition U := Type. -Module Type MT. +Module Type MT. Parameter t : T. -End MT. +End MT. Module Type MU. Parameter t : U. diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v index 049f97f2..034b7f09 100644 --- a/test-suite/failure/universes-buraliforti-redef.v +++ b/test-suite/failure/universes-buraliforti-redef.v @@ -64,7 +64,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + 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). @@ -72,7 +72,7 @@ Section Burali_Forti_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 + - 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 *) @@ -85,7 +85,7 @@ Section Burali_Forti_Paradox. (* 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 := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -168,7 +168,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + 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) diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index d18d2119..1f96ab34 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -47,7 +47,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + 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). @@ -55,7 +55,7 @@ Section Burali_Forti_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 + - 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 *) @@ -68,7 +68,7 @@ Section Burali_Forti_Paradox. (* 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 := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -152,7 +152,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + 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) diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v new file mode 100644 index 00000000..8fb414d5 --- /dev/null +++ b/test-suite/failure/universes3.v @@ -0,0 +1,25 @@ +(* This example (found by coqchk) checks that an inductive cannot be + polymorphic if its constructors induce upper universe constraints. + Here: I cannot be polymorphic because its type is less than the + type of the argument of impl. *) + +Definition Type1 := Type. +Definition Type3 : Type1 := Type. (* Type3 < Type1 *) +Definition Type4 := Type. +Definition impl (A B:Type3) : Type4 := A->B. (* Type3 <= Type4 *) +Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B). + (* Type(6) <= Type(7) because I contains, via C, elements in B + Type(7) <= Type3 because (I B) is argument of impl + Type(4) <= Type(7) because type of C less than I (see remark below) + + where Type(7) is the auxiliary level used to infer the type of I +*) + +(* We cannot enforce Type1 < Type(6) while we already have + Type(6) <= Type(7) < Type3 < Type1 *) +Definition J := I Type1. + +(* Open question: should the type of an inductive be the max of the + types of the _arguments_ of its constructors (here B and Prop, + after unfolding of impl), or of the max of types of the + constructors itself (here B -> impl Prop (I B)), as done above. *) -- cgit v1.2.3