diff options
Diffstat (limited to 'test-suite/failure')
70 files changed, 1818 insertions, 0 deletions
diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v new file mode 100644 index 0000000000..6e76d42d24 --- /dev/null +++ b/test-suite/failure/Case1.v @@ -0,0 +1,4 @@ +Fail Type match 0 with + | x => 0 + | O => 1 + end. diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v new file mode 100644 index 0000000000..661d98cd56 --- /dev/null +++ b/test-suite/failure/Case10.v @@ -0,0 +1,3 @@ +Fail Type (fun x : nat => match x return nat with + | S x as b => S b + end). diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v new file mode 100644 index 0000000000..675f79e6e1 --- /dev/null +++ b/test-suite/failure/Case11.v @@ -0,0 +1,3 @@ +Fail Type (fun x : nat => match x return nat with + | S x as b => S b x + end). diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v new file mode 100644 index 0000000000..4a77f139cb --- /dev/null +++ b/test-suite/failure/Case12.v @@ -0,0 +1,8 @@ + +Fail Type + (fun x : nat => + match x return nat with + | S x as b => match x with + | x => x + end + end). diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v new file mode 100644 index 0000000000..5c0aa3e12d --- /dev/null +++ b/test-suite/failure/Case13.v @@ -0,0 +1,7 @@ +Fail Type + (fun x : nat => + match x return nat with + | S x as b => match x with + | x => S b x + end + end). diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v new file mode 100644 index 0000000000..29cae76456 --- /dev/null +++ b/test-suite/failure/Case14.v @@ -0,0 +1,9 @@ +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Definition NIL := Nil nat. +Fail Type match Nil nat return (List nat) with + | NIL => NIL + | _ => NIL + end. diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v new file mode 100644 index 0000000000..ec08e6142f --- /dev/null +++ b/test-suite/failure/Case15.v @@ -0,0 +1,9 @@ +(* Non exhaustive pattern-matching *) + +Fail Check + (fun x => + match x, x with + | O, S (S y) => true + | O, S x => false + | S y, O => true + end). diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v new file mode 100644 index 0000000000..df15a42836 --- /dev/null +++ b/test-suite/failure/Case16.v @@ -0,0 +1,11 @@ +(* Check for redundant clauses *) + +Fail Check + (fun x => + match x, x with + | O, S (S y) => true + | S _, S (S y) => true + | _, S (S x) => false + | S y, O => true + | _, _ => true + end). diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v new file mode 100644 index 0000000000..f8c95b1ecb --- /dev/null +++ b/test-suite/failure/Case2.v @@ -0,0 +1,13 @@ +Inductive IFExpr : Set := + | Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. + +Fail Type + (fun F : IFExpr => + match F return Prop with + | IfE (Var _) H I => True + | IfE _ _ _ => False + | _ => True + end). diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v new file mode 100644 index 0000000000..eaafd41fa8 --- /dev/null +++ b/test-suite/failure/Case3.v @@ -0,0 +1,10 @@ +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Fail Type + (fun l : List nat => + match l return nat with + | Nil nat => 0 + | Cons a l => S a + end). diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v new file mode 100644 index 0000000000..4da7ef0cb3 --- /dev/null +++ b/test-suite/failure/Case4.v @@ -0,0 +1,7 @@ + +Fail Definition Berry (x y z : bool) := + match x, y, z with + | true, false, _ => 0 + | false, _, true => 1 + | _, true, false => 2 + end. diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v new file mode 100644 index 0000000000..70e5b98861 --- /dev/null +++ b/test-suite/failure/Case5.v @@ -0,0 +1,7 @@ +Inductive MS : Set := + | X : MS -> MS + | Y : MS -> MS. + +Fail Type (fun p : MS => match p return nat with + | X x => 0 + end). diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v new file mode 100644 index 0000000000..cb7b7de0d8 --- /dev/null +++ b/test-suite/failure/Case6.v @@ -0,0 +1,8 @@ +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Fail Type (match Nil nat return List nat with + | NIL => NIL + | (CONS _ _) => NIL + end). diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v new file mode 100644 index 0000000000..e1fd7df06b --- /dev/null +++ b/test-suite/failure/Case7.v @@ -0,0 +1,20 @@ +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). + +Definition length1 (n : nat) (l : listn n) := + match l with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => 1 + | _ => 0 + end. + +Fail Type + (fun (n : nat) (l : listn n) => + match n return nat with + | O => 0 + | S n => match l return nat with + | niln => 1 + | l' => length1 (S n) l' + end + end). diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v new file mode 100644 index 0000000000..035629fef5 --- /dev/null +++ b/test-suite/failure/Case8.v @@ -0,0 +1,8 @@ +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Fail Type match Nil nat return nat with + | b => b + | Cons _ _ _ as d => d + end. diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v new file mode 100644 index 0000000000..642f85d7be --- /dev/null +++ b/test-suite/failure/Case9.v @@ -0,0 +1,8 @@ +Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. +Fail Type + match compare 0 0 return nat with + + (* k<i *) | left _ (left _ _) => 0 + (* k=i *) | left _ _ => 0 + (* k>i *) | right _ _ => 0 + end. diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v new file mode 100644 index 0000000000..e865f121e8 --- /dev/null +++ b/test-suite/failure/ClearBody.v @@ -0,0 +1,9 @@ +(* ClearBody must check that removing the body of definition does not + invalidate the well-typabilility of the visible goal *) + +Goal True. +set (n := 0) in *. +set (I := refl_equal 0) in *. +change (n = 0) in (type of I). +Fail clearbody n. +Abort. diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v new file mode 100644 index 0000000000..1cac69f4b3 --- /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 *) + +Fail Check (0 = true). diff --git a/test-suite/failure/Notations.v b/test-suite/failure/Notations.v new file mode 100644 index 0000000000..83459de371 --- /dev/null +++ b/test-suite/failure/Notations.v @@ -0,0 +1,7 @@ +(* Submitted by Roland Zumkeller *) + +Notation "! A" := (forall i:nat, A) (at level 60). + +(* Should fail: no dynamic capture *) +Fail Check ! (i=i). + diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v new file mode 100644 index 0000000000..75cf372b43 --- /dev/null +++ b/test-suite/failure/Reordering.v @@ -0,0 +1,6 @@ +(* Testing that hypothesis order (following a conversion/folding) is checked *) + +Goal forall (A:Set) (x:A) (A':=A), True. +intros. +Fail change ((fun (_:A') => Set) x) in (type of A). +Abort. diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v new file mode 100644 index 0000000000..815fadd8a5 --- /dev/null +++ b/test-suite/failure/Sections.v @@ -0,0 +1,6 @@ +Module A. +Section B. +Fail End A. +(*End A.*) +End B. +End A. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v new file mode 100644 index 0000000000..c10cb0b869 --- /dev/null +++ b/test-suite/failure/Tauto.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(**** Tactics Tauto and Intuition ****) + +(**** Tauto: + Tactic for automating proof in Intuionnistic Propositional Calculus, based on + the contraction-free LJT of Dickhoff ****) + +(**** Intuition: + Simplifications of goals, based on LJT calcul ****) + +(* Fails because Tauto does not perform any Apply *) +Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y. +Proof. + Fail tauto. +Abort. diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v new file mode 100644 index 0000000000..cc31c7ae6b --- /dev/null +++ b/test-suite/failure/Uminus.v @@ -0,0 +1,21 @@ +(* Check that the encoding of system U- fails *) + +Require Hurkens. + +Inductive prop : Prop := down : Prop -> prop. + +(* Coq should reject the following access of a Prop buried inside + a prop. *) + +Fail Definition up (p:prop) : Prop := let (A) := p in A. + +(* Otherwise, we would have a proof of False via Hurkens' paradox *) + +Fail Definition paradox : False := + Hurkens.NoRetractFromSmallPropositionToProp.paradox + prop + down + up + (fun (A:Prop) (x:up (down A)) => (x:A)) + (fun (A:Prop) (x:A) => (x:up (down A))) + False. diff --git a/test-suite/failure/autorewritein.v b/test-suite/failure/autorewritein.v new file mode 100644 index 0000000000..b734d85933 --- /dev/null +++ b/test-suite/failure/autorewritein.v @@ -0,0 +1,13 @@ +Variable Ack : nat -> nat -> nat. + +Axiom Ack0 : forall m : nat, Ack 0 m = S m. +Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. +Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + +Hint Rewrite Ack0 Ack1 Ack2 : base0. + +Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H -> False. +Proof. + intros. + Fail autorewrite with base0 in * using try (apply H1;reflexivity). +Abort. diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v new file mode 100644 index 0000000000..ec08e6142f --- /dev/null +++ b/test-suite/failure/cases.v @@ -0,0 +1,9 @@ +(* Non exhaustive pattern-matching *) + +Fail Check + (fun x => + match x, x with + | O, S (S y) => true + | O, S x => false + | S y, O => true + end). diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v new file mode 100644 index 0000000000..0ef4b417a5 --- /dev/null +++ b/test-suite/failure/check.v @@ -0,0 +1,3 @@ +Arguments eq [A]. + +Fail Check (bool = true). diff --git a/test-suite/failure/circular_subtyping.v b/test-suite/failure/circular_subtyping.v new file mode 100644 index 0000000000..9eb7e3bc20 --- /dev/null +++ b/test-suite/failure/circular_subtyping.v @@ -0,0 +1,10 @@ +(* 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. + +Fail Module P <: T with Module M:=NN := NN. + +Module F (X:S) (Y:T with Module M:=X). End F. +Fail Module G := F N N. diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v new file mode 100644 index 0000000000..89299110be --- /dev/null +++ b/test-suite/failure/clash_cons.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* Teste la verification d'unicite des noms de constr *) + + +Inductive X : Set := + cons : X. + +Fail Inductive Y : Set := + cons : Y. diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v new file mode 100644 index 0000000000..1abec329c4 --- /dev/null +++ b/test-suite/failure/clashes.v @@ -0,0 +1,10 @@ +(* Submitted by David Nowak *) + +(* Simpler to forbid the definition of n as a global than to write it + S.n to keep n accessible... *) + +Section S. +Variable n : nat. +Fail Inductive P : Set := + n : P. +End S. diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v new file mode 100644 index 0000000000..d193dc484f --- /dev/null +++ b/test-suite/failure/cofixpoint.v @@ -0,0 +1,15 @@ +(* A bug in the guard checking of nested cofixpoints. *) +(* Posted by Maxime Dénès on coqdev (Apr 9, 2014). *) + +CoInductive CoFalse := . + +CoInductive CoTrue := I. + +Fail CoFixpoint loop : CoFalse := + (cofix f := loop with g := loop for f). + +Fail CoFixpoint loop : CoFalse := + (cofix f := I with g := loop for g). + +Fail CoFixpoint loop : CoFalse := + (cofix f := loop with g := I for f). diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v new file mode 100644 index 0000000000..79ea5ede47 --- /dev/null +++ b/test-suite/failure/coqbugs0266.v @@ -0,0 +1,9 @@ +(* It is forbidden to erase a variable (or a local def) that is used in + the current goal. *) +Section S. +Let a := 0. +Definition b := a. +Goal b = b. +Fail clear a. +Abort. +End S. diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v new file mode 100644 index 0000000000..2b6fe76545 --- /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 *) + +Fail Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A). diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v new file mode 100644 index 0000000000..82697bf41e --- /dev/null +++ b/test-suite/failure/evarclear1.v @@ -0,0 +1,10 @@ +Set Printing Existential Instances. +Set Printing All. +Goal forall y, let z := S y in exists x, x = 0. +intros. +eexists. +unfold z. +clear y z. +(* should fail because the evar should no longer be allowed to depend on z *) +Fail instantiate (1:=z). +Abort. diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v new file mode 100644 index 0000000000..45eeef6aa7 --- /dev/null +++ b/test-suite/failure/evarclear2.v @@ -0,0 +1,10 @@ +Set Printing Existential Instances. +Set Printing All. +Goal let y:=0 in exists x:y=y, x = x. +intros. +eexists. +rename y into z. +unfold z at 1 2. +(* should fail because the evar type depends on z *) +Fail clear z. +Abort. diff --git a/test-suite/failure/evarlemma.v b/test-suite/failure/evarlemma.v new file mode 100644 index 0000000000..ae40774c95 --- /dev/null +++ b/test-suite/failure/evarlemma.v @@ -0,0 +1,3 @@ +(* Check success of inference of evars in the context of lemmas *) + +Fail Lemma foo x : True. diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v new file mode 100644 index 0000000000..eb3d94526c --- /dev/null +++ b/test-suite/failure/fixpoint1.v @@ -0,0 +1,12 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +Fail Fixpoint PreParadox (u : unit) : False := PreParadox u. +(*Definition Paradox := PreParadox tt.*) + diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v new file mode 100644 index 0000000000..2d2d6a02cd --- /dev/null +++ b/test-suite/failure/fixpoint2.v @@ -0,0 +1,7 @@ +(* Check Guard in proofs *) + +Goal nat->nat. +fix f 1. +intro n; apply f; assumption. +Fail Guarded. +Abort. diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v new file mode 100644 index 0000000000..7d1d3ee692 --- /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). + +Fail 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 0000000000..bf6133f1c9 --- /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))). + +Fail 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/fixpointeta.v b/test-suite/failure/fixpointeta.v new file mode 100644 index 0000000000..9af719322f --- /dev/null +++ b/test-suite/failure/fixpointeta.v @@ -0,0 +1,70 @@ + +Set Primitive Projections. + +Record R := C { p : nat }. +(* R is defined +p is defined *) + +Unset Primitive Projections. +Record R' := C' { p' : nat }. + + + +Fail Definition f := fix f (x : R) : nat := p x. +(** Not allowed to make fixpoint defs on (non-recursive) records + having eta *) + +Fail Definition f := fix f (x : R') : nat := p' x. +(** Even without eta (R' is not primitive here), as long as they're + found to be BiFinite (non-recursive), we disallow it *) + +(* + +(* Subject reduction failure example, if we allowed fixpoints *) + +Set Primitive Projections. + +Record R := C { p : nat }. + +Definition f := fix f (x : R) : nat := p x. + +(* eta rule for R *) +Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x + := v. + +Definition goal := forall x, f x = p x. + +(* when we compute the Rtr away typechecking will fail *) +Definition thing : goal := fun x => +(Rtr (fun x => f x = p x) x (eq_refl _)). + +Definition thing' := Eval compute in thing. + +Fail Check (thing = thing'). +(* +The command has indeed failed with message: +The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)" +and "f x = p x"). +*) + +Definition thing_refl := eq_refl thing. + +Fail Definition thing_refl' := Eval compute in thing_refl. +(* +The command has indeed failed with message: +Illegal application: +The term "@eq_refl" of type "forall (A : Type) (x : A), x = x" +cannot be applied to the terms + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop" + "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +which should be coercible to + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)". + *) + +Definition more_refls : thing_refl = thing_refl. +Proof. + compute. reflexivity. +Fail Defined. Abort. + *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v new file mode 100644 index 0000000000..2a5ad7789c --- /dev/null +++ b/test-suite/failure/guard.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +(* +Fixpoint F (n:nat) : False := F (match F n with end). +*) +(* de Bruijn mix-up *) +(* If accepted, Eval compute in f 0. loops *) +Fail Definition f := + let f (f1 f2:nat->nat) := f1 in + let _ := 0 in + let _ := 0 in + let g (f1 f2:nat->nat) := f2 in + 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/guard_cofix.v b/test-suite/failure/guard_cofix.v new file mode 100644 index 0000000000..3ae8770546 --- /dev/null +++ b/test-suite/failure/guard_cofix.v @@ -0,0 +1,43 @@ +(* This script shows, in two different ways, the inconsistency of the +propositional extensionality axiom with the guard condition for cofixpoints. It +is the dual of the problem on fixpoints (cf subterm.v, subterm2.v, +subterm3.v). Posted on Coq-club by Maxime Dénès (02/26/2014). *) + +(* First example *) + +CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse. + +CoInductive Pandora : Prop := C : CoFalse -> Pandora. + +Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q. + +Lemma foo : Pandora = CoFalse. +apply prop_ext. +constructor. +intro x; destruct x; assumption. +exact C. +Qed. + +Fail CoFixpoint loop : CoFalse := +match foo in (_ = T) return T with eq_refl => C loop end. + +Fail Definition ff : False := match loop with CF _ t => t end. + +(* Second example *) + +Inductive omega : Prop := Omega : omega -> omega. + +Lemma H : omega = CoFalse. +Proof. +apply prop_ext; constructor. + induction 1; assumption. +destruct 1; destruct H0. +Qed. + +Fail CoFixpoint loop' : CoFalse := + match H in _ = T return T with + eq_refl => + Omega match eq_sym H in _ = T return T with eq_refl => loop' end + end. + +Fail Definition ff' : False := match loop' with CF _ t => t end. diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v new file mode 100644 index 0000000000..ec43ea5fc8 --- /dev/null +++ b/test-suite/failure/illtype1.v @@ -0,0 +1,10 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +Fail Check (S S). diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v new file mode 100644 index 0000000000..f3e47bfd21 --- /dev/null +++ b/test-suite/failure/inductive.v @@ -0,0 +1,27 @@ +(* A check that sort-polymorphic product is not set too low *) + +Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. +Fail Check (fun (A:Type) (B:Prop) => (prod A B : Prop)). +Fail Check (fun (A:Prop) (B:Type) => (prod A B : Prop)). + +(* 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. +Fail Inductive u : Type := d : u | e : t u -> u. + +(* This used to succeed in versions 8.1 to 8.3 *) + +Require Import Logic. +Require Hurkens. +Definition Ti := Type. +Inductive prod2 (X Y:Ti) := pair2 : X -> Y -> prod2 X Y. +Fail Definition B : Prop := let F := prod2 True in F Prop. (* Aie! *) +(*Definition p2b (P:Prop) : B := pair2 True Prop I P. +Definition b2p (b:B) : Prop := match b with pair2 _ P => P end. +Lemma L1 : forall A : Prop, b2p (p2b A) -> A. +Proof (fun A x => x). +Lemma L2 : forall A : Prop, A -> b2p (p2b A). +Proof (fun A x => x). +Check Hurkens.paradox B p2b b2p L1 L2.*) + diff --git a/test-suite/failure/int63.v b/test-suite/failure/int63.v new file mode 100644 index 0000000000..0bb87c6548 --- /dev/null +++ b/test-suite/failure/int63.v @@ -0,0 +1,16 @@ +Require Import Int63 Cyclic63. + +Open Scope int63_scope. + +(* This used to go through because of an unbalanced stack bug in the bytecode +interpreter *) + +Lemma bad : False. +assert (1 = 2). +change 1 with (Int63.add (Int63.addmuldiv 129 (Int63.add 1 1) 2) 1). +Fail vm_compute; reflexivity. +(* +discriminate. +Qed. +*) +Abort. diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v new file mode 100644 index 0000000000..1cd119f3eb --- /dev/null +++ b/test-suite/failure/ltac1.v @@ -0,0 +1,8 @@ +(* Check all variables are different in a Context *) +Ltac X := match goal with + | x:_,x:_ |- _ => apply x + end. +Goal True -> True -> True. +intros. +Fail X. +Abort. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v new file mode 100644 index 0000000000..8a9157df84 --- /dev/null +++ b/test-suite/failure/ltac2.v @@ -0,0 +1,7 @@ +(* Check that Match arguments are forbidden *) +Ltac E x := apply x. +Goal True -> True. +Fail E ltac:(match goal with + | |- _ => intro H + end). +Abort. diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v new file mode 100644 index 0000000000..58b791eb38 --- /dev/null +++ b/test-suite/failure/ltac4.v @@ -0,0 +1,6 @@ +(* Check static globalisation of tactic names *) +(* Proposed by Benjamin (mars 2002) *) +Goal forall n : nat, n = n. +induction n. +Fail try REflexivity. +Abort. diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v new file mode 100644 index 0000000000..480f579502 --- /dev/null +++ b/test-suite/failure/pattern.v @@ -0,0 +1,10 @@ +(* Check that untypable beta-expansion are trapped *) + +Variable A : nat -> Type. +Variable n : nat. +Variable P : forall m : nat, m = n -> Prop. + +Goal forall p : n = n, P n p. +intro. +Fail pattern n, p. +Abort. diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v new file mode 100644 index 0000000000..2798dcf974 --- /dev/null +++ b/test-suite/failure/positivity.v @@ -0,0 +1,53 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Negative occurrence *) +Fail Inductive t : Type := + c : (t -> nat) -> t. + +(* Non-strictely positive occurrence *) +Fail Inductive t : Type := + c : ((t -> nat) -> nat) -> t. + +(* Self-nested type (no proof of + soundness yet *) +Fail Inductive t (A:Type) : Type := + c : t (t A) -> t A. + +(* Nested inductive types *) + +Inductive pos (A:Type) := + p : pos A -> pos A. + +Inductive nnpos (A:Type) := + nnp : ((A -> nat) -> nat) -> nnpos A. + +Inductive neg (A:Type) := + n : (A->neg A) -> neg A. + +Inductive arg : Type -> Prop := + a : forall A, arg A -> arg A. + +(* Strictly covariant parameter: accepted. *) +Fail Fail Inductive t := + c : pos t -> t. + +(* Non-strictly covariant parameter: not + strictly positive. *) +Fail Inductive t := + c : nnpos t -> t. + +(* Contravariant parameter: not positive. *) +Fail Inductive t := + c : neg t -> t. + +(* Strict index: not positive. *) +Fail Inductive t := + c : arg t -> t. diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v new file mode 100644 index 0000000000..bb9579d487 --- /dev/null +++ b/test-suite/failure/proofirrelevance.v @@ -0,0 +1,13 @@ +(* This was working in version 8.1beta (bug in template polymorphism), + but this is inconsistent with classical logic in Prop *) + +Inductive bool_in_prop : Type := hide : bool -> bool_in_prop +with bool : Type := true : bool | false : bool. + +Lemma not_proof_irrelevance : ~ forall (P:Prop) (p p':P), p=p'. +intro H. +Fail pose proof (H bool_in_prop (hide true) (hide false)). +Abort. +(*discriminate. +Qed.*) + diff --git a/test-suite/failure/prop_set_proof_irrelevance.v b/test-suite/failure/prop_set_proof_irrelevance.v new file mode 100644 index 0000000000..ed6d4300e0 --- /dev/null +++ b/test-suite/failure/prop_set_proof_irrelevance.v @@ -0,0 +1,13 @@ +Require Import ProofIrrelevance. + +Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. + Fail exact proof_irrelevance. +(*Qed. + +Lemma paradox : False. + assert (H : 0 <> 1) by discriminate. + apply H. + Fail apply proof_irrelevance. (* inlined version is rejected *) + apply proof_irrelevance_set. +Qed.*) +Abort. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v new file mode 100644 index 0000000000..981d14387d --- /dev/null +++ b/test-suite/failure/redef.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +Definition toto := Set. +Fail Definition toto := Set. diff --git a/test-suite/failure/rewrite_in_goal.v b/test-suite/failure/rewrite_in_goal.v new file mode 100644 index 0000000000..e7823f1cb1 --- /dev/null +++ b/test-suite/failure/rewrite_in_goal.v @@ -0,0 +1,4 @@ +Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type. + intros until x. + Fail rewrite H in x. +Abort. diff --git a/test-suite/failure/rewrite_in_hyp.v b/test-suite/failure/rewrite_in_hyp.v new file mode 100644 index 0000000000..f1b2203acc --- /dev/null +++ b/test-suite/failure/rewrite_in_hyp.v @@ -0,0 +1,4 @@ +Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1. + intros T1 T2 f x H fx. + Fail rewrite H in x. +Abort. diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v new file mode 100644 index 0000000000..60994fe1ed --- /dev/null +++ b/test-suite/failure/rewrite_in_hyp2.v @@ -0,0 +1,9 @@ +(* 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. + Fail rewrite H in H0. +Abort. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v new file mode 100644 index 0000000000..058c427c93 --- /dev/null +++ b/test-suite/failure/search.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Fail SearchPattern (_ = _) outside n_existe_pas. diff --git a/test-suite/failure/sortelim.v b/test-suite/failure/sortelim.v new file mode 100644 index 0000000000..3d2eef6a98 --- /dev/null +++ b/test-suite/failure/sortelim.v @@ -0,0 +1,149 @@ +(* This is a proof of false which used to be accepted by Coq (Jan 12, 2014) due +to a DeBruijn index error in the check for allowed elimination sorts. + +Proof by Maxime Dénès, using a proof of Hurkens' paradox by Hugo Herbelin to derive +inconsistency. *) + +(* We start by adapting the proof of Hurkens' paradox by Hugo in +theories/Logic/Hurkens.v, so that instead of requiring a retract +from Type into Prop up to equality, we require it only up to +equivalence. +*) + +Section Hurkens. + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +(** Assumption of a retract from Type into Prop *) + +Variable down : Type1 -> Prop. +Variable up : Prop -> Type1. + +Hypothesis back : forall A, up (down A) -> A. + +Hypothesis forth : forall A, A -> up (down A). + +Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A), + P (back A (forth A a)) -> P a. + +Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A), + P a -> P (back A (forth A a)). + +(** Proof *) + +Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. +Definition U : Type1 := V -> Prop. + +Definition sb (z:V) : V := fun A r a => r (z A r) a. +Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). +Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x). +Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). +Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))). +Definition I (x:U) : Prop := + (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False. + +Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). +Proof. +intros i y. +apply y. +unfold le, WF, induct. +apply forth. +intros x H0. +apply y. +unfold sb, le', le. +compute. +apply backforth_r. +exact H0. +Qed. + +Lemma lemma1 : induct (fun u => down (I u)). +Proof. +unfold induct. +intros x p. +apply forth. +intro q. +generalize (q (fun u => down (I u)) p). +intro r. +apply back in r. +apply r. +intros i j. +unfold le, sb, le', le in j |-. +apply backforth in j. +specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))). +apply q. +exact j. +Qed. + +Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. +Proof. +intro x. +generalize (x (fun u => down (I u)) lemma1). +intro r; apply back in r. +apply r. +intros i H0. +apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))). +unfold le, WF in H0. +apply back in H0. +exact H0. +Qed. + +Theorem paradox : False. +Proof. +exact (lemma2 Omega). +Qed. + +End Hurkens. + +(* Alright, now we use a DeBruijn index off-by-1 error to build a type +satisfying the hypotheses of the paradox. What is tricky is that the pretyper is +not affected by the bug (only the kernel is). Even worse, since our goal is to +bypass the elimination restriction for types in Prop, we have to devise a way to +feed the kernel with an illegal pattern matching without going through the +pattern matching compiler (which calls the pretyper). The trick is to use the +record machinery, which defines projections, checking if the kernel accepts +it. *) + +Definition informative (x : bool) := + match x with + | true => Type + | false => Prop + end. + +Definition depsort (T : Type) (x : bool) : informative x := + match x with + | true => T + | false => True + end. + +(* The let-bound parameters in the record below trigger the error *) + +Record Box (ff := false) (tt := true) (T : Type) : Prop := + wrap {prop : depsort T tt}. + +Definition down (x : Type) : Prop := Box x. +Definition up (x : Prop) : Type := x. + +Fail Definition back A : up (down A) -> A := prop A. + +(* If the projection has been defined, the following script derives a proof of +false. + +Definition forth A : A -> up (down A) := wrap A. + +Definition backforth (A:Type) (P:A->Type) (a:A) : + P (back A (forth A a)) -> P a := fun H => H. + +Definition backforth_r (A:Type) (P:A->Type) (a:A) : + P a -> P (back A (forth A a)) := fun H => H. + +(* Everything set up, we just check that we built the right context for the +paradox to apply. *) + +Theorem pandora : False. +apply (paradox down up back forth backforth backforth_r). +Qed. + +Print Assumptions pandora. + +*) diff --git a/test-suite/failure/subterm.v b/test-suite/failure/subterm.v new file mode 100644 index 0000000000..3798bc48fc --- /dev/null +++ b/test-suite/failure/subterm.v @@ -0,0 +1,45 @@ +Module Foo. + Inductive True2:Prop:= I2: (False->True2)->True2. + + Axiom Heq: (False->True2)=True2. + + Fail Fixpoint con (x:True2) :False := + match x with + I2 f => con (match Heq with @eq_refl _ _ => f end) + end. +End Foo. + +Require Import ClassicalFacts. + +Inductive True1 : Prop := I1 : True1 +with True2 : Prop := I2 : True1 -> True2. + +Section func_unit_discr. + +Hypothesis Heq : True1 = True2. + +Fail Fixpoint contradiction (u : True2) : False := +contradiction ( + match u with + | I2 Tr => + match Heq in (_ = T) return T with + | eq_refl => Tr + end + end). + +End func_unit_discr. + +Require Import Vectors.VectorDef. + +About caseS. +About tl. +Open Scope vector_scope. +Local Notation "[]" := (@nil _). +Local Notation "h :: t" := (@cons _ h _ t) (at level 60, right associativity). +Definition is_nil {A n} (v : t A n) : bool := match v with [] => true | _ => false end. + +Fixpoint id {A n} (v : t A n) : t A n := + match v in t _ n' return t A n' with + | (h :: t) as v' => h :: id (tl v') + |_ => [] + end. diff --git a/test-suite/failure/subterm2.v b/test-suite/failure/subterm2.v new file mode 100644 index 0000000000..a420a4d79c --- /dev/null +++ b/test-suite/failure/subterm2.v @@ -0,0 +1,48 @@ +(* An example showing that prop-extensionality is incompatible with + powerful extensions of the guard condition. + Unlike the example in guard2, it is not exploiting the fact that + the elimination of False always produces a subterm. + + Example due to Cristobal Camarero on Coq-Club. + Adapted to nested types by Bruno Barras. + *) + +Axiom prop_ext: forall P Q, (P<->Q)->P=Q. + +Module Unboxed. + +Inductive True2:Prop:= I2: (False->True2)->True2. + +Theorem Heq: (False->True2)=True2. +Proof. +apply prop_ext. split. +- intros. constructor. exact H. +- intros. exact H. +Qed. + +Fail Fixpoint con (x:True2) :False := +match x with +I2 f => con (match Heq in _=T return T with eq_refl => f end) +end. + +End Unboxed. + +(* This boxed example shows that it is not enough to just require + that the return type of the match on Heq is an inductive type + *) +Module Boxed. + +Inductive box (T:Type) := Box (_:T). +Definition unbox {T} (b:box T) : T := let (x) := b in x. + +Inductive True2:Prop:= I2: box(False->True2)->True2. + +Definition Heq: (False->True2) <-> True2 := + conj (fun f => I2 (Box _ f)) (fun x _ => x). + +Fail Fixpoint con (x:True2) :False := +match x with +I2 f => con (unbox(match prop_ext _ _ Heq in _=T return box T with eq_refl => f end)) +end. + +End Boxed. diff --git a/test-suite/failure/subterm3.v b/test-suite/failure/subterm3.v new file mode 100644 index 0000000000..2cef635756 --- /dev/null +++ b/test-suite/failure/subterm3.v @@ -0,0 +1,29 @@ +(* An example showing that prop-extensionality is incompatible with + powerful extensions of the guard condition. + This is a variation on the example in subterm2, exploiting + missing typing constraints in the commutative cut subterm rule + (subterm2 is using the same flaw but for the match rule). + + Example due to Cristóbal Camarero on Coq-Club. + *) + +Axiom prop_ext: forall P Q, (P <-> Q) -> P=Q. + +Inductive True2 : Prop := I3 : (False -> True2) -> True2. + +Theorem T3T: True2 = True. +Proof. +apply prop_ext; split; auto. +intros; constructor; apply False_rect. +Qed. + +Theorem T3F_FT3F : (True2 -> False) = ((False -> True2) -> False). +Proof. +rewrite T3T. +apply prop_ext; split; auto. +Qed. + +Fail Fixpoint loop (x : True2) : False := +match x with +I3 f => (match T3F_FT3F in _=T return T with eq_refl=> loop end) f +end. diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v new file mode 100644 index 0000000000..6996f4232a --- /dev/null +++ b/test-suite/failure/subtyping.v @@ -0,0 +1,28 @@ +(* 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. + +Fail End TT. + + Reset L. + Inductive L : Prop := + | 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 0000000000..8b2dc1dc69 --- /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; 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; 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; 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; 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; 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; simpl; intros. +trivial. + +unfold Rof, fsub; simpl; 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. +case H; simpl. +exists (fun x : X1 => x). +red; 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. +*) + + Fail 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 0000000000..28a3263d32 --- /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. + +Fail 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. *) + + diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v new file mode 100644 index 0000000000..d708b01ffc --- /dev/null +++ b/test-suite/failure/universes.v @@ -0,0 +1,3 @@ +Definition Type2 := Type. +Definition Type1 : Type2 := Type. +Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v new file mode 100644 index 0000000000..ee7a63c849 --- /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 *) +Fail 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. *) diff --git a/test-suite/failure/universes_buraliforti.v b/test-suite/failure/universes_buraliforti.v new file mode 100644 index 0000000000..dba1a794fa --- /dev/null +++ b/test-suite/failure/universes_buraliforti.v @@ -0,0 +1,237 @@ +(* Check that Burali-Forti paradox does not go through *) + +(* Source: contrib/Rocq/PARADOX/{Logics,BuraliForti},v *) + +(* Some properties about relations on objects in Type *) + + 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; intros; apply ACC_inverse_image; auto. + Qed. + +End Inverse_Image. + + +(* Remark: the paradox is written in Type, but also works in Prop or Set. *) + +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; 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; 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; 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; 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; simpl; intros. +trivial. + +unfold Rof, fsub; simpl; 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. + + + (* The following type seems to satisfy the hypothesis of the paradox. + But it does not! + *) + Record A0 : Type := (* Type_i' *) + i0 {X0 : Type; R0 : X0 -> X0 -> Prop}. (* X0: Type_j' *) + + + (* 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. +case H; simpl. +exists (fun x : X1 => x). +red; 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. +*) + + Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes_buraliforti_redef.v b/test-suite/failure/universes_buraliforti_redef.v new file mode 100644 index 0000000000..e016815880 --- /dev/null +++ b/test-suite/failure/universes_buraliforti_redef.v @@ -0,0 +1,246 @@ +(* A variant of Burali-Forti that used to pass in V8.1beta, because of + a bug in the instantiation of sort-polymorphic inductive types *) + +(* The following type seems to satisfy the hypothesis of the paradox below *) +(* It should infer constraints forbidding the paradox to go through, but via *) +(* a redefinition that did not propagate constraints correctly in V8.1beta *) +(* it was exploitable to derive an inconsistency *) + +(* We keep the file as a non regression test of the bug *) + + Record A1 (B:Type) (g:B->Type) : Type := (* Type_i' *) + i1 {X0 : B; R0 : g X0 -> g X0 -> Prop}. (* X0: Type_j' *) + + Definition A2 := A1. (* here was the bug *) + + Definition A0 := (A2 Type (fun x => x)). + Definition i0 := (i1 Type (fun x => x)). + +(* The rest is as in universes-buraliforti.v *) + + +(* Some properties about relations on objects in Type *) + + 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; intros; apply ACC_inverse_image; auto. + Qed. + +End Inverse_Image. + + +(* Remark: the paradox is written in Type, but also works in Prop or Set. *) + +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 X1 R1 eqx X2 R2 eqy; intros. +case H0; intros X3 R3 eqx0 X4 R4 eqy0; intros. +generalize eqx0; clear eqx0. +elim eqy using eq_ind_r; intro. +case (inj _ _ _ _ eqx0); intros. +exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. +red; 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; 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; 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; 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; simpl; intros. +trivial. + +unfold Rof, fsub; simpl; 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. + + + (* 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 + | i1 _ _ x1 r1, i1 _ _ x2 r2 => exists f : _, morphism x1 r1 x2 r2 f + end. +case H; simpl. +exists (fun x : X1 => x). +red; trivial. +Defined. + +(* The following command should raise '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. +*) + + Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes_sections1.v b/test-suite/failure/universes_sections1.v new file mode 100644 index 0000000000..3f8e444623 --- /dev/null +++ b/test-suite/failure/universes_sections1.v @@ -0,0 +1,8 @@ +(* Check that constraints on definitions are preserved by discharging *) + +Section A. + Definition Type2 := Type. + Definition Type1 : Type2 := Type. +End A. + +Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes_sections2.v b/test-suite/failure/universes_sections2.v new file mode 100644 index 0000000000..34b2a11ded --- /dev/null +++ b/test-suite/failure/universes_sections2.v @@ -0,0 +1,10 @@ +(* Check that constraints on locals are preserved by discharging *) + +Definition Type2 := Type. + +Section A. + Let Type1 : Type2 := Type. + Definition Type1' := Type1. +End A. + +Fail Definition Inconsistency : Type1' := Type2. |