coq
coq copied to clipboard
HoTT
Anomaly: Uncaught exception Not_found(_). Please report.
The code at https://github.com/JasonGross/HoTT-categories/blob/coq-bug-004/theories/NaturalTransformation/Composition/Functorial.v#L33 gives
Toplevel input, characters 0-323:
Anomaly: Uncaught exception Not_found(_). Please report.
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "toplevel/command.ml", line 175, characters 4-86
frame @ file "toplevel/command.ml", line 100, characters 16-89
frame @ file "pretyping/pretyping.ml", line 780, characters 2-70
frame @ file "pretyping/pretyping.ml", line 711, characters 3-36
frame @ file "pretyping/pretyping.ml", line 438, characters 17-49
rame @ file "pretyping/pretyping.ml", line 417, characters 13-52
frame @ file "pretyping/pretyping.ml", line 455, characters 15-60
frame @ file "pretyping/pretyping.ml", line 455, characters 15-60
frame @ file "pretyping/pretyping.ml", line 455, characters 15-60
frame @ file "pretyping/pretyping.ml", line 455, characters 15-60
frame @ file "pretyping/pretyping.ml", line 455, characters 15-60
frame @ file "pretyping/evarutil.ml", line 34, characters 17-30
raise @ unknown
frame @ file "pretyping/coercion.ml", line 466, characters 6-81
raise @ unknown
frame @ file "pretyping/coercion.ml", line 431, characters 7-34
frame @ file "pretyping/evarconv.ml", line 950, characters 8-42
frame @ file "pretyping/evarconv.ml", line 159, characters 8-17
frame @ file "pretyping/evarconv.ml", line 226, characters 12-63
frame @ file "pretyping/evarconv.ml", line 171, characters 15-26
frame @ file "pretyping/evarconv.ml", line 172, characters 33-41
frame @ file "pretyping/evarconv.ml", line 137, characters 12-18
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1404, characters 10-69
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1306, characters 22-71
frame @ file "pretyping/evarsolve.ml", line 1283, characters 13-32
frame @ file "pretyping/termops.ml", line 381, characters 15-38
frame @ file "pretyping/termops.ml", line 385, characters 16-34
frame @ file "array.ml", line 80, characters 21-40
frame @ file "pretyping/termops.ml", line 385, characters 16-34
frame @ file "array.ml", line 80, characters 21-40
frame @ file "pretyping/evarsolve.ml", line 1231, characters 13-74
frame @ file "pretyping/evarsolve.ml", line 486, characters 4-797
frame @ file "pretyping/evarsolve.ml", line 494, characters 22-112
frame @ file "pretyping/evarsolve.ml", line 455, characters 12-62
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1329, characters 15-58
frame @ file "pretyping/evarsolve.ml", line 1050, characters 8-61
frame @ file "pretyping/evarconv.ml", line 137, characters 12-18
frame @ file "pretyping/evarconv.ml", line 159, characters 8-17
frame @ file "array.ml", line 80, characters 21-40
frame @ file "pretyping/termops.ml", line 385, characters 16-34
frame @ file "array.ml", line 80, characters 21-40
frame @ file "pretyping/evarsolve.ml", line 1231, characters 13-74
frame @ file "pretyping/evarsolve.ml", line 486, characters 4-797
frame @ file "pretyping/evarsolve.ml", line 494, characters 22-112
frame @ file "pretyping/evarsolve.ml", line 455, characters 12-62
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1329, characters 15-58
frame @ file "pretyping/evarsolve.ml", line 1050, characters 8-61
frame @ file "pretyping/evarconv.ml", line 137, characters 12-18
frame @ file "pretyping/evarconv.ml", line 159, characters 8-17
frame @ file "pretyping/evarconv.ml", line 226, characters 12-63
frame @ file "pretyping/evarconv.ml", line 171, characters 15-26
frame @ file "pretyping/evarconv.ml", line 172, characters 33-41
frame @ file "pretyping/evarconv.ml", line 137, characters 12-18
frame @ file "pretyping/evarconv.ml", line 159, characters 8-17
frame @ file "pretyping/evarconv.ml", line 226, characters 12-63
frame @ file "pretyping/evarconv.ml", line 171, characters 15-26
frame @ file "pretyping/evarconv.ml", line 172, characters 33-41
frame @ file "pretyping/evarconv.ml", line 137, characters 12-18
frame @ file "pretyping/evarconv.ml", line 159, characters 8-17
frame @ file "pretyping/evarconv.ml", line 226, characters 12-63
frame @ file "pretyping/evarconv.ml", line 171, characters 15-26
frame @ file "pretyping/evarconv.ml", line 172, characters 33-41
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1404, characters 10-69
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1029, characters 8-55
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 1010, characters 19-67
frame @ file "pretyping/evarsolve.ml", line 995, characters 5-62
frame @ file "pretyping/evarsolve.ml", line 358, characters 14-65
frame @ file "pretyping/evarsolve.ml", line 347, characters 52-77
raise @ unknown
frame @ file "pretyping/evarsolve.ml", line 123, characters 6-19
frame @ file "array.ml", line 73, characters 31-48
frame @ file "kernel/environ.ml", line 64, characters 2-34
raise @ file "kernel/term.ml", line 859, characters 26-35
This bug is still open in trunk-polyproj (and does not need -indices-matter). Here is a small reproducing test case:
(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines. *)
Set Implicit Arguments.
Set Universe Polymorphism.
Definition admit {T} : T.
Admitted.
Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope functor_scope with functor.
Delimit Scope natural_transformation_scope with natural_transformation.
Reserved Infix "o" (at level 40, left associativity).
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
:= match p with idpath => idpath end.
Record PreCategory :=
{
Object :> Type;
Morphism : Object -> Object -> Type;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g)
}.
Bind Scope category_scope with PreCategory.
Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
Infix "o" := Compose : morphism_scope.
Local Open Scope morphism_scope.
Record Functor (C D : PreCategory) :=
{
ObjectOf :> C -> D;
MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1)
}.
Bind Scope functor_scope with Functor.
Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
Definition ComposeFunctors C D E
(G : Functor D E) (F : Functor C D) : Functor C E
:= Build_Functor C E
(fun c => G (F c))
admit
admit.
Infix "o" := ComposeFunctors : functor_scope.
Record NaturalTransformation C D (F G : Functor C D) :=
{
ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
Commutes : forall s d (m : C.(Morphism) s d),
ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s
}.
Generalizable All Variables.
Section NTComposeT.
Variable C : PreCategory.
Variable D : PreCategory.
Variables F F' F'' : Functor C D.
Variable T' : NaturalTransformation F' F''.
Variable T : NaturalTransformation F F'.
Let CO := fun c => T' c o T c.
Definition NTComposeT_Commutes s d (m : Morphism C s d)
: CO d o MorphismOf F m = MorphismOf F'' m o CO s.
admit.
Defined.
Definition NTComposeT
: NaturalTransformation F F''
:= Build_NaturalTransformation F F''
(fun c => T' c o T c)
NTComposeT_Commutes.
End NTComposeT.
Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
(G : Functor C D)
:= Build_NaturalTransformation (F o G) (F' o G)
(fun c => T (G c))
admit.
Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
Notation "T 'o' U"
:= (@NTC_Composable_term _ _ T%natural_transformation U%natural_transformation _ _ _)
: natural_transformation_scope.
Local Open Scope natural_transformation_scope.
Lemma NTWhiskerR_CompositionOf C D
(F G H : Functor C D)
(T : NaturalTransformation G H)
(T' : NaturalTransformation F G) B (I : Functor B C)
: NTWhiskerR (NTComposeT T T') I = NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I).
admit.
Defined.
Definition FunctorCategory C D : PreCategory
:= @Build_PreCategory (Functor C D)
(NaturalTransformation (C := C) (D := D))
admit.
Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
Variable C : PreCategory.
Variable D : PreCategory.
Variable E : PreCategory.
Definition NTWhiskerR_Functorial (G : [C, D]%category)
: [[D, E], [C, E]]%category
:= Build_Functor
[C, D] [C, E]
(fun F => F o G)
(fun _ _ T => T o G)
(fun _ _ _ _ _ => inverse (NTWhiskerR_CompositionOf _ _ _)).
(* Anomaly: Uncaught exception Not_found(_). Please report. *)