aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2015-02-27 14:01:41 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-02-27 14:01:41 +0100
commitdbdf0648f4588d812a20ea4ba7d3e866f024073c (patch)
tree8bcb445586154a99b70b17fd9ca4b87e3cd0252b /test-suite
parent7012d65f71752a89cded69d6c2e7045f3a7cadde (diff)
Add test-suite file for #3649.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/3649.v57
1 files changed, 57 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
new file mode 100644
index 000000000..06188e7b1
--- /dev/null
+++ b/test-suite/bugs/closed/3649.v
@@ -0,0 +1,57 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
+ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y" (at level 70, no associativity).
+Open Scope type_scope.
+Axiom admit : forall {T}, T.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Reserved Infix "o" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Ltac constr_eq a b := let test := constr:(@idpath _ _ : a = b) in idtac.
+Global Set Primitive Projections.
+Delimit Scope morphism_scope with morphism.
+Record PreCategory :=
+ { object :> Type;
+ morphism : object -> object -> Type;
+
+ identity : forall x, morphism x x;
+ compose : forall s d d',
+ morphism d d'
+ -> morphism s d
+ -> morphism s d'
+ where "f 'o' g" := (compose f g) }.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+ { object_of :> C -> D;
+ morphism_of : forall s d, morphism C s d
+ -> morphism D (object_of s) (object_of d) }.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+ { morphism_inverse : morphism C d s }.
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Definition composeT C D (F F' F'' : Functor C D) (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
+: NaturalTransformation F F''.
+ exact admit.
+Defined.
+Definition functor_category (C D : PreCategory) : PreCategory.
+ exact (@Build_PreCategory (Functor C D)
+ (@NaturalTransformation C D)
+ admit
+ (@composeT C D)).
+Defined.
+Goal forall (C D : PreCategory) (G G' : Functor C D)
+ (T : @NaturalTransformation C D G G')
+ (H : @IsIsomorphism (@functor_category C D) G G' T)
+ (x : C),
+ @paths (morphism D (G x) (G x))
+ (@compose D (G x) (G' x) (G x)
+ ((@morphism_inverse (@functor_category C D) G G' T H) x)
+ (T x)) (@identity D (G x)).
+ intros.
+ (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
+ let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
+ let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
+ progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). \ No newline at end of file