|
Unset Strict Universe Declaration.
Module withoutpoly.
Inductive empty :=.
Inductive emptyt : Type :=.
Inductive singleton : Type :=
single.
Inductive singletoninfo : Type :=
singleinfo : unit -> singletoninfo.
Inductive singletonset : Set :=
singleset.
Inductive singletonnoninfo : Type :=
singlenoninfo : empty -> singletonnoninfo.
Inductive singletoninfononinfo : Prop :=
singleinfononinfo : unit -> singletoninfononinfo.
Inductive bool : Type :=
| true | false.
Inductive smashedbool : Prop :=
| trueP | falseP.
End withoutpoly.
Set Universe Polymorphism.
Inductive empty :=.
Inductive emptyt : Type :=.
Inductive singleton : Type :=
single.
Inductive singletoninfo : Type :=
singleinfo : unit -> singletoninfo.
Inductive singletonset : Set :=
singleset.
Inductive singletonnoninfo : Type :=
singlenoninfo : empty -> singletonnoninfo.
Inductive singletoninfononinfo : Prop :=
singleinfononinfo : unit -> singletoninfononinfo.
Inductive bool : Type :=
| true | false.
Inductive smashedbool : Prop :=
| trueP | falseP.
Section foo.
Let T := Type.
Inductive polybool : T :=
| trueT | falseT.
End foo.
Inductive list (A: Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.
Module ftypSetSet.
Inductive ftyp : Type :=
| Funit : ftyp
| Ffun : list ftyp -> ftyp
| Fref : area -> ftyp
with area : Type :=
| Stored : ftyp -> area
.
End ftypSetSet.
Module ftypSetProp.
Inductive ftyp : Type :=
| Funit : ftyp
| Ffun : list ftyp -> ftyp
| Fref : area -> ftyp
with area : Type :=
| Stored : (* ftyp -> *)area
.
End ftypSetProp.
Module ftypSetSetForced.
Inductive ftyp : Type :=
| Funit : ftyp
| Ffun : list ftyp -> ftyp
| Fref : area -> ftyp
with area : Set (* Type *) :=
| Stored : (* ftyp -> *)area
.
End ftypSetSetForced.
Unset Universe Polymorphism.
Set Printing Universes.
Module Easy.
Polymorphic Inductive prod (A : Type) (B : Type) : Type :=
pair : A -> B -> prod A B.
Check prod nat nat.
Print Universes.
Polymorphic Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
Print sum.
Check (sum nat nat).
End Easy.
Section Hierarchy.
Definition Type3 := Type.
Definition Type2 := Type : Type3.
Definition Type1 := Type : Type2.
Definition id1 := ((forall A : Type1, A) : Type2).
Definition id2 := ((forall A : Type2, A) : Type3).
Definition id1' := ((forall A : Type1, A) : Type3).
Fail Definition id1impred := ((forall A : Type1, A) : Type1).
End Hierarchy.
Section structures.
Record hypo : Type := mkhypo {
hypo_type : Type;
hypo_proof : hypo_type
}.
Definition typehypo (A : Type) : hypo := {| hypo_proof := A |}.
Polymorphic Record dyn : Type :=
mkdyn {
dyn_type : Type;
dyn_proof : dyn_type
}.
Definition monotypedyn (A : Type) : dyn := {| dyn_proof := A |}.
Polymorphic Definition typedyn (A : Type) : dyn := {| dyn_proof := A |}.
Definition atypedyn : dyn := typedyn Type.
Definition projdyn := dyn_type atypedyn.
Definition nested := {| dyn_type := dyn; dyn_proof := atypedyn |}.
Definition nested2 := {| dyn_type := dyn; dyn_proof := nested |}.
Definition projnested2 := dyn_type nested2.
Polymorphic Definition nest (d : dyn) := {| dyn_proof := d |}.
Polymorphic Definition twoprojs (d : dyn) := dyn_proof d = dyn_proof d.
End structures.
Module binders.
Definition mynat@{|} := nat.
Definition foo@{i j | i < j, i < j} (A : Type@{i}) : Type@{j}.
exact A.
Defined.
Polymorphic Lemma hidden_strict_type : Type.
Proof.
exact Type.
Qed.
Check hidden_strict_type@{_}.
Fail Check hidden_strict_type@{Set}.
Fail Definition morec@{i j|} (A : Type@{i}) : Type@{j} := A.
(* By default constraints are extensible *)
Polymorphic Definition morec@{i j} (A : Type@{i}) : Type@{j} := A.
Check morec@{_ _}.
(* Handled in proofs as well *)
Lemma bar@{i j | } : Type@{i}.
exact Type@{j}.
Fail Defined.
Abort.
Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat.
Lemma bar@{i j| i < j} : Type@{j}.
Proof.
exact Type@{i}.
Qed.
Lemma barext@{i j|+} : Type@{j}.
Proof.
exact Type@{i}.
Qed.
Monomorphic Universe M.
Fail Definition with_mono@{u|} : Type@{M} := Type@{u}.
Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
End binders.
Section cats.
Local Set Universe Polymorphism.
Require Import Utf8.
Definition fibration (A : Type) := A -> Type.
Definition Hom (A : Type) := A -> A -> Type.
Record sigma (A : Type) (P : fibration A) :=
{ proj1 : A; proj2 : P proj1} .
Class Identity {A} (M : Hom A) :=
identity : ∀ x, M x x.
Class Inverse {A} (M : Hom A) :=
inverse : ∀ x y:A, M x y -> M y x.
Class Composition {A} (M : Hom A) :=
composition : ∀ {x y z:A}, M x y -> M y z -> M x z.
Notation "g ° f" := (composition f g) (at level 50).
Class Equivalence T (Eq : Hom T):=
{
Equivalence_Identity :> Identity Eq ;
Equivalence_Inverse :> Inverse Eq ;
Equivalence_Composition :> Composition Eq
}.
Class EquivalenceType (T : Type) : Type :=
{
m2: Hom T;
equiv_struct :> Equivalence T m2 }.
Polymorphic Record cat (T : Type) :=
{ cat_hom : Hom T;
cat_equiv : forall x y, EquivalenceType (cat_hom x y) }.
Definition catType := sigma Type cat.
Notation "[ T ]" := (proj1 T).
Require Import Program.
Program Definition small_cat : cat Empty_set :=
{| cat_hom x y := unit |}.
Next Obligation.
refine ({|m2:=fun x y => True|}).
constructor; red; intros; trivial.
Defined.
Record iso (T U : Set) :=
{ f : T -> U;
g : U -> T }.
Program Definition Set_cat : cat Set :=
{| cat_hom := iso |}.
Next Obligation.
refine ({|m2:=fun x y => True|}).
constructor; red; intros; trivial.
Defined.
Record isoT (T U : Type) :=
{ isoT_f : T -> U;
isoT_g : U -> T }.
Program Definition Type_cat : cat Type :=
{| cat_hom := isoT |}.
Next Obligation.
refine ({|m2:=fun x y => True|}).
constructor; red; intros; trivial.
Defined.
Polymorphic Record cat1 (T : Type) :=
{ cat1_car : Type;
cat1_hom : Hom cat1_car;
cat1_hom_cat : forall x y, cat (cat1_hom x y) }.
End cats.
Polymorphic Definition id {A : Type} (a : A) : A := a.
Definition typeid := (@id Type).
Fail Check (Prop : Set).
Fail Check (Set : Set).
Check (Set : Type).
Check (Prop : Type).
Definition setType := ltac:(let t := type of Set in exact t).
Definition foo (A : Prop) := A.
Fail Check foo Set.
Check fun A => foo A.
Fail Check fun A : Type => foo A.
Check fun A : Prop => foo A.
Fail Definition bar := fun A : Set => foo A.
Fail Check (let A := Type in foo (id A)).
Definition fooS (A : Set) := A.
Check (let A := nat in fooS (id A)).
Fail Check (let A := Set in fooS (id A)).
Fail Check (let A := Prop in fooS (id A)).
(* Some tests of sort-polymorphisme *)
Section S.
Polymorphic Variable A:Type.
(*
Definition f (B:Type) := (A * B)%type.
*)
Polymorphic Inductive I (B:Type) : Type := prod : A->B->I B.
Check I nat.
End S.
(*
Check f nat nat : Set.
*)
Definition foo' := I nat nat.
Print Universes. Print foo. Set Printing Universes. Print foo.
(* Polymorphic axioms: *)
Polymorphic Axiom funext : forall (A B : Type) (f g : A -> B),
(forall x, f x = g x) -> f = g.
(* Check @funext. *)
(* Check funext. *)
Polymorphic Definition fun_ext (A B : Type) :=
forall (f g : A -> B),
(forall x, f x = g x) -> f = g.
Polymorphic Class Funext A B := extensional : fun_ext A B.
Section foo2.
Context `{forall A B, Funext A B}.
Print Universes.
End foo2.
Module eta.
Set Universe Polymorphism.
Set Printing Universes.
Axiom admit : forall A, A.
Record R := {O : Type}.
Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}.
Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
Definition RLRL' : forall x : R, RL x = RL (RL x).
intros. apply eq_refl.
Qed.
End eta.
Module Hurkens'.
Require Import Hurkens.
Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
Type)) eq_refl.
End Hurkens'.
Module Anonymous.
Set Universe Polymorphism.
Definition defaultid := (fun x => x) : Type -> Type.
Definition collapseid := defaultid@{_ _}.
Check collapseid@{_}.
Definition anonid := (fun x => x) : Type -> Type@{_}.
Check anonid@{_}.
Definition defaultalg := (fun x : Type => x) (Type : Type).
Definition usedefaultalg := defaultalg@{_ _ _}.
Check usedefaultalg@{_ _}.
Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
Check anonalg@{_ _}.
Definition unrelated@{i j} := nat.
Definition useunrelated := unrelated@{_ _}.
Check useunrelated@{_ _}.
Definition inthemiddle@{i j k} :=
let _ := defaultid@{i j} in
anonalg@{k j}.
(* i <= j < k *)
Definition collapsethemiddle := inthemiddle@{i _ j}.
Check collapsethemiddle@{_ _}.
End Anonymous.
Module Restrict.
(* Universes which don't appear in the term should be pruned, unless they have names *)
Set Universe Polymorphism.
Ltac exact0 := let x := constr:(Type) in exact 0.
Definition dummy_pruned@{} : nat := ltac:(exact0).
Definition named_not_pruned@{u} : nat := 0.
Check named_not_pruned@{_}.
Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
Check named_not_pruned_nonstrict@{_}.
Lemma lemma_restrict_poly@{} : nat.
Proof. exact0. Defined.
Unset Universe Polymorphism.
Lemma lemma_restrict_mono_qed@{} : nat.
Proof. exact0. Qed.
Lemma lemma_restrict_abstract@{} : nat.
Proof. abstract exact0. Qed.
End Restrict.
Module F.
Context {A B : Type}.
Definition foo : Type := B.
End F.
Set Universe Polymorphism.
Cumulative Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
Section test_letin_subtyping.
Universe i j k i' j' k'.
Constraint j < j'.
Context (W : Type) (X : box@{i j k} W).
Definition Y := X : box@{i' j' k'} W.
Universe i1 j1 k1 i2 j2 k2.
Constraint i1 < i2.
Constraint k2 < k1.
Context (V : Type).
Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
Proof.
Set Printing All. Set Printing Universes.
cbv.
reflexivity.
Qed.
End test_letin_subtyping.
Module ObligationRegression.
(** Test for a regression encountered when fixing obligations for
stronger restriction of universe context. *)
Require Import CMorphisms.
Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}.
End ObligationRegression.
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
