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/opened/3754.v | 282 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 282 insertions(+) create mode 100644 test-suite/bugs/opened/3754.v (limited to 'test-suite/bugs/opened/3754.v') diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v new file mode 100644 index 00000000..c7441882 --- /dev/null +++ b/test-suite/bugs/opened/3754.v @@ -0,0 +1,282 @@ +(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) +(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 + coqtop version trunk (October 2014) *) + +Notation Type0 := Set. + +Notation idmap := (fun x => x). + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. + +Notation pr1 := projT1. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. + +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := + fun x => g (f x). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. +admit. +Defined. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p q) (at level 20) : path_scope. + +Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope. + +Notation "p @' q" := (concat p q) (at level 21, left associativity, + format "'[v' p '/' '@'' q ']'") : long_path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. +exact (match p with idpath => u end). +Defined. + +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. +exact (match p with idpath => idpath end). +Defined. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +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 {_} _. + +Record Equiv A B := BuildEquiv { + equiv_fun : A -> B ; + equiv_isequiv : IsEquiv equiv_fun +}. + +Coercion equiv_fun : Equiv >-> Funclass. + +Global Existing Instance equiv_isequiv. + +Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Local Open Scope path_scope. + +Definition concat_p1 {A : Type} {x y : A} (p : x = y) : + p @ 1 = p + := + match p with idpath => 1 end. + +Definition concat_1p {A : Type} {x y : A} (p : x = y) : + 1 @ p = p + := + match p with idpath => 1 end. + +Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + p @ (q @ r) = (p @ q) @ r := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + (p @ q) @ r = p @ (q @ r) := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : + r^ @ q = p -> q = r @ p. +admit. +Defined. + +Ltac with_rassoc tac := + repeat rewrite concat_pp_p; + tac; + + repeat rewrite concat_p_pp. + +Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp). + +Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A} + (r : w = f x) (p : x = y) (q : y = z) : + r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q). +admit. +Defined. + +Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : + ap (g o f) p = ap g (ap f p) + := + match p with idpath => 1 end. + +Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) : + (ap f q) @ (p y) = (p x) @ (ap g q) + := + match q with + | idpath => concat_1p _ @ ((concat_p1 _) ^) + end. + +Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) + {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) + : D x2 (p # y) (p # z) + := + match p with idpath => w end. +Local Open Scope equiv_scope. + +Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2) + : (transport (fun x => B x -> C) p f) y = f (p^ # y). +admit. +Defined. + +Definition transport_arrow_fromconst {A B : Type} {C : A -> Type} + {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B) + : (transport (fun x => B -> C x) p f) y = p # (f y). +admit. +Defined. + +Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) + : ap (transport (fun x => B x -> C) p f) q + @ transport_arrow_toconst p f y2 + = transport_arrow_toconst p f y1 + @ ap (fun y => f (p^ # y)) q. +admit. +Defined. + +Class Univalence. +Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B). +admit. +Defined. +Definition transport_path_universe + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A) + : transport (fun X:Type => X) (path_universe f) z = f z. +admit. +Defined. +Definition transport_path_universe_V `{Funext} + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) + : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z. +admit. +Defined. + +Ltac simpl_do_clear tac term := + let H := fresh in + assert (H := term); + simpl in H |- *; + tac H; + clear H. + +Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term. + +Global Instance Univalence_implies_Funext `{Univalence} : Funext. +Admitted. + +Section Factorization. + + Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)} + {A B : Type@{i}} {f : A -> B}. + + Record Factorization := + { intermediate : Type ; + factor1 : A -> intermediate ; + factor2 : intermediate -> B ; + fact_factors : factor2 o factor1 == f ; + inclass1 : class1 _ _ factor1 ; + inclass2 : class2 _ _ factor2 + }. + + Record PathFactorization {fact fact' : Factorization} := + { path_intermediate : intermediate fact <~> intermediate fact' ; + path_factor1 : path_intermediate o factor1 fact == factor1 fact' ; + path_factor2 : factor2 fact == factor2 fact' o path_intermediate ; + path_fact_factors : forall a, path_factor2 (factor1 fact a) + @ ap (factor2 fact') (path_factor1 a) + @ fact_factors fact' a + = fact_factors fact a + }. + Context `{Univalence} {fact fact' : Factorization} + (pf : @PathFactorization fact fact'). + + Let II := path_intermediate pf. + Let ff1 := path_factor1 pf. + Let ff2 := path_factor2 pf. +Local Definition II' : intermediate fact = intermediate fact'. +admit. +Defined. + + Local Definition fff' (a : A) + : (transportD2 (fun X => A -> X) (fun X => X -> B) + (fun X g h => {_ : forall a : A, h (g a) = f a & + {_ : class1 A X g & class2 X B h}}) + II' (factor1 fact) (factor2 fact) + (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a = + ap (transport (fun X => X -> B) II' (factor2 fact)) + (transport_arrow_fromconst II' (factor1 fact) a + @ transport_path_universe II (factor1 fact a) + @ ff1 a) + @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a) + @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a)) + @ ff2 (II^-1 (factor1 fact' a)) + @ ap (factor2 fact') (eisretr II (factor1 fact' a)) + @ fact_factors fact' a. + Proof. + + Open Scope long_path_scope. + + rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)). + + simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^) + (factor2 fact)). + rewrite <- ap_p_pp; rewrite_moveL_Mp_p. + Set Debug Tactic Unification. + Fail rewrite (concat_Ap ff2). -- cgit v1.2.3