From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/bugs/opened/3926.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 test-suite/bugs/opened/3926.v (limited to 'test-suite/bugs/opened/3926.v') diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v new file mode 100644 index 00000000..cfad7635 --- /dev/null +++ b/test-suite/bugs/opened/3926.v @@ -0,0 +1,30 @@ +Notation compose := (fun g f 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. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. +Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. +Local Open Scope equiv_scope. +Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. +Generalizable Variables A B C f g. +Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 + := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). +Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g + := Build_IsEquiv _ _ g (f ^-1). +Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 + := Build_IsEquiv B A f^-1 f. +Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} + `{IsEquiv A B f} `{IsEquiv A C (g o f)} + : IsEquiv g. +Proof. + Unset Typeclasses Modulo Eta. + exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))) || fail "too early". + Undo. + Set Typeclasses Modulo Eta. + Set Typeclasses Dependency Order. + Set Typeclasses Debug. + Fail exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))). -- cgit v1.2.3