Merge pull request #2329 from jdchristensen/setoidrewrite-cleanup

SetoidRewrite: various cleanups and simplifications

Author: jdchristensen

contrib/SetoidRewrite.v

@@ -1,12 +1,8 @@
-(* Typeclass instances to allow rewriting in categories. Examples are given later in the file. *)
+(** * Typeclass instances to allow rewriting in categories *)
 
-(* Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database. It must be imported before Basics.Overture. *)
+(** The file using the setoid rewriting machinery from the Coq standard library to allow rewriting in wild-categories.  Examples are given later in the file. *)
 
-(** Warning: This imports Coq.Setoids.Setoid from the standard library. Currently the setoid rewriting machinery requires this to work, it depends on this file explicitly. This imports the whole standard library into the namespace.
-
-All files that import WildCat/SetoidRewrite.v will also recursively import the entire Coq.Init standard library.  *)
-
-(** Because of this, this file needs to be the *first* file Require'd in any file that uses it.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on. In the long term it would be good if this could be avoided.*)
+(** Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database.  It must be imported before Basics.Overture.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Because of this, this file also needs to be the first file Require'd in any file that uses it.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on.  In the long term it would be good if this could be avoided. *)
 
 #[warnings="-deprecated-from-Coq"]
 From Coq Require Init.Tactics.
@@ -18,36 +14,43 @@ Import CMorphisms.ProperNotations.
 From HoTT Require Import WildCat.Core
   WildCat.NatTrans WildCat.Equiv.
 
+(** ** Setoid rewriting *)
+
 #[export] Instance reflexive_proper_proxy {A : Type}
   {R : Relation A} `(Reflexive A R) (x : A)
   : CMorphisms.ProperProxy R x := reflexivity x.
 
-(* forall (x y : A), x $== y -> forall (a b : A), a $== b -> y $== b -> x $==a *)
+(** forall (x y : A), x $== y -> forall (a b : A), a $== b -> y $== b -> x $==a *)
 #[export] Instance IsProper_GpdHom_from {A : Type} `{Is0Gpd A}
   : CMorphisms.Proper
       (GpdHom ==>
          GpdHom ==>
          CRelationClasses.flip CRelationClasses.arrow) GpdHom.
 Proof.
+  (* Add the next line to the start of any proof to see what it means: *)
+  unfold "==>", CMorphisms.Proper, CRelationClasses.arrow, CRelationClasses.flip in *.
   intros x y eq_xy a b eq_ab eq_yb.
   exact (transitivity eq_xy (transitivity eq_yb
                               (symmetry _ _ eq_ab))).
+  (* We could also just write:
+    exact (eq_xy $@ eq_yb $@ eq_ab^$).
+  The advantage of the above proof is that it works for other transitive and symmetric relations. *)
 Defined.
 
-(* forall (x y : A), x $== y -> forall (a b : A), a $== b -> x $== a -> y $== b *)
+(** forall (x y : A), x $== y -> forall (a b : A), a $== b -> x $== a -> y $== b *)
 #[export] Instance IsProper_GpdHom_to {A : Type} `{Is0Gpd A}
   : CMorphisms.Proper
       (GpdHom ==>
          GpdHom ==>
          CRelationClasses.arrow) GpdHom.
 Proof.
-  intros x y eq_xy a b eq_ab eq_yb.
-  unshelve refine (transitivity _ eq_ab).
-  unshelve refine (transitivity _ eq_yb).
+  intros x y eq_xy a b eq_ab eq_xa.
+  refine (transitivity _ eq_ab).
+  refine (transitivity _ eq_xa).
   exact (symmetry _ _ eq_xy).
 Defined.
 
-(* forall a : A, x $== y -> a $== x -> a $== y *)
+(** forall a x y : A, x $== y -> a $== x -> a $== y *)
 #[export] Instance IsProper_GpdHom_to_a {A : Type} `{Is0Gpd A}
   {a : A}
   : CMorphisms.Proper
@@ -58,7 +61,7 @@ Proof.
   by transitivity x.
 Defined.
 
-(* forall a : A, x $== y -> a $== y -> a $== x *)
+(** forall a x y : A, x $== y -> a $== y -> a $== x *)
 #[export] Instance IsProper_GpdHom_from_a {A : Type} `{Is0Gpd A}
   {a : A}
   : CMorphisms.Proper
@@ -71,15 +74,17 @@ Defined.
 
 Open Scope signatureT_scope.
 
+(** If [R] is symmetric and [R x y -> R' (f x) (f y)], then [R y x -> R' (f x) (f y)]. *)
 #[export] Instance symmetry_flip {A B : Type} {f : A -> B}
   {R : Relation A} {R' : Relation B} `{Symmetric _ R}
   (H0 : CMorphisms.Proper (R ++> R') f)
   : CMorphisms.Proper (R --> R') f.
 Proof.
-  intros a b Rab.
-  apply H0. unfold CRelationClasses.flip. symmetry. exact Rab.
+  intros a b Rba; unfold CRelationClasses.flip in Rba.
+  apply H0. symmetry. exact Rba.
 Defined.
 
+(** If [R'] is symmetric and [R x y -> R' x' y' -> R'' (f x x') (f y y')], then [R x y -> R' y' x' -> R'' (f x x') (f y y')]. *)
 #[export] Instance symmetric_flip_snd {A B C : Type} {R : Relation A}
   {R' : Relation B} {R'' : Relation C} `{Symmetric _ R'}
   (f : A -> B -> C) (H1 : CMorphisms.Proper (R ++> R' ++> R'') f)
@@ -88,40 +93,36 @@ Proof.
   intros a b Rab x y R'yx. apply H1; [ assumption | symmetry; assumption ].
 Defined.
 
-#[export] Instance IsProper_fmap {A B : Type} `{Is1Cat A}
-  `{Is1Cat A} (F : A -> B) `{Is1Functor _ _ F} (a b : A)
-  : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b) := fun _ _ eq => fmap2 F eq.
+#[export] Instance IsProper_fmap {A B : Type}
+  (F : A -> B) `{Is1Functor _ _ F} (a b : A)
+  : CMorphisms.Proper (GpdHom ==> GpdHom) (@fmap _ _ _ _ F _ a b)
+  := fun _ _ => fmap2 F.
 
 #[export] Instance IsProper_catcomp_g {A : Type} `{Is1Cat A}
   {a b c : A} (g : b $-> c)
-  : CMorphisms.Proper (GpdHom ==> GpdHom) (@cat_comp _ _ _ a b c g).
-Proof.
-  intros f1 f2.
-  apply (is0functor_postcomp a b c g ).
-Defined.
+  : CMorphisms.Proper (GpdHom ==> GpdHom) (@cat_comp _ _ _ a b c g)
+  := fun _ _ => cat_postwhisker g.
 
 #[export] Instance IsProper_catcomp {A : Type} `{Is1Cat A}
   {a b c : A}
   : CMorphisms.Proper (GpdHom ==> GpdHom ==> GpdHom)
       (@cat_comp _ _ _ a b c).
 Proof.
   intros g1 g2 eq_g f1 f2 eq_f.
-  rewrite eq_f.
-  apply (is0functor_precomp a b c f2).
-  exact eq_g.
+  exact (cat_comp2 eq_f eq_g).
 Defined.
 
 #[export] Instance gpd_hom_to_hom_proper {A B : Type} `{Is0Gpd A}
   {R : Relation B} (F : A -> B)
-  `{CMorphisms.Proper _ (GpdHom ==> R) F}
+  {H2 : CMorphisms.Proper (GpdHom ==> R) F}
   : CMorphisms.Proper (Hom ==> R) F.
 Proof.
   intros a b eq_ab; apply H2; exact eq_ab.
 Defined.
 
-#[export] Instance gpd_hom_is_proper1 {A : Type} `{Is0Gpd A}
- : CMorphisms.Proper
-     (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
+#[export] Instance IsProper_Hom {A : Type} `{Is0Gpd A}
+  : CMorphisms.Proper
+      (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
 Proof.
   intros x y eq_xy a b eq_ab f.
   refine (transitivity _ eq_ab).
@@ -130,35 +131,33 @@ Proof.
 Defined.
 
 #[export] Instance transitive_hom {A : Type} `{Is01Cat A} {x : A}
- : CMorphisms.Proper
-     (Hom ==> CRelationClasses.arrow) (Hom x).
-Proof.
-  intros y z g f.
-  exact (g $o f).
-Defined.
+  : CMorphisms.Proper
+      (Hom ==> CRelationClasses.arrow) (Hom x)
+  := fun y z => cat_comp.
+
+(** ** Examples of setoid rewriting *)
 
+(** Rewriting works in hypotheses. *)
 Proposition IsEpic_HasSection {A} `{Is1Cat A}
   {a b : A} (f : a $-> b) :
   SectionOf f -> Epic f.
 Proof.
-  intros section c g h eq_gf_hf.
-  destruct section as [right_inverse is_section].
-  apply (is0functor_precomp _ _ _ right_inverse) in eq_gf_hf;
-    unfold cat_precomp in eq_gf_hf.
+  intros [right_inverse is_section] c g h eq_gf_hf.
+  apply cat_prewhisker with (h:=right_inverse) in eq_gf_hf.
   rewrite 2 cat_assoc, is_section, 2 cat_idr in eq_gf_hf.
   exact eq_gf_hf.
 Defined.
 
+(** A different approach, working in the goal. *)
 Proposition IsMonic_HasRetraction {A} `{Is1Cat A}
   {b c : A} (f : b $-> c) :
   RetractionOf f -> Monic f.
 Proof.
-  intros retraction a g h eq_fg_fh.
-  destruct retraction as [left_inverse is_retraction].
-  apply (is0functor_postcomp _ _ _ left_inverse) in eq_fg_fh;
-    unfold cat_postcomp in eq_fg_fh.
-  rewrite <- 2 cat_assoc, is_retraction, 2 cat_idl in eq_fg_fh.
-  assumption.
+  intros [left_inverse is_retraction] a g h eq_fg_fh.
+  rewrite <- (cat_idl g), <- (cat_idl h).
+  rewrite <- is_retraction.
+  rewrite 2 cat_assoc.
+  exact (_ $@L eq_fg_fh).
 Defined.
 
 Proposition nat_equiv_faithful {A B : Type}
@@ -168,19 +167,10 @@ Proposition nat_equiv_faithful {A B : Type}
   : Faithful F -> Faithful G.
 Proof.
   intros faithful_F x y f g eq_Gf_Gg.
-  apply (@fmap _ _ _ _ _ (is0functor_precomp _
-       _ _ (cat_equiv_natequiv tau x))) in eq_Gf_Gg.
-  cbn in eq_Gf_Gg.
-  unfold cat_precomp in eq_Gf_Gg.
-  rewrite <- 2 (isnat tau) in eq_Gf_Gg.
   apply faithful_F.
-  assert (X : RetractionOf (tau y)). {
-    unshelve eapply Build_RetractionOf.
-    - exact ((tau y)^-1$).
-    - exact (cate_issect _ ).
-  }
-  apply IsMonic_HasRetraction in X.
-  apply X in eq_Gf_Gg. assumption.
+  apply (cate_monic_equiv (tau y)).
+  rewrite 2 (isnat tau).
+  by apply cat_prewhisker.
 Defined.
 
 Section SetoidRewriteTests.