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/closed/HoTT_coq_118.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_118.v (limited to 'test-suite/bugs/closed/HoTT_coq_118.v') diff --git a/test-suite/bugs/closed/HoTT_coq_118.v b/test-suite/bugs/closed/HoTT_coq_118.v new file mode 100644 index 00000000..14ad0e49 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_118.v @@ -0,0 +1,35 @@ +(* File reduced by coq-bug-finder from original input, then from 5631 lines to 557 lines, then from 526 lines to 181 lines, then from 189 lines to 154 lines, then from 153 lines to 107 lines, then from 97 lines to 56 lines, then from 50 lines to 37 lines *) +Generalizable All Variables. +Set Universe Polymorphism. +Definition admit {T} : T. +Admitted. +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (@paths _ x y) : type_scope. +Class Contr_internal (A : Type) := BuildContr { center : A }. +Arguments center A {_}. +Instance contr_paths_contr `{Contr_internal A} (x y : A) : Contr_internal (x = y) := admit. +Inductive Unit : Set := tt. +Instance contr_unit : Contr_internal Unit | 0 := admit. +Record PreCategory := { morphism : Type }. +Class IsIsomorphism {C : PreCategory} (m : morphism C) := { left_inverse : m = m }. +Definition indiscrete_category : PreCategory := @Build_PreCategory Unit. +Goal forall (X : Type) (_ : forall x y : X, Contr_internal (@paths X x y)) (s : X), + @IsIsomorphism indiscrete_category tt -> True. +Proof. + intros X H s [p]. + simpl in *. + assert (idpath = p). + clear. + assert (H : forall p : tt = tt, idpath = p) by (intro; exact (center _)). + clear H. + exact (center _). + (* Toplevel input, characters 15-32: +Error: +Unable to satisfy the following constraints: +In environment: +p : tt = tt + +?46 : "Contr_internal (idpath = p)" + *) -- cgit v1.2.3