feat: Prove Lemma M7.5. (#58)

* feat(M7.5): Mostly proven.

* feat(M7.5): Finish proving forwards direction.

* feat(M7.5): Fully proven.

There's most likely a cleaner way to do this, rather than brute-forcing
both directions of the proof.

Author: kylechui

Appendix/A2_UnitaryMatrices.v

@@ -261,7 +261,7 @@ Proof.
           P01† × P01 .+ P11† × P11 = I 2).
   {
     apply block_equalities; solve_WF_matrix.
-    rewrite V_inv.
+    rewrite V_inv at 1.
     Msimpl_light.
     rewrite <- kron_plus_distr_r.
     rewrite Mplus01, id_kron.

Appendix/A5_ControlledUnitaries.v

@@ -187,7 +187,7 @@ assert (equal_blocks: (P00) † × P00 = I 2 /\ (Zero (m:= 2) (n:=2)) = (Zero (m
 /\ (Zero (m:= 2) (n:=2)) = (Zero (m:= 2) (n:=2)) /\ (P11) † × P11 = I 2).
 {
     apply block_equalities; solve_WF_matrix.
-    rewrite <- U_adj_mult_1, <- I_4_block_decomp.
+    rewrite <- U_adj_mult_1, <- I_4_block_decomp at 1.
     apply U_unitary.
 }
 split.
@@ -331,8 +331,7 @@ assert (Main: ∣0⟩ ⊗ psi ⊗ beta .+ ∣0⟩ ⊗ phi ⊗ beta_p =
         rewrite <- swapbc_3q; solve_WF_matrix.
         rewrite <- swapbc_3q with (b := beta_p); solve_WF_matrix.
         rewrite <- Mmult_plus_distr_l.
-        rewrite kron_assoc; solve_WF_matrix.
-        rewrite kron_assoc; solve_WF_matrix.
+        repeat rewrite (@kron_assoc 2 1 2 1 2 1); solve_WF_matrix.
     }
     rewrite Step1. clear Step1.
     assert (Step2: swapbc × (∣0⟩ ⊗ (beta ⊗ psi) .+ ∣0⟩ ⊗ (beta_p ⊗ phi)) = swapbc × (∣0⟩ ⊗ w)).
@@ -372,7 +371,7 @@ assert (Main: ∣0⟩ ⊗ psi ⊗ beta .+ ∣0⟩ ⊗ phi ⊗ beta_p =
     unfold abgate.
     rewrite kron_mixed_product. rewrite kron_mixed_product.
     Msimpl_light; solve_WF_matrix.
-    repeat rewrite <- Mscale_kron_dist_l.
+    repeat rewrite <- (@Mscale_kron_dist_l 4 1 2 1).
     reflexivity.
 }
 (* Moving terms in main to apply a16*)

Appendix/A6_TensorProducts.v

@@ -421,10 +421,10 @@ destruct (Classical_Prop.classic (TensorProd (U × (∣0⟩ ⊗ ∣0⟩)))).
     unfold a. unfold not. intro.
     apply H.
     rewrite a20; solve_WF_matrix.
-    fold a00 a11 a01 a10.
     apply (f_equal (fun f => f + a01 * a10)) in H0.
     rewrite Cplus_0_l in H0.
-    rewrite <- H0.
+    unfold a00, a11, a01, a10 in H0.
+    rewrite <- H0 at 1.
     lca.
 }
 Qed.
@@ -586,10 +586,10 @@ destruct (Classical_Prop.classic (TensorProd (U × (∣1⟩ ⊗ ∣0⟩)))).
     unfold a. unfold not. intro.
     apply H.
     rewrite a20; solve_WF_matrix.
-    fold a00 a11 a01 a10.
     apply (f_equal (fun f => f + a01 * a10)) in H0.
     rewrite Cplus_0_l in H0.
-    rewrite <- H0.
+    unfold a00, a11, a01, a10 in H0.
+    rewrite <- H0 at 1.
     lca.
 }
 Qed.

Appendix/A7_OtherProperties.v

@@ -185,7 +185,7 @@ Zero = I 2 ⊗ Q10 /\
 {
     apply block_eq.
     all: solve_WF_matrix.
-    rewrite <- V3_way1. apply V3_way2.
+    rewrite <- V3_way1 at 1. apply V3_way2.
 }
 destruct eq as [q00_val [q01_zero [q10_zero q11_val]]].
 assert (ztotens: (@Zero 4 4) = I 2 ⊗ (@Zero 2 2)). lma'.
@@ -896,7 +896,7 @@ split.
     apply (f_equal (fun f => I 2 ⊗ U2 × f)).
     assert (assoc_help: I 2 ⊗ (I 2 ⊗ W1) = I 2 ⊗ I 2 ⊗ W1). symmetry. apply kron_assoc. 1,2,3: solve_WF_matrix.
     rewrite assoc_help at 1.
-    rewrite <- swapbc_3gate. 2,3,4: solve_WF_matrix.
+    rewrite <- swapbc_3gate; solve_WF_matrix.
     unfold acgate at 1.
     unfold abgate at 1.
     unfold V3.
@@ -908,14 +908,7 @@ split.
     repeat rewrite Mmult_assoc.
     rewrite <- Mmult_assoc with (A:= swapbc) (B:= swapbc).
     rewrite swapbc_inverse at 1.
-    rewrite Mmult_1_l. 
-    2: {
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_bcgate. solve_WF_matrix.
-    }
+    rewrite Mmult_1_l; solve_WF_matrix.
     rewrite <- Mmult_assoc with (A:= I 2 ⊗ W1 ⊗ I 2).
     assert (kron_mix_help: I 2 ⊗ W1 ⊗ I 2 × ((W0) † ⊗ (W1) † ⊗ I 2) =
     (I 2 ⊗ W1 × ((W0) † ⊗ (W1) †)) ⊗ (I 2 × I 2)). apply kron_mixed_product.
@@ -930,16 +923,8 @@ split.
     repeat rewrite Mmult_assoc.
     rewrite <- Mmult_assoc with (A:= swapbc).
     rewrite swapbc_inverse at 1.
-    rewrite Mmult_1_l.
-    2: {
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_bcgate. solve_WF_matrix.
-    }
-    rewrite kron_assoc. 2,3,4: solve_WF_matrix.
+    rewrite Mmult_1_l; solve_WF_matrix.
+    rewrite (@kron_assoc 2 2 2 2). 2,3,4: solve_WF_matrix.
     rewrite <- Mmult_assoc with (A:= W0 ⊗ I 4).
     rewrite id_kron. simpl.
     assert (kron_mix_help: W0 ⊗ I 4 × ((W0) † ⊗ I 4) = (W0 × (W0) †) ⊗ (I 4 × I 4)). apply kron_mixed_product.
@@ -950,11 +935,7 @@ split.
     rewrite Mmult_1_l.
     2: 
     {
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_mult. solve_WF_matrix.
-        apply WF_bcgate. solve_WF_matrix.
+      solve_WF_matrix.
     }
     rewrite <- swapbc_3gate. 2,3,4: solve_WF_matrix.
     repeat rewrite <- Mmult_assoc.

Helpers/GateHelpers.v

@@ -11,9 +11,6 @@ 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).
@@ -1264,3 +1261,31 @@ rewrite Mmult_1_l. 2: solve_WF_matrix.
 reflexivity.
 Qed.
 
+Definition TwoQubitGate (U : Square 8) := exists (V : Square 4), WF_Unitary V /\ (U = abgate V \/ U = acgate V \/ U = bcgate V).
+
+Lemma abgate_twoqubitgate : forall (U : Square 4), WF_Unitary U -> TwoQubitGate (abgate U).
+Proof.
+  intros U U_unitary.
+  unfold TwoQubitGate.
+  exists U.
+  split. assumption.
+  left. reflexivity.
+Qed.
+
+Lemma acgate_twoqubitgate : forall (U : Square 4), WF_Unitary U -> TwoQubitGate (acgate U).
+Proof.
+  intros U U_unitary.
+  unfold TwoQubitGate.
+  exists U.
+  split. assumption.
+  right. left. reflexivity.
+Qed.
+
+Lemma bcgate_twoqubitgate : forall (U : Square 4), WF_Unitary U -> TwoQubitGate (bcgate U).
+Proof.
+  intros U U_unitary.
+  unfold TwoQubitGate.
+  exists U.
+  split. assumption.
+  right. right. reflexivity.
+Qed.

Helpers/TraceoutHelpers.v

@@ -49,7 +49,7 @@ assert (kron_mix_help: U ⊗ I 2 × (a × (a) † ⊗ (c × (c) †) ⊗ (b × (
  (U × (a × (a) † ⊗ (c × (c) †))) ⊗ (b × (b) †) ).
 {
     rewrite <- Mmult_1_l with (A:= (b × (b) †)) at 2; solve_WF_matrix.
-    apply kron_mixed_product.
+    apply (@kron_mixed_product 4 4 4 2 2 2).
 }
 rewrite kron_mix_help at 1.
 clear kron_mix_help.
@@ -61,7 +61,7 @@ assert (kron_mix_help: U × (a × (a) † ⊗ (c × (c) †)) ⊗ (b × (b) †)
 (U × (a × (a) † ⊗ (c × (c) †)) × (U) †) ⊗ (b × (b) †)).
 {
     rewrite <- Mmult_1_r with (A:= (b × (b) †)) at 2; solve_WF_matrix.
-    apply kron_mixed_product.
+    apply (@kron_mixed_product 4 4 4 2 2 2).
 }
 rewrite kron_mix_help at 1.
 assert (WF_helper1: WF_Matrix (U × (a × (a) † ⊗ (c × (c) †)) × (U) † ⊗ (b × (b) †) × swapbc)).

Helpers/UnitaryHelpers.v

@@ -35,7 +35,7 @@ Proof.
   repeat rewrite kron_0_l.
   rewrite Mplus_0_l, Mplus_0_r.
   rewrite Unitary_P, Unitary_Q.
-  rewrite <- kron_plus_distr_r.
+  rewrite <- (@kron_plus_distr_r 2 2 n n).
   rewrite Mplus01.
   rewrite id_kron.
   reflexivity.

Helpers/WFHelpers.v

@@ -25,19 +25,22 @@ Ltac solve_WF_matrix :=
       | |- WF_Matrix ?A => match goal with
                            | [ H : WF_Matrix A |- _ ] => apply H
                            | [ H : WF_Unitary A |- _ ] => apply H
+                           | [ H : WF_Diagonal A |- _ ] => apply H
                            | [ H : WF_Qubit A |- _ ] => apply H
                            | _ => auto_wf; autounfold with M_db; try unfold A
                            end
       | |- WF_Unitary (adjoint _) => apply adjoint_unitary
       | |- WF_Unitary (Mopp _) => unfold Mopp
-      | |- WF_Unitary (_ × _) => apply Mmult_unitary
+      | |- WF_Unitary (?A × _) => match type of A with
+                                  | Square ?n => apply (@Mmult_unitary n)
+                                  end
       (* TODO: Upstream `direct_sum_unitary`, otherwise we can't have this case *)
       (*| |- WF_Unitary (_ .⊕ _) => apply direct_sum_unitary *)
       | |- WF_Unitary (?A ⊗ ?B) => match type of A with
-                                     | Square ?m => match type of B with
-                                                    | Square ?n => apply (@kron_unitary m n)
-                                                    end
-                                     end
+                                   | Square ?m => match type of B with
+                                                  | Square ?n => apply (@kron_unitary m n)
+                                                  end
+                                   end
       | |- WF_Unitary (control ?A) => match type of A with
                                       | Square ?n => apply (@control_unitary n)
                                       end