Fixed cup-cap-flip

inQWIRE · May 3, 2024 · 7937031 · 7937031
1 parent 772846c
commit 7937031
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 14 deletions.
diff --git a/src/CoreData/ZXCore.v b/src/CoreData/ZXCore.v
@@ -16,8 +16,8 @@ Open Scope ZX_scope.
 
 Inductive ZX : nat -> nat -> Type :=
   | Empty : ZX 0 0
-  | Cap  : ZX 0 2
-  | Cup  : ZX 2 0
+  | Cup  : ZX 0 2
+  | Cap  : ZX 2 0
   | Swap : ZX 2 2
   | Wire : ZX 1 1
   | Box  : ZX 1 1
@@ -37,8 +37,8 @@ Defined.
 
 (* Notations for the ZX diagrams *)
 Notation "⦰" := Empty : ZX_scope. (* \revemptyset *)
-Notation "⊂" := Cap : ZX_scope. (* \subset *)
-Notation "⊃" := Cup : ZX_scope. (* \supset *)
+Notation "⊂" := Cup : ZX_scope. (* \subset *)
+Notation "⊃" := Cap : ZX_scope. (* \supset *)
 Notation "⨉" := Swap : ZX_scope. (* \bigtimes *)
 Notation "—" := Wire : ZX_scope. (* \emdash *)
 Notation "□" := Box : ZX_scope. (* \square *)

diff --git a/src/CoreRules/SpiderInduction.v b/src/CoreRules/SpiderInduction.v
@@ -211,7 +211,7 @@ Proof.
 Qed.
 
 Lemma Z_wrap_over_top_right_base : forall n α,
-  (— ↕ Z n 2 α) ⟷ (Cup ↕ —) ∝ Z (S n) 1 α.
+  (— ↕ Z n 2 α) ⟷ (Cap ↕ —) ∝ Z (S n) 1 α.
 Proof.
   intros.
   prop_exists_nonzero 1.
@@ -326,7 +326,7 @@ Proof.
 Qed.
 
 Lemma Z_wrap_over_top_right_0 : forall n α,
-  (— ↕ Z n 1 α) ⟷ Cup ∝ Z (S n) 0 α.
+  (— ↕ Z n 1 α) ⟷ Cap ∝ Z (S n) 0 α.
 Proof.
   intros.
   prop_exists_nonzero 1.
@@ -451,12 +451,12 @@ Proof.
 Qed.
 
 Lemma Z_wrap_over_top_left_0 : forall n α,
-  Cap ⟷ (— ↕ Z 1 n α) ∝ Z 0 (S n) α.
+  Cup ⟷ (— ↕ Z 1 n α) ∝ Z 0 (S n) α.
 Proof.
   intros.
   apply transpose_diagrams.
   simpl.
   apply Z_wrap_over_top_right_0.
 Qed.
 
-Ltac spider_induction n := induction n; [ | destruct n ].
+Ltac spider_induction n := induction n; [ | destruct n ].
diff --git a/src/CoreRules/XRules.v b/src/CoreRules/XRules.v
@@ -49,11 +49,11 @@ Lemma X_appendix_rot_r : forall n m α β,
 Proof. intros. colorswap_of Z_appendix_rot_r. Qed.
 
 Lemma X_wrap_over_top_left : forall n m α,
-	X (S n) m α ∝ (Wire ↕ X n (S m) α) ⟷  (Cup ↕ n_wire m).
+	X (S n) m α ∝ (Wire ↕ X n (S m) α) ⟷  (Cap ↕ n_wire m).
 Proof. intros. colorswap_of Z_wrap_over_top_left. Qed.
 
 Lemma X_wrap_over_top_right : forall n m α,
-	X n (S m) α ∝ (Cap ↕ n_wire n) ⟷ (Wire ↕ X (S n) m α).
+	X n (S m) α ∝ (Cup ↕ n_wire n) ⟷ (Wire ↕ X (S n) m α).
 Proof. intros. colorswap_of Z_wrap_over_top_right. Qed.
 
 Lemma X_add_r : forall {n} m o {α β γ},
@@ -199,4 +199,4 @@ Proof. transpose_of X_n_wrap_under_r_base. Qed.
 (* @nocheck name *)
 (* PI is captialized in Coq R *)
 Lemma X_2_PI : forall n m a, X n m (INR a * 2 * PI) ∝ X n m 0.
-Proof. colorswap_of Z_2_PI. Qed.
+Proof. colorswap_of Z_2_PI. Qed.
diff --git a/src/CoreRules/ZRules.v b/src/CoreRules/ZRules.v
@@ -129,7 +129,7 @@ Proof.
 Qed.
 
 Lemma Z_wrap_over_top_left : forall n m α,
-	Z (S n) m α ∝ (Wire ↕ Z n (S m) α) ⟷  (Cup ↕ n_wire m).
+	Z (S n) m α ∝ (Wire ↕ Z n (S m) α) ⟷  (Cap ↕ n_wire m).
 Proof.
 	induction m.
 	- intros.
@@ -188,7 +188,7 @@ all: lia.
 Qed.
 
 Lemma Z_wrap_over_top_right : forall n m α,
-	Z n (S m) α ∝ (Cap ↕ n_wire n) ⟷ (Wire ↕ Z (S n) m α).
+	Z n (S m) α ∝ (Cup ↕ n_wire n) ⟷ (Wire ↕ Z (S n) m α).
 Proof. 
 	intros. apply transpose_diagrams. simpl. 
 	rewrite nstack1_transpose. rewrite transpose_wire.
@@ -861,4 +861,4 @@ Proof.
 	rewrite Cexp_2_PI.
 	rewrite Cexp_0.
 	easy.
-Qed.
+Qed.