feat: State all the lemmas in section 7.

kylechui · Jun 17, 2024 · 3024c4f · 3024c4f
1 parent d00ac9d
commit 3024c4f
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 0 deletions.
diff --git a/Helpers/GateHelpers.v b/Helpers/GateHelpers.v
@@ -11,6 +11,9 @@ Definition bcgate (U : Square 4) := I 2 ⊗ U.
 Definition acgate (U : Square 4) := swapbc × (abgate U) × swapbc.
 Definition ccu (U : Square 2) := control (control U).
 
+Definition TwoQubitGate (U : Square 8) := exists (V : Square 4), WF_Unitary V /\ (U = abgate V \/ U = acgate V \/ U = bcgate V).
+
+
 #[global] Hint Unfold abgate bcgate acgate ccu : M_db.
 
 Lemma WF_abgate : forall (U : Square 4), WF_Matrix U -> WF_Matrix (abgate U).

diff --git a/Main.v b/Main.v
@@ -3174,3 +3174,43 @@ Proof.
     }
   }
 Qed.
+
+Lemma m7_2 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 ->
+  (exists (V1 V2 V3 V4 : Square 8),
+    TwoQubitGate V1 /\ TwoQubitGate V2 /\ TwoQubitGate V3 /\ TwoQubitGate V4 /\
+    V1 × V2 × V3 × V4 = ccu (diag2 u0 u1)) ->
+  (exists (U1 U2 U3 U4 : Square 4),
+    WF_Unitary U1 /\ WF_Unitary U2 /\ WF_Unitary U3 /\ WF_Unitary U4 /\
+    (exists (u2 u3 : C), ((u2, u3) = (u0, u1) \/ (u2, u3) = (C1, u0^* * u1)) /\
+      bcgate U1 × acgate U2 × abgate U3 × bcgate U4 = ccu (diag2 u2 u3)))
+  \/
+  (exists (U1 U2 U3 U4 : Square 4),
+    WF_Unitary U1 /\ WF_Unitary U2 /\ WF_Unitary U3 /\ WF_Unitary U4 /\
+    (exists (u2 u3 : C), ((u2, u3) = (u0, u1) \/ (u2, u3) = (C1, u0^* * u1)) /\
+      acgate U1 × bcgate U2 × acgate U3 × bcgate U4 = ccu (diag2 u2 u3))).
+Proof.
+Admitted.
+
+Lemma m7_3 : forall (u0 u1 u2 u3 : C), Cmod u0 = 1 -> Cmod u1 = 1 ->
+  (u2, u3) = (u0, u1) \/ (u2, u3) = (C1, u0^* * u1) -> u2 = u3 \/ u2 * u3 = C1 ->
+  (u0 = u1 \/ u0 * u1 = C1).
+Proof.
+Admitted.
+
+Theorem m7_4 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 ->
+  (exists (V1 V2 V3 V4 : Square 8),
+    TwoQubitGate V1 /\ TwoQubitGate V2 /\ TwoQubitGate V3 /\ TwoQubitGate V4 /\
+    V1 × V2 × V3 × V4 = ccu (diag2 u0 u1)) <->
+  u0 = u1 \/ u0 * u1 = C1.
+Proof.
+Admitted.
+
+Corollary m7_5 : forall (U : Square 2), WF_Unitary U ->
+  (exists (V1 V2 V3 V4 : Square 8),
+    TwoQubitGate V1 /\ TwoQubitGate V2 /\ TwoQubitGate V3 /\ TwoQubitGate V4 /\
+    V1 × V2 × V3 × V4 = ccu U)
+  <->
+  (exists (V D : Square 2), WF_Unitary V /\ WF_Diagonal D /\
+    U = V × D × V† /\ (D 0 0 = D 1 1)%nat) /\ Determinant U = C1.
+Proof.
+Admitted.