From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/HoTT_coq_090.v | 187 ++++++++++++++++++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_090.v (limited to 'test-suite/bugs/closed/HoTT_coq_090.v') diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v new file mode 100644 index 00000000..5c704147 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_090.v @@ -0,0 +1,187 @@ +(** I'm not sure if this tests what I want it to test... *) +Set Implicit Arguments. +Set Universe Polymorphism. + +Notation idmap := (fun x => x). + +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 Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +(** 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 {_} _. + + +Record Equiv A B := BuildEquiv { + equiv_fun :> A -> B ; + equiv_isequiv :> IsEquiv equiv_fun +}. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +(** See above for the meaning of [simpl nomatch]. *) +Arguments concat {A x y z} p q : simpl nomatch. + +(** The inverse of a path. *) +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +(** Declaring this as [simpl nomatch] prevents the tactic [simpl] from expanding it out into [match] statements. We only want [inverse] to simplify when applied to an identity path. *) +Arguments inverse {A x y} p : simpl nomatch. + +(** Note that you can use the built-in Coq tactics [reflexivity] and [transitivity] when working with paths, but not [symmetry], because it is too smart for its own good. Instead, you can write [apply symmetry] or [eapply symmetry]. *) + +(** The identity path. *) +Notation "1" := idpath : path_scope. + +(** The composition of two paths. *) +Notation "p @ q" := (concat p q) (at level 20) : path_scope. + +(** The inverse of a path. *) +Notation "p ^" := (inverse p) (at level 3) : path_scope. + +(** An alternative notation which puts each path on its own line. Useful as a temporary device during proofs of equalities between very long composites; to turn it on inside a section, say [Open Scope long_path_scope]. *) +Notation "p @' q" := (concat p q) (at level 21, left associativity, + format "'[v' p '/' '@'' q ']'") : long_path_scope. + + +(** An important instance of [paths_rect] is that given any dependent type, one can _transport_ elements of instances of the type along equalities in the base. + + [transport P p u] transports [u : P x] to [P y] along [p : x = y]. *) +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. + +(** See above for the meaning of [simpl nomatch]. *) +Arguments transport {A} P {x y} p%path_scope u : simpl nomatch. + + + +Instance isequiv_path {A B : Type} (p : A = B) + : IsEquiv (transport (fun X:Type => X) p) | 0. +Proof. + refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); + admit. +Defined. + +Definition equiv_path (A B : Type) (p : A = B) : Equiv A B + := @BuildEquiv _ _ (transport (fun X:Type => X) p) _. + +Arguments equiv_path : clear implicits. + +Definition equiv_adjointify A B (f : A -> B) (g : B -> A) (r : Sect g f) (s : Sect f g) : Equiv A B. +Proof. + refine (@BuildEquiv A B f (@BuildIsEquiv A B f g r s _)). + admit. +Defined. + + +Set Printing Universes. + +Definition lift_id_type : Type. +Proof. + let U0 := constr:(Type) in + let U1 := constr:(Type) in + let unif := constr:(U0 : U1) in + exact (forall (A : Type) (B : Type), @paths U0 A B -> @paths U1 A B). +Defined. + +Definition lower_id_type : Type. +Proof. + let U0 := constr:(Type) in + let U1 := constr:(Type) in + let unif := constr:(U0 : U1) in + exact ((forall (A : Type) (B : Type), IsEquiv (equiv_path (A : U0) (B : U0))) + -> forall (A : Type) (B : Type), @paths U1 A B -> @paths U0 A B). +Defined. + +Definition lift_id : lift_id_type := + fun A B p => match p in @paths _ _ B return @paths Type (A : Type) (B : Type) with + | idpath => idpath + end. + +Definition lower_id : lower_id_type. +Proof. + intros ua A B p. + specialize (ua A B). + apply (@equiv_inv _ _ (equiv_path A B) _). + simpl. + pose (f := transport idmap p : A -> B). + pose (g := transport idmap p^ : B -> A). + refine (@equiv_adjointify + _ _ + f g + _ _); + subst f g; unfold transport, inverse; + clear ua; + [ intro x + | exact match p as p in (_ = B) return + (forall x : (A : Type), + @paths (* Top.904 *) + A + match + match + p in (paths _ a) + return (@paths (* Top.906 *) Type (* Top.900 *) a A) + with + | idpath => @idpath (* Top.906 *) Type (* Top.900 *) A + end in (paths _ a) return a + with + | idpath => match p in (paths _ a) return a with + | idpath => x + end + end x) + with + | idpath => fun _ => idpath + end ]. + + - pose proof (match p as p in (_ = B) return + (forall x : (B : Type), + match p in (_ = a) return (a : Type) with + | idpath => + match + match p in (_ = a) return (@paths Type (a : Type) (A : Type)) with + | idpath => idpath + end in (_ = a) return (a : Type) + with + | idpath => x + end + end = x) + with + | idpath => fun _ => idpath + end x) as p'. + admit. +Defined. +(* Error: Illegal application: +The term "paths (* Top.96 *)" of type + "forall A : Type (* Top.96 *), A -> A -> Type (* Top.96 *)" +cannot be applied to the terms + "Type (* Top.100 *)" : "Type (* Top.100+1 *)" + "a" : "Type (* Top.60 *)" + "A" : "Type (* Top.57 *)" +The 2nd term has type "Type (* Top.60 *)" which should be coercible to + "Type (* Top.100 *)". + *) -- cgit v1.2.3