1 files changed, 374 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
new file mode 100644
index 00000000..1449f242
--- /dev/null
+++ b/test-suite/bugs/closed/4089.v
@@ -0,0 +1,374 @@
+Require Import TestSuite.admit.
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Open Scope type_scope.
+
+Global Set Universe Polymorphism.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+
+Ltac rapply p :=
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
+
+Local Unset Elimination Schemes.
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Ltac transitivity x := etransitivity x.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Definition paths_rect := paths_ind.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Local Open Scope path_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_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.
+
+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 apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : f == g
+  := fun x => match h with idpath => 1 end.
+
+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}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Arguments eisadj {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Bind Scope equiv_scope with Equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+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 ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+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_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ q
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+  := match r with idpath => 1 end.
+Module Export Equivalences.
+
+Generalizable Variables A B C f g.
+
+Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  BuildIsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+
+Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.
+
+Arguments equiv_idmap {A} , A.
+
+Notation "1" := equiv_idmap : equiv_scope.
+
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000
+  := BuildIsEquiv A C (compose g f)
+    (compose f^-1 g^-1)
+    (fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
+    (fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
+    (fun a =>
+      (whiskerL _ (eisadj g (f a))) @
+      (ap_pp g _ _)^ @
+      ap02 g
+      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
+        (ap_compose f^-1 f _ @@ eisadj f a) @
+        (ap_pp f _ _)^
+      ) @
+      (ap_compose f g _)^
+    ).
+
+Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
+  `{IsEquiv B C g} `{IsEquiv A B f}
+  : A <~> C
+  := BuildEquiv A C (compose g f) _.
+
+Global Instance transitive_equiv : Transitive Equiv | 0 :=
+  fun _ _ _ f g => equiv_compose g f.
+
+Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
+admit.
+Defined.
+
+Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.
+
+End Equivalences.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z').
+admit.
+Defined.
+
+Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
+: IsEquiv (path_prod_uncurried z z') | 0.
+admit.
+Defined.
+
+Definition equiv_path_prod {A B : Type} (z z' : A * B)
+  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
+  := BuildEquiv _ _ (path_prod_uncurried z z') _.
+
+Generalizable Variables X A B C f g n.
+
+Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) (g : forall a, P a -> Q (f a))
+: sigT P -> sigT Q
+  := fun u => (f u.1 ; g u.1 u.2).
+
+Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: IsEquiv (functor_sigma f g) | 1000.
+admit.
+Defined.
+
+Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) `{IsEquiv A B f}
+           (g : forall a, P a -> Q (f a))
+           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: sigT P <~> sigT Q
+  := BuildEquiv _ _ (functor_sigma f g) _.
+
+Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
+           (f : A <~> B)
+           (g : forall a, P a <~> Q (f a))
+: sigT P <~> sigT Q
+  := equiv_functor_sigma f g.
+
+Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
+           (g : forall a, P a <~> Q a)
+: sigT P <~> sigT Q
+  := equiv_functor_sigma' 1 g.
+
+Definition Bip : Type := { C : Type &  C * C }.
+
+Definition BipMor (X Y : Bip) : Type :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) =>
+    { f : C -> D & (f c0 = d0) * (f c1 = d1) }
+  end.
+
+Definition bipmor2map {X Y : Bip} : BipMor X Y -> X.1 -> Y.1 :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) => fun i =>
+    match i with (f;_) => f end
+  end.
+
+Definition bipidmor {X : Bip} : BipMor X X :=
+  match X with (C;(c0,c1)) => (idmap; (1, 1)) end.
+
+Definition bipcompmor {X Y Z : Bip} : BipMor X Y -> BipMor Y Z -> BipMor X Z :=
+  match X, Y, Z with (C;(c0,c1)), (D;(d0,d1)), (E;(e0,e1)) => fun i j =>
+    match i, j with (f;(f0,f1)), (g;(g0,g1)) =>
+      (g o f; (ap g f0 @ g0, ap g f1 @ g1))
+    end
+  end.
+
+Definition isbipequiv {X Y : Bip} (i : BipMor X Y) : Type :=
+  { l : BipMor Y X & bipcompmor i l = bipidmor } *
+  { r : BipMor Y X & bipcompmor r i = bipidmor }.
+
+Lemma bipequivEQequiv : forall {X Y : Bip} (i : BipMor X Y),
+  isbipequiv i <~> IsEquiv (bipmor2map i).
+Proof.
+assert (equivcompmor : forall {X Y : Bip} (i : BipMor X Y) j,
+(bipcompmor i j = bipidmor) <~> Unit).
+  intros; set (U := X); set (V := Y); destruct X as [C [c0 c1]], Y as [D [d0 d1]].
+  transitivity { n : (bipcompmor i j).1 = (@bipidmor U).1 &
+  (bipcompmor i j).2 = transport (fun h => (h c0 = c0) * (h c1 = c1)) n^ (@bipidmor U).2}.
+    admit.
+  destruct i as [f [f0 f1]]; destruct j as [g [g0 g1]].
+
+  transitivity { n : g o f = idmap & (ap g f0 @ g0 = apD10 n c0 @ 1) *
+  (ap g f1 @ g1 = apD10 n c1 @ 1)}.
+    apply equiv_functor_sigma_id; intro n.
+    assert (Ggen : forall (h0 h1 : C -> C) (p : h0 = h1) u0 u1 v0 v1,
+    ((u0, u1) = transport (fun h => (h c0 = c0) * (h c1 = c1)) p^ (v0, v1)) <~>
+    (u0 = apD10 p c0 @ v0) * (u1 = apD10 p c1 @ v1)).
+      induction p; intros; simpl; rewrite !concat_1p; apply symmetry.
+      by apply (equiv_path_prod (u0,u1) (v0,v1)).
+    rapply Ggen.
+    pose (@paths C).
+    Check (@paths C).
+    Undo.
+    Check (@paths C). (* Toplevel input, characters 0-17:
+Error: Illegal application:
+The term "@paths" of type "forall A : Type, A -> A -> Type"
+cannot be applied to the term
+ "C" : "Type"
+This term has type "Type@{Top.892}" which should be coercible to
+ "Type@{Top.882}".
+*)