feat(M7.1): Stated + proven.

TODO: We really need something similar to `list2DtoMatrix` but for
diagonal matrices in general, so we can stop proving these specific cases.

Author: kylechui

Helpers/DiagonalHelpers.v

@@ -2,6 +2,65 @@ Require Import QuantumLib.Eigenvectors.
 Require Import MatrixHelpers.
 Require Import GateHelpers.
 
+Lemma Diag_diag2: forall (c1 c2 : C), WF_Diagonal (diag2 c1 c2).
+Proof.
+  intros.
+  unfold WF_Diagonal.
+  split. apply WF_diag2.
+  intros.
+  unfold diag2; simpl.
+  destruct i.
+  - destruct j.
+    + contradiction.
+    + reflexivity.
+  - destruct i.
+    + destruct j.
+      * reflexivity.
+      * destruct j.
+        -- contradiction.
+        -- reflexivity.
+    + reflexivity.
+Qed.
+
+Lemma Diag_diag4: forall (c1 c2 c3 c4 : C), WF_Diagonal (diag4 c1 c2 c3 c4).
+Proof.
+  intros.
+  unfold WF_Diagonal.
+  split; try apply WF_diag4.
+  intros.
+  unfold diag4; simpl.
+  destruct i.
+  - destruct j.
+    + contradiction.
+    + reflexivity.
+  - destruct i.
+    + destruct j.
+      * reflexivity.
+      * destruct j.
+        -- contradiction.
+        -- reflexivity.
+    + destruct i.
+      * destruct j.
+        -- reflexivity.
+        -- destruct j.
+           ++ reflexivity.
+           ++ destruct j.
+              ** contradiction.
+              ** reflexivity.
+      * destruct i.
+        -- destruct j.
+           ++ reflexivity.
+           ++ destruct j.
+              ** reflexivity.
+              ** destruct j.
+                 --- reflexivity.
+                 --- destruct j.
+                     +++ contradiction.
+                     +++ reflexivity.
+        -- reflexivity.
+Qed.
+
+
 Lemma diag00 :  WF_Diagonal ∣0⟩⟨0∣.
 Proof.
   split; auto with wf_db.

Helpers/MatrixHelpers.v

@@ -82,44 +82,6 @@ Proof.
   unfold diag2, Determinant, big_sum, parity, get_minor; lca.
 Qed.
 
-Lemma Diag_diag4: forall (c1 c2 c3 c4 : C), WF_Diagonal (diag4 c1 c2 c3 c4).
-Proof.
-  intros.
-  unfold WF_Diagonal.
-  split; try apply WF_diag4.
-  intros.
-  unfold diag4; simpl.
-  destruct i.
-  - destruct j.
-    + contradiction.
-    + reflexivity.
-  - destruct i.
-    + destruct j.
-      * reflexivity.
-      * destruct j.
-        -- contradiction.
-        -- reflexivity.
-    + destruct i.
-      * destruct j.
-        -- reflexivity.
-        -- destruct j.
-           ++ reflexivity.
-           ++ destruct j.
-              ** contradiction.
-              ** reflexivity.
-      * destruct i.
-        -- destruct j.
-           ++ reflexivity.
-           ++ destruct j.
-              ** reflexivity.
-              ** destruct j.
-                 --- reflexivity.
-                 --- destruct j.
-                     +++ contradiction.
-                     +++ reflexivity.
-        -- reflexivity.
-Qed.
-
 Lemma row_out_of_bounds: forall {m n} (A : Matrix m n) (i : nat),
   WF_Matrix A -> (i >= m)%nat -> forall (j : nat), A i j = C0.
 Proof.

Main.v

@@ -3095,3 +3095,82 @@ Proof.
     assumption.
   }
 Qed.
+
+Lemma m7_1 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 ->
+  forall (U : Square 8), WF_Unitary U ->
+  forall (W : Square 4), WF_Unitary W ->
+  ccu (diag2 u0 u1) = abgate W × U -> exists (V : Square 4), WF_Unitary V /\
+  ccu (diag2 C1 (u0^* * u1)) = abgate V × U.
+Proof.
+  intros u0 u1 u0_unit u1_unit U U_unitary W W_unitary H.
+  exists (control (diag2 C1 (u0^*)) × W).
+  split.
+  {
+    solve_WF_matrix.
+    apply diag2_unitary.
+    apply Cmod_1.
+    rewrite Cmod_Cconj.
+    exact u0_unit.
+  }
+  {
+    unfold abgate.
+    rewrite <- Mmult_1_l with (A := I 2); solve_WF_matrix.
+    rewrite <- kron_mixed_product.
+    unfold abgate in H.
+    rewrite Mmult_assoc.
+    rewrite <- H at 1; clear H.
+    (* For performance reasons, we'll show both sides are diagonal first,
+       instead of directly invoking lma'. *)
+    assert (WF_Diagonal (ccu (diag2 C1 (u0 ^* * u1)))).
+    {
+      apply ccu_diag.
+      apply Diag_diag2.
+    }
+    assert (WF_Diagonal (control (diag2 C1 (u0 ^*)) ⊗ I 2 × ccu (diag2 u0 u1))).
+    {
+      apply diag_mult.
+      apply diag_kron.
+      apply diag_control.
+      apply Diag_diag2.
+      apply diag_I.
+      apply ccu_diag.
+      apply Diag_diag2.
+    }
+    prep_matrix_equality.
+    bdestruct (x =? y).
+    {
+      rewrite <- H1; clear H1.
+      destruct H as [H _].
+      destruct H0 as [H0 _].
+      specialize (H x x).
+      specialize (H0 x x).
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; simpl; Csimpl.
+      rewrite <- Cmod_sqr, u0_unit; lca.
+      destruct x.
+      unfold ccu, control, diag2, I, kron, Mmult; lca.
+      rewrite H, <- H0.
+      reflexivity.
+      all: lia.
+    }
+    {
+      destruct H as [_ H].
+      destruct H0 as [_ H0].
+      specialize (H x y H1).
+      specialize (H0 x y H1).
+      rewrite H, <- H0; reflexivity.
+    }
+  }
+Qed.