feat(M3.3): Fully stated and formalized. (#37)

* refactor: Remove `n <> 0` case for `block_decomp_general`.

* feat(M3.3): Reverse direction.

* refactor(M3.2): Use new permutation decomp.

* feat(M3.3): Restate and reprove reverse direction.

* feat(A.6): Restate and reprove (almost).

Still missing some minor proof about natural numbers and modulo.

* fix: Finish/simplify proof for `direct_sum_diagonal`.

* feat(M3.3): Finish formalizing.

Author: kylechui

AlgebraHelpers.v

@@ -2,6 +2,16 @@ Require Import QuantumLib.Complex.
 (* @Kyle: this Matrix dependency is for just 1 thing. Maybe better to rewrite the sub_mul_mod
 proof in here *)
 Require Import QuantumLib.Matrix.
+
+Lemma Cmult_nonzero : forall (a b : C), a <> C0 -> b <> C0 -> a * b <> C0.
+Proof.
+  intros.
+  intro.
+  contradict H0.
+  apply (Cmult_cancel_l a); auto.
+  rewrite H1; lca.
+Qed.
+
 Lemma conj_mult_re_is_nonneg: forall (a: C),
 Re (a^* * a) >= 0.
 Proof.

ControlledUnitaries.v

@@ -80,7 +80,7 @@ assert (prod_decomp_1 : forall (w : Vector 2), WF_Matrix w -> U × (I 2 ⊗ Q) 
     rewrite U_beta at 1. rewrite U_beta_p at 1.
     lma'.
 }
-destruct (@block_decomp_general 2 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]]. lia.
+destruct (@block_decomp 2 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]].
 apply U_unitary.
 assert (prod_decomp_2: forall (w : Vector 2), WF_Matrix w -> U × (I 2 ⊗ Q) × (∣0⟩ ⊗ w) = ∣0⟩ ⊗ (P00 × Q × w) .+ ∣1⟩ ⊗ (P10 × Q × w)).
 {
@@ -189,7 +189,7 @@ assert (I_4_block_decomp: I 4 = ∣0⟩⟨0∣ ⊗ I 2 .+ ∣0⟩⟨1∣ ⊗ Zer
 assert (equal_blocks: (P00) † × P00 = I 2 /\ (Zero (m:= 2) (n:=2)) = (Zero (m:= 2) (n:=2)) 
 /\ (Zero (m:= 2) (n:=2)) = (Zero (m:= 2) (n:=2)) /\ (P11) † × P11 = I 2).
 {
-    apply block_equalities_general with (U := (U) † × U) (V := I 4).
+    apply block_equalities with (U := (U) † × U) (V := I 4).
     lia.
     1,2,3,4,5,6,7,8: solve_WF_matrix.
     1,2: assumption.
@@ -497,4 +497,4 @@ exists (/ √ r .* psi), (/ √ (1 - r) .* phi).
 split. solve_WF_matrix.
 split. solve_WF_matrix.
 split. all: assumption.
-Qed.
+Qed.

GateHelpers.v

@@ -641,8 +641,8 @@ abgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣0⟩⟨1∣ ⊗ TR .+ ∣1⟩⟨1∣ ⊗
 Proof.
 intros U U_unitary zeropassthrough.
 destruct zeropassthrough as [y [WF_y zeropassthrough]].
-destruct (@block_decomp_general 2 U) as [TL [TR [BL [BR [WF_TL [WF_TR [WF_BL [WF_BR decomp]]]]]]]].
-lia. apply U_unitary.
+destruct (@block_decomp 2 U) as [TL [TR [BL [BR [WF_TL [WF_TR [WF_BL [WF_BR decomp]]]]]]]].
+apply U_unitary.
 exists (TL ⊗ I 2), (TR ⊗ I 2), (BR ⊗ I 2).
 split. solve_WF_matrix.
 split. solve_WF_matrix.
@@ -1265,7 +1265,7 @@ assert (WF_BL_block: WF_Matrix ((TR0) † × TL0)). solve_WF_matrix.
 assert (WF_BR_block: WF_Matrix ((TR0) † × TR0 .+ (BR0) † × BR0)). solve_WF_matrix.
 assert (self_eq: (abgate U) † × abgate U = (abgate U) † × abgate U). reflexivity.
 assert (neq40: 4%nat <> 0%nat). lia.
-assert (block_eq:= @block_equalities_general 4%nat ((abgate U) † × abgate U) ((abgate U) † × abgate U) 
+assert (block_eq:= @block_equalities 4%nat ((abgate U) † × abgate U) ((abgate U) † × abgate U) 
 ((TL0) † × TL0) ((TL0) † × TR0) ((TR0) † × TL0) ((TR0) † × TR0 .+ (BR0) † × BR0) (I 4) Zero Zero (I 4) neq40 
 WF_TL0_inv WF_TR_block WF_BL_block WF_BR_block
 (@WF_I 4) (@WF_Zero 4 4) (@WF_Zero 4 4) (@WF_I 4) block_mult abU_inv self_eq).
@@ -1340,4 +1340,4 @@ unfold swapbc.
 rewrite kron_mixed_product.
 rewrite Mmult_1_l. 2: solve_WF_matrix.
 reflexivity.
-Qed.
+Qed.