Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Diagnose bad coercion #39

Open
wants to merge 2 commits into
base: ps/branch/remove_workaround_for_coq_coq_8994
Choose a base branch
from
Open

Diagnose bad coercion #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c830a8b
Fix resolution in WildCat/DisplayedEquiv.v
gio256 Feb 19, 2024
8b15ef2
Wildcat equivs: remove prime fields, dx bad coercion
gio256 Feb 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions theories/Homotopy/ExactSequence.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -461,6 +461,7 @@ Definition connecting_map {F X Y}
: loops Y ->* F
:= i_fiberseq (connect_fiberseq i f).

Set Printing Coercions.
Global Instance isexact_connect_R {F X Y}
(i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
: IsExact purely (fmap loops f) (connecting_map i f).
Expand All @@ -472,6 +473,7 @@ Proof.
(pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))))^-1*)
(((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*)
_ (pfib i)).
(** @todo: this proof hangs on Defined when the method cate_fun is directly declared as a coercion CatEquiv >-> Hom *)
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is likely because typeclass resolution is hanging. You can try to see what it is doing with Set Typeclasses Depth 3 and Set Typeclasses Debug. Alternatively, you can use nrefine which is short for notypeclasses refine, this will leave the goals that are typeclasses out. We probably don't need many typeclasses for the goal to be well-typed here anyway. Once you've used nrefine or snrefine for the simple variant which doesn't hide goals that can be inferred, you can resolve the typeclass proofs with 1: exact _..

refine (vinverse
((loops_inv X) o*E
(pfiber2_loops (pfib f)) o*E
Expand Down
14 changes: 7 additions & 7 deletions theories/WildCat/DisplayedEquiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,11 @@ Class DHasEquivs {A : Type} `{HasEquivs A}
DCatEquiv f a' b' -> DHom f a' b';
dcate_isequiv : forall {a b} {f : a $<~> b} {a'} {b'}
(f' : DCatEquiv f a' b'), DCatIsEquiv (dcate_fun f');
dcate_buildequiv : forall {a b} {f : a $-> b} `{!CatIsEquiv f} {a'} {b'}
dcate_buildequiv : forall {a b} {f : a $-> b} {fe : CatIsEquiv f} {a'} {b'}
(f' : DHom f a' b') {fe' : DCatIsEquiv f'},
DCatEquiv (Build_CatEquiv f) a' b';
dcate_buildequiv_fun : forall {a b} {f : a $-> b} `{!CatIsEquiv f}
{a'} {b'} (f' : DHom f a' b') {fe' : DCatIsEquiv f'},
DCatEquiv (Build_CatEquiv (fe:=fe) f) a' b';
dcate_buildequiv_fun : forall {a b} {f : a $-> b} {fe : CatIsEquiv f}
{a'} {b'} (f' : DHom f a' b') {fe' : DCatIsEquiv (fe:=fe) f'},
DGpdHom (cate_buildequiv_fun f)
(dcate_fun (dcate_buildequiv f' (fe':=fe'))) f';
dcate_inv' : forall {a b} {f : a $<~> b} {a'} {b'} (f' : DCatEquiv f a' b'),
Expand All @@ -44,8 +44,8 @@ Global Existing Instance dcate_isequiv.
Coercion dcate_fun : DCatEquiv >-> DHom.

Definition Build_DCatEquiv {A} {D : A -> Type} `{DHasEquivs A D}
{a b : A} {f : a $-> b} `{!CatIsEquiv f} {a' : D a} {b' : D b}
(f' : DHom f a' b') {fe' : DCatIsEquiv f'}
{a b : A} {f : a $-> b} {fe : CatIsEquiv f} {a' : D a} {b' : D b}
(f' : DHom f a' b') {fe' : DCatIsEquiv (fe:=fe) f'}
: DCatEquiv (Build_CatEquiv f) a' b'
:= dcate_buildequiv f' (fe':=fe').

Expand Down Expand Up @@ -142,7 +142,7 @@ Proof.
snrapply Build_HasEquivs.
1:{ intros [a a'] [b b']. exact {f : a $<~> b & DCatEquiv f a' b'}. }
all: intros aa' bb' [f f'].
- exact {fe : CatIsEquiv f & DCatIsEquiv f'}.
- exact {fe : CatIsEquiv f & DCatIsEquiv (fe:=fe) f'}.
- exists f. exact f'.
- exact (cate_isequiv f; dcate_isequiv f').
- intros [fe fe'].
Expand Down
39 changes: 14 additions & 25 deletions theories/WildCat/Equiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,30 +12,29 @@ Declare Scope wc_iso_scope.

Class HasEquivs (A : Type) `{Is1Cat A} :=
{
CatEquiv' : A -> A -> Type where "a $<~> b" := (CatEquiv' a b);
CatEquiv : A -> A -> Type where "a $<~> b" := (CatEquiv a b);
CatIsEquiv : forall a b, (a $-> b) -> Type;
cate_fun' : forall a b, (a $<~> b) -> (a $-> b);
cate_isequiv : forall a b (f : a $<~> b), CatIsEquiv a b (cate_fun' a b f);
cate_buildequiv' : forall a b (f : a $-> b), CatIsEquiv a b f -> CatEquiv' a b;
cate_buildequiv_fun' : forall a b (f : a $-> b) (fe : CatIsEquiv a b f),
cate_fun' a b (cate_buildequiv' a b f fe) $== f;
cate_buildequiv : forall a b (f : a $-> b), CatIsEquiv a b f -> CatEquiv a b;
cate_buildequiv_fun : forall a b (f : a $-> b) (fe : CatIsEquiv a b f),
cate_fun' a b (cate_buildequiv a b f fe) $== f;
cate_inv' : forall a b (f : a $<~> b), b $-> a;
cate_issect' : forall a b (f : a $<~> b),
cate_inv' _ _ f $o cate_fun' _ _ f $== Id a;
cate_isretr' : forall a b (f : a $<~> b),
cate_fun' _ _ f $o cate_inv' _ _ f $== Id b;
catie_adjointify' : forall a b (f : a $-> b) (g : b $-> a)
catie_adjointify : forall a b (f : a $-> b) (g : b $-> a)
(r : f $o g $== Id b) (s : g $o f $== Id a), CatIsEquiv a b f;
}.

Existing Class CatIsEquiv.
Arguments CatIsEquiv {A _ _ _ _ _ a b} f.
Global Existing Instance cate_isequiv.

(** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)
Arguments cate_isequiv {A _ _ _ _ _ a b} f.
Arguments cate_buildequiv_fun {A _ _ _ _ _ a b} f {fe}.
Arguments catie_adjointify {A _ _ _ _ _ a b} f g r s.

Definition CatEquiv {A} `{HasEquivs A} (a b : A)
:= @CatEquiv' A _ _ _ _ _ a b.
Existing Class CatIsEquiv.
Global Existing Instance cate_isequiv.

Notation "a $<~> b" := (CatEquiv a b).
Infix "≅" := CatEquiv : wc_iso_scope.
Expand All @@ -45,23 +44,13 @@ Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
: a $-> b
:= @cate_fun' A _ _ _ _ _ a b f.

Arguments cate_fun {A _ _ _ _ _ a b} f.
Coercion cate_fun : CatEquiv >-> Hom.

Definition Build_CatEquiv {A} `{HasEquivs A} {a b : A}
(f : a $-> b) {fe : CatIsEquiv f}
: a $<~> b
:= cate_buildequiv' a b f fe.

Definition cate_buildequiv_fun {A} `{HasEquivs A} {a b : A}
(f : a $-> b) {fe : CatIsEquiv f}
: cate_fun (Build_CatEquiv f) $== f
:= cate_buildequiv_fun' a b f fe.

Definition catie_adjointify {A} `{HasEquivs A} {a b : A}
(f : a $-> b) (g : b $-> a)
(r : f $o g $== Id b) (s : g $o f $== Id a)
: CatIsEquiv f
:= catie_adjointify' a b f g r s.
:= cate_buildequiv a b f fe.

Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
(f : a $-> b) (g : b $-> a)
Expand All @@ -86,15 +75,15 @@ Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
Proof.
refine (_ $@ cate_issect' a b f).
refine (_ $@R f).
apply cate_buildequiv_fun'.
apply cate_buildequiv_fun.
Defined.

Definition cate_isretr {A} `{HasEquivs A} {a b} (f : a $<~> b)
: f $o f^-1$ $== Id b.
Proof.
refine (_ $@ cate_isretr' a b f).
refine (f $@L _).
apply cate_buildequiv_fun'.
apply cate_buildequiv_fun.
Defined.

(** If [g] is a section of an equivalence, then it is the inverse. *)
Expand Down
6 changes: 3 additions & 3 deletions theories/WildCat/Induced.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,12 +81,12 @@ Section Induced_category.
+ apply CatIsEquiv.
+ apply cate_fun.
+ apply cate_isequiv.
+ apply cate_buildequiv'.
+ nrapply cate_buildequiv_fun'.
+ apply Build_CatEquiv.
+ nrapply cate_buildequiv_fun.
+ apply cate_inv'.
+ nrapply cate_issect'.
+ nrapply cate_isretr'.
+ nrapply catie_adjointify'.
+ nrapply catie_adjointify.
Defined.

End Induced_category.
6 changes: 3 additions & 3 deletions theories/WildCat/Opposite.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,10 +163,10 @@ Proof.
srapply Build_HasEquivs; intros a b; unfold op in *; cbn.
- exact (b $<~> a).
- apply CatIsEquiv.
- apply cate_fun'.
- apply cate_fun.
- apply cate_isequiv.
- apply cate_buildequiv'.
- rapply cate_buildequiv_fun'.
- apply Build_CatEquiv.
- rapply cate_buildequiv_fun.
- apply cate_inv'.
- rapply cate_isretr'.
- rapply cate_issect'.
Expand Down