Small proof repair + coq-action update

.github/workflows/coq-action.yml

@@ -12,11 +12,10 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.14'
-          - '8.15'
           - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         ocaml_version:
           - 'default'

README.md

@@ -6,10 +6,18 @@
 
 ## Building ViCAR
 
-Tested with Coq 8.14-8.18.
+Currently supports Coq 8.16-8.19.
 
-To build ViCaR, run `make vicar`
+To build ViCaR, run `make vicar`.
 
+## Installing ViCAR through opam
+
+To install ViCAR through opam, run 
+```bash
+opam pin -y coq-vicar https://github.com/inQWIRE/ViCAR.git
+```
+
+To use the visualizer, first have [coq-lsp](https://github.com/ejgallego/coq-lsp) installed, then install the VSCode extension found at [https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizcar]. After instantiating the appropriate typeclass you would like to visualize you can run the vizcar command in vscode to activate visualizing. The vizcar plugin only visualizes terms using the ViCAR grammar. To automatically take a term with an instantiated typeclass to the ViCAR grammar, use the `to_Cat` tactic.
 
 ## Examples
 

ViCaR/Classes/BraidedMonoidal.v

@@ -75,13 +75,15 @@ Lemma hexagon_resultant_1 {C} {cC : Category C} {mC : MonoidalCategory cC}
   id_ B ⊗ B_ M, A ∘ B_ B, (A×M) ∘ associator A M B ∘ id_ A ⊗ (B_ B, M)^-1
   ≃ associator B M A ^-1 ∘ B_ (B × M), A.
 Proof.
-  (* rewrite <- compose_iso_l. *)
   pose proof (hexagon_2 A B M) as hex2.
-  rewrite <- (compose_tensor_iso_r' _ (IdentityIsomorphism _)).
+  replace (id_ A) with (IdentityIsomorphism A ^-1) by easy.
+  rewrite <- (compose_tensor_iso_r' (associator B M A ^-1 ∘ B_ B × M, A) (IdentityIsomorphism A) (B_ B, M)).
   simpl.
   rewrite 2!compose_iso_r.
   rewrite !assoc.
   rewrite <- compose_iso_l.
+  Check compose_tensor_iso_r.
+  replace (id_ B) with (forward (IdentityIsomorphism B)) by easy.
   rewrite (compose_tensor_iso_r _ (IdentityIsomorphism _)).
   rewrite assoc, compose_iso_l'.
   symmetry in hex2.
@@ -93,6 +95,7 @@ Proof.
   apply compose_cancel_r.
   pose proof (hexagon_1 B A M) as hex1.
   rewrite <- compose_iso_l'.
+  replace (id_ M) with (IdentityIsomorphism M ^-1) by easy.
   rewrite <- (compose_tensor_iso_l' _ (IdentityIsomorphism _)).
   simpl.
   rewrite <- 3!assoc.
@@ -101,5 +104,4 @@ Proof.
   easy.
 Qed.
 
-
-Local Close Scope Cat.
+Local Close Scope Cat.

coq-vicar.opam

@@ -1,19 +1,19 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1.0"
+version: "0.1.1"
 synopsis: "Coq library reasoning about categorical string diagrams"
 description: """
-inQWIRE's ViCaR is a library for reasoning about
+inQWIRE's ViCAR is a library for reasoning about
  categorical string diagrams
 """
 maintainer: ["inQWIRE Developers"]
 authors: ["inQWIRE"]
 license: "MIT"
-homepage: "https://github.com/inQWIRE/ViCaR"
-bug-reports: "https://github.com/inQWIRE/ViCaR/issues"
+homepage: "https://github.com/inQWIRE/ViCAR"
+bug-reports: "https://github.com/inQWIRE/ViCAR/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq" {>= "8.12"}
+  "coq" {>= "8.16"}
   "odoc" {with-doc}
 ]
 build: [
@@ -30,4 +30,4 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/ViCaR.git"
+dev-repo: "git+https://github.com/inQWIRE/ViCAR.git"

dune-project

@@ -18,4 +18,4 @@
  )
 
  (depends
-   (coq (>= 8.12))))
+   (coq (>= 8.16))))