diff options
Diffstat (limited to 'test-suite/failure')
73 files changed, 459 insertions, 173 deletions
diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v index df11ed38..6e76d42d 100644 --- a/test-suite/failure/Case1.v +++ b/test-suite/failure/Case1.v @@ -1,4 +1,4 @@ -Type match 0 with +Fail Type match 0 with | x => 0 | O => 1 end. diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v index 43cc1e34..661d98cd 100644 --- a/test-suite/failure/Case10.v +++ b/test-suite/failure/Case10.v @@ -1,3 +1,3 @@ -Type (fun x : nat => match x return nat with +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 index e76d0609..675f79e6 100644 --- a/test-suite/failure/Case11.v +++ b/test-suite/failure/Case11.v @@ -1,3 +1,3 @@ -Type (fun x : nat => match x return nat with +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 index cf6c2026..4a77f139 100644 --- a/test-suite/failure/Case12.v +++ b/test-suite/failure/Case12.v @@ -1,5 +1,5 @@ -Type +Fail Type (fun x : nat => match x return nat with | S x as b => match x with diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v index 994dfd20..5c0aa3e1 100644 --- a/test-suite/failure/Case13.v +++ b/test-suite/failure/Case13.v @@ -1,4 +1,4 @@ -Type +Fail Type (fun x : nat => match x return nat with | S x as b => match x with diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v index ba0c51a1..29cae764 100644 --- a/test-suite/failure/Case14.v +++ b/test-suite/failure/Case14.v @@ -3,7 +3,7 @@ Inductive List (A : Set) : Set := | Cons : A -> List A -> List A. Definition NIL := Nil nat. -Type match Nil nat return (List nat) with +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 index 18faaf5c..ec08e614 100644 --- a/test-suite/failure/Case15.v +++ b/test-suite/failure/Case15.v @@ -1,6 +1,6 @@ (* Non exhaustive pattern-matching *) -Check +Fail Check (fun x => match x, x with | O, S (S y) => true diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v index 3739adae..df15a428 100644 --- a/test-suite/failure/Case16.v +++ b/test-suite/failure/Case16.v @@ -1,6 +1,6 @@ (* Check for redundant clauses *) -Check +Fail Check (fun x => match x, x with | O, S (S y) => true diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v index 7d81ee81..f8c95b1e 100644 --- a/test-suite/failure/Case2.v +++ b/test-suite/failure/Case2.v @@ -4,7 +4,7 @@ Inductive IFExpr : Set := | Fa : IFExpr | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. -Type +Fail Type (fun F : IFExpr => match F return Prop with | IfE (Var _) H I => True diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v index ca450d5b..eaafd41f 100644 --- a/test-suite/failure/Case3.v +++ b/test-suite/failure/Case3.v @@ -2,7 +2,7 @@ Inductive List (A : Set) : Set := | Nil : List A | Cons : A -> List A -> List A. -Type +Fail Type (fun l : List nat => match l return nat with | Nil nat => 0 diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v index de63c3f7..4da7ef0c 100644 --- a/test-suite/failure/Case4.v +++ b/test-suite/failure/Case4.v @@ -1,5 +1,5 @@ -Definition Berry (x y z : bool) := +Fail Definition Berry (x y z : bool) := match x, y, z with | true, false, _ => 0 | false, _, true => 1 diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v index 494443f1..70e5b988 100644 --- a/test-suite/failure/Case5.v +++ b/test-suite/failure/Case5.v @@ -2,6 +2,6 @@ Inductive MS : Set := | X : MS -> MS | Y : MS -> MS. -Type (fun p : MS => match p return nat with +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 index fb8659bf..cb7b7de0 100644 --- a/test-suite/failure/Case6.v +++ b/test-suite/failure/Case6.v @@ -2,7 +2,7 @@ Inductive List (A : Set) : Set := | Nil : List A | Cons : A -> List A -> List A. -Type (match Nil nat return List nat with +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 index 64453481..e1fd7df0 100644 --- a/test-suite/failure/Case7.v +++ b/test-suite/failure/Case7.v @@ -9,7 +9,7 @@ Definition length1 (n : nat) (l : listn n) := | _ => 0 end. -Type +Fail Type (fun (n : nat) (l : listn n) => match n return nat with | O => 0 diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v index feae29a7..035629fe 100644 --- a/test-suite/failure/Case8.v +++ b/test-suite/failure/Case8.v @@ -2,7 +2,7 @@ Inductive List (A : Set) : Set := | Nil : List A | Cons : A -> List A -> List A. -Type match Nil nat return nat with +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 index d63c4940..642f85d7 100644 --- a/test-suite/failure/Case9.v +++ b/test-suite/failure/Case9.v @@ -1,8 +1,8 @@ Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. -Type +Fail Type match compare 0 0 return nat with - (* k<i *) | left _ _ (left _ _ _) => 0 - (* k=i *) | left _ _ _ => 0 - (* k>i *) | right _ _ _ => 0 + (* 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 index 609d5b3b..e321e59f 100644 --- a/test-suite/failure/ClearBody.v +++ b/test-suite/failure/ClearBody.v @@ -5,4 +5,4 @@ Goal True. set (n := 0) in *. set (I := refl_equal 0) in *. change (n = 0) in (type of I). -clearbody n. +Fail clearbody n. diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v index 0a69b851..1cac69f4 100644 --- a/test-suite/failure/ImportedCoercion.v +++ b/test-suite/failure/ImportedCoercion.v @@ -4,4 +4,4 @@ Require Import make_local. (* Local coercion must not be used *) -Check (0 = true). +Fail Check (0 = true). diff --git a/test-suite/failure/Notations.v b/test-suite/failure/Notations.v index 074e176a..83459de3 100644 --- a/test-suite/failure/Notations.v +++ b/test-suite/failure/Notations.v @@ -3,5 +3,5 @@ Notation "! A" := (forall i:nat, A) (at level 60). (* Should fail: no dynamic capture *) -Check ! (i=i). +Fail Check ! (i=i). diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v index 7b36d1c3..e79b2073 100644 --- a/test-suite/failure/Reordering.v +++ b/test-suite/failure/Reordering.v @@ -2,4 +2,4 @@ Goal forall (A:Set) (x:A) (A':=A), True. intros. -change ((fun (_:A') => Set) x) in (type of A). +Fail change ((fun (_:A') => Set) x) in (type of A). diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v index 9b3b35c1..928e214f 100644 --- a/test-suite/failure/Sections.v +++ b/test-suite/failure/Sections.v @@ -1,4 +1,4 @@ Module A. Section B. -End A. -End A. +Fail End A. +(*End A.*) diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 11b40951..749db000 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -17,4 +17,4 @@ (* Fails because Tauto does not perform any Apply *) Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y. Proof. - tauto. + Fail tauto. diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v index 3c3bf375..cc31c7ae 100644 --- a/test-suite/failure/Uminus.v +++ b/test-suite/failure/Uminus.v @@ -1,62 +1,21 @@ (* Check that the encoding of system U- fails *) -Inductive prop : Prop := down : Prop -> prop. - -Definition up (p:prop) : Prop := let (A) := p in A. - -Lemma p2p1 : forall A:Prop, up (down A) -> A. -Proof. -exact (fun A x => x). -Qed. +Require Hurkens. -Lemma p2p2 : forall A:Prop, A -> up (down A). -Proof. -exact (fun A x => x). -Qed. - -(** Hurkens' paradox *) - -Definition V := forall A:Prop, ((A -> prop) -> A -> prop) -> A -> prop. -Definition U := 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 induct (i:U -> prop) : Prop := - forall x:U, up (le i x) -> up (i x). -Definition WF : U := fun z => down (induct (z U le)). -Definition I (x:U) : Prop := - (forall i:U -> prop, up (le i x) -> up (i (fun v => sb v U le x))) -> False. +Inductive prop : Prop := down : Prop -> prop. -Lemma Omega : forall i:U -> prop, induct i -> up (i WF). -Proof. -intros i y. -apply y. -unfold le, WF, induct. -intros x H0. -apply y. -exact H0. -Qed. +(* Coq should reject the following access of a Prop buried inside + a prop. *) -Lemma lemma1 : induct (fun u => down (I u)). -Proof. -unfold induct. -intros x p. -intro q. -apply (q (fun u => down (I u)) p). -intro i. -apply q with (i := fun y => i (fun v:V => sb v U le y)). -Qed. +Fail Definition up (p:prop) : Prop := let (A) := p in A. -Lemma lemma2 : (forall i:U -> prop, induct i -> up (i WF)) -> False. -Proof. -intro x. -apply (x (fun u => down (I u)) lemma1). -intros i H0. -apply (x (fun y => i (fun v => sb v U le y))). -apply H0. -Qed. +(* Otherwise, we would have a proof of False via Hurkens' paradox *) -Theorem paradox : False. -Proof. -exact (lemma2 Omega). -Qed. +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 index dc17742a..191e035b 100644 --- a/test-suite/failure/autorewritein.v +++ b/test-suite/failure/autorewritein.v @@ -9,7 +9,7 @@ Hint Rewrite Ack0 Ack1 Ack2 : base0. Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H -> False. Proof. intros. - autorewrite with base0 in * using try (apply H1;reflexivity). + Fail autorewrite with base0 in * using try (apply H1;reflexivity). diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v index 18faaf5c..ec08e614 100644 --- a/test-suite/failure/cases.v +++ b/test-suite/failure/cases.v @@ -1,6 +1,6 @@ (* Non exhaustive pattern-matching *) -Check +Fail Check (fun x => match x, x with | O, S (S y) => true diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index 649fdd2d..a148ebe8 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ Implicit Arguments eq [A]. -Check (bool = true). +Fail Check (bool = true). diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping.v index 0b3a8688..ceccd460 100644 --- a/test-suite/failure/circular_subtyping1.v +++ b/test-suite/failure/circular_subtyping.v @@ -1,7 +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. -Module P <: T with Module M:=NN := 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.
\ No newline at end of file diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v deleted file mode 100644 index 3bacdc65..00000000 --- a/test-suite/failure/circular_subtyping2.v +++ /dev/null @@ -1,8 +0,0 @@ -(*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/clash_cons.v b/test-suite/failure/clash_cons.v index 17e56763..8e34ffbd 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,5 +11,5 @@ Inductive X : Set := cons : X. -Inductive Y : Set := +Fail Inductive Y : Set := cons : Y. diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v index 207d62b9..1a59ec66 100644 --- a/test-suite/failure/clashes.v +++ b/test-suite/failure/clashes.v @@ -5,5 +5,5 @@ Section S. Variable n : nat. -Inductive P : Set := +Fail Inductive P : Set := n : P. diff --git a/test-suite/failure/cofixpoint.v b/test-suite/failure/cofixpoint.v new file mode 100644 index 00000000..cb39893f --- /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).
\ No newline at end of file diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v index 79eef5c9..cc3f307a 100644 --- a/test-suite/failure/coqbugs0266.v +++ b/test-suite/failure/coqbugs0266.v @@ -4,4 +4,4 @@ Section S. Let a := 0. Definition b := a. Goal b = b. -clear a. +Fail clear a. diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v index 1a4e42a8..2b6fe765 100644 --- a/test-suite/failure/evar1.v +++ b/test-suite/failure/evar1.v @@ -1,3 +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). +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 index 2e9fa0f3..60adadef 100644 --- a/test-suite/failure/evarclear1.v +++ b/test-suite/failure/evarclear1.v @@ -6,5 +6,5 @@ eexists. unfold z. clear y z. (* should fail because the evar should no longer be allowed to depend on z *) -instantiate (1:=z). +Fail instantiate (1:=z). diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v index e606a06f..0f776811 100644 --- a/test-suite/failure/evarclear2.v +++ b/test-suite/failure/evarclear2.v @@ -6,4 +6,4 @@ eexists. rename y into z. unfold z at 1 2. (* should fail because the evar type depends on z *) -clear z. +Fail clear z. diff --git a/test-suite/failure/evarlemma.v b/test-suite/failure/evarlemma.v index ea753e79..ae40774c 100644 --- a/test-suite/failure/evarlemma.v +++ b/test-suite/failure/evarlemma.v @@ -1,3 +1,3 @@ (* Check success of inference of evars in the context of lemmas *) -Lemma foo x : True. +Fail Lemma foo x : True. diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index bea21f33..7b52316e 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,10 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Fixpoint PreParadox (u : unit) : False := PreParadox u. -Definition Paradox := PreParadox tt. +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 index d2f02ea1..7f11a99b 100644 --- a/test-suite/failure/fixpoint2.v +++ b/test-suite/failure/fixpoint2.v @@ -3,4 +3,4 @@ Goal nat->nat. fix f 1. intro n; apply f; assumption. -Guarded. +Fail Guarded. diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v index 42f06916..7d1d3ee6 100644 --- a/test-suite/failure/fixpoint3.v +++ b/test-suite/failure/fixpoint3.v @@ -6,7 +6,7 @@ Inductive I : Prop := Definition i0 := C (fun _ x => x). -Definition Paradox : False := +Fail Definition Paradox : False := (fix ni i : False := match i with | C f => ni (f _ i) diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v index fd956373..bf6133f1 100644 --- a/test-suite/failure/fixpoint4.v +++ b/test-suite/failure/fixpoint4.v @@ -8,7 +8,7 @@ Inductive IMP : Prop := Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))). -Definition Paradox : False := +Fail Definition Paradox : False := (fix F y o {struct o} : False := match y with | tt => fun f => diff --git a/test-suite/failure/guard-cofix.v b/test-suite/failure/guard-cofix.v new file mode 100644 index 00000000..64faa0ce --- /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 := 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.
\ No newline at end of file diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 78a0782a..b3a0a335 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,16 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \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). - +*) (* de Bruijn mix-up *) (* If accepted, Eval compute in f 0. loops *) -Definition f := +Fail Definition f := let f (f1 f2:nat->nat) := f1 in let _ := 0 in let _ := 0 in diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 5781c96b..7e4c5ac5 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,8 +1,8 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Check (S S). +Fail Check (S S). diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v new file mode 100644 index 00000000..f3e47bfd --- /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/inductive1.v b/test-suite/failure/inductive1.v deleted file mode 100644 index 3b57d919..00000000 --- a/test-suite/failure/inductive1.v +++ /dev/null @@ -1,4 +0,0 @@ -(* A check that sort-polymorphic product is not set too low *) - -Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. -Check (fun (A:Type) (B:Prop) => (prod A B : Prop)). diff --git a/test-suite/failure/inductive2.v b/test-suite/failure/inductive2.v deleted file mode 100644 index b77474be..00000000 --- a/test-suite/failure/inductive2.v +++ /dev/null @@ -1,4 +0,0 @@ -(* A check that sort-polymorphic product is not set too low *) - -Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. -Check (fun (A:Prop) (B:Type) => (prod A B : Prop)). diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v deleted file mode 100644 index cf035edf..00000000 --- a/test-suite/failure/inductive3.v +++ /dev/null @@ -1,5 +0,0 @@ -(* 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. -Inductive u : Type := d : u | e : t u -> u. diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v deleted file mode 100644 index 6ba36fd2..00000000 --- a/test-suite/failure/inductive4.v +++ /dev/null @@ -1,15 +0,0 @@ -(* This used to succeed in versions 8.1 to 8.3 *) - -Require Import Logic. -Require Hurkens. -Definition Ti := Type. -Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y. -Definition B : Prop := let F := prod True in F Prop. (* Aie! *) -Definition p2b (P:Prop) : B := pair True Prop I P. -Definition b2p (b:B) : Prop := match b with pair _ 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/ltac1.v b/test-suite/failure/ltac1.v index 7b496a75..eef16525 100644 --- a/test-suite/failure/ltac1.v +++ b/test-suite/failure/ltac1.v @@ -4,4 +4,4 @@ Ltac X := match goal with end. Goal True -> True -> True. intros. -X. +Fail X. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v index 14436e58..d66fb680 100644 --- a/test-suite/failure/ltac2.v +++ b/test-suite/failure/ltac2.v @@ -1,6 +1,6 @@ (* Check that Match arguments are forbidden *) Ltac E x := apply x. Goal True -> True. -E ltac:(match goal with +Fail E ltac:(match goal with | |- _ => intro H end). diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v index 41471275..5b0396d1 100644 --- a/test-suite/failure/ltac4.v +++ b/test-suite/failure/ltac4.v @@ -1,5 +1,6 @@ (* Check static globalisation of tactic names *) (* Proposed by Benjamin (mars 2002) *) Goal forall n : nat, n = n. -induction n; try REflexivity. +induction n. +Fail try REflexivity. diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v index a24beaa2..216eb254 100644 --- a/test-suite/failure/pattern.v +++ b/test-suite/failure/pattern.v @@ -6,4 +6,4 @@ Variable P : forall m : nat, m = n -> Prop. Goal forall p : n = n, P n p. intro. -pattern n, p. +Fail pattern n, p. diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 1c1080d1..d44bccdf 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,9 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Inductive t : Set := +Fail Inductive t : Set := c : (t -> nat) -> t. diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index 93e159e8..b62f9b68 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -6,6 +6,9 @@ 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; pose proof (H bool_in_prop (hide true) (hide false)); discriminate. -Qed. +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 index ad494108..fee33432 100644 --- a/test-suite/failure/prop-set-proof-irrelevance.v +++ b/test-suite/failure/prop-set-proof-irrelevance.v @@ -1,12 +1,12 @@ Require Import ProofIrrelevance. Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2. - exact proof_irrelevance. -Qed. + 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. +Qed.*) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index ef6d01d0..e5db8176 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,9 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) Definition toto := Set. -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 index c11a6237..dedfdf01 100644 --- a/test-suite/failure/rewrite_in_goal.v +++ b/test-suite/failure/rewrite_in_goal.v @@ -1,3 +1,3 @@ Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type. intros until x. - rewrite H in x. + Fail rewrite H in x. diff --git a/test-suite/failure/rewrite_in_hyp.v b/test-suite/failure/rewrite_in_hyp.v index 613d707c..1eef0fa0 100644 --- a/test-suite/failure/rewrite_in_hyp.v +++ b/test-suite/failure/rewrite_in_hyp.v @@ -1,3 +1,3 @@ Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1. intros T1 T2 f x H fx. - rewrite H in x. + Fail rewrite H in x. diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v index 1533966e..112a856e 100644 --- a/test-suite/failure/rewrite_in_hyp2.v +++ b/test-suite/failure/rewrite_in_hyp2.v @@ -5,4 +5,4 @@ Goal forall b, S b = O -> (fun a => 0 = (S a)) b -> True. intros b H H0. - rewrite H in H0. + Fail rewrite H in H0. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 9c35ecfb..a6e6bc48 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,9 +1,9 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -SearchPattern (_ = _) outside n_existe_pas. +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 00000000..2b3cf106 --- /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. + +*)
\ No newline at end of file diff --git a/test-suite/failure/subterm.v b/test-suite/failure/subterm.v new file mode 100644 index 00000000..3798bc48 --- /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 00000000..a420a4d7 --- /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 00000000..2cef6357 --- /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 index 127da851..e48c6689 100644 --- a/test-suite/failure/subtyping.v +++ b/test-suite/failure/subtyping.v @@ -18,4 +18,4 @@ Module TT : T. | L0 | L1 : (A -> Prop) -> L. -End TT. +Fail End TT. diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v index 48fc2fff..8b2dc1dc 100644 --- a/test-suite/failure/subtyping2.v +++ b/test-suite/failure/subtyping2.v @@ -242,4 +242,4 @@ Defined. with the constraint j >= i in the paradox. *) - Definition Paradox : False := Burali_Forti A0 i0' inj. + 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 index 56f04f9d..28a3263d 100644 --- a/test-suite/failure/univ_include.v +++ b/test-suite/failure/univ_include.v @@ -23,8 +23,8 @@ Module Mt. Definition t := T. End Mt. -Module P := G Mt. (* should yield Universe inconsistency *) +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. +(* Eval cbv delta [P.elt Mt.t] in P.elt. *) diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v index a8b5b975..e0168158 100644 --- a/test-suite/failure/universes-buraliforti-redef.v +++ b/test-suite/failure/universes-buraliforti-redef.v @@ -230,17 +230,17 @@ End Burali_Forti_Paradox. intros. change match i0 X1 R1, i0 X2 R2 with - | i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f + | 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 raises 'Error: Universe Inconsistency'. +(* 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. *) - Definition Paradox : False := Burali_Forti A0 i0 inj. + Fail Definition Paradox : False := Burali_Forti A0 i0 inj. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index 7b62a0c5..dba1a794 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -234,4 +234,4 @@ Defined. with the constraint j >= i in the paradox. *) - Definition Paradox : False := Burali_Forti A0 i0 inj. + 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 index 6cd04349..3f8e4446 100644 --- a/test-suite/failure/universes-sections1.v +++ b/test-suite/failure/universes-sections1.v @@ -5,4 +5,4 @@ Section A. Definition Type1 : Type2 := Type. End A. -Definition Inconsistency : Type1 := Type2. +Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v index 98fdbc0d..34b2a11d 100644 --- a/test-suite/failure/universes-sections2.v +++ b/test-suite/failure/universes-sections2.v @@ -7,4 +7,4 @@ Section A. Definition Type1' := Type1. End A. -Definition Inconsistency : Type1' := Type2. +Fail Definition Inconsistency : Type1' := Type2. diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v index 938c29b8..d708b01f 100644 --- a/test-suite/failure/universes.v +++ b/test-suite/failure/universes.v @@ -1,3 +1,3 @@ Definition Type2 := Type. Definition Type1 : Type2 := Type. -Definition Inconsistency : Type1 := Type2. +Fail Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v index 8fb414d5..ee7a63c8 100644 --- a/test-suite/failure/universes3.v +++ b/test-suite/failure/universes3.v @@ -17,7 +17,7 @@ Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B). (* We cannot enforce Type1 < Type(6) while we already have Type(6) <= Type(7) < Type3 < Type1 *) -Definition J := I 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, |