aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-07-16 04:34:30 -0400
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-08-26 18:02:24 +0200
commitc70d5b27ad5872c74e20b6c997383fb4462a68dc (patch)
treeebd4bad1d86798d2d67cfb79a502105bf280787a
parent99861d4ba6cd07025bd2117c0539ffc113833b67 (diff)
Add a regression test for 3427
-rw-r--r--test-suite/bugs/closed/3427.v195
1 files changed, 195 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3427.v b/test-suite/bugs/closed/3427.v
new file mode 100644
index 000000000..8483a4ecf
--- /dev/null
+++ b/test-suite/bugs/closed/3427.v
@@ -0,0 +1,195 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 0 lines to 7171 lines, then from 7184 lines to 558 lines, then from 556 lines to 209 lines *)
+Generalizable All Variables.
+Set Universe Polymorphism.
+Notation Type0 := Set.
+Notation idmap := (fun x => x).
+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 where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x := match p with 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) : 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.
+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 := 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) : forall x, f x = g x := fun x => match h with idpath => idpath 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)
+ }.
+Record Equiv A B := BuildEquiv {
+ equiv_fun :> A -> B ;
+ equiv_isequiv :> IsEquiv equiv_fun
+ }.
+
+Delimit Scope equiv_scope with equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : 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.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+ := match n with
+ | 0 => trunc_S (trunc_S minus_two)
+ | S n' => trunc_S (nat_to_trunc_index n')
+ end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+ match n with
+ | minus_two => Contr_internal A
+ | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+ end.
+
+Notation minus_one:=(trunc_S minus_two).
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+ Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc minus_two).
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext :=
+ { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Definition concat_pV {A : Type} {x y : A} (p : x = y) :
+ p @ p^ = 1
+ :=
+ match p with idpath => 1 end.
+
+Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
+ p^ @ p = 1
+ :=
+ match p with idpath => 1 end.
+
+Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
+ p @ q # u = q # p # u :=
+ match q with idpath =>
+ match p with idpath => 1 end
+ end.
+
+Definition transport2 {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
+ (r : p = q) (z : P x)
+: p # z = q # z
+ := ap (fun p' => p' # z) r.
+
+Inductive Unit : Type0 :=
+ tt : Unit.
+
+Instance contr_unit : Contr Unit | 0 := let x := {|
+ center := tt;
+ contr := fun t : Unit => match t with tt => 1 end
+ |} in x.
+
+Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
+admit.
+Defined.
+
+Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+Definition Unit_hp:hProp:=(hp Unit _).
+
+Global Instance isequiv_ap_hproptype `{Funext} X Y : IsEquiv (@ap _ _ hproptype X Y).
+admit.
+Defined.
+
+Definition path_hprop `{Funext} X Y := (@ap _ _ hproptype X Y)^-1%equiv.
+
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Local Open Scope equiv_scope.
+
+Instance isequiv_path {A B : Type} (p : A = B)
+: IsEquiv (transport (fun X:Type => X) p) | 0
+ := BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^)
+ (fun b => ((transport_pp idmap p^ p b)^ @ transport2 idmap (concat_Vp p) b))
+ (fun a => ((transport_pp idmap p p^ a)^ @ transport2 idmap (concat_pV p) a))
+ (fun a => match p in _ = C return
+ (transport_pp idmap p^ p (transport idmap p a))^ @
+ transport2 idmap (concat_Vp p) (transport idmap p a) =
+ ap (transport idmap p) ((transport_pp idmap p p^ a) ^ @
+ transport2 idmap (concat_pV p) a) with idpath => 1 end).
+
+Definition equiv_path (A B : Type) (p : A = B) : A <~> B
+ := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
+
+Class Univalence := {
+ isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+ }.
+
+Section Univalence.
+ Context `{Univalence}.
+
+ Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
+ := (equiv_path A B)^-1 f.
+End Univalence.
+
+Local Inductive minus1Trunc (A :Type) : Type :=
+ min1 : A -> minus1Trunc A.
+
+Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0.
+admit.
+Defined.
+
+Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT P).
+
+Section AssumingUA.
+
+ Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
+ forall g h: Y -> Z, g o f = h o f -> g = h.
+ Context {X Y : hSet} (f : X -> Y) (Hisepi : isepi f).
+
+ Goal forall (X Y : hSet) (f : forall _ : setT X, setT Y),
+ let fib :=
+ fun y : setT Y =>
+ hp (@hexists (setT X) (fun x : setT X => @paths (setT Y) (f x) y))
+ (@minus1Trunc_is_prop
+ (@sigT (setT X) (fun x : setT X => @paths (setT Y) (f x) y))) in
+ forall (x : setT X) (_ : Univalence) (_ : Funext),
+ @paths hProp (fib (f x)) Unit_hp.
+ intros.
+
+ apply path_hprop.
+ simpl.
+ Set Printing Universes.
+ Set Printing All.
+ refine (path_universe_uncurried _).
+ Undo.
+ apply path_universe_uncurried. (* Toplevel input, characters 21-44:
+Error: Refiner was given an argument
+ "@path_universe_uncurried (* Top.425 Top.426 Top.427 Top.428 Top.429 *) X1
+ (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+ (fun x0 : setT (* Top.405 *) X0 =>
+ @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit
+ ?63" of type
+ "@paths (* Top.428 *) Type (* Top.425 *)
+ (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+ (fun x0 : setT (* Top.405 *) X0 =>
+ @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit"
+instead of
+ "@paths (* Top.413 *) Type (* Set *)
+ (@hexists (* Top.405 Top.404 Set Set *) (setT (* Top.405 *) X0)
+ (fun x0 : setT (* Top.405 *) X0 =>
+ @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit".
+ *)