diff options
Diffstat (limited to 'test-suite/failure')
38 files changed, 320 insertions, 271 deletions
diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v index fafcafc1..df11ed38 100644 --- a/test-suite/failure/Case1.v +++ b/test-suite/failure/Case1.v @@ -1 +1,4 @@ -Type Cases O of x => O | O => (S O) end. +Type match 0 with + | x => 0 + | O => 1 + end. diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v index ee47544d..43cc1e34 100644 --- a/test-suite/failure/Case10.v +++ b/test-suite/failure/Case10.v @@ -1 +1,3 @@ -Type [x:nat]<nat> Cases x of ((S x) as b) => (S b) end. +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 c39a76ca..e76d0609 100644 --- a/test-suite/failure/Case11.v +++ b/test-suite/failure/Case11.v @@ -1 +1,3 @@ -Type [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end. +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 b56eac0d..cf6c2026 100644 --- a/test-suite/failure/Case12.v +++ b/test-suite/failure/Case12.v @@ -1,7 +1,8 @@ -Type [x:nat]<nat> Cases x of - ((S x) as b) => <nat>Cases x of - x => x - end - end. - +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 index 8a4d75b6..994dfd20 100644 --- a/test-suite/failure/Case13.v +++ b/test-suite/failure/Case13.v @@ -1,5 +1,7 @@ -Type [x:nat]<nat> Cases x of - ((S x) as b) => <nat>Cases x of - x => (S b x) - end - end. +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 index a198d068..ba0c51a1 100644 --- a/test-suite/failure/Case14.v +++ b/test-suite/failure/Case14.v @@ -1,8 +1,9 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. -Definition NIL := (Nil nat). -Type <(List nat)>Cases (Nil nat) of - NIL => NIL - | _ => NIL - end. +Definition NIL := Nil nat. +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 a27b07f8..18faaf5c 100644 --- a/test-suite/failure/Case15.v +++ b/test-suite/failure/Case15.v @@ -1,6 +1,9 @@ (* Non exhaustive pattern-matching *) -Check [x]Cases x x of - O (S (S y)) => true - | O (S x) => false - | (S y) O => true end.
\ No newline at end of file +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 index f994a8f2..3739adae 100644 --- a/test-suite/failure/Case16.v +++ b/test-suite/failure/Case16.v @@ -1,9 +1,11 @@ (* Check for redundant clauses *) -Check [x]Cases x x of - O (S (S y)) => true - | (S _) (S (S y)) => true - | _ (S (S x)) => false - | (S y) O => true - | _ _ => true -end. +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 index 183f612b..7d81ee81 100644 --- a/test-suite/failure/Case2.v +++ b/test-suite/failure/Case2.v @@ -1,13 +1,13 @@ -Inductive IFExpr : Set := - Var : nat -> IFExpr - | Tr : IFExpr - | Fa : IFExpr - | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. - -Type [F:IFExpr] - <Prop>Cases F of - (IfE (Var _) H I) => True - | (IfE _ _ _) => False - | _ => True - end. +Inductive IFExpr : Set := + | Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. +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 index 2c651b87..ca450d5b 100644 --- a/test-suite/failure/Case3.v +++ b/test-suite/failure/Case3.v @@ -1,7 +1,10 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. -Type [l:(List nat)]<nat>Cases l of - (Nil nat) =>O - | (Cons a l) => (S a) - end. +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 index d00c9a05..de63c3f7 100644 --- a/test-suite/failure/Case4.v +++ b/test-suite/failure/Case4.v @@ -1,7 +1,7 @@ -Definition Berry := [x,y,z:bool] - Cases x y z of - true false _ => O - | false _ true => (S O) - | _ true false => (S (S O)) -end. +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 index bdb5544b..29996fd4 100644 --- a/test-suite/failure/Case5.v +++ b/test-suite/failure/Case5.v @@ -1,3 +1,7 @@ -Inductive MS: Set := X:MS->MS | Y:MS->MS. +Inductive MS : Set := + | X : MS -> MS + | Y : MS -> MS. -Type [p:MS]<nat>Cases p of (X x) => O end. +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 f588d275..fb8659bf 100644 --- a/test-suite/failure/Case6.v +++ b/test-suite/failure/Case6.v @@ -1,10 +1,8 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). - - -Type <(List nat)>Cases (Nil nat) of - NIL => NIL - | (CONS _ _) => NIL - - end. - +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +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 3718f198..64453481 100644 --- a/test-suite/failure/Case7.v +++ b/test-suite/failure/Case7.v @@ -1,22 +1,20 @@ -Inductive listn : nat-> Set := - niln : (listn O) -| consn : (n:nat)nat->(listn n) -> (listn (S n)). +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). -Definition length1:= [n:nat] [l:(listn n)] - Cases l of - (consn n _ (consn m _ _)) => (S (S m)) - |(consn n _ _) => (S O) - | _ => O - end. - -Type [n:nat] - [l:(listn n)] - <nat>Cases n of - O => O - | (S n) => - <([_:nat]nat)>Cases l of - niln => (S O) - | l' => (length1 (S n) l') - end - end. +Definition length1 (n : nat) (l : listn n) := + match l with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => 1 + | _ => 0 + end. +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 index 7f6bb615..feae29a7 100644 --- a/test-suite/failure/Case8.v +++ b/test-suite/failure/Case8.v @@ -1,8 +1,8 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). - -Type <nat>Cases (Nil nat) of - ((Nil_) as b) =>b - |((Cons _ _ _) as d) => d - end. +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. +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 e8d8e89a..a3b99f63 100644 --- a/test-suite/failure/Case9.v +++ b/test-suite/failure/Case9.v @@ -1,6 +1,8 @@ -Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. -Type <nat>Cases (compare O O) of - (* k<i *) (left _ _ (left _ _ _)) => O - | (* k=i *) (left _ _ _) => O - | (* k>i *) (right _ _ _) => O end. - +Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. +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 index ca8e3c68..609d5b3b 100644 --- a/test-suite/failure/ClearBody.v +++ b/test-suite/failure/ClearBody.v @@ -2,7 +2,7 @@ invalidate the well-typabilility of the visible goal *) Goal True. -LetTac n:=O. -LetTac I:=(refl_equal nat O). -Change (n=O) in (Type of I). -ClearBody n. +set (n := 0) in *. +set (I := refl_equal 0) in *. +change (n = 0) in (type of I). +clearbody n. diff --git a/test-suite/failure/Notations.v b/test-suite/failure/Notations.v new file mode 100644 index 00000000..074e176a --- /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 *) +Check ! (i=i). + diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index fb9a27bb..cda2d51e 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -15,6 +15,6 @@ Simplifications of goals, based on LJT calcul ****) (* Fails because Tauto does not perform any Apply *) -Goal ((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y. Proof. - Tauto. + tauto. diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v index a27b07f8..18faaf5c 100644 --- a/test-suite/failure/cases.v +++ b/test-suite/failure/cases.v @@ -1,6 +1,9 @@ (* Non exhaustive pattern-matching *) -Check [x]Cases x x of - O (S (S y)) => true - | O (S x) => false - | (S y) O => true end.
\ No newline at end of file +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 index 0bf7091c..649fdd2d 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ -Implicits eq [1]. +Implicit Arguments eq [A]. -Check (eq bool true). +Check (bool = true). diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index 56cd73f4..07db69a9 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -8,9 +8,8 @@ (* Teste la verification d'unicite des noms de constr *) -Inductive X : Set := +Inductive X : Set := cons : X. -Inductive Y : Set := +Inductive Y : Set := cons : Y. - diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v index fcfd29fe..207d62b9 100644 --- a/test-suite/failure/clashes.v +++ b/test-suite/failure/clashes.v @@ -4,5 +4,6 @@ S.n to keep n accessible... *) Section S. -Variable n:nat. -Inductive P : Set := n : P. +Variable n : nat. +Inductive P : Set := + n : P. diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v index 2ac6c4f0..79eef5c9 100644 --- a/test-suite/failure/coqbugs0266.v +++ b/test-suite/failure/coqbugs0266.v @@ -1,7 +1,7 @@ (* It is forbidden to erase a variable (or a local def) that is used in the current goal. *) Section S. -Local a:=O. -Definition b:=a. -Goal b=b. -Clear a. +Let a := 0. +Definition b := a. +Goal b = b. +clear a. diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index 742e9774..7d0d9d2d 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -5,5 +5,6 @@ (* // * 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).
\ No newline at end of file +Fixpoint PreParadox (u : unit) : False := PreParadox u. +Definition Paradox := PreParadox tt. + diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v index d0256619..7b496a75 100644 --- a/test-suite/failure/ltac1.v +++ b/test-suite/failure/ltac1.v @@ -1,5 +1,7 @@ (* Check all variables are different in a Context *) -Tactic Definition X := Match Context With [ x:?; x:? |- ? ] -> Apply x. -Goal True->True->True. -Intros. +Ltac X := match goal with + | x:_,x:_ |- _ => apply x + end. +Goal True -> True -> True. +intros. X. diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v index 55925a7a..14436e58 100644 --- a/test-suite/failure/ltac2.v +++ b/test-suite/failure/ltac2.v @@ -1,6 +1,6 @@ (* Check that Match arguments are forbidden *) -Tactic Definition E x := Apply x. -Goal True->True. -E (Match Context With [ |- ? ] -> Intro H). -(* Should fail with "Immediate Match producing tactics not allowed in - local definitions" *) +Ltac E x := apply x. +Goal True -> True. +E ltac:(match goal with + | |- _ => intro H + end). diff --git a/test-suite/failure/ltac3.v b/test-suite/failure/ltac3.v deleted file mode 100644 index bfccc546..00000000 --- a/test-suite/failure/ltac3.v +++ /dev/null @@ -1,2 +0,0 @@ -(* Proposed by Benjamin *) -Definition A := Try REflexivity. diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v index d1e4e892..41471275 100644 --- a/test-suite/failure/ltac4.v +++ b/test-suite/failure/ltac4.v @@ -1,4 +1,5 @@ (* Check static globalisation of tactic names *) (* Proposed by Benjamin (mars 2002) *) -Goal (n:nat)n=n. -Induction n; Try REflexivity. +Goal forall n : nat, n = n. +induction n; try REflexivity. + diff --git a/test-suite/failure/params_ind.v b/test-suite/failure/params_ind.v deleted file mode 100644 index 20689128..00000000 --- a/test-suite/failure/params_ind.v +++ /dev/null @@ -1,4 +0,0 @@ -Inductive list [A:Set] : Set := - nil : (list A) -| cons : A -> (list A->A)-> (list A). - diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v new file mode 100644 index 00000000..129c380e --- /dev/null +++ b/test-suite/failure/pattern.v @@ -0,0 +1,9 @@ +(* 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. +pattern n, p in |- *. diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index b43eb899..21683605 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -5,4 +5,5 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Inductive t:Set := c: (t -> nat) -> t. +Inductive t : Set := + c : (t -> nat) -> t. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index e8ca8494..ef750b50 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -5,4 +5,5 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -SearchPattern ? = ? outside n_existe_pas. + +SearchPattern (_ = _) outside n_existe_pas. diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index 01d46133..d18d2119 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -4,38 +4,41 @@ (* Some properties about relations on objects in Type *) - Inductive ACC [A : Type; R : A->A->Prop] : A->Prop := - ACC_intro : (x:A)((y:A)(R y x)->(ACC A R y))->(ACC A R x). + 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: - (A:Type)(R:A->A->Prop)(x:A)(ACC A R x)->(R x x)->False. -Induction 1; Intros. -Exact (H1 x0 H2 H2). -Save. + 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](x:A)(ACC A R x). + 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. + Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B). - Definition Rof : A->A->Prop := [x,y:A](R (f x) (f y)). + Definition Rof (x y : A) : Prop := R (f x) (f y). - Remark ACC_lemma : (y:B)(ACC B R y)->(x:A)(y==(f x))->(ACC A Rof x). - Induction 1; Intros. - Constructor; Intros. - Apply (H1 (f y0)); Trivial. - Elim H2 using eqT_ind_r; Trivial. - Save. + 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 : (x:A)(ACC B R (f x)) -> (ACC A Rof x). - Intros; Apply (ACC_lemma (f x)); Trivial. - Save. + 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. - Save. + Lemma WF_inverse_image : WF B R -> WF A Rof. + red in |- *; intros; apply ACC_inverse_image; auto. + Qed. End Inverse_Image. @@ -44,8 +47,9 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism := [A:Type][R:A->A->Prop][B:Type][S:B->B->Prop][f:A->B] - (x,y:A)(R x y)->(S (f x) (f y)). + 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: @@ -53,120 +57,125 @@ Section Burali_Forti_Paradox. - 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 : (X:Type)(X->X->Prop)->A0. (* X: Type_j *) - Hypothesis inj : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) - (i0 X1 R1)==(i0 X2 R2) - ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). + 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: (z:X1)(R2 (f z) maj) }. - - - Lemma emb_trans: (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 eqT_ind_r; Intro. -Case (inj ? ? ? ? eqx0); Intros. -Exists X1 R1 X3 R3 [x:X1](f0 (x0 (f x))) maj0; Trivial. -Red; Auto. + Record emb (x y : A0) : Prop := + {X1 : Type; + R1 : X1 -> X1 -> Prop; + eqx : x = i0 X1 R1; + X2 : Type; + R2 : X2 -> X2 -> Prop; + eqy : y = i0 X2 R2; + W2 : WF X2 R2; + f : X1 -> X2; + fmorph : morphism X1 R1 X2 R2 f; + maj : X2; + majf : forall z : X1, R2 (f z) maj}. + + + Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z. +intros. +case H; intros. +case H0; intros. +generalize eqx0; clear eqx0. +elim eqy using eq_ind_r; intro. +case (inj _ _ _ _ eqx0); intros. +exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial. +red in |- *; auto. Defined. - Lemma ACC_emb: (X:Type)(R:X->X->Prop)(x:X)(ACC X R x) - ->(Y:Type)(S:Y->Y->Prop)(f:Y->X)(morphism Y S X R f) - ->((y:Y)(R (f y) x)) - ->(ACC A0 emb (i0 Y S)). -Induction 1; Intros. -Constructor; Intros. -Case H4; Intros. -Elim eqx using eqT_ind_r. -Case (inj X2 R2 Y S). -Apply sym_eqT; Assumption. - -Intros. -Apply H1 with y:=(f (x1 maj)) f:=[x:X1](f (x1 (f0 x))); Try Red; Auto. + Lemma ACC_emb : + forall (X : Type) (R : X -> X -> Prop) (x : X), + ACC X R x -> + forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X), + morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S). +simple induction 1; intros. +constructor; intros. +case H4; intros. +elim eqx using eq_ind_r. +case (inj X2 R2 Y S). +apply sym_eq; assumption. + +intros. +apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x))); + try red in |- *; auto. Defined. (* The embedding relation is well founded *) - Lemma WF_emb: (WF A0 emb). -Constructor; Intros. -Case H; Intros. -Elim eqx using eqT_ind_r. -Apply ACC_emb with X:=X2 R:=R2 x:=maj f:=f; Trivial. + 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). + Definition Omega : A0 := i0 A0 emb. Section Subsets. - Variable a: A0. + 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) }. + Record sub : Type := {witness : A0; emb_wit : emb witness a}. (* F is its image through i0 *) - Definition F : A0 := (i0 sub (Rof ? ? emb witness)). + 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. + Lemma F_emb_Omega : emb F Omega. +exists sub (Rof _ _ emb witness) A0 emb witness a; trivial. +exact WF_emb. -Red; Trivial. +red in |- *; trivial. -Exact emb_wit. +exact emb_wit. Defined. End Subsets. - Definition fsub: (a,b:A0)(emb a b)->(sub a)->(sub b):= - [_,_][H][x] - (Build_sub ? (witness ? x) (emb_trans ? ? ? (emb_wit ? x) H)). + 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. + Lemma F_morphism : morphism A0 emb A0 emb F. +red in |- *; intros. +exists + (sub x) + (Rof _ _ emb (witness x)) + (sub y) + (Rof _ _ emb (witness y)) + (fsub x y H) + (Build_sub _ x H); trivial. +apply WF_inverse_image. +exact WF_emb. + +unfold morphism, Rof, fsub in |- *; simpl in |- *; intros. +trivial. + +unfold Rof, fsub in |- *; simpl in |- *; intros. +apply emb_wit. Defined. @@ -174,23 +183,23 @@ Defined. - 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. + Lemma Omega_refl : emb Omega Omega. +exists A0 emb A0 emb F Omega; trivial. +exact WF_emb. -Exact F_morphism. +exact F_morphism. -Exact F_emb_Omega. +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. + Theorem Burali_Forti : False. +apply ACC_nonreflexive with A0 emb Omega. +apply WF_emb. -Exact Omega_refl. +exact Omega_refl. Defined. @@ -200,21 +209,23 @@ 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' *) + 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 : (X1:Type)(R1:X1->X1->Prop)(X2:Type)(R2:X2->X2->Prop) - (i0 X1 R1)==(i0 X2 R2) - ->(EXT f:X1->X2 | (morphism X1 R1 X2 R2 f)). -Intros. -Change Cases (i0 X1 R1) (i0 X2 R2) of - (i0 x1 r1) (i0 x2 r2) => (EXT f | (morphism x1 r1 x2 r2 f)) - end. -Case H; Simpl. -Exists [x:X1]x. -Red; Trivial. + Lemma inj : + forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type) + (R2 : X2 -> X2 -> Prop), + i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f. +intros. +change + match i0 X1 R1, i0 X2 R2 with + | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f + end in |- *. +case H; simpl in |- *. +exists (fun x : X1 => x). +red in |- *; trivial. Defined. (* The following command raises 'Error: Universe Inconsistency'. @@ -223,5 +234,4 @@ Defined. with the constraint j >= i in the paradox. *) - Definition Paradox: False := (Burali_Forti A0 i0 inj). - + 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 c4eef34b..6cd04349 100644 --- a/test-suite/failure/universes-sections1.v +++ b/test-suite/failure/universes-sections1.v @@ -2,7 +2,7 @@ Section A. Definition Type2 := Type. - Definition Type1 := Type : Type2. + Definition Type1 : Type2 := Type. End A. -Definition Inconsistency := Type2 : Type1. +Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v index 1872dac1..98fdbc0d 100644 --- a/test-suite/failure/universes-sections2.v +++ b/test-suite/failure/universes-sections2.v @@ -3,8 +3,8 @@ Definition Type2 := Type. Section A. - Local Type1 := Type : Type2. + Let Type1 : Type2 := Type. Definition Type1' := Type1. End A. -Definition Inconsistency := Type2 : Type1'. +Definition Inconsistency : Type1' := Type2. diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v index 6fada6f1..938c29b8 100644 --- a/test-suite/failure/universes.v +++ b/test-suite/failure/universes.v @@ -1,3 +1,3 @@ Definition Type2 := Type. -Definition Type1 := Type : Type2. -Definition Inconsistency := Type2 : Type1. +Definition Type1 : Type2 := Type. +Definition Inconsistency : Type1 := Type2. diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v index a6c8ba43..e74de70f 100644 --- a/test-suite/failure/universes2.v +++ b/test-suite/failure/universes2.v @@ -1,5 +1,4 @@ (* Example submitted by Randy Pollack *) -Parameter K: (T:Type)T->T. -Check (K ((T:Type)T->T) K). -(* Universe Inconsistency *) +Parameter K : forall T : Type, T -> T. +Check (K (forall T : Type, T -> T) K). |