diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/HoTT_coq_091.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_091.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_091.v | 191 |
1 files changed, 191 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_091.v b/test-suite/bugs/closed/HoTT_coq_091.v new file mode 100644 index 00000000..1e4497e7 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_091.v @@ -0,0 +1,191 @@ +Set Implicit Arguments. + +Set Printing Universes. + +Set Asymmetric Patterns. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Arguments paths_ind [A] a P f y p. +Arguments paths_rec [A] a P f y p. +Arguments paths_rect [A] a P f y p. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Arguments ap {A B} f {x y} p : simpl nomatch. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +(** A typeclass that includes the data making [f] into an adjoint equivalence. *) +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B} f {_} _. +Arguments eissect {A B} f {_} _. +Arguments eisadj {A B} f {_} _. + + +Inductive type_eq (A : Type) : Type -> Type := +| type_eq_refl : type_eq A A +| type_eq_impossible : False -> forall B : Type, type_eq A B. + +Definition type_eq_sym {A B} (p : type_eq A B) : type_eq B A + := match p in (type_eq _ B) return (type_eq B A) with + | type_eq_refl => type_eq_refl _ + | type_eq_impossible f B => type_eq_impossible _ f A + end. + +Definition type_eq_sym_type_eq_sym {A B} (p : type_eq A B) : type_eq_sym (type_eq_sym p) = p + := match p as p return type_eq_sym (type_eq_sym p) = p with + | type_eq_refl => idpath + | type_eq_impossible f _ => idpath + end. + +Module Type LiftT. + Section local. + Let type_cast_up_type : Type. + Proof. + let U0 := constr:(Type) in + let U1 := constr:(Type) in + let unif := constr:(U0 : U1) in + exact (forall T : U0, { T' : U1 & type_eq T' T }). + Defined. + + Axiom type_cast_up : type_cast_up_type. + End local. + + Definition Lift (T : Type) := projT1 (type_cast_up T). + Definition lift {T} : T -> Lift T + := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with + | type_eq_refl => fun x => x + | type_eq_impossible bad _ => match bad with end + end. + Section equiv. + Definition lower' {T} : Lift T -> T + := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with + | type_eq_refl => fun x => x + | type_eq_impossible bad _ => match bad with end + end. + Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x. + Proof. + unfold lower', lift. + destruct (projT2 (type_cast_up T)) as [|[]]. + reflexivity. + Defined. + Definition lower_lift {T} (x : T) : lower' (lift x) = x. + Proof. + unfold lower', lift, Lift in *. + destruct (type_cast_up T) as [T' p]; simpl. + let y := match goal with |- ?y => constr:(y) end in + let P := match (eval pattern p in y) with ?f p => constr:(f) end in + apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *. + generalize (type_eq_sym p); intro p'; clear p. + destruct p' as [|[]]; simpl. + reflexivity. + Defined. + + Global Instance isequiv_lift A : IsEquiv (@lift A). + Proof. + refine (@BuildIsEquiv + _ _ + lift lower' + lift_lower + lower_lift + _). + compute. + intro x. + destruct (type_cast_up A) as [T' p]. + let y := match goal with |- ?y => constr:(y) end in + let P := match (eval pattern p in y) with ?f p => constr:(f) end in + apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *. + generalize (type_eq_sym p); intro p'; clear p. + destruct p' as [|[]]; simpl. + reflexivity. + Defined. + End equiv. + Definition lower {A} := (@equiv_inv _ _ (@lift A) _). +End LiftT. + +Module Lift : LiftT. + Section local. + Let type_cast_up_type : Type. + Proof. + let U0 := constr:(Type) in + let U1 := constr:(Type) in + let unif := constr:(U0 : U1) in + exact (forall T : U0, { T' : U1 & type_eq T' T }). + Defined. + + Definition type_cast_up : type_cast_up_type + := fun T => existT (fun T' => type_eq T' T) T (type_eq_refl _). + End local. + + Definition Lift (T : Type) := projT1 (type_cast_up T). + Definition lift {T} : T -> Lift T + := match projT2 (type_cast_up T) in (type_eq _ T') return T' -> Lift T with + | type_eq_refl => fun x => x + | type_eq_impossible bad _ => match bad with end + end. + Section equiv. + Definition lower' {T} : Lift T -> T + := match projT2 (type_cast_up T) in (type_eq _ T') return Lift T -> T' with + | type_eq_refl => fun x => x + | type_eq_impossible bad _ => match bad with end + end. + Definition lift_lower {T} (x : Lift T) : lift (lower' x) = x. + Proof. + unfold lower', lift. + destruct (projT2 (type_cast_up T)) as [|[]]. + reflexivity. + Defined. + Definition lower_lift {T} (x : T) : lower' (lift x) = x. + Proof. + unfold lower', lift, Lift in *. + destruct (type_cast_up T) as [T' p]; simpl. + let y := match goal with |- ?y => constr:(y) end in + let P := match (eval pattern p in y) with ?f p => constr:(f) end in + apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *. + generalize (type_eq_sym p); intro p'; clear p. + destruct p' as [|[]]; simpl. + reflexivity. + Defined. + + + Global Instance isequiv_lift A : IsEquiv (@lift A). + Proof. + refine (@BuildIsEquiv + _ _ + lift lower' + lift_lower + lower_lift + _). + compute. + intro x. + destruct (type_cast_up A) as [T' p]. + let y := match goal with |- ?y => constr:(y) end in + let P := match (eval pattern p in y) with ?f p => constr:(f) end in + apply (@transport _ P _ _ (type_eq_sym_type_eq_sym p)); simpl in *. + generalize (type_eq_sym p); intro p'; clear p. + destruct p' as [|[]]; simpl. + reflexivity. + Defined. + End equiv. + Definition lower {A} := (@equiv_inv _ _ (@lift A) _). +End Lift. +(* Toplevel input, characters 15-24: +Anomaly: Invalid argument: enforce_eq_instances called with instances of different lengths. +Please report. *) |