From 8a6d90d8833146e3e73327d90c61e98c75771b4e Mon Sep 17 00:00:00 2001 From: Kyle Chui Date: Sun, 16 Jun 2024 23:51:15 -0700 Subject: [PATCH 1/4] feat(M7.4): Fully proven. --- Main.v | 122 +++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 118 insertions(+), 4 deletions(-) diff --git a/Main.v b/Main.v index 851da3b..144b4bd 100644 --- a/Main.v +++ b/Main.v @@ -3191,9 +3191,9 @@ Lemma m7_2 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 -> 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). +Lemma m7_3 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 -> + forall (u2 u3 : C), (u2, u3) = (u0, u1) \/ (u2, u3) = (C1, u0^* * u1) -> + u2 = u3 \/ u2 * u3 = C1 -> (u0 = u1 \/ u0 * u1 = C1). Proof. intros. destruct H1, H2. @@ -3247,7 +3247,121 @@ Theorem m7_4 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 -> V1 × V2 × V3 × V4 = ccu (diag2 u0 u1)) <-> u0 = u1 \/ u0 * u1 = C1. Proof. -Admitted. + intros u0 u1 u0_unit u1_unit. + split. + { + intros. + pose proof (m7_2 u0 u1 u0_unit u1_unit H). + destruct H0. + { + destruct H0 as [U1 [U2 [U3 [U4 [U1_unitary [U2_unitary [U3_unitary [U4_unitary [u2 [u3 [H1 H2]]]]]]]]]]]. + assert (u2_u3_unit : Cmod u2 = 1 /\ Cmod u3 = 1). + { + destruct H1. + { + rewrite pair_equal_spec in H0. + destruct H0. + rewrite H0, H1. + split; auto. + } + { + rewrite pair_equal_spec in H0. + destruct H0. + rewrite H0, H1. + split. apply Cmod_1. + rewrite Cmod_mult. + rewrite Cmod_Cconj. + rewrite u0_unit, u1_unit. + lra. + } + } + destruct u2_u3_unit as [u2_unit u3_unit]. + pose proof (m5_1 u2 u3 u2_unit u3_unit). + assert (u2 = u3 \/ u2 * u3 = C1). + { + rewrite <- H0. + exists U1, U2, U3, U4. + split. assumption. + split. assumption. + split. assumption. + split; assumption. + } + apply (m7_3 u0 u1 u0_unit u1_unit u2 u3); auto. + } + { + destruct H0 as [U1 [U2 [U3 [U4 [U1_unitary [U2_unitary [U3_unitary [U4_unitary [u2 [u3 [H1 H2]]]]]]]]]]]. + assert (u2_u3_unit : Cmod u2 = 1 /\ Cmod u3 = 1). + { + destruct H1. + { + rewrite pair_equal_spec in H0. + destruct H0. + rewrite H0, H1. + split; auto. + } + { + rewrite pair_equal_spec in H0. + destruct H0. + rewrite H0, H1. + split. apply Cmod_1. + rewrite Cmod_mult. + rewrite Cmod_Cconj. + rewrite u0_unit, u1_unit. + lra. + } + } + destruct u2_u3_unit as [u2_unit u3_unit]. + pose proof (m6_4 u2 u3 u2_unit u3_unit). + assert (u2 = u3 \/ u2 * u3 = C1). + { + rewrite <- H0. + exists U1, U2, U3, U4. + split. assumption. + split. assumption. + split. assumption. + split; assumption. + } + apply (m7_3 u0 u1 u0_unit u1_unit u2 u3); auto. + } + } + { + intros. + rewrite <- m5_1 in H; auto. + destruct H as [U1 [U2 [U3 [U4 [U1_unitary [U2_unitary [U3_unitary [U4_unitary H]]]]]]]]. + exists (bcgate U1), (acgate U2), (abgate U3), (bcgate U4). + split. + { + unfold TwoQubitGate. + exists U1. + split. assumption. + right; right; reflexivity. + } + split. + { + unfold TwoQubitGate. + exists U2. + split. assumption. + right; left; reflexivity. + } + split. + { + unfold TwoQubitGate. + exists U3. + split. assumption. + left; reflexivity. + } + split. + { + unfold TwoQubitGate. + exists U4. + split. assumption. + right; right; reflexivity. + } + { + exact H. + } + } +Qed. Corollary m7_5 : forall (U : Square 2), WF_Unitary U -> (exists (V1 V2 V3 V4 : Square 8), From 9602da2a5ba09bab1c420d8cac62e45f37ca25ea Mon Sep 17 00:00:00 2001 From: Kyle Chui Date: Mon, 17 Jun 2024 17:38:06 -0700 Subject: [PATCH 2/4] feat(M7.5): Mostly proven. --- Appendix/A2_UnitaryMatrices.v | 2 +- Appendix/A5_ControlledUnitaries.v | 7 +- Appendix/A6_TensorProducts.v | 8 +- Appendix/A7_OtherProperties.v | 31 +- Helpers/GateHelpers.v | 31 +- Helpers/TraceoutHelpers.v | 4 +- Helpers/UnitaryHelpers.v | 2 +- Helpers/WFHelpers.v | 13 +- Main.v | 593 +++++++++++++++++++++++++++++- 9 files changed, 642 insertions(+), 49 deletions(-) diff --git a/Appendix/A2_UnitaryMatrices.v b/Appendix/A2_UnitaryMatrices.v index 2f04b7a..53fa37d 100644 --- a/Appendix/A2_UnitaryMatrices.v +++ b/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. diff --git a/Appendix/A5_ControlledUnitaries.v b/Appendix/A5_ControlledUnitaries.v index 5dcd5e9..6bdd940 100644 --- a/Appendix/A5_ControlledUnitaries.v +++ b/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*) diff --git a/Appendix/A6_TensorProducts.v b/Appendix/A6_TensorProducts.v index 5f361e4..0c853b4 100644 --- a/Appendix/A6_TensorProducts.v +++ b/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. diff --git a/Appendix/A7_OtherProperties.v b/Appendix/A7_OtherProperties.v index bc62597..db963db 100644 --- a/Appendix/A7_OtherProperties.v +++ b/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. diff --git a/Helpers/GateHelpers.v b/Helpers/GateHelpers.v index fab587c..682e723 100644 --- a/Helpers/GateHelpers.v +++ b/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. diff --git a/Helpers/TraceoutHelpers.v b/Helpers/TraceoutHelpers.v index c0658ca..f3da036 100644 --- a/Helpers/TraceoutHelpers.v +++ b/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)). diff --git a/Helpers/UnitaryHelpers.v b/Helpers/UnitaryHelpers.v index 402ec86..70301d7 100644 --- a/Helpers/UnitaryHelpers.v +++ b/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. diff --git a/Helpers/WFHelpers.v b/Helpers/WFHelpers.v index 7bbeca8..e8929ed 100644 --- a/Helpers/WFHelpers.v +++ b/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 diff --git a/Main.v b/Main.v index 144b4bd..401fa25 100644 --- a/Main.v +++ b/Main.v @@ -1470,7 +1470,7 @@ Proof. apply (f_equal (fun f => f × (I 2 ⊗ P0 × V2 × (I 2 ⊗ Q0))†)) in H3. assert (H4 : WF_Unitary (I 2 ⊗ P0 × V2 × (I 2 ⊗ Q0))†). { - solve_WF_matrix. + simpl; solve_WF_matrix. } destruct H4 as [_ H4]. rewrite adjoint_involutive in H4. @@ -1529,7 +1529,7 @@ Proof. exists (P0 × P1†). split; solve_WF_matrix. exists (W × (I 2 ⊗ V)). - split; solve_WF_matrix. + split. apply Mmult_unitary; solve_WF_matrix. exists (D 0 0)%nat, (D 1 1)%nat. rewrite <- H4. reflexivity. @@ -3368,7 +3368,592 @@ Corollary m7_5 : forall (U : Square 2), WF_Unitary U -> 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. + 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. + intros U U_unitary. + + split. + { + pose proof (a3 U U_unitary). + destruct H as [V [D [V_unitary [D_diagonal H]]]]. + set (u0 := (D 0 0)%nat). + set (u1 := (D 1 1)%nat). + assert (ccu U = (I 2 ⊗ I 2 ⊗ V) × ccu (diag2 u0 u1) × (I 2 ⊗ I 2 ⊗ V†)). + { + assert (diag2 u0 u1 = D). + { + destruct D_diagonal as [WF_D D_diag]. + lma'; solve_WF_matrix. + all: unfold diag2; simpl. + rewrite (D_diag 0 1)%nat. reflexivity. lia. + rewrite (D_diag 1 0)%nat. reflexivity. lia. + } + rewrite H0; clear H0. + unfold ccu at 2. + repeat rewrite control_decomp; solve_WF_matrix. + repeat rewrite kron_plus_distr_l. + repeat rewrite Mmult_plus_distr_l. + repeat rewrite Mmult_plus_distr_r. + repeat rewrite kron_assoc. + repeat rewrite (@kron_mixed_product 2 2 2 4 4 4). + Msimpl_light. + repeat rewrite (@kron_mixed_product 2 2 2 2 2 2). + Msimpl_light. + rewrite (other_unitary_decomp V V_unitary). + rewrite <- H; clear H. + rewrite <- kron_plus_distr_l. + rewrite <- control_decomp. + rewrite id_kron, <- control_decomp. + unfold ccu. + all: solve_WF_matrix. + } + rewrite H0; clear H0. + assert (u0 * u1 = C1 <-> Determinant U = C1). + { + rewrite H. + repeat rewrite <- Determinant_multiplicative. + rewrite <- Cmult_assoc, Cmult_comm with (x := Determinant D), Cmult_assoc. + rewrite Determinant_multiplicative. + rewrite (other_unitary_decomp V V_unitary). + rewrite Det_I. + assert (Determinant D = u0 * u1). + { + subst u0 u1. + unfold Determinant, get_minor; simpl; Csimpl. + destruct D_diagonal as [_ D_diag]. + specialize (D_diag 0 1)%nat as H1. + specialize (D_diag 1 0)%nat as H2. + rewrite H1, H2; auto. + lca. + } + rewrite H0, Cmult_1_l. + reflexivity. + } + intros. + exists V, D. + split. assumption. + split. assumption. + split. assumption. + fold u0 u1. + rewrite <- H0; clear H0. + rewrite <- m7_4. 2, 3: admit. (* TODO: Prove that eigenvalues are units! *) + destruct H1 as [V1 [V2 [V3 [V4 [V1_gate [V2_gate [V3_gate [V4_gate H1]]]]]]]]. + assert (abgate_comm : forall (U : Square 4) (V : Square 2), + WF_Matrix U -> WF_Matrix V -> + abgate U × (I 2 ⊗ I 2 ⊗ V) = (I 2 ⊗ I 2 ⊗ V) × abgate U). + { + intros. + unfold abgate. + repeat rewrite kron_mixed_product. + rewrite id_kron. + Msimpl_light; solve_WF_matrix. + } + assert (bcgate_absorb_l : forall (U : Square 4) (V : Square 2), + WF_Unitary U -> WF_Unitary V -> + (I 2 ⊗ I 2 ⊗ V) × bcgate U = bcgate (I 2 ⊗ V × U)). + { + intros. + unfold bcgate. + rewrite kron_assoc. + rewrite (@kron_mixed_product 2 2 2 4 4 4). + rewrite Mmult_1_l. + all: solve_WF_matrix. + } + assert (bcgate_absorb_r : forall (U : Square 4) (V : Square 2), + WF_Unitary U -> WF_Unitary V -> + bcgate U × (I 2 ⊗ I 2 ⊗ V) = bcgate (U × (I 2 ⊗ V))). + { + intros. + unfold bcgate. + rewrite kron_assoc. + rewrite (@kron_mixed_product 2 2 2 4 4 4). + rewrite Mmult_1_r. + all: solve_WF_matrix. + } + assert (acgate_absorb_l : forall (U : Square 4) (V : Square 2), + WF_Unitary U -> WF_Unitary V -> + (I 2 ⊗ I 2 ⊗ V) × acgate U = acgate (I 2 ⊗ V × U)). + { + intros. + unfold acgate. + rewrite <- Mmult_1_l at 1. + rewrite <- swapbc_inverse at 1. + repeat rewrite <- Mmult_assoc. + do 2 rewrite Mmult_assoc with (A := swapbc). + rewrite swapbc_3gate. + unfold abgate. + rewrite Mmult_assoc with (A := swapbc). + rewrite (@kron_mixed_product 4 4 4 2 2 2). + rewrite Mmult_1_l. + all: solve_WF_matrix. + } + assert (acgate_absorb_r : forall (U : Square 4) (V : Square 2), + WF_Unitary U -> WF_Unitary V -> + acgate U × (I 2 ⊗ I 2 ⊗ V) = acgate (U × (I 2 ⊗ V))). + { + intros. + unfold acgate. + rewrite <- Mmult_1_r at 1. + rewrite <- swapbc_inverse at 1. + repeat rewrite Mmult_assoc. + rewrite <- Mmult_assoc with (A := I 2 ⊗ I 2 ⊗ V0). + do 2 rewrite <- Mmult_assoc with (A := swapbc) (C := swapbc). + rewrite swapbc_3gate. + unfold abgate. + repeat rewrite <- Mmult_assoc. + rewrite Mmult_assoc with (A := swapbc). + rewrite (@kron_mixed_product 4 4 4 2 2 2). + rewrite Mmult_1_r. + all: solve_WF_matrix. + } + + apply (f_equal (fun f => I 2 ⊗ I 2 ⊗ V† × f × (I 2 ⊗ I 2 ⊗ V))) in H1. + repeat rewrite Mmult_assoc in H1. + rewrite (@kron_mixed_product 4 4 4 2 2 2) in H1. + repeat rewrite <- Mmult_assoc in H1. + rewrite kron_mixed_product in H1. + pose proof V_unitary as V_unit. + destruct V_unit as [WF_V V_unit]. + rewrite V_unit in H1. + rewrite id_kron in H1 at 3 4 5 6. + do 2 rewrite Mmult_1_l in H1. + do 2 rewrite (id_kron (2 * 2) 2) in H1 at 1. + rewrite Mmult_1_l, Mmult_1_r in H1. + all: solve_WF_matrix. + + (* Show that ccu uses at most 4 two qubit gates *) + destruct V1_gate as [V1' [V1'_unitary [V1_ab | [V1_ac | V1_bc]]]]. + { + rewrite V1_ab, <- abgate_comm in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V1') in H1. + destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. + { + rewrite V2_ab, <- abgate_comm in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V2') in H1. + destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. + { + rewrite V3_ab, <- abgate_comm in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V3') in H1. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + rewrite V4_ab, <- abgate_comm in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V4') in H1. + rewrite id_kron in H1. + rewrite kron_mixed_product in H1. + rewrite V_unit in H1. + rewrite Mmult_1_l in H1; solve_WF_matrix. + rewrite id_kron in H1. + rewrite Mmult_1_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (abgate V3'), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V4_ac, acgate_absorb_l, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (abgate V3'), (acgate ((I 2 ⊗ V†) × V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. + apply acgate_twoqubitgate. simpl. solve_WF_matrix. + assumption. + } + { + rewrite V4_bc, bcgate_absorb_l, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (abgate V3'), (bcgate ((I 2 ⊗ V†) × V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. + apply bcgate_twoqubitgate. simpl. solve_WF_matrix. + assumption. + } + } + { + rewrite V3_ac, acgate_absorb_l in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (B := V4) in H1. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4') in H1. + rewrite acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate. simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3')), (acgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply acgate_twoqubitgate; solve_WF_matrix. + assumption. + } + { + rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3')), (bcgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + assumption. + } + } + { + rewrite V3_bc, bcgate_absorb_l in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc with (B := V4) in H1. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4') in H1. + rewrite bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate. simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3')), (acgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply acgate_twoqubitgate; solve_WF_matrix. + assumption. + } + { + rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3')), (bcgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + assumption. + } + } + } + { + rewrite V2_ac, acgate_absorb_l in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc in H1. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4') in H1. + destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. + { + rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + repeat rewrite Mmult_assoc with (A := abgate V1') in H1. + rewrite acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate. simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), V3, (acgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + assumption. + } + { + rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), V3, (bcgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + assumption. + } + } + { + rewrite V2_bc, bcgate_absorb_l in H1; solve_WF_matrix. + repeat rewrite Mmult_assoc in H1. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4') in H1. + destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. + { + rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + repeat rewrite Mmult_assoc with (A := abgate V1') in H1. + rewrite bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate. simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), V3, (acgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + assumption. + } + { + rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), V3, (bcgate (V4' × (I 2 ⊗ V))). + split. apply abgate_twoqubitgate; assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + assumption. + } + } + } + { + rewrite V1_ac, acgate_absorb_l in H1; solve_WF_matrix. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + repeat rewrite Mmult_assoc in H1. + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (A := V3) in H1. + destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. + { + rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc with (A := V2) in H1. + destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. + { + rewrite V2_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + rewrite acgate_absorb_r in H1; solve_WF_matrix. + exists (acgate ((I 2 ⊗ V†) × V1' × (I 2 ⊗ V))), (abgate V2'), (abgate V3'), (abgate V4'). + split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V2_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (acgate ((I 2 ⊗ V†) × V1')), (acgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V2_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (acgate ((I 2 ⊗ V†) × V1')), (bcgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (acgate ((I 2 ⊗ V†) × V1')), V2, (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (acgate ((I 2 ⊗ V†) × V1')), V2, (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + exists (acgate ((I 2 ⊗ V†) × V1')), V2, V3, (V4 × (I 2 ⊗ I 2 ⊗ V)). + split. + apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. assumption. + split. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + apply acgate_twoqubitgate; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + assumption. + } + { + exists (acgate ((I 2 ⊗ V†) × V1')), V2, V3, (V4 × (I 2 ⊗ I 2 ⊗ V)). + split. + apply acgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. assumption. + split. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + apply bcgate_twoqubitgate; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + assumption. + } + } + { + rewrite V1_bc, bcgate_absorb_l in H1; solve_WF_matrix. + destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. + { + repeat rewrite Mmult_assoc in H1. + rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. + rewrite <- Mmult_assoc with (A := V3) in H1. + destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. + { + rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc with (A := V2) in H1. + destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. + { + rewrite V2_ab, abgate_comm in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + rewrite bcgate_absorb_r in H1; solve_WF_matrix. + exists (bcgate ((I 2 ⊗ V†) × V1' × (I 2 ⊗ V))), (abgate V2'), (abgate V3'), (abgate V4'). + split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V2_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), (acgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V2_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), (bcgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). + split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), V2, (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + { + rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), V2, (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. apply abgate_twoqubitgate; assumption. + assumption. + } + } + { + repeat rewrite Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), V2, V3, (acgate (V4' × (I 2 ⊗ V))). + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. assumption. + split. apply acgate_twoqubitgate; solve_WF_matrix. + assumption. + } + { + repeat rewrite Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. + repeat rewrite <- Mmult_assoc in H1. + exists (bcgate ((I 2 ⊗ V†) × V1')), V2, V3, (bcgate (V4' × (I 2 ⊗ V))). + split. apply bcgate_twoqubitgate; solve_WF_matrix. + split. assumption. + split. assumption. + split. apply bcgate_twoqubitgate; solve_WF_matrix. + assumption. + } + } Admitted. From 9f57446b43a75ce5693656e8cd7f2dedbfe9049a Mon Sep 17 00:00:00 2001 From: Kyle Chui Date: Mon, 17 Jun 2024 18:13:39 -0700 Subject: [PATCH 3/4] feat(M7.5): Finish proving forwards direction. --- Main.v | 88 ++++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 76 insertions(+), 12 deletions(-) diff --git a/Main.v b/Main.v index 401fa25..75e70cf 100644 --- a/Main.v +++ b/Main.v @@ -1715,7 +1715,7 @@ Proof. repeat rewrite Mmult_plus_distr_l. repeat rewrite Mmult_plus_distr_r. repeat rewrite kron_mixed_product. - (* PERF: These Msimpl_lights are non-trivially expensive, can optimize later*) + (* PERF: These Msimpl_lights are non-trivially expensive, can optimize later *) repeat rewrite Mmult_1_r. repeat rewrite <- kron_assoc. repeat rewrite (@kron_mixed_product 4 4 4 2 2 2). @@ -1776,14 +1776,14 @@ Proof. destruct H. { left. - apply (f_equal (fun f => f^*)) in H. + apply (f_equal (fun f => f^* )) in H. repeat rewrite Cconj_involutive in H. exact H. } { right. rewrite <- Cconj_mult_distr in H. - apply (f_equal (fun f => f^*)) in H. + apply (f_equal (fun f => f^* )) in H. rewrite Cconj_involutive in H. rewrite H; lca. } @@ -1802,7 +1802,7 @@ Proof. } } } - assert (diag2_adjoint : diag2 (u0 ^*) (u1 ^*) = (diag2 u0 u1)†). + assert (diag2_adjoint : diag2 (u0 ^* ) (u1 ^* ) = (diag2 u0 u1)†). { lma'. all: unfold diag2, adjoint; simpl; reflexivity. @@ -1867,7 +1867,7 @@ Proof. rewrite <- Cmod_Cconj in unit_u0, unit_u1. pose proof ( m4_3 - (u0^*) (u1^*) + (u0^* ) (u1^* ) unit_u0 unit_u1 ). rewrite <- H0 in H; clear H0. @@ -1890,7 +1890,7 @@ Proof. reflexivity. } { - (* TODO: A bit repetitive here; we can probably pull this out to an assertion*) + (* TODO: A bit repetitive here; we can probably pull this out to an assertion *) rewrite diag2_adjoint in H0. unfold ccu in H0. repeat rewrite <- control_adjoint in H0. @@ -3103,7 +3103,7 @@ Lemma m7_1 : forall (u0 u1 : C), Cmod u0 = 1 -> Cmod u1 = 1 -> 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). + exists (control (diag2 C1 (u0^* )) × W). split. { solve_WF_matrix. @@ -3126,7 +3126,7 @@ Proof. apply ccu_diag. apply Diag_diag2. } - assert (WF_Diagonal (control (diag2 C1 (u0 ^*)) ⊗ I 2 × ccu (diag2 u0 u1))). + assert (WF_Diagonal (control (diag2 C1 (u0 ^* )) ⊗ I 2 × ccu (diag2 u0 u1))). { apply diag_mult. apply diag_kron. @@ -3220,7 +3220,7 @@ Proof. rewrite Cmult_1_r in H3. rewrite H3. rewrite Cmult_assoc. - replace (u0 * u0^*) with ((u0^* * u0)^*) by lca. + replace (u0 * u0^* ) with ((u0^* * u0)^* ) by lca. rewrite <- Cmod_sqr. rewrite H. lca. @@ -3234,7 +3234,7 @@ Proof. rewrite Cmult_1_r in H2. rewrite <- H2. rewrite Cmult_assoc. - replace (u0 * u0^*) with ((u0^* * u0)^*) by lca. + replace (u0 * u0^* ) with ((u0^* * u0)^* ) by lca. rewrite <- Cmod_sqr. rewrite H. lca. @@ -3372,7 +3372,6 @@ Corollary m7_5 : forall (U : Square 2), WF_Unitary U -> U = V × D × V† /\ ((D 0 0 = D 1 1)%nat \/ Determinant U = C1). Proof. intros U U_unitary. - split. { pose proof (a3 U U_unitary). @@ -3430,6 +3429,67 @@ Proof. rewrite H0, Cmult_1_l. reflexivity. } + assert (Cmod u0 = 1 /\ Cmod u1 = 1). + { + destruct U_unitary as [WF_U U_unit]. + destruct V_unitary as [WF_V V_unit]. + revert U_unit. + rewrite H; clear H. + distribute_adjoint. + rewrite adjoint_involutive. + repeat rewrite <- Mmult_assoc. + do 2 rewrite Mmult_assoc with (A := V). + rewrite Mmult_assoc with (A := D†). + rewrite V_unit, Mmult_1_r; solve_WF_matrix. + intro H. + apply (f_equal (fun f => V† × f × V)) in H. + repeat rewrite Mmult_assoc in H. + rewrite V_unit in H. + repeat rewrite <- Mmult_assoc in H. + rewrite V_unit in H. + rewrite Mmult_1_l in H; solve_WF_matrix. + do 2 rewrite Mmult_1_r in H; solve_WF_matrix. + rewrite V_unit in H. + destruct D_diagonal as [WF_D D_diag]. + split. + { + apply (f_equal (fun f => f 0 0)%nat) in H. + unfold adjoint, Mmult, I in H; simpl in H. + rewrite (@D_diag 1 0)%nat in H; try lia. + revert H; Csimpl; intro H. + rewrite <- Cmod_sqr in H. + fold u0 in H. + apply Rsqr_inj. + apply Cmod_ge_0. + lra. + apply pair_equal_spec in H. + destruct H as [H _]. + rewrite Rsqr_1. + unfold Rsqr. + rewrite <- H; clear H. + Csimpl; simpl. + lra. + } + { + apply (f_equal (fun f => f 1 1)%nat) in H. + unfold adjoint, Mmult, I in H; simpl in H. + rewrite (@D_diag 0 1)%nat in H; try lia. + revert H; Csimpl; intro H. + rewrite <- Cmod_sqr in H. + fold u1 in H. + apply Rsqr_inj. + apply Cmod_ge_0. + lra. + apply pair_equal_spec in H. + destruct H as [H _]. + rewrite Rsqr_1. + unfold Rsqr. + rewrite <- H; clear H. + Csimpl; simpl. + lra. + } + } + destruct H1 as [u0_unit u1_unit]. intros. exists V, D. split. assumption. @@ -3437,7 +3497,7 @@ Proof. split. assumption. fold u0 u1. rewrite <- H0; clear H0. - rewrite <- m7_4. 2, 3: admit. (* TODO: Prove that eigenvalues are units! *) + rewrite <- m7_4; auto. destruct H1 as [V1 [V2 [V3 [V4 [V1_gate [V2_gate [V3_gate [V4_gate H1]]]]]]]]. assert (abgate_comm : forall (U : Square 4) (V : Square 2), WF_Matrix U -> WF_Matrix V -> @@ -3956,4 +4016,8 @@ Proof. assumption. } } + } + { + admit. + } Admitted. From 1e429f001d067b03076bf9a5dbc9fe0fc45dcdbb Mon Sep 17 00:00:00 2001 From: Kyle Chui Date: Tue, 18 Jun 2024 22:07:11 -0700 Subject: [PATCH 4/4] feat(M7.5): Fully proven. There's most likely a cleaner way to do this, rather than brute-forcing both directions of the proof. --- Main.v | 667 ++++++++++++++++++++++++++++++++------------------------- 1 file changed, 377 insertions(+), 290 deletions(-) diff --git a/Main.v b/Main.v index 75e70cf..b739b58 100644 --- a/Main.v +++ b/Main.v @@ -3371,134 +3371,13 @@ Corollary m7_5 : forall (U : Square 2), WF_Unitary 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. - intros U U_unitary. - split. + assert (absorption_helper : forall (V : Square 2), WF_Unitary V -> + forall (V1 V2 V3 V4 : Square 8), + TwoQubitGate V1 -> TwoQubitGate V2 -> TwoQubitGate V3 -> TwoQubitGate V4 -> + exists (W1 W2 W3 W4 : Square 8), + TwoQubitGate W1 /\ TwoQubitGate W2 /\ TwoQubitGate W3 /\ TwoQubitGate W4 /\ + W1 × W2 × W3 × W4 = (I 2 ⊗ I 2 ⊗ V†) × V1 × V2 × V3 × V4 × (I 2 ⊗ I 2 ⊗ V)). { - pose proof (a3 U U_unitary). - destruct H as [V [D [V_unitary [D_diagonal H]]]]. - set (u0 := (D 0 0)%nat). - set (u1 := (D 1 1)%nat). - assert (ccu U = (I 2 ⊗ I 2 ⊗ V) × ccu (diag2 u0 u1) × (I 2 ⊗ I 2 ⊗ V†)). - { - assert (diag2 u0 u1 = D). - { - destruct D_diagonal as [WF_D D_diag]. - lma'; solve_WF_matrix. - all: unfold diag2; simpl. - rewrite (D_diag 0 1)%nat. reflexivity. lia. - rewrite (D_diag 1 0)%nat. reflexivity. lia. - } - rewrite H0; clear H0. - unfold ccu at 2. - repeat rewrite control_decomp; solve_WF_matrix. - repeat rewrite kron_plus_distr_l. - repeat rewrite Mmult_plus_distr_l. - repeat rewrite Mmult_plus_distr_r. - repeat rewrite kron_assoc. - repeat rewrite (@kron_mixed_product 2 2 2 4 4 4). - Msimpl_light. - repeat rewrite (@kron_mixed_product 2 2 2 2 2 2). - Msimpl_light. - rewrite (other_unitary_decomp V V_unitary). - rewrite <- H; clear H. - rewrite <- kron_plus_distr_l. - rewrite <- control_decomp. - rewrite id_kron, <- control_decomp. - unfold ccu. - all: solve_WF_matrix. - } - rewrite H0; clear H0. - assert (u0 * u1 = C1 <-> Determinant U = C1). - { - rewrite H. - repeat rewrite <- Determinant_multiplicative. - rewrite <- Cmult_assoc, Cmult_comm with (x := Determinant D), Cmult_assoc. - rewrite Determinant_multiplicative. - rewrite (other_unitary_decomp V V_unitary). - rewrite Det_I. - assert (Determinant D = u0 * u1). - { - subst u0 u1. - unfold Determinant, get_minor; simpl; Csimpl. - destruct D_diagonal as [_ D_diag]. - specialize (D_diag 0 1)%nat as H1. - specialize (D_diag 1 0)%nat as H2. - rewrite H1, H2; auto. - lca. - } - rewrite H0, Cmult_1_l. - reflexivity. - } - assert (Cmod u0 = 1 /\ Cmod u1 = 1). - { - destruct U_unitary as [WF_U U_unit]. - destruct V_unitary as [WF_V V_unit]. - revert U_unit. - rewrite H; clear H. - distribute_adjoint. - rewrite adjoint_involutive. - repeat rewrite <- Mmult_assoc. - do 2 rewrite Mmult_assoc with (A := V). - rewrite Mmult_assoc with (A := D†). - rewrite V_unit, Mmult_1_r; solve_WF_matrix. - intro H. - apply (f_equal (fun f => V† × f × V)) in H. - repeat rewrite Mmult_assoc in H. - rewrite V_unit in H. - repeat rewrite <- Mmult_assoc in H. - rewrite V_unit in H. - rewrite Mmult_1_l in H; solve_WF_matrix. - do 2 rewrite Mmult_1_r in H; solve_WF_matrix. - rewrite V_unit in H. - destruct D_diagonal as [WF_D D_diag]. - split. - { - apply (f_equal (fun f => f 0 0)%nat) in H. - unfold adjoint, Mmult, I in H; simpl in H. - rewrite (@D_diag 1 0)%nat in H; try lia. - revert H; Csimpl; intro H. - rewrite <- Cmod_sqr in H. - fold u0 in H. - apply Rsqr_inj. - apply Cmod_ge_0. - lra. - apply pair_equal_spec in H. - destruct H as [H _]. - rewrite Rsqr_1. - unfold Rsqr. - rewrite <- H; clear H. - Csimpl; simpl. - lra. - } - { - apply (f_equal (fun f => f 1 1)%nat) in H. - unfold adjoint, Mmult, I in H; simpl in H. - rewrite (@D_diag 0 1)%nat in H; try lia. - revert H; Csimpl; intro H. - rewrite <- Cmod_sqr in H. - fold u1 in H. - apply Rsqr_inj. - apply Cmod_ge_0. - lra. - apply pair_equal_spec in H. - destruct H as [H _]. - rewrite Rsqr_1. - unfold Rsqr. - rewrite <- H; clear H. - Csimpl; simpl. - lra. - } - } - destruct H1 as [u0_unit u1_unit]. - intros. - exists V, D. - split. assumption. - split. assumption. - split. assumption. - fold u0 u1. - rewrite <- H0; clear H0. - rewrite <- m7_4; auto. - destruct H1 as [V1 [V2 [V3 [V4 [V1_gate [V2_gate [V3_gate [V4_gate H1]]]]]]]]. assert (abgate_comm : forall (U : Square 4) (V : Square 2), WF_Matrix U -> WF_Matrix V -> abgate U × (I 2 ⊗ I 2 ⊗ V) = (I 2 ⊗ I 2 ⊗ V) × abgate U). @@ -3557,7 +3436,7 @@ Proof. rewrite <- Mmult_1_r at 1. rewrite <- swapbc_inverse at 1. repeat rewrite Mmult_assoc. - rewrite <- Mmult_assoc with (A := I 2 ⊗ I 2 ⊗ V0). + rewrite <- Mmult_assoc with (A := I 2 ⊗ I 2 ⊗ V). do 2 rewrite <- Mmult_assoc with (A := swapbc) (C := swapbc). rewrite swapbc_3gate. unfold abgate. @@ -3568,339 +3447,327 @@ Proof. all: solve_WF_matrix. } - apply (f_equal (fun f => I 2 ⊗ I 2 ⊗ V† × f × (I 2 ⊗ I 2 ⊗ V))) in H1. - repeat rewrite Mmult_assoc in H1. - rewrite (@kron_mixed_product 4 4 4 2 2 2) in H1. - repeat rewrite <- Mmult_assoc in H1. - rewrite kron_mixed_product in H1. - pose proof V_unitary as V_unit. - destruct V_unit as [WF_V V_unit]. - rewrite V_unit in H1. - rewrite id_kron in H1 at 3 4 5 6. - do 2 rewrite Mmult_1_l in H1. - do 2 rewrite (id_kron (2 * 2) 2) in H1 at 1. - rewrite Mmult_1_l, Mmult_1_r in H1. - all: solve_WF_matrix. - + intros V V_unitary V1 V2 V3 V4 V1_gate V2_gate V3_gate V4_gate. + pose proof V_unitary as [WF_V V_unit]. (* Show that ccu uses at most 4 two qubit gates *) destruct V1_gate as [V1' [V1'_unitary [V1_ab | [V1_ac | V1_bc]]]]. { - rewrite V1_ab, <- abgate_comm in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (A := abgate V1') in H1. + rewrite V1_ab, <- abgate_comm; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V1'). destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. { - rewrite V2_ab, <- abgate_comm in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (A := abgate V2') in H1. + rewrite V2_ab, <- abgate_comm; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V2'). destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. { - rewrite V3_ab, <- abgate_comm in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (A := abgate V3') in H1. + rewrite V3_ab, <- abgate_comm; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V3'). destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - rewrite V4_ab, <- abgate_comm in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (A := abgate V4') in H1. - rewrite id_kron in H1. - rewrite kron_mixed_product in H1. - rewrite V_unit in H1. - rewrite Mmult_1_l in H1; solve_WF_matrix. - rewrite id_kron in H1. - rewrite Mmult_1_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ab, <- abgate_comm; solve_WF_matrix. + repeat rewrite Mmult_assoc with (A := abgate V4'). + rewrite id_kron. + rewrite (@kron_mixed_product 4 4 4 2 2 2). + rewrite V_unit. + rewrite Mmult_1_l; solve_WF_matrix. + rewrite id_kron. + rewrite Mmult_1_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (abgate V3'), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V4_ac, acgate_absorb_l, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_l, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (abgate V3'), (acgate ((I 2 ⊗ V†) × V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate. simpl. solve_WF_matrix. - assumption. + reflexivity. } { - rewrite V4_bc, bcgate_absorb_l, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_l, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (abgate V3'), (bcgate ((I 2 ⊗ V†) × V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate. simpl. solve_WF_matrix. - assumption. + reflexivity. } } { - rewrite V3_ac, acgate_absorb_l in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (B := V4) in H1. + rewrite V3_ac, acgate_absorb_l; solve_WF_matrix. + repeat rewrite Mmult_assoc with (B := V4). destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (C := abgate V4') in H1. - rewrite acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4'). + rewrite acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate. simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3')), (acgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply acgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } { - rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (acgate ((I 2 ⊗ V†) × V3')), (bcgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } } { - rewrite V3_bc, bcgate_absorb_l in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc with (B := V4) in H1. + rewrite V3_bc, bcgate_absorb_l; solve_WF_matrix. + repeat rewrite Mmult_assoc with (B := V4). destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (C := abgate V4') in H1. - rewrite bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4'). + rewrite bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate. simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3')), (acgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply acgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } { - rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (abgate V2'), (bcgate ((I 2 ⊗ V†) × V3')), (bcgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } } } { - rewrite V2_ac, acgate_absorb_l in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc in H1. + rewrite V2_ac, acgate_absorb_l; solve_WF_matrix. + repeat rewrite Mmult_assoc. destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (C := abgate V4') in H1. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4'). destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. { - rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. - repeat rewrite Mmult_assoc with (A := abgate V1') in H1. - rewrite acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + repeat rewrite Mmult_assoc with (A := abgate V1'). + rewrite acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate. simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { - rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), V3, (acgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } { - rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (acgate ((I 2 ⊗ V†) × V2')), V3, (bcgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } } { - rewrite V2_bc, bcgate_absorb_l in H1; solve_WF_matrix. - repeat rewrite Mmult_assoc in H1. + rewrite V2_bc, bcgate_absorb_l; solve_WF_matrix. + repeat rewrite Mmult_assoc. destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (C := abgate V4') in H1. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (C := abgate V4'). destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. { - rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. - repeat rewrite Mmult_assoc with (A := abgate V1') in H1. - rewrite bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + repeat rewrite Mmult_assoc with (A := abgate V1'). + rewrite bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate. simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { - rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), V3, (acgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } { - rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (abgate V1'), (bcgate ((I 2 ⊗ V†) × V2')), V3, (bcgate (V4' × (I 2 ⊗ V))). split. apply abgate_twoqubitgate; assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } } } { - rewrite V1_ac, acgate_absorb_l in H1; solve_WF_matrix. + rewrite V1_ac, acgate_absorb_l; solve_WF_matrix. destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - repeat rewrite Mmult_assoc in H1. - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (A := V3) in H1. + repeat rewrite Mmult_assoc. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (A := V3). destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. { - rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc with (A := V2) in H1. + rewrite V3_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc with (A := V2). destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. { - rewrite V2_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. - rewrite acgate_absorb_r in H1; solve_WF_matrix. + rewrite V2_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + rewrite acgate_absorb_r; solve_WF_matrix. exists (acgate ((I 2 ⊗ V†) × V1' × (I 2 ⊗ V))), (abgate V2'), (abgate V3'), (abgate V4'). split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V2_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V2_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (acgate ((I 2 ⊗ V†) × V1')), (acgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V2_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V2_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (acgate ((I 2 ⊗ V†) × V1')), (bcgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply acgate_twoqubitgate; simpl; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { - rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (acgate ((I 2 ⊗ V†) × V1')), V2, (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply acgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (acgate ((I 2 ⊗ V†) × V1')), V2, (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply acgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { @@ -3913,7 +3780,7 @@ Proof. rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. apply acgate_twoqubitgate; solve_WF_matrix. repeat rewrite <- Mmult_assoc. - assumption. + reflexivity. } { exists (acgate ((I 2 ⊗ V†) × V1')), V2, V3, (V4 × (I 2 ⊗ I 2 ⊗ V)). @@ -3925,99 +3792,319 @@ Proof. rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. apply bcgate_twoqubitgate; solve_WF_matrix. repeat rewrite <- Mmult_assoc. - assumption. + reflexivity. } } { - rewrite V1_bc, bcgate_absorb_l in H1; solve_WF_matrix. + rewrite V1_bc, bcgate_absorb_l; solve_WF_matrix. destruct V4_gate as [V4' [V4'_unitary [V4_ab | [V4_ac | V4_bc]]]]. { - repeat rewrite Mmult_assoc in H1. - rewrite V4_ab, abgate_comm in H1; solve_WF_matrix. - rewrite <- Mmult_assoc with (A := V3) in H1. + repeat rewrite Mmult_assoc. + rewrite V4_ab, abgate_comm; solve_WF_matrix. + rewrite <- Mmult_assoc with (A := V3). destruct V3_gate as [V3' [V3'_unitary [V3_ab | [V3_ac | V3_bc]]]]. { - rewrite V3_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc with (A := V2) in H1. + rewrite V3_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc with (A := V2). destruct V2_gate as [V2' [V2'_unitary [V2_ab | [V2_ac | V2_bc]]]]. { - rewrite V2_ab, abgate_comm in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. - rewrite bcgate_absorb_r in H1; solve_WF_matrix. + rewrite V2_ab, abgate_comm; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. + rewrite bcgate_absorb_r; solve_WF_matrix. exists (bcgate ((I 2 ⊗ V†) × V1' × (I 2 ⊗ V))), (abgate V2'), (abgate V3'), (abgate V4'). split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V2_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V2_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), (acgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V2_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V2_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), (bcgate (V2' × (I 2 ⊗ V))), (abgate V3'), (abgate V4'). split. apply bcgate_twoqubitgate; simpl; solve_WF_matrix. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { - rewrite V3_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), V2, (acgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } { - rewrite V3_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + rewrite V3_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), V2, (bcgate (V3' × (I 2 ⊗ V))), (abgate V4'). split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. split. apply abgate_twoqubitgate; assumption. - assumption. + reflexivity. } } { - repeat rewrite Mmult_assoc in H1. - rewrite V4_ac, acgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + repeat rewrite Mmult_assoc. + rewrite V4_ac, acgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), V2, V3, (acgate (V4' × (I 2 ⊗ V))). split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. assumption. split. apply acgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } { - repeat rewrite Mmult_assoc in H1. - rewrite V4_bc, bcgate_absorb_r in H1; solve_WF_matrix. - repeat rewrite <- Mmult_assoc in H1. + repeat rewrite Mmult_assoc. + rewrite V4_bc, bcgate_absorb_r; solve_WF_matrix. + repeat rewrite <- Mmult_assoc. exists (bcgate ((I 2 ⊗ V†) × V1')), V2, V3, (bcgate (V4' × (I 2 ⊗ V))). split. apply bcgate_twoqubitgate; solve_WF_matrix. split. assumption. split. assumption. split. apply bcgate_twoqubitgate; solve_WF_matrix. - assumption. + reflexivity. } } } + assert (forall (U D V : Square 2), WF_Unitary V -> WF_Matrix D -> + U = V × D × V† -> + ccu U = (I 2 ⊗ I 2 ⊗ V) × ccu D × (I 2 ⊗ I 2 ⊗ V†)). { - admit. + intros U D V V_unitary WF_D U_decomp. + rewrite U_decomp; clear U_decomp. + unfold ccu at 2. + repeat rewrite control_decomp; solve_WF_matrix. + repeat rewrite kron_plus_distr_l. + repeat rewrite Mmult_plus_distr_l. + repeat rewrite Mmult_plus_distr_r. + repeat rewrite kron_assoc. + repeat rewrite (@kron_mixed_product 2 2 2 4 4 4). + Msimpl_light. + repeat rewrite (@kron_mixed_product 2 2 2 2 2 2). + Msimpl_light. + rewrite (other_unitary_decomp V V_unitary). + rewrite <- kron_plus_distr_l. + rewrite <- control_decomp. + rewrite id_kron, <- control_decomp. + unfold ccu. + all: solve_WF_matrix. } -Admitted. + assert (forall (U D V : Square 2), WF_Unitary U -> WF_Diagonal D -> WF_Unitary V -> + U = V × D × V† -> Cmod (D 0 0)%nat = 1 /\ Cmod (D 1 1)%nat = 1). + { + intros U D V U_unitary D_diagonal V_unitary U_decomp. + destruct U_unitary as [WF_U U_unit]. + destruct V_unitary as [WF_V V_unit]. + revert U_unit. + rewrite U_decomp; clear U_decomp. + distribute_adjoint. + rewrite adjoint_involutive. + repeat rewrite <- Mmult_assoc. + do 2 rewrite Mmult_assoc with (A := V). + rewrite Mmult_assoc with (A := D†). + rewrite V_unit, Mmult_1_r; solve_WF_matrix. + intro H0. + apply (f_equal (fun f => V† × f × V)) in H0. + repeat rewrite Mmult_assoc in H0. + rewrite V_unit in H0. + repeat rewrite <- Mmult_assoc in H0. + rewrite V_unit in H0. + rewrite Mmult_1_l in H0; solve_WF_matrix. + do 2 rewrite Mmult_1_r in H0; solve_WF_matrix. + rewrite V_unit in H0. + destruct D_diagonal as [WF_D D_diag]. + split. + { + apply (f_equal (fun f => f 0 0)%nat) in H0. + unfold adjoint, Mmult, I in H0; simpl in H0. + rewrite (@D_diag 1 0)%nat in H0; try lia. + revert H0; Csimpl; intro H0. + rewrite <- Cmod_sqr in H0. + apply Rsqr_inj. + apply Cmod_ge_0. + lra. + apply pair_equal_spec in H0. + destruct H0 as [H0 _]. + rewrite Rsqr_1. + unfold Rsqr. + rewrite <- H0; clear H0. + Csimpl; simpl. + lra. + } + { + apply (f_equal (fun f => f 1 1)%nat) in H0. + unfold adjoint, Mmult, I in H0; simpl in H0. + rewrite (@D_diag 0 1)%nat in H0; try lia. + revert H0; Csimpl; intro H0. + rewrite <- Cmod_sqr in H0. + apply Rsqr_inj. + apply Cmod_ge_0. + lra. + apply pair_equal_spec in H0. + destruct H0 as [H0 _]. + rewrite Rsqr_1. + unfold Rsqr. + rewrite <- H0; clear H0. + Csimpl; simpl. + lra. + } + } + assert (forall (U D V : Square 2), WF_Unitary U -> WF_Diagonal D -> WF_Unitary V -> + U = V × D × V† -> (D 0 0)%nat * (D 1 1)%nat = C1 <-> Determinant U = C1). + { + intros U D V U_unitary D_diagonal V_unitary U_decomp. + rewrite U_decomp. + repeat rewrite <- Determinant_multiplicative. + rewrite <- Cmult_assoc, Cmult_comm with (x := Determinant D), Cmult_assoc. + rewrite Determinant_multiplicative. + rewrite (other_unitary_decomp V V_unitary). + rewrite Det_I. + assert (Determinant D = (D 0 0)%nat * (D 1 1)%nat). + { + unfold Determinant, get_minor; simpl; Csimpl. + destruct D_diagonal as [_ D_diag]. + specialize (D_diag 0 1)%nat as H1. + specialize (D_diag 1 0)%nat as H2. + rewrite H1, H2; auto. + lca. + } + rewrite H1, Cmult_1_l. + reflexivity. + } + + intros U U_unitary. + split. + { + pose proof (a3 U U_unitary). + destruct H2 as [V [D [V_unitary [D_diagonal U_decomp]]]]. + pose proof V_unitary as [WF_V V_unit]. + set (u0 := (D 0 0)%nat). + set (u1 := (D 1 1)%nat). + assert (ccu U = (I 2 ⊗ I 2 ⊗ V) × ccu (diag2 u0 u1) × (I 2 ⊗ I 2 ⊗ V†)). + { + assert (diag2 u0 u1 = D). + { + destruct D_diagonal as [WF_D D_diag]. + lma'; solve_WF_matrix. + all: unfold diag2; simpl. + rewrite (D_diag 0 1)%nat. reflexivity. lia. + rewrite (D_diag 1 0)%nat. reflexivity. lia. + } + rewrite (H U D V), H2; solve_WF_matrix. + } + rewrite H2; clear H2. + assert (u0 * u1 = C1 <-> Determinant U = C1). + { + rewrite U_decomp. + repeat rewrite <- Determinant_multiplicative. + rewrite <- Cmult_assoc, Cmult_comm with (x := Determinant D), Cmult_assoc. + rewrite Determinant_multiplicative. + rewrite (other_unitary_decomp V V_unitary). + rewrite Det_I. + assert (Determinant D = u0 * u1). + { + subst u0 u1. + unfold Determinant, get_minor; simpl; Csimpl. + destruct D_diagonal as [_ D_diag]. + rewrite (D_diag 0 1)%nat, (D_diag 1 0)%nat; auto. + lca. + } + rewrite H2, Cmult_1_l. + reflexivity. + } + assert (Cmod u0 = 1 /\ Cmod u1 = 1). + { + apply (H0 U D V); auto. + } + destruct H3 as [u0_unit u1_unit]. + intros. + destruct H3 as [V1 [V2 [V3 [V4 [V1_gate [V2_gate [V3_gate [V4_gate H3]]]]]]]]. + exists V, D. + split. assumption. + split. assumption. + split. assumption. + rewrite <- (H1 U D V); auto; clear H1. + fold u0 u1. + rewrite <- m7_4; auto. + pose proof ( + absorption_helper V V_unitary V1 V2 V3 V4 V1_gate V2_gate V3_gate V4_gate + ) as [W1 [W2 [W3 [W4 [W1_gate [W2_gate [W3_gate [W4_gate H1]]]]]]]]. + clear absorption_helper. + do 3 rewrite Mmult_assoc with (A := I 2 ⊗ I 2 ⊗ V†) in H1. + rewrite H3 in H1 at 1; clear H3. + exists W1, W2, W3, W4. + split. assumption. + split. assumption. + split. assumption. + split. assumption. + rewrite H1; clear H1. + repeat rewrite Mmult_assoc. + rewrite (@kron_mixed_product 4 4 4 2 2 2). + repeat rewrite <- Mmult_assoc. + rewrite (@kron_mixed_product 4 4 4 2 2 2). + rewrite V_unit. + rewrite id_kron. + Msimpl_light. + rewrite id_kron. + Msimpl_light. + reflexivity. + } + { + intros. + destruct H2 as [V [D [V_unitary [D_diagonal [U_decomp H2]]]]]. + { + set (u0 := (D 0 0)%nat). + set (u1 := (D 1 1)%nat). + rewrite <- (H1 U D V) in H2; auto. + fold u0 u1 in H2. + assert (Cmod u0 = 1 /\ Cmod u1 = 1). + { + apply (H0 U D V); auto. + } + destruct H3 as [u0_unit u1_unit]. + rewrite <- m7_4 in H2; auto. + destruct H2 as [V1 [V2 [V3 [V4 [V1_gate [V2_gate [V3_gate [V4_gate H2]]]]]]]]. + rewrite (H U D V); auto. 2: apply D_diagonal. + assert (diag2 u0 u1 = D). + { + destruct D_diagonal as [WF_D D_diag]. + lma'; solve_WF_matrix. + all: unfold diag2; simpl. + rewrite (D_diag 0 1)%nat. reflexivity. lia. + rewrite (D_diag 1 0)%nat. reflexivity. lia. + } + rewrite H3 in H2; clear H3. + rewrite <- H2. + repeat rewrite <- Mmult_assoc. + assert (Vdag_unitary : WF_Unitary V†) by solve_WF_matrix. + pose proof ( + absorption_helper V† Vdag_unitary V1 V2 V3 V4 V1_gate V2_gate V3_gate V4_gate + ) as [W1 [W2 [W3 [W4 [W1_gate [W2_gate [W3_gate [W4_gate H3]]]]]]]]. + rewrite adjoint_involutive in H3. + exists W1, W2, W3, W4. + split. assumption. + split. assumption. + split. assumption. + split. assumption. + assumption. + } + } +Qed.