Migrated ViCaR out of VyZX, added build system separated examples.

.github/workflows/coq-action.yml

@@ -0,0 +1,30 @@
+name: Coq Build
+
+on:
+  push:
+    branches: ['main']
+  pull_request:
+    branches: ['**'] # for all submitted Pull Requests
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        coq_version:
+          - '8.14'
+          - '8.15'
+          - '8.16'
+          - '8.17'
+          - 'dev'
+        ocaml_version:
+          - 'default'
+      fail-fast: false # don't stop jobs if one fails
+    steps:
+      - uses: actions/checkout@v3
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-vicar.opam'
+          coq_version: ${{ matrix.coq_version }}
+          ocaml_version: ${{ matrix.ocaml_version }}
+

.gitignore

@@ -0,0 +1,162 @@
+
+# Created by https://www.toptal.com/developers/gitignore/api/coq,emacs,macos,windows
+# Edit at https://www.toptal.com/developers/gitignore?templates=coq,emacs,macos,windows
+
+### Coq ###
+.*.aux
+.*.d
+*.a
+*.cma
+*.cmi
+*.cmo
+*.cmx
+*.cmxa
+*.cmxs
+*.glob
+*.ml.d
+*.ml4.d
+*.mlg.d
+*.mli.d
+*.mllib.d
+*.mlpack.d
+*.native
+*.o
+*.v.d
+*.vio
+*.vo
+*.vok
+*.vos
+.coq-native
+.csdp.cache
+.lia.cache
+.nia.cache
+.nlia.cache
+.nra.cache
+csdp.cache
+lia.cache
+nia.cache
+nlia.cache
+nra.cache
+native_compute_profile_*.data
+
+# generated timing files
+*.timing.diff
+*.v.after-timing
+*.v.before-timing
+*.v.timing
+time-of-build-after.log
+time-of-build-before.log
+time-of-build-both.log
+time-of-build-pretty.log
+
+### Emacs ###
+# -*- mode: gitignore; -*-
+*~
+\#*\#
+/.emacs.desktop
+/.emacs.desktop.lock
+*.elc
+auto-save-list
+tramp
+.\#*
+
+# Org-mode
+.org-id-locations
+*_archive
+
+# flymake-mode
+*_flymake.*
+
+# eshell files
+/eshell/history
+/eshell/lastdir
+
+# elpa packages
+/elpa/
+
+# reftex files
+*.rel
+
+# AUCTeX auto folder
+/auto/
+
+# cask packages
+.cask/
+dist/
+
+# Flycheck
+flycheck_*.el
+
+# server auth directory
+/server/
+
+# projectiles files
+.projectile
+
+# directory configuration
+.dir-locals.el
+
+# network security
+/network-security.data
+
+
+### macOS ###
+# General
+.DS_Store
+.AppleDouble
+.LSOverride
+
+# Icon must end with two \r
+Icon
+
+
+# Thumbnails
+._*
+
+# Files that might appear in the root of a volume
+.DocumentRevisions-V100
+.fseventsd
+.Spotlight-V100
+.TemporaryItems
+.Trashes
+.VolumeIcon.icns
+.com.apple.timemachine.donotpresent
+
+# Directories potentially created on remote AFP share
+.AppleDB
+.AppleDesktop
+Network Trash Folder
+Temporary Items
+.apdisk
+
+### Windows ###
+# Windows thumbnail cache files
+Thumbs.db
+Thumbs.db:encryptable
+ehthumbs.db
+ehthumbs_vista.db
+
+# Dump file
+*.stackdump
+
+# Folder config file
+[Dd]esktop.ini
+
+# Recycle Bin used on file shares
+$RECYCLE.BIN/
+
+# Windows Installer files
+*.cab
+*.msi
+*.msix
+*.msm
+*.msp
+
+# Windows shortcuts
+*.lnk
+
+# End of https://www.toptal.com/developers/gitignore/api/coq,emacs,macos,windows
+
+_build
+
+settings.json

.vscode/settings.json

@@ -0,0 +1,15 @@
+{
+  "files.exclude": {
+    "**/*.vo": true,
+    "**/*.vok": true,
+    "**/*.vos": true,
+    "**/*.aux": true,
+    "**/*.glob": true,
+    "**/.git": true,
+    "**/.svn": true,
+    "**/.hg": true,
+    "**/CVS": true,
+    "**/.DS_Store": true,
+    "**/Thumbs.db": true
+  }
+}

Makefile

@@ -0,0 +1,31 @@
+.DEFAULT_GOAL := vicar
+
+all:
+	@dune build
+
+vicar: FORCE
+	@dune build ViCaR
+
+examples: FORCE
+	@dune build examples
+
+clean:
+	@dune clean
+
+install:
+	@dune install
+
+uninstall:
+	@dune uninstall
+
+# hacky :) we should replace with dune in a future version
+FILES=$(shell find . -name "*.v" -depth 1) 
+doc: all
+	mkdir -p docs
+	cd _build/default && coqdoc -g --utf8 --toc --no-lib-name -d ../../docs -R . QuantumLib $(FILES)
+
+hooks:
+	@git config core.hooksPath .hooks
+
+.PHONY: all clean install uninstall doc
+FORCE:

README.md

@@ -0,0 +1,44 @@
+# ViCaR
+
+Verified Categorical String Diagrams in Roq
+
+## Building ViCaR
+
+Tested with Coq 8.14-8.16.
+
+To build ViCaR, run `make vicar`
+
+For examples to compile, do the following.
+
+First, install [QuantumLib](https://github.com/inQWIRE/QuantumLib) through opam.
+
+```bash
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam update
+opam install coq-quantumlib
+```
+
+Then install [SQIR and VOQC](https://github.com/inQWIRE/SQIR)
+
+```bash
+opam pin -y coq-sqir https://github.com/inQWIRE/SQIR.git
+opam pin -y coq-voqc https://github.com/inQWIRE/SQIR.git
+```
+
+Then install [VyZX](https://github.com/inQWIRE/VyZX)
+
+```bash
+opam pin -y coq-vicar https://github.com/inQWIRE/VyZX.git
+```
+
+Then install [ViCaR](https://github.com/inQWIRE/ViCaR) while in the directory by running
+
+```bash
+opam pin -y coq-vicar ./
+```
+
+then run
+
+```bash
+make examples
+```

ViCaR/Classes/BraidedMonoidal.v

@@ -0,0 +1,20 @@
+Require Import Category.
+Require Import Monoidal.
+
+Local Open Scope Cat.
+
+Class BraidedMonoidalCategory (C : Type) `{MonoidalCategory C} : Type := {
+    braiding {A B : C} : A × B ~> B × A;
+    inv_braiding {A B : C} : B × A ~> A × B;
+    braiding_inv_compose {A B : C} : braiding ∘ inv_braiding ≃ c_identity (A × B);
+    inv_braiding_compose {A B : C} : inv_braiding ∘ braiding ≃ c_identity (B × A);
+
+    hexagon_1 {A B M : C} : 
+        (braiding ⊗ c_identity M) ∘ associator ∘ (c_identity B ⊗ braiding)
+        ≃ associator ∘ (@braiding A (B × M)) ∘ associator;
+
+    hexagon_2 {A B M : C} : (inv_braiding ⊗ c_identity M) ∘ associator ∘ (c_identity B ⊗ inv_braiding)
+        ≃ associator ∘ (@inv_braiding (B × M) A) ∘ associator;
+}.
+
+Local Close Scope Cat.

ViCaR/Classes/Category.v

@@ -0,0 +1,80 @@
+Require Import Setoid.
+
+Declare Scope Cat_scope.
+Delimit Scope Cat_scope with Cat.
+Local Open Scope Cat.
+
+Reserved Notation "A ~> B" (at level 50).
+Reserved Notation "f ≃ g" (at level 60).
+Reserved Notation "A ≅ B" (at level 60).
+
+(* 
+    Might use these to abstract out the equality relations.
+        
+    Definition relation (A : Type) := A -> A -> Prop.
+    Definition reflexive {A : Type} (R : relation A) :=
+        forall a : A, R a a.
+    Definition transitive {A: Type} (R: relation A) :=
+        forall a b c : A, (R a b) -> (R b c) -> (R a c).
+    Definition symmetric {A: Type} (R: relation A) :=
+        forall a b : A, (R a b) -> (R b a).
+    Definition equivalence {A : Type} (R : relation A) := 
+        (reflexive R) /\ (symmetric R) /\ (transitive R). 
+*)
+
+Class Category (C : Type) : Type := {
+    morphism : C -> C -> Type
+        where "A ~> B" := (morphism A B);
+
+    equiv {A B : C} (f g : A ~> B) : Prop 
+        where "f ≃ g" := (equiv f g) : Cat_scope;
+    equiv_symm {A B : C} {f g : A ~> B} : 
+        f ≃ g -> g ≃ f;
+    equiv_trans {A B : C} {f g h : A ~> B} :
+        f ≃ g -> g ≃ h -> f ≃ h;
+    equiv_refl {A B : C} {f : A ~> B} :
+        f ≃ f;
+
+    obj_equiv (A B : C) : Prop 
+        where "A ≅ B" := (obj_equiv A B);
+    obj_equiv_symm {A B : C} : 
+        A ≅ B -> B ≅ A;
+    obj_equiv_trans {A B M : C} :
+        A ≅ B -> B ≅ M -> A ≅ M;
+    obj_equiv_refl {A : C} :
+        A ≅ A;
+
+    c_identity (A : C) : A ~> A;
+
+    compose {A B M : C} : 
+        (A ~> B) -> (B ~> M) -> (A ~> M);
+    compose_compat {A B M : C} : 
+        forall (f g : A ~> B), f ≃ g ->
+        forall (h j : B ~> M), h ≃ j ->
+        compose f h ≃ compose g j;
+
+    left_unit {A B : C} {f : A ~> B} : compose (c_identity A) f ≃ f;
+    right_unit {A B : C} {f : A ~> B} : compose f (c_identity B) ≃ f;
+    assoc {A B M N : C}
+        {f : A ~> B} {g : B ~> M} {h : M ~> N} : 
+        compose (compose f g) h ≃ compose f (compose g h);
+}.
+
+Add Parametric Relation {C : Type} {Cat : Category C} 
+    (n m : C) : (morphism n m) (equiv)
+  reflexivity proved by (@equiv_refl C Cat n m)
+  symmetry proved by (@equiv_symm C Cat n m)
+  transitivity proved by (@equiv_trans C Cat n m)
+  as prop_equiv_rel.
+
+Add Parametric Morphism {C : Type} {Cat : Category C} (n o m : C) : compose
+  with signature (@equiv C Cat n m) ==> (@equiv C Cat m o) ==> 
+                 equiv as compose_mor.
+Proof. apply compose_compat; assumption. Qed.
+
+Notation "A ~> B" := (morphism A B) : Cat_scope.
+Notation "f ≃ g" := (equiv f g) : Cat_scope. (* \simeq *)
+Notation "A ≅ B" := (obj_equiv A B) : Cat_scope. (* \cong *)
+Infix "∘" := compose (at level 40, left associativity) : Cat_scope. (* \circ *)
+
+Local Close Scope Cat.