diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/coqchk | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/coqchk')
-rw-r--r-- | test-suite/coqchk/bug_7539.v | 26 | ||||
-rw-r--r-- | test-suite/coqchk/cumulativity.v | 67 | ||||
-rw-r--r-- | test-suite/coqchk/include.v | 11 | ||||
-rw-r--r-- | test-suite/coqchk/primproj2.v | 10 | ||||
-rw-r--r-- | test-suite/coqchk/univ.v | 54 |
5 files changed, 168 insertions, 0 deletions
diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v new file mode 100644 index 00000000..74ebe929 --- /dev/null +++ b/test-suite/coqchk/bug_7539.v @@ -0,0 +1,26 @@ +Set Primitive Projections. + +CoInductive Stream : Type := Cons { tl : Stream }. + +Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream := + match n with + | O => s + | S m => Str_nth_tl m (tl s) + end. + +CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_tl : EqSt (tl s1) (tl s2); +}. + +Axiom EqSt_reflex : forall (s : Stream), EqSt s s. + +CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)). + +Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)). +Proof. +induction n. ++ intros; apply EqSt_reflex. ++ cbn; intros s; apply IHn. +Qed. + +Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl. diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v new file mode 100644 index 00000000..03468405 --- /dev/null +++ b/test-suite/coqchk/cumulativity.v @@ -0,0 +1,67 @@ +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +Inductive List (A: Type) := nil | cons : A -> List A -> List A. + +Section ListLift. + Universe i j. + + Constraint i < j. + + Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x. + +End ListLift. + +Lemma LiftL_Lem A (l : List A) : l = LiftL l. +Proof. reflexivity. Qed. + +Section ListLower. + Universe i j. + + Constraint i < j. + + Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x. + +End ListLower. + +Lemma LowerL_Lem@{i j|j<i+} (A : Type@{j}) (l : List@{i} A) : l = LowerL@{j i} l. +Proof. reflexivity. Qed. +(* +I disable these tests because cqochk can't process them when compiled with + ocaml-4.02.3+32bit and camlp5-4.16 which is the case for Travis! + + I have added this file (including the commented parts below) in + test-suite/success/cumulativity.v which doesn't run coqchk on them. +*) +(* Inductive Tp := tp : Type -> Tp. *) + +(* Section TpLift. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x. *) + +(* End TpLift. *) + +(* Lemma LiftC_Lem (t : Tp) : LiftTp t = t. *) +(* Proof. reflexivity. Qed. *) + +(* Section TpLower. *) +(* Universe i j. *) + +(* Constraint i < j. *) + +(* Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x. *) + +(* End TpLower. *) + + +(* Section subtyping_test. *) +(* Universe i j. *) +(* Constraint i < j. *) + +(* Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2. *) + +(* End subtyping_test. *) diff --git a/test-suite/coqchk/include.v b/test-suite/coqchk/include.v new file mode 100644 index 00000000..6232c1b8 --- /dev/null +++ b/test-suite/coqchk/include.v @@ -0,0 +1,11 @@ +(* See https://github.com/coq/coq/issues/5747 *) +Module Type S. +End S. + +Module N. +Inductive I := . +End N. + +Module M : S. + Include N. +End M. diff --git a/test-suite/coqchk/primproj2.v b/test-suite/coqchk/primproj2.v new file mode 100644 index 00000000..f73c627e --- /dev/null +++ b/test-suite/coqchk/primproj2.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +Record Pack (A : Type) := pack { unpack : A }. + +Definition p : Pack bool. +Proof. +refine (pack _ true). +Qed. + +Definition boom : unpack bool p = let u := unpack _ in u p := eq_refl. diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 84a4009d..21633861 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -33,3 +33,57 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) := (rank_injective : injective_in T natural D rank) (rank_onto : forall i, equivalent (less_than i n) (in_image T natural D rank i)). + +(* Constraints *) +Universes i j. +Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})). +Constraint i < j. +Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}). +Universes i' j'. +Constraint i' = j'. +Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})). +Inductive constraint4 : (Type -> Type) -> Type + := mk_constraint4 : let U1 := Type in + let U2 := Type in + constraint4 (fun x : U1 => (x : U2)). + +Module CMP_CON. + (* Comparison of opaque constants MUST be up to the universe graph. + See #6798. *) + Universe big. + + Polymorphic Lemma foo@{u} : Type@{big}. + Proof. exact Type@{u}. Qed. + + Universes U V. + + Definition yo : foo@{U} = foo@{V} := eq_refl. +End CMP_CON. + +Set Universe Polymorphism. + +Module POLY_SUBTYP. + + Module Type T. + Axiom foo : Type. + Parameter bar@{u v|u = v} : foo@{u}. + End T. + + Module M. + Axiom foo : Type. + Axiom bar@{u v|u = v} : foo@{v}. + End M. + + Module F (A:T). End F. + + Module X := F M. + +End POLY_SUBTYP. + +Module POLY_IND. + + Polymorphic Inductive ind@{u v | u < v} : Prop := . + + Polymorphic Definition cst@{u v | v < u} := Prop. + +End POLY_IND. |