From 4d11b83b7d860e1047714e61c5650a239c72bd56 Mon Sep 17 00:00:00 2001 From: Laura Zielinski Date: Sun, 11 Feb 2024 12:27:05 -0600 Subject: [PATCH] nicer equivalence relations in category --- .vscode/settings.json | 15 ------- ViCaR/Classes/Category.v | 68 ++++++++++------------------- ViCaR/{Classes => }/GeneralLemmas.v | 0 examples/ZXExample.v | 33 +++++++++----- 4 files changed, 45 insertions(+), 71 deletions(-) delete mode 100644 .vscode/settings.json rename ViCaR/{Classes => }/GeneralLemmas.v (100%) diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 987c45c..0000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,15 +0,0 @@ -{ - "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 - } -} \ No newline at end of file diff --git a/ViCaR/Classes/Category.v b/ViCaR/Classes/Category.v index f756e32..afc00bb 100644 --- a/ViCaR/Classes/Category.v +++ b/ViCaR/Classes/Category.v @@ -8,43 +8,19 @@ 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 + (* Morphism equivalence *) + equiv {A B : C} : relation (A ~> B) 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; + equiv_rel {A B : C} : equivalence (A ~> B) equiv; - c_identity (A : C) : A ~> A; + (* Object equivalence *) + obj_equiv : relation C + where "A ≅ B" := (obj_equiv A B) : Cat_scope; + obj_equiv_rel : equivalence C obj_equiv; compose {A B M : C} : (A ~> B) -> (B ~> M) -> (A ~> M); @@ -52,29 +28,29 @@ Class Category (C : Type) : Type := { 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); + + c_identity (A : C) : A ~> A; + 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; }. +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 *) + 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) + (A B : C) : (A ~> B) equiv + reflexivity proved by (equiv_refl (A ~> B) equiv equiv_rel) + symmetry proved by (equiv_sym (A ~> B) equiv equiv_rel) + transitivity proved by (equiv_trans (A ~> B) equiv equiv_rel) 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. + 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. \ No newline at end of file +Local Close Scope Cat. diff --git a/ViCaR/Classes/GeneralLemmas.v b/ViCaR/GeneralLemmas.v similarity index 100% rename from ViCaR/Classes/GeneralLemmas.v rename to ViCaR/GeneralLemmas.v diff --git a/examples/ZXExample.v b/examples/ZXExample.v index 3d8b82a..a28c506 100644 --- a/examples/ZXExample.v +++ b/examples/ZXExample.v @@ -1,29 +1,42 @@ +Require Import Setoid. + From VyZX Require Import CoreData. From VyZX Require Import CoreRules. From VyZX Require Import PermutationRules. From ViCaR Require Export CategoryTypeclass. +Lemma proportional_equiv {n m : nat} : equivalence (ZX n m) proportional. +Proof. + constructor. + unfold reflexive; apply proportional_refl. + unfold transitive; apply proportional_trans. + unfold symmetric; apply proportional_symm. +Qed. + +Lemma equality_equiv : equivalence nat eq. +Proof. + constructor. + unfold reflexive; easy. + unfold transitive; apply eq_trans. + unfold symmetric; apply eq_sym. +Qed. + #[export] Instance ZXCategory : Category nat := { morphism := ZX; equiv := @proportional; - equiv_symm := @proportional_symm; - equiv_trans := @proportional_trans; - equiv_refl := @proportional_refl; + equiv_rel := @proportional_equiv; obj_equiv := eq; - obj_equiv_symm := @eq_sym nat; - obj_equiv_trans := @eq_trans nat; - obj_equiv_refl := @eq_refl nat; - - c_identity n := n_wire n; + obj_equiv_rel := equality_equiv; compose := @Compose; compose_compat := @Proportional.compose_compat; + assoc := @ComposeRules.compose_assoc; + c_identity n := n_wire n; left_unit _ _ := nwire_removal_l; right_unit _ _ := nwire_removal_r; - assoc := @ComposeRules.compose_assoc; }. Definition zx_associator {n m o} := @@ -266,7 +279,7 @@ Proof. apply functional_extensionality; intros. bdestruct_all; simpl in *; try lia. all: solve_simple_mod_eqns. -Admitted. +Qed. Lemma hexagon_lemma_1 : forall {n m o}, (zx_braiding ↕ n_wire o) ⟷ zx_associator ⟷ (n_wire m ↕ zx_braiding)