From 8103026474f593a23d9605dab60fe11bd6de85f6 Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 17 Apr 2024 09:40:48 -0500 Subject: [PATCH 1/5] Small proof repair + coq-action update --- .github/workflows/coq-action.yml | 1 + ViCaR/Classes/BraidedMonoidal.v | 14 ++++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index 413a028..8fe9435 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -17,6 +17,7 @@ jobs: - '8.16' - '8.17' - '8.18' + - '8.19' - 'dev' ocaml_version: - 'default' diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v index 347a26b..af8af03 100644 --- a/ViCaR/Classes/BraidedMonoidal.v +++ b/ViCaR/Classes/BraidedMonoidal.v @@ -40,8 +40,8 @@ Class BraidedMonoidalCategory {C : Type} {cC : Category C} MonoidalCategory_of_BraidedMonoidalCategory := mC; }. -Arguments BraidedMonoidalCategory {_} {_}%Cat (_)%Cat. -Arguments braiding {_} {_}%Cat {_}%Cat (_)%Cat. +Arguments BraidedMonoidalCategory {_} {_}%_Cat (_)%_Cat. +Arguments braiding {_} {_}%_Cat {_}%_Cat (_)%_Cat. Notation "'B_' x , y" := (braiding _%Cat x%Obj y%Obj) (at level 20) : Brd_scope. @@ -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. \ No newline at end of file +Local Close Scope Cat. From 3ef69c0f485b35ca1ad49043260ffc94b5b13226 Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 17 Apr 2024 09:44:15 -0500 Subject: [PATCH 2/5] Undid change from %Cat to %_Cat, is a breaking change --- ViCaR/Classes/BraidedMonoidal.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ViCaR/Classes/BraidedMonoidal.v b/ViCaR/Classes/BraidedMonoidal.v index af8af03..cabbf7b 100644 --- a/ViCaR/Classes/BraidedMonoidal.v +++ b/ViCaR/Classes/BraidedMonoidal.v @@ -40,8 +40,8 @@ Class BraidedMonoidalCategory {C : Type} {cC : Category C} MonoidalCategory_of_BraidedMonoidalCategory := mC; }. -Arguments BraidedMonoidalCategory {_} {_}%_Cat (_)%_Cat. -Arguments braiding {_} {_}%_Cat {_}%_Cat (_)%_Cat. +Arguments BraidedMonoidalCategory {_} {_}%Cat (_)%Cat. +Arguments braiding {_} {_}%Cat {_}%Cat (_)%Cat. Notation "'B_' x , y" := (braiding _%Cat x%Obj y%Obj) (at level 20) : Brd_scope. From 195647c7d011b5073a00b936b7ee46b30fc34291 Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 17 Apr 2024 09:49:59 -0500 Subject: [PATCH 3/5] Updated README.md, coq-vicar.opam version, dune-project version, and coq-action version. --- .github/workflows/coq-action.yml | 2 -- README.md | 4 ++-- coq-vicar.opam | 4 ++-- dune-project | 2 +- 4 files changed, 5 insertions(+), 7 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index 8fe9435..49704c4 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -12,8 +12,6 @@ jobs: strategy: matrix: coq_version: - - '8.14' - - '8.15' - '8.16' - '8.17' - '8.18' diff --git a/README.md b/README.md index 3eea313..4998320 100644 --- a/README.md +++ b/README.md @@ -6,9 +6,9 @@ ## 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`. ## Examples diff --git a/coq-vicar.opam b/coq-vicar.opam index b630cfb..41644b4 100644 --- a/coq-vicar.opam +++ b/coq-vicar.opam @@ -1,6 +1,6 @@ # 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 @@ -13,7 +13,7 @@ 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: [ diff --git a/dune-project b/dune-project index a57ea96..c9f0a92 100644 --- a/dune-project +++ b/dune-project @@ -18,4 +18,4 @@ ) (depends - (coq (>= 8.12)))) + (coq (>= 8.16)))) From bd6ae287051a0c6f96743e95224a280d28a8aa89 Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 17 Apr 2024 10:02:47 -0500 Subject: [PATCH 4/5] Updated README with basic instructions for visualization. --- README.md | 8 ++++++++ coq-vicar.opam | 8 ++++---- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 4998320..a70642e 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,14 @@ Currently supports Coq 8.16-8.19. 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 to the ViCAR grammar, use the `categorify` tactic. ## Examples diff --git a/coq-vicar.opam b/coq-vicar.opam index 41644b4..72db620 100644 --- a/coq-vicar.opam +++ b/coq-vicar.opam @@ -3,14 +3,14 @@ opam-version: "2.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.16"} @@ -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" From 0bc61ab66bac82c7bfc9fc429fffc606ad62469e Mon Sep 17 00:00:00 2001 From: Ben Caldwell Date: Wed, 17 Apr 2024 10:14:35 -0500 Subject: [PATCH 5/5] Updated README visualization instructions --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index a70642e..8d418ea 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ To install ViCAR through opam, run 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 to the ViCAR grammar, use the `categorify` tactic. +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