diff --git a/AlgebraHelpers.v b/AlgebraHelpers.v index eb6a6fb..69ecccb 100644 --- a/AlgebraHelpers.v +++ b/AlgebraHelpers.v @@ -1,4 +1,7 @@ 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 conj_mult_re_is_nonneg: forall (a: C), Re (a^* * a) >= 0. Proof. @@ -772,4 +775,31 @@ lca. 8,9: assumption. all: apply RtoC_neq. all: lra. +Qed. + +Lemma nat_tight_bound: forall (i j: nat), +(i <= j -> j < S i -> i = j)%nat. +Proof. +intros i j lb up. +apply Nat.le_antisymm. +assumption. +apply le_S_n. apply up. +Qed. + +Lemma sub_mod_equiv: forall (i j: nat), +(i < j * 2 -> j <= i -> (i mod j) = i - j)%nat. +Proof. +intros. +assert ((i - j) = ((i - j) mod j))%nat. +{ + symmetry. + apply Nat.mod_small. + lia. +} +rewrite H1. +symmetry. +rewrite <- Nat.mul_1_l with (n := j) at 1. +apply sub_mul_mod. +rewrite Nat.mul_1_l. +assumption. Qed. \ No newline at end of file diff --git a/ControlledUnitaries.v b/ControlledUnitaries.v index 0748c58..bb450ed 100644 --- a/ControlledUnitaries.v +++ b/ControlledUnitaries.v @@ -80,7 +80,8 @@ 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_4 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]]. apply U_unitary. +destruct (@block_decomp_general 2 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]]. lia. +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)). { intros w WF_w. diff --git a/ExplicitDecompositions.v b/ExplicitDecompositions.v index da68b53..84f4ed4 100644 --- a/ExplicitDecompositions.v +++ b/ExplicitDecompositions.v @@ -250,46 +250,6 @@ intros. lca. Qed. -Lemma vector2_inner_prod_decomp: forall (a b : Vector 2), -(⟨ a, b ⟩ = (a 0%nat 0%nat)^* * (b 0%nat 0%nat) + (a 1%nat 0%nat)^* * (b 1%nat 0%nat)). -Proof. -intros. -lca. -Qed. - -Lemma Mmult_square2_explicit: forall (A B: Square 2), -WF_Matrix A -> WF_Matrix B -> -(A × B) = (fun x y => A x 0%nat * B 0%nat y + A x 1%nat * B 1%nat y). -Proof. -intros. lma'. -unfold WF_Matrix. -intros. -destruct H1. -repeat rewrite H. lca. 1,2: lia. -repeat rewrite H0. lca. 1,2: lia. -Qed. - -Lemma Mv_prod_21_explicit: forall (A: Square 2) (v : Vector 2), -WF_Matrix A -> WF_Matrix v -> -(A × v) = ((fun x y => -match (x,y) with -| (0,0) => (A 0 0)%nat * (v 0 0)%nat + (A 0 1)%nat * (v 1 0)%nat -| (1,0) => (A 1 0)%nat * (v 0 0)%nat + (A 1 1)%nat * (v 1 0)%nat -| _ => C0 -end): Square 2). -Proof. -intros. -lma'. -unfold WF_Matrix. -intros. -destruct H1. -destruct x as [|a]. contradict H. lia. -destruct a as [|x]. contradict H. lia. reflexivity. -destruct x as [|a]. destruct y as [|b]. contradict H. lia. -reflexivity. -destruct a as [|x]. destruct y as [|b]. contradict H. lia. reflexivity. reflexivity. -Qed. - Lemma trace_outer_zero_vec2: forall (a : Vector 2), WF_Matrix a -> trace (a × (a) †) = 0 -> a = Zero. diff --git a/GateHelpers.v b/GateHelpers.v index bcee286..9e766a2 100644 --- a/GateHelpers.v +++ b/GateHelpers.v @@ -1,7 +1,9 @@ Require Import QuantumLib.Quantum. +From Proof Require Import AlgebraHelpers. From Proof Require Import MatrixHelpers. From Proof Require Import SwapHelpers. From Proof Require Import SwapProperty. +From Proof Require Import QubitHelpers. Definition abgate (U : Square 4) := U ⊗ I 2. Definition bcgate (U : Square 4) := I 2 ⊗ U. @@ -172,4 +174,1170 @@ rewrite Mmult_1_l in gate_eq. 2: solve_WF_matrix. apply (@kron_cancel_r 4 1 2 1) with (C:= b). 1,2,3: solve_WF_matrix. 1,2: assumption. +Qed. + +Lemma abgate_control: forall (U W0 W1: Square 4), +WF_Unitary U -> WF_Unitary W0 -> WF_Unitary W1 -> +abgate U = ∣0⟩⟨0∣ ⊗ W0 .+ ∣1⟩⟨1∣ ⊗ W1 -> +exists (P0 P1: Square 2), WF_Unitary P0 /\ WF_Unitary P1 /\ +abgate U = ∣0⟩⟨0∣ ⊗ P0 ⊗ I 2 .+ ∣1⟩⟨1∣ ⊗ P1 ⊗ I 2. +Proof. +intros U W0 W1 U_unitary W0_unitary W1_unitary abgate_c. +assert (temp: WF_Unitary W0). assumption. +destruct temp as [WF_W0 W0_inv]. +assert (temp: WF_Unitary W1). assumption. +destruct temp as [WF_W1 W1_inv]. +unfold abgate in *. +assert (W0_11: W0 1%nat 1%nat = W0 0%nat 0%nat). +{ + assert (W0 1%nat 1%nat = (U ⊗ I 2) 1%nat 1%nat). rewrite abgate_c. lca. + assert (W0 0%nat 0%nat = (U ⊗ I 2) 0%nat 0%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W0_13: W0 1%nat 3%nat = W0 0%nat 2%nat). +{ + assert (W0 1%nat 3%nat = (U ⊗ I 2) 1%nat 3%nat). rewrite abgate_c. lca. + assert (W0 0%nat 2%nat = (U ⊗ I 2) 0%nat 2%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W0_31: W0 3%nat 1%nat = W0 2%nat 0%nat). +{ + assert (W0 3%nat 1%nat = (U ⊗ I 2) 3%nat 1%nat). rewrite abgate_c. lca. + assert (W0 2%nat 0%nat = (U ⊗ I 2) 2%nat 0%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W0_33: W0 3%nat 3%nat = W0 2%nat 2%nat). +{ + assert (W0 3%nat 3%nat = (U ⊗ I 2) 3%nat 3%nat). rewrite abgate_c. lca. + assert (W0 2%nat 2%nat = (U ⊗ I 2) 2%nat 2%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W0_01: W0 0%nat 1%nat = 0). +{ + assert (W0 0%nat 1%nat = (U ⊗ I 2) 0%nat 1%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_03: W0 0%nat 3%nat = 0). +{ + assert (W0 0%nat 3%nat = (U ⊗ I 2) 0%nat 3%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_10: W0 1%nat 0%nat = 0). +{ + assert (W0 1%nat 0%nat = (U ⊗ I 2) 1%nat 0%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_12: W0 1%nat 2%nat = 0). +{ + assert (W0 1%nat 2%nat = (U ⊗ I 2) 1%nat 2%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_21: W0 2%nat 1%nat = 0). +{ + assert (W0 2%nat 1%nat = (U ⊗ I 2) 2%nat 1%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_23: W0 2%nat 3%nat = 0). +{ + assert (W0 2%nat 3%nat = (U ⊗ I 2) 2%nat 3%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_30: W0 3%nat 0%nat = 0). +{ + assert (W0 3%nat 0%nat = (U ⊗ I 2) 3%nat 0%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W0_32: W0 3%nat 2%nat = 0). +{ + assert (W0 3%nat 2%nat = (U ⊗ I 2) 3%nat 2%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (P0_inv_00: (W0 0%nat 0%nat)^* * (W0 0%nat 0%nat) + (W0 2%nat 0%nat)^* * (W0 2%nat 0%nat) = 1). +{ + assert ((W0 0%nat 0%nat) ^* * W0 0%nat 0%nat + (W0 1%nat 0%nat) ^* * W0 1%nat 0%nat + + (W0 2%nat 0%nat) ^* * W0 2%nat 0%nat + (W0 3%nat 0%nat) ^* * W0 3%nat 0%nat = ((W0) † × W0) 0%nat 0%nat). lca. + rewrite W0_10 in H. + rewrite W0_30 in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W0_inv. + lca. +} +assert (P0_inv_01: (W0 0%nat 0%nat)^* * (W0 0%nat 2%nat) + (W0 2%nat 0%nat)^* * (W0 2%nat 2%nat) = 0). +{ + assert ((W0 0%nat 0%nat) ^* * W0 0%nat 2%nat + (W0 1%nat 0%nat) ^* * W0 1%nat 2%nat + + (W0 2%nat 0%nat) ^* * W0 2%nat 2%nat + (W0 3%nat 0%nat) ^* * W0 3%nat 2%nat = ((W0) † × W0) 0%nat 2%nat). lca. + rewrite W0_10 in H. + rewrite W0_30 in H. + rewrite Cconj_0 in H. + do 2 rewrite Cmult_0_l in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W0_inv. + lca. +} +assert (P0_inv_10: (W0 0%nat 2%nat)^* * (W0 0%nat 0%nat) + (W0 2%nat 2%nat)^* * (W0 2%nat 0%nat) = 0). +{ + assert ((W0 0%nat 2%nat) ^* * W0 0%nat 0%nat + (W0 1%nat 2%nat) ^* * W0 1%nat 0%nat + + (W0 2%nat 2%nat) ^* * W0 2%nat 0%nat + (W0 3%nat 2%nat) ^* * W0 3%nat 0%nat = ((W0) † × W0) 2%nat 0%nat). lca. + rewrite W0_10 in H. + rewrite W0_30 in H. + rewrite Cmult_0_r in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W0_inv. + lca. +} +assert (P0_inv_11: (W0 0%nat 2%nat)^* * (W0 0%nat 2%nat) + (W0 2%nat 2%nat)^* * (W0 2%nat 2%nat) = 1). +{ + assert ((W0 0%nat 2%nat) ^* * W0 0%nat 2%nat + (W0 1%nat 2%nat) ^* * W0 1%nat 2%nat + + (W0 2%nat 2%nat) ^* * W0 2%nat 2%nat + (W0 3%nat 2%nat) ^* * W0 3%nat 2%nat = ((W0) † × W0) 2%nat 2%nat). lca. + rewrite W0_12 in H. + rewrite W0_32 in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W0_inv. + lca. +} +set (P0 := (fun x y => match (x,y) with +| (0,0) => W0 0%nat 0%nat +| (0,1) => W0 0%nat 2%nat +| (1,0) => W0 2%nat 0%nat +| (1,1) => W0 2%nat 2%nat +| _ => 0 +end) : Square 2). +assert (WF_P0: WF_Matrix P0). +{ + unfold WF_Matrix. + intros. + unfold P0. + destruct H. + { + destruct x as [| x']. + contradict H. lia. + destruct x' as [|x]. + contradict H. lia. reflexivity. + } + { + destruct x as [| x']. + destruct y as [|y']. contradict H. lia. + destruct y' as [|y]. contradict H. lia. reflexivity. + destruct x' as [|x]. + destruct y as [|y']. contradict H. lia. + destruct y' as [|y]. contradict H. lia. reflexivity. reflexivity. + } +} +assert (P0_unitary: WF_Unitary P0). +{ + split. assumption. + lma'. + assert (unfold_help: ((P0) † × P0) 0%nat 0%nat = (P0 0%nat 0%nat) ^* * P0 0%nat 0%nat + + (P0 1%nat 0%nat) ^* * P0 1%nat 0%nat). lca. + rewrite unfold_help. unfold P0. rewrite P0_inv_00. lca. + assert (unfold_help: ((P0) † × P0) 0%nat 1%nat = (P0 0%nat 0%nat) ^* * P0 0%nat 1%nat + + (P0 1%nat 0%nat) ^* * P0 1%nat 1%nat). lca. + rewrite unfold_help. unfold P0. rewrite P0_inv_01. lca. + assert (unfold_help: ((P0) † × P0) 1%nat 0%nat = (P0 0%nat 1%nat) ^* * P0 0%nat 0%nat + + (P0 1%nat 1%nat) ^* * P0 1%nat 0%nat). lca. + rewrite unfold_help. unfold P0. rewrite P0_inv_10. lca. + assert (unfold_help: ((P0) † × P0) 1%nat 1%nat = (P0 0%nat 1%nat) ^* * P0 0%nat 1%nat + + (P0 1%nat 1%nat) ^* * P0 1%nat 1%nat). lca. + rewrite unfold_help. unfold P0. rewrite P0_inv_11. lca. +} +assert (P0_tens_W0: P0 ⊗ I 2 = W0). +{ + lma'. + unfold kron, P0. simpl. lca. + rewrite W0_01. lca. + unfold kron, P0. simpl. lca. + rewrite W0_03. lca. + rewrite W0_10. lca. + unfold kron, P0. simpl. rewrite W0_11. lca. + rewrite W0_12. lca. + unfold kron, P0. simpl. rewrite W0_13. lca. + unfold kron, P0. simpl. lca. + rewrite W0_21. lca. + unfold kron, P0. simpl. lca. + rewrite W0_23. lca. + rewrite W0_30. lca. + unfold kron, P0. simpl. rewrite W0_31. lca. + rewrite W0_32. lca. + unfold kron, P0. simpl. rewrite W0_33. lca. +} +assert (W1_11: W1 1%nat 1%nat = W1 0%nat 0%nat). +{ + assert (W1 1%nat 1%nat = (U ⊗ I 2) 5%nat 5%nat). rewrite abgate_c. lca. + assert (W1 0%nat 0%nat = (U ⊗ I 2) 4%nat 4%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W1_13: W1 1%nat 3%nat = W1 0%nat 2%nat). +{ + assert (W1 1%nat 3%nat = (U ⊗ I 2) 5%nat 7%nat). rewrite abgate_c. lca. + assert (W1 0%nat 2%nat = (U ⊗ I 2) 4%nat 6%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W1_31: W1 3%nat 1%nat = W1 2%nat 0%nat). +{ + assert (W1 3%nat 1%nat = (U ⊗ I 2) 7%nat 5%nat). rewrite abgate_c. lca. + assert (W1 2%nat 0%nat = (U ⊗ I 2) 6%nat 4%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W1_33: W1 3%nat 3%nat = W1 2%nat 2%nat). +{ + assert (W1 3%nat 3%nat = (U ⊗ I 2) 7%nat 7%nat). rewrite abgate_c. lca. + assert (W1 2%nat 2%nat = (U ⊗ I 2) 6%nat 6%nat). rewrite abgate_c. lca. + rewrite H, H0. + lca. +} +assert (W1_01: W1 0%nat 1%nat = 0). +{ + assert (W1 0%nat 1%nat = (U ⊗ I 2) 4%nat 5%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_03: W1 0%nat 3%nat = 0). +{ + assert (W1 0%nat 3%nat = (U ⊗ I 2) 4%nat 7%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_10: W1 1%nat 0%nat = 0). +{ + assert (W1 1%nat 0%nat = (U ⊗ I 2) 5%nat 4%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_12: W1 1%nat 2%nat = 0). +{ + assert (W1 1%nat 2%nat = (U ⊗ I 2) 5%nat 6%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_21: W1 2%nat 1%nat = 0). +{ + assert (W1 2%nat 1%nat = (U ⊗ I 2) 6%nat 5%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_23: W1 2%nat 3%nat = 0). +{ + assert (W1 2%nat 3%nat = (U ⊗ I 2) 6%nat 7%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_30: W1 3%nat 0%nat = 0). +{ + assert (W1 3%nat 0%nat = (U ⊗ I 2) 7%nat 4%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (W1_32: W1 3%nat 2%nat = 0). +{ + assert (W1 3%nat 2%nat = (U ⊗ I 2) 7%nat 6%nat). rewrite abgate_c. lca. + rewrite H. + lca. +} +assert (P1_inv_00: (W1 0%nat 0%nat)^* * (W1 0%nat 0%nat) + (W1 2%nat 0%nat)^* * (W1 2%nat 0%nat) = 1). +{ + assert ((W1 0%nat 0%nat) ^* * W1 0%nat 0%nat + (W1 1%nat 0%nat) ^* * W1 1%nat 0%nat + + (W1 2%nat 0%nat) ^* * W1 2%nat 0%nat + (W1 3%nat 0%nat) ^* * W1 3%nat 0%nat = ((W1) † × W1) 0%nat 0%nat). lca. + rewrite W1_10 in H. + rewrite W1_30 in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W1_inv. + lca. +} +assert (P1_inv_01: (W1 0%nat 0%nat)^* * (W1 0%nat 2%nat) + (W1 2%nat 0%nat)^* * (W1 2%nat 2%nat) = 0). +{ + assert ((W1 0%nat 0%nat) ^* * W1 0%nat 2%nat + (W1 1%nat 0%nat) ^* * W1 1%nat 2%nat + + (W1 2%nat 0%nat) ^* * W1 2%nat 2%nat + (W1 3%nat 0%nat) ^* * W1 3%nat 2%nat = ((W1) † × W1) 0%nat 2%nat). lca. + rewrite W1_10 in H. + rewrite W1_30 in H. + rewrite Cconj_0 in H. + do 2 rewrite Cmult_0_l in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W1_inv. + lca. +} +assert (P1_inv_10: (W1 0%nat 2%nat)^* * (W1 0%nat 0%nat) + (W1 2%nat 2%nat)^* * (W1 2%nat 0%nat) = 0). +{ + assert ((W1 0%nat 2%nat) ^* * W1 0%nat 0%nat + (W1 1%nat 2%nat) ^* * W1 1%nat 0%nat + + (W1 2%nat 2%nat) ^* * W1 2%nat 0%nat + (W1 3%nat 2%nat) ^* * W1 3%nat 0%nat = ((W1) † × W1) 2%nat 0%nat). lca. + rewrite W1_10 in H. + rewrite W1_30 in H. + rewrite Cmult_0_r in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W1_inv. + lca. +} +assert (P1_inv_11: (W1 0%nat 2%nat)^* * (W1 0%nat 2%nat) + (W1 2%nat 2%nat)^* * (W1 2%nat 2%nat) = 1). +{ + assert ((W1 0%nat 2%nat) ^* * W1 0%nat 2%nat + (W1 1%nat 2%nat) ^* * W1 1%nat 2%nat + + (W1 2%nat 2%nat) ^* * W1 2%nat 2%nat + (W1 3%nat 2%nat) ^* * W1 3%nat 2%nat = ((W1) † × W1) 2%nat 2%nat). lca. + rewrite W1_12 in H. + rewrite W1_32 in H. + rewrite Cmult_0_r in H. + do 2 rewrite Cplus_0_r in H. + rewrite H. + rewrite W1_inv. + lca. +} +set (P1 := (fun x y => match (x,y) with +| (0,0) => W1 0%nat 0%nat +| (0,1) => W1 0%nat 2%nat +| (1,0) => W1 2%nat 0%nat +| (1,1) => W1 2%nat 2%nat +| _ => 0 +end) : Square 2). +assert (WF_P1: WF_Matrix P1). +{ + unfold WF_Matrix. + intros. + unfold P1. + destruct H. + { + destruct x as [| x']. + contradict H. lia. + destruct x' as [|x]. + contradict H. lia. reflexivity. + } + { + destruct x as [| x']. + destruct y as [|y']. contradict H. lia. + destruct y' as [|y]. contradict H. lia. reflexivity. + destruct x' as [|x]. + destruct y as [|y']. contradict H. lia. + destruct y' as [|y]. contradict H. lia. reflexivity. reflexivity. + } +} +assert (P1_unitary: WF_Unitary P1). +{ + split. assumption. + lma'. + assert (unfold_help: ((P1) † × P1) 0%nat 0%nat = (P1 0%nat 0%nat) ^* * P1 0%nat 0%nat + + (P1 1%nat 0%nat) ^* * P1 1%nat 0%nat). lca. + rewrite unfold_help. unfold P1. rewrite P1_inv_00. lca. + assert (unfold_help: ((P1) † × P1) 0%nat 1%nat = (P1 0%nat 0%nat) ^* * P1 0%nat 1%nat + + (P1 1%nat 0%nat) ^* * P1 1%nat 1%nat). lca. + rewrite unfold_help. unfold P1. rewrite P1_inv_01. lca. + assert (unfold_help: ((P1) † × P1) 1%nat 0%nat = (P1 0%nat 1%nat) ^* * P1 0%nat 0%nat + + (P1 1%nat 1%nat) ^* * P1 1%nat 0%nat). lca. + rewrite unfold_help. unfold P1. rewrite P1_inv_10. lca. + assert (unfold_help: ((P1) † × P1) 1%nat 1%nat = (P1 0%nat 1%nat) ^* * P1 0%nat 1%nat + + (P1 1%nat 1%nat) ^* * P1 1%nat 1%nat). lca. + rewrite unfold_help. unfold P1. rewrite P1_inv_11. lca. +} +assert (P1_tens_W1: P1 ⊗ I 2 = W1). +{ + lma'. + unfold kron, P1. simpl. lca. + rewrite W1_01. lca. + unfold kron, P1. simpl. lca. + rewrite W1_03. lca. + rewrite W1_10. lca. + unfold kron, P1. simpl. rewrite W1_11. lca. + rewrite W1_12. lca. + unfold kron, P1. simpl. rewrite W1_13. lca. + unfold kron, P1. simpl. lca. + rewrite W1_21. lca. + unfold kron, P1. simpl. lca. + rewrite W1_23. lca. + rewrite W1_30. lca. + unfold kron, P1. simpl. rewrite W1_31. lca. + rewrite W1_32. lca. + unfold kron, P1. simpl. rewrite W1_33. lca. +} +exists P0, P1. +split. assumption. +split. assumption. +rewrite kron_assoc. 2,3,4: solve_WF_matrix. +rewrite kron_assoc. 2,3,4: solve_WF_matrix. +rewrite P0_tens_W0. rewrite P1_tens_W1. +apply abgate_c. +Qed. + +Lemma acgate_control: forall (U W0 W1: Square 4), +WF_Unitary U -> WF_Unitary W0 -> WF_Unitary W1 -> +acgate U = ∣0⟩⟨0∣ ⊗ W0 .+ ∣1⟩⟨1∣ ⊗ W1 -> +exists (P0 P1: Square 2), WF_Unitary P0 /\ WF_Unitary P1 /\ +acgate U = ∣0⟩⟨0∣ ⊗ I 2 ⊗ P0 .+ ∣1⟩⟨1∣ ⊗ I 2 ⊗ P1. +Proof. +intros U W0 W1 U_unitary W0_unitary W1_unitary acgate_c. +assert (temp: WF_Unitary U). assumption. +destruct temp as [WF_U U_inv]. +unfold acgate in acgate_c. +apply (f_equal (fun f => swapbc × f)) in acgate_c. +repeat rewrite <- Mmult_assoc in acgate_c. +rewrite swapbc_inverse in acgate_c. rewrite Mmult_1_l in acgate_c. 2: apply WF_abgate; solve_WF_matrix. +rewrite Mmult_plus_distr_l in acgate_c. +unfold swapbc in acgate_c at 2. rewrite kron_mixed_product in acgate_c. +unfold swapbc in acgate_c at 2. rewrite kron_mixed_product in acgate_c. +rewrite Mmult_1_l in acgate_c. 2: solve_WF_matrix. +rewrite Mmult_1_l in acgate_c. 2: solve_WF_matrix. +apply (f_equal (fun f => f × swapbc)) in acgate_c. +rewrite Mmult_assoc in acgate_c. +rewrite swapbc_inverse in acgate_c at 1. rewrite Mmult_1_r in acgate_c. 2: apply WF_abgate; solve_WF_matrix. +rewrite Mmult_plus_distr_r in acgate_c. +unfold swapbc in acgate_c at 2. rewrite kron_mixed_product in acgate_c. +unfold swapbc in acgate_c at 1. rewrite kron_mixed_product in acgate_c. +rewrite Mmult_1_r in acgate_c. 2: solve_WF_matrix. +rewrite Mmult_1_r in acgate_c. 2: solve_WF_matrix. +assert (swapW0_unit: WF_Unitary (swap × W0 × swap)). +{ + apply Mmult_unitary. apply Mmult_unitary. + apply swap_unitary. assumption. apply swap_unitary. +} +assert (swapW1_unit: WF_Unitary (swap × W1 × swap)). +{ + apply Mmult_unitary. apply Mmult_unitary. + apply swap_unitary. assumption. apply swap_unitary. +} +assert (abgate_control_partial := abgate_control U (swap × W0 × swap) (swap × W1 × swap) U_unitary +swapW0_unit swapW1_unit acgate_c). +destruct abgate_control_partial as [P0 [P1 [P0_unitary [P1_unitary abgate_prop]]]]. +exists P0,P1. +split. assumption. +split. assumption. +unfold acgate. +rewrite abgate_prop. +destruct P0_unitary as [WF_P0 P0_inv]. +destruct P1_unitary as [WF_P1 P1_inv]. +rewrite Mmult_plus_distr_l. +rewrite Mmult_plus_distr_r. +rewrite swapbc_3gate. 2,3,4: solve_WF_matrix. +rewrite swapbc_3gate. 2,3,4: solve_WF_matrix. +reflexivity. +Qed. + +Lemma abgate_0prop_bottomleft_0block: forall (U: Square 4), +WF_Unitary U -> (exists (y: Vector 2), WF_Qubit y /\ +forall (x : Vector 2), WF_Qubit x -> (exists (phi: Vector 4), WF_Matrix phi /\ +(abgate U) × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi)) -> exists (TL TR BR: Square 4), +WF_Matrix TL /\ WF_Matrix TR /\ WF_Matrix BR /\ +abgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣0⟩⟨1∣ ⊗ TR .+ ∣1⟩⟨1∣ ⊗ BR. +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. +exists (TL ⊗ I 2), (TR ⊗ I 2), (BR ⊗ I 2). +split. solve_WF_matrix. +split. solve_WF_matrix. +split. solve_WF_matrix. +assert (abgate_decomp: abgate U = ∣0⟩⟨0∣ ⊗ (TL ⊗ I 2) .+ ∣0⟩⟨1∣ ⊗ (TR ⊗ I 2) .+ ∣1⟩⟨0∣ ⊗ (BL ⊗ I 2) +.+ ∣1⟩⟨1∣ ⊗ (BR ⊗ I 2)). +{ + rewrite decomp. + unfold abgate. + repeat rewrite kron_plus_distr_r. + repeat rewrite kron_assoc. + reflexivity. + all: solve_WF_matrix. +} +assert (goal_change: BL = Zero -> abgate U = ∣0⟩⟨0∣ ⊗ (TL ⊗ I 2) .+ ∣0⟩⟨1∣ ⊗ (TR ⊗ I 2) + .+ ∣1⟩⟨1∣ ⊗ (BR ⊗ I 2)). +{ + intros. + rewrite abgate_decomp. + rewrite H. + rewrite kron_0_l. rewrite kron_0_r. + rewrite Mplus_0_r. + reflexivity. +} +apply goal_change. clear goal_change. +assert (zerotens_040: forall (y0: Vector 2), (∣0⟩ ⊗ ∣0⟩ ⊗ y0) 4%nat 0%nat = 0). intros. lca. +assert (zerotens_050: forall (y0: Vector 2), (∣0⟩ ⊗ ∣0⟩ ⊗ y0) 5%nat 0%nat = 0). intros. lca. +assert (zerotens_060: forall (y0: Vector 2), (∣0⟩ ⊗ ∣0⟩ ⊗ y0) 6%nat 0%nat = 0). intros. lca. +assert (zerotens_070: forall (y0: Vector 2), (∣0⟩ ⊗ ∣0⟩ ⊗ y0) 7%nat 0%nat = 0). intros. lca. +assert (zerotens_140: forall (y0: Vector 2), (∣0⟩ ⊗ ∣1⟩ ⊗ y0) 4%nat 0%nat = 0). intros. lca. +assert (zerotens_150: forall (y0: Vector 2), (∣0⟩ ⊗ ∣1⟩ ⊗ y0) 5%nat 0%nat = 0). intros. lca. +assert (zerotens_160: forall (y0: Vector 2), (∣0⟩ ⊗ ∣1⟩ ⊗ y0) 6%nat 0%nat = 0). intros. lca. +assert (zerotens_170: forall (y0: Vector 2), (∣0⟩ ⊗ ∣1⟩ ⊗ y0) 7%nat 0%nat = 0). intros. lca. +assert (case000_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 2%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣0⟩ ⊗ y) 3%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 0%nat 0%nat <> 0 -> (abgate U) 4%nat 0%nat <> 0 -> +(abgate U) 4%nat 1%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣0⟩ ⊗ y)) 4%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣0⟩ ⊗ y0)) 4%nat 0%nat) with ( + (abgate U0 4%nat 0%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 4%nat 1%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 4%nat 2%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 4%nat 3%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 4%nat 4%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 4%nat 5%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 4%nat 6%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 4%nat 7%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_040, zerotens_050, zerotens_060, zerotens_070. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case000_el_eq: abgate U 4%nat 0%nat = BL 0%nat 0%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case001_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 2%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣0⟩ ⊗ y) 3%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 1%nat 0%nat <> 0 -> (abgate U) 5%nat 1%nat <> 0 -> +(abgate U) 5%nat 0%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣0⟩ ⊗ y)) 5%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣0⟩ ⊗ y0)) 5%nat 0%nat) with ( + (abgate U0 5%nat 0%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 5%nat 1%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 5%nat 2%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 5%nat 3%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 5%nat 4%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 5%nat 5%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 5%nat 6%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 5%nat 7%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_040, zerotens_050, zerotens_060, zerotens_070. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case001_el_eq: abgate U 5%nat 1%nat = BL 0%nat 0%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case010_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 0%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣1⟩ ⊗ y) 1%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 2%nat 0%nat <> 0 -> (abgate U) 4%nat 2%nat <> 0 -> +(abgate U) 4%nat 3%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣1⟩ ⊗ y)) 4%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣1⟩ ⊗ y0)) 4%nat 0%nat) with ( + (abgate U0 4%nat 0%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 4%nat 1%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 4%nat 2%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 4%nat 3%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 4%nat 4%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 4%nat 5%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 4%nat 6%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 4%nat 7%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_140, zerotens_150, zerotens_160, zerotens_170. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case010_el_eq: abgate U 4%nat 2%nat = BL 0%nat 1%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case011_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 0%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣1⟩ ⊗ y) 1%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 3%nat 0%nat <> 0 -> (abgate U) 5%nat 3%nat <> 0 -> +(abgate U) 5%nat 2%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣1⟩ ⊗ y)) 5%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣1⟩ ⊗ y0)) 5%nat 0%nat) with ( + (abgate U0 5%nat 0%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 5%nat 1%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 5%nat 2%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 5%nat 3%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 5%nat 4%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 5%nat 5%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 5%nat 6%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 5%nat 7%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_140, zerotens_150, zerotens_160, zerotens_170. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case011_el_eq: abgate U 5%nat 3%nat = BL 0%nat 1%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case100_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 2%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣0⟩ ⊗ y) 3%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 0%nat 0%nat <> 0 -> (abgate U) 6%nat 0%nat <> 0 -> +(abgate U) 6%nat 1%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣0⟩ ⊗ y)) 6%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣0⟩ ⊗ y0)) 6%nat 0%nat) with ( + (abgate U0 6%nat 0%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 6%nat 1%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 6%nat 2%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 6%nat 3%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 6%nat 4%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 6%nat 5%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 6%nat 6%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 6%nat 7%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_040, zerotens_050, zerotens_060, zerotens_070. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case100_el_eq: abgate U 6%nat 0%nat = BL 1%nat 0%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case101_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 2%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣0⟩ ⊗ y) 3%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣0⟩ ⊗ y) 1%nat 0%nat <> 0 -> (abgate U) 7%nat 1%nat <> 0 -> +(abgate U) 7%nat 0%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣0⟩ ⊗ y)) 7%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣0⟩ ⊗ y0)) 7%nat 0%nat) with ( + (abgate U0 7%nat 0%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 7%nat 1%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 7%nat 2%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 7%nat 3%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 7%nat 4%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 7%nat 5%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 7%nat 6%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 7%nat 7%nat) * ((∣0⟩ ⊗ ∣0⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_040, zerotens_050, zerotens_060, zerotens_070. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case101_el_eq: abgate U 7%nat 1%nat = BL 1%nat 0%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case110_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 0%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣1⟩ ⊗ y) 1%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 2%nat 0%nat <> 0 -> (abgate U) 6%nat 2%nat <> 0 -> +(abgate U) 6%nat 3%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣1⟩ ⊗ y)) 6%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣1⟩ ⊗ y0)) 6%nat 0%nat) with ( + (abgate U0 6%nat 0%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 6%nat 1%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 6%nat 2%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 6%nat 3%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 6%nat 4%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 6%nat 5%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 6%nat 6%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 6%nat 7%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_140, zerotens_150, zerotens_160, zerotens_170. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case110_el_eq: abgate U 6%nat 2%nat = BL 1%nat 1%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (case111_goal_change: forall (U: Square 4) (y: Vector 2), +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 0%nat 0%nat = 0 -> (∣0⟩ ⊗ ∣1⟩ ⊗ y) 1%nat 0%nat = 0 -> +(∣0⟩ ⊗ ∣1⟩ ⊗ y) 3%nat 0%nat <> 0 -> (abgate U) 7%nat 3%nat <> 0 -> +(abgate U) 7%nat 2%nat = 0 -> (abgate U × (∣0⟩ ⊗ ∣1⟩ ⊗ y)) 7%nat 0%nat <> 0). +{ + intros. + replace ((abgate U0 × (∣0⟩ ⊗ ∣1⟩ ⊗ y0)) 7%nat 0%nat) with ( + (abgate U0 7%nat 0%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 0%nat 0%nat) + + (abgate U0 7%nat 1%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 1%nat 0%nat) + + (abgate U0 7%nat 2%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 2%nat 0%nat) + + (abgate U0 7%nat 3%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 3%nat 0%nat) + + (abgate U0 7%nat 4%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 4%nat 0%nat) + + (abgate U0 7%nat 5%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 5%nat 0%nat) + + (abgate U0 7%nat 6%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 6%nat 0%nat) + + (abgate U0 7%nat 7%nat) * ((∣0⟩ ⊗ ∣1⟩ ⊗ y0) 7%nat 0%nat) + ) by lca. + rewrite H, H0, H3, zerotens_140, zerotens_150, zerotens_160, zerotens_170. + Csimpl. + apply Cmult_neq_0. + all: assumption. +} +assert (case111_el_eq: abgate U 7%nat 3%nat = BL 1%nat 1%nat). +{ + rewrite abgate_decomp. + repeat rewrite Mplus_access. + rewrite upper_left_block_nonentries. + rewrite upper_right_block_nonentries. + rewrite lower_right_block_nonentries. + rewrite lower_left_block_entries. + Csimpl. simpl. + lca. + 1,4,7,10: solve_WF_matrix. + 1,3,5,7: lia. + split. lia. lia. + right. lia. left. lia. + left. lia. +} +assert (cntrps: not (BL = Zero) -> not (forall x : Vector 2, +WF_Qubit x -> exists phi : Vector 4, +WF_Matrix phi /\ abgate U × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi)). +{ + intros BLn0. + apply Coq.Logic.Classical_Pred_Type.ex_not_not_all. + rewrite nonzero_def in BLn0. + destruct BLn0 as [i [j n0point]]. + assert (y <> Zero). apply qubit_implies_nonzero. apply WF_y. + assert (yeln0: (y 0%nat 0%nat) <> 0 \/ (y 1%nat 0%nat) <> 0). + { + apply Coq.Logic.Classical_Prop.not_and_or. + unfold not. + intro. + apply H. + destruct H0. + lma'. apply WF_y. + rewrite H0. lca. + rewrite H1. lca. + } + destruct (le_lt_dec 2 i). + { + contradict n0point. + rewrite WF_BL. reflexivity. + left. lia. + } + { + destruct (le_lt_dec 1 i). + { + assert (ival := nat_tight_bound 1 i l0 l). + destruct (le_lt_dec 2 j). + { + contradict n0point. + rewrite WF_BL. reflexivity. + right. lia. + } + { + destruct (le_lt_dec 1 j). + { + assert (jval := nat_tight_bound 1 j l2 l1). + destruct yeln0. + { + exists ∣1⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit1_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 6%nat. + split. lia. + apply case110_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣1⟩ ⊗ y) 2%nat 0%nat) with (y 0%nat 0%nat) by lca. + assumption. + replace (abgate U 6%nat 2%nat) with (BL 1%nat 1%nat). + rewrite ival at 1. rewrite jval. assumption. lca. + } + { + exists ∣1⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit1_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 7%nat. + split. lia. + apply case111_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣1⟩ ⊗ y) 3%nat 0%nat) with (y 1%nat 0%nat) by lca. + assumption. + replace (abgate U 7%nat 3%nat) with (BL 1%nat 1%nat). + rewrite ival at 1. rewrite jval. assumption. lca. + } + } + { + rewrite Nat.lt_1_r in l2. + destruct yeln0. + { + exists ∣0⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit0_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 6%nat. + split. lia. + apply case100_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣0⟩ ⊗ y) 0%nat 0%nat) with (y 0%nat 0%nat) by lca. + assumption. + replace (abgate U 6%nat 0%nat) with (BL 1%nat 0%nat). + rewrite ival at 1. rewrite <- l2. assumption. lca. + } + { + exists ∣0⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit0_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 7%nat. + split. lia. + apply case101_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣0⟩ ⊗ y) 1%nat 0%nat) with (y 1%nat 0%nat) by lca. + assumption. + replace (abgate U 7%nat 1%nat) with (BL 1%nat 0%nat). + rewrite ival at 1. rewrite <- l2. assumption. lca. + } + } + } + } + { + rewrite Nat.lt_1_r in l0. + destruct (le_lt_dec 2 j). + { + contradict n0point. + rewrite WF_BL. reflexivity. + right. lia. + } + { + destruct (le_lt_dec 1 j). + { + assert (jval := nat_tight_bound 1 j l2 l1). + destruct yeln0. + { + exists ∣1⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit1_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 4%nat. + split. lia. + apply case010_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣1⟩ ⊗ y) 2%nat 0%nat) with (y 0%nat 0%nat) by lca. + assumption. + replace (abgate U 4%nat 2%nat) with (BL 0%nat 1%nat). + rewrite <- l0 at 1. rewrite jval. assumption. lca. + } + { + exists ∣1⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit1_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 5%nat. + split. lia. + apply case011_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣1⟩ ⊗ y) 3%nat 0%nat) with (y 1%nat 0%nat) by lca. + assumption. + replace (abgate U 5%nat 3%nat) with (BL 0%nat 1%nat). + rewrite <- l0 at 1. rewrite jval. assumption. lca. + } + } + { + rewrite Nat.lt_1_r in l2. + destruct yeln0. + { + exists ∣0⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit0_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 4%nat. + split. lia. + apply case000_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣0⟩ ⊗ y) 0%nat 0%nat) with (y 0%nat 0%nat) by lca. + assumption. + replace (abgate U 4%nat 0%nat) with (BL 0%nat 0%nat). + rewrite <- l0 at 1. rewrite <- l2. assumption. lca. + } + { + exists ∣0⟩. + rewrite implication_decomp. + apply Coq.Logic.Classical_Prop.and_not_or. + split. + unfold not. + intro. apply H1. apply qubit0_qubit. + apply Coq.Logic.Classical_Pred_Type.all_not_not_ex. + intros. + apply Coq.Logic.Classical_Prop.or_not_and. + rewrite <- implication_decomp. + apply qubit_not_0tens. lia. solve_WF_matrix. apply U_unitary. apply WF_y. + exists 5%nat. + split. lia. + apply case001_goal_change. + lca. lca. + replace ((∣0⟩ ⊗ ∣0⟩ ⊗ y) 1%nat 0%nat) with (y 1%nat 0%nat) by lca. + assumption. + replace (abgate U 5%nat 1%nat) with (BL 0%nat 0%nat). + rewrite <- l0 at 1. rewrite <- l2. assumption. lca. + } + } + } + } + } +} +apply Coq.Logic.Classical_Prop.NNPP. +unfold not at 1. +intros cntrps_premise. +apply cntrps in cntrps_premise. +apply cntrps_premise. +apply zeropassthrough. +Qed. + +Lemma abgate_diagblock: forall (U: Square 4), +WF_Unitary U -> (exists (y: Vector 2), WF_Qubit y /\ +forall (x : Vector 2), WF_Qubit x -> (exists (phi: Vector 4), WF_Matrix phi /\ +(abgate U) × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi)) -> +exists (TL BR: Square 4), WF_Unitary TL /\ WF_Unitary BR /\ +abgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR. +Proof. +intros U U_unitary zeropassthrough. +assert (zpass_decomp:= abgate_0prop_bottomleft_0block U U_unitary zeropassthrough). +destruct zpass_decomp as [TL0 [TR0 [BR0 [WF_TL0 [WF_TR0 [WF_BR0 zpass_decomp]]]]]]. +replace (∣0⟩⟨0∣ ⊗ TL0 .+ ∣0⟩⟨1∣ ⊗ TR0 .+ ∣1⟩⟨1∣ ⊗ BR0) with +(∣0⟩⟨0∣ ⊗ TL0 .+ ∣0⟩⟨1∣ ⊗ TR0 .+ ∣1⟩⟨0∣ ⊗ Zero .+ ∣1⟩⟨1∣ ⊗ BR0) in zpass_decomp. +2: rewrite kron_0_r; rewrite Mplus_0_r; reflexivity. +assert (abgate_U_unitary: WF_Unitary (abgate U)). apply abgate_unitary; assumption. +destruct abgate_U_unitary as [WF_abU abU_inv]. +replace (I (4 * 2)) with (∣0⟩⟨0∣ ⊗ I 4 .+ ∣0⟩⟨1∣ ⊗ Zero .+ ∣1⟩⟨0∣ ⊗ Zero .+ ∣1⟩⟨1∣ ⊗ I 4) in abU_inv. +2: lma'; solve_WF_matrix. +assert (block_mult_partial := @block_multiply 4 (abgate U) † (abgate U) TL0† Zero TR0† BR0† +TL0 TR0 Zero BR0). +assert (block_mult: (abgate U) † × abgate U = +∣0⟩⟨0∣ ⊗ ((TL0) † × TL0 .+ (@Zero 4 4) × Zero) .+ ∣0⟩⟨1∣ ⊗ ((TL0) † × TR0 .+ Zero × BR0) +.+ ∣1⟩⟨0∣ ⊗ ((TR0) † × TL0 .+ (BR0) † × Zero) +.+ ∣1⟩⟨1∣ ⊗ ((TR0) † × TR0 .+ (BR0) † × BR0)). +{ + apply block_mult_partial. + 1,2,3,4,5,6,7,8: solve_WF_matrix. + rewrite zpass_decomp. + repeat rewrite Mplus_adjoint. + repeat rewrite kron_adjoint. + rewrite adjoint00, adjoint01, adjoint10, adjoint11. + rewrite zero_adjoint_eq. + repeat rewrite kron_0_r. + repeat rewrite Mplus_0_r. + reflexivity. + apply zpass_decomp. +} +clear block_mult_partial. +repeat rewrite Mmult_0_r in block_mult. +repeat rewrite Mmult_0_l in block_mult. +repeat rewrite Mplus_0_r in block_mult. +repeat rewrite Mplus_0_l in block_mult. +assert (WF_TL0_inv: WF_Matrix ((TL0) † × TL0)). solve_WF_matrix. +assert (WF_TR_block: WF_Matrix ((TL0) † × TR0)). solve_WF_matrix. +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) +((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). +destruct block_eq as [TL0_inv [_ [TR_is_Zero BR0_inv]]]. +assert (TL0_unitary: WF_Unitary TL0). split. 1,2: assumption. +apply unitary_mult_zero_cancel_r in TR_is_Zero. 2,3: solve_WF_matrix. +rewrite <- zero_adjoint_eq in TR_is_Zero. +apply (f_equal (fun f => f †)) in TR_is_Zero. +repeat rewrite adjoint_involutive in TR_is_Zero. +rewrite TR_is_Zero in BR0_inv. +rewrite Mmult_0_r in BR0_inv. +rewrite Mplus_0_l in BR0_inv. +exists TL0, BR0. +split. assumption. +split. split. 1,2: assumption. +rewrite zpass_decomp. +rewrite TR_is_Zero. +repeat rewrite kron_0_r. +repeat rewrite Mplus_0_r. +reflexivity. +Qed. + +Lemma acgate_diagblock: forall (U: Square 4), +WF_Unitary U -> (exists (x: Vector 2), WF_Qubit x /\ +forall (y : Vector 2), WF_Qubit y -> (exists (phi: Vector 4), WF_Matrix phi /\ +(acgate U) × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi)) -> +exists (TL BR: Square 4), WF_Unitary TL /\ WF_Unitary BR /\ +acgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR. +Proof. +intros U U_unitary zeropassthrough. +assert (goal_change: (exists TL BR : Square 4, +WF_Unitary TL /\ WF_Unitary BR /\ abgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR) -> +exists TL BR : Square 4, WF_Unitary TL /\ WF_Unitary BR /\ +acgate U = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR). +{ + intros. + destruct H as [TLs [BRs [TLs_unitary [BRs_unitary abs]]]]. + exists (swap × TLs × swap), (swap × BRs × swap). + split. apply Mmult_unitary. apply Mmult_unitary. 1,3: apply swap_unitary. assumption. + split. apply Mmult_unitary. apply Mmult_unitary. 1,3: apply swap_unitary. assumption. + unfold acgate. + rewrite abs. + unfold swapbc. + rewrite Mmult_plus_distr_l. + repeat rewrite kron_mixed_product. + repeat rewrite Mmult_1_l. 2,3: solve_WF_matrix. + rewrite Mmult_plus_distr_r. + repeat rewrite kron_mixed_product. + repeat rewrite Mmult_1_r. 2,3: solve_WF_matrix. + reflexivity. +} +apply goal_change. +apply abgate_diagblock. +assumption. +destruct zeropassthrough as [x [x_qubit zeropassthrough]]. +exists x. +split. assumption. +intros y y_qubit. +specialize (zeropassthrough y y_qubit). +destruct zeropassthrough as [phis [WF_phis zeropassthrough]]. +exists (swap × phis). +split. solve_WF_matrix. +unfold acgate in zeropassthrough. +apply (f_equal (fun f => swapbc × f)) in zeropassthrough. +repeat rewrite <- Mmult_assoc in zeropassthrough. +rewrite swapbc_inverse in zeropassthrough at 1. +rewrite Mmult_1_l in zeropassthrough. 2: apply WF_abgate; apply U_unitary. +rewrite Mmult_assoc in zeropassthrough. +rewrite swapbc_3q in zeropassthrough. 2: solve_WF_matrix. 2: apply x_qubit. 2: apply y_qubit. +rewrite zeropassthrough at 1. +unfold swapbc. +rewrite kron_mixed_product. +rewrite Mmult_1_l. 2: solve_WF_matrix. +reflexivity. Qed. \ No newline at end of file diff --git a/MatrixHelpers.v b/MatrixHelpers.v index 2fdae98..89d7906 100644 --- a/MatrixHelpers.v +++ b/MatrixHelpers.v @@ -449,34 +449,6 @@ Proof. all: solve_WF_matrix. Qed. -Lemma nat_tight_bound: forall (i j: nat), -(i <= j -> j < S i -> i = j)%nat. -Proof. -intros i j lb up. -apply Nat.le_antisymm. -assumption. -apply le_S_n. apply up. -Qed. - -Lemma sub_mod_equiv: forall (i j: nat), -(i < j * 2 -> j <= i -> (i mod j) = i - j)%nat. -Proof. -intros. -assert ((i - j) = ((i - j) mod j))%nat. -{ - symmetry. - apply Nat.mod_small. - lia. -} -rewrite H1. -symmetry. -rewrite <- Nat.mul_1_l with (n := j) at 1. -apply sub_mul_mod. -rewrite Nat.mul_1_l. -assumption. -Qed. - - Lemma upper_left_block_entries {n}: forall (A : Square n) (i j: nat), (i < n /\ j < n)%nat -> (∣0⟩⟨0∣ ⊗ A) i j = A i j. Proof. @@ -1226,7 +1198,7 @@ assert (WF_TL: WF_Matrix TL). unfold TL. destruct H. replace (x -exists (P00 P01 P10 P11: Square 2), -WF_Matrix P00 /\ WF_Matrix P01 /\ WF_Matrix P10 /\ WF_Matrix P11 /\ -U = ∣0⟩⟨0∣ ⊗ P00 .+ ∣0⟩⟨1∣ ⊗ P01 .+ ∣1⟩⟨0∣ ⊗ P10 .+ ∣1⟩⟨1∣ ⊗ P11. -Proof. -intros U WF_U. -set (P00 := (fun x y => -match (x,y) with -| (0,0) => (U 0 0)%nat -| (0,1) => (U 0 1)%nat -| (1,0) => (U 1 0)%nat -| (1,1) => (U 1 1)%nat -| _ => C0 -end) : (Square 2)). -set (P01 := (fun x y => -match (x,y) with -| (0,0) => (U 0 2)%nat -| (0,1) => (U 0 3)%nat -| (1,0) => (U 1 2)%nat -| (1,1) => (U 1 3)%nat -| _ => C0 -end) : (Square 2)). -set (P10 := (fun x y => -match (x,y) with -| (0,0) => (U 2 0)%nat -| (0,1) => (U 2 1)%nat -| (1,0) => (U 3 0)%nat -| (1,1) => (U 3 1)%nat -| _ => C0 -end) : (Square 2)). -set (P11 := (fun x y => -match (x,y) with -| (0,0) => (U 2 2)%nat -| (0,1) => (U 2 3)%nat -| (1,0) => (U 3 2)%nat -| (1,1) => (U 3 3)%nat -| _ => C0 -end) : (Square 2)). -exists P00, P01, P10, P11. -assert (WF_P00: WF_Matrix P00). -{ - unfold WF_Matrix. intros. - unfold P00. - destruct H. - destruct x as [|x']. contradict H. lia. - destruct x' as [| x'']. contradict H. lia. - reflexivity. - destruct x as [|x']. - destruct y as [|y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - destruct x' as [| x'']. - destruct y as [| y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - reflexivity. -} -split. assumption. -assert (WF_P01: WF_Matrix P01). -{ - unfold WF_Matrix. intros. - unfold P01. - destruct H. - destruct x as [|x']. contradict H. lia. - destruct x' as [| x'']. contradict H. lia. - reflexivity. - destruct x as [|x']. - destruct y as [|y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - destruct x' as [| x'']. - destruct y as [| y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - reflexivity. -} -split. assumption. -assert (WF_P10: WF_Matrix P10). -{ - unfold WF_Matrix. intros. - unfold P10. - destruct H. - destruct x as [|x']. contradict H. lia. - destruct x' as [| x'']. contradict H. lia. - reflexivity. - destruct x as [|x']. - destruct y as [|y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - destruct x' as [| x'']. - destruct y as [| y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - reflexivity. -} -split. assumption. -assert (WF_P11: WF_Matrix P11). -{ - unfold WF_Matrix. intros. - unfold P11. - destruct H. - destruct x as [|x']. contradict H. lia. - destruct x' as [| x'']. contradict H. lia. - reflexivity. - destruct x as [|x']. - destruct y as [|y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - destruct x' as [| x'']. - destruct y as [| y']. contradict H. lia. - destruct y' as [| y'']. contradict H. lia. - reflexivity. - reflexivity. -} -split. assumption. -lma'. apply (@WF_blockmatrix 2). 1,2,3,4: assumption. -all: unfold Mplus, kron, "∣0⟩⟨0∣", "∣0⟩⟨1∣", "∣1⟩⟨0∣", "∣1⟩⟨1∣", Mmult, adjoint. -all: simpl. -all: Csimpl. -1,2,5,6: unfold P00. -5,6,7,8: unfold P01. -9,10,13,14: unfold P10. -13,14,15,16: unfold P11. -all: lca. -Qed. - Lemma element_equiv_vec_element {m n}: forall (A: Matrix m n), WF_Matrix A -> forall (i j: nat), @@ -2370,3 +2216,43 @@ Proof. } } Qed. + +Lemma vector2_inner_prod_decomp: forall (a b : Vector 2), +(⟨ a, b ⟩ = (a 0%nat 0%nat)^* * (b 0%nat 0%nat) + (a 1%nat 0%nat)^* * (b 1%nat 0%nat)). +Proof. +intros. +lca. +Qed. + +Lemma Mmult_square2_explicit: forall (A B: Square 2), +WF_Matrix A -> WF_Matrix B -> +(A × B) = (fun x y => A x 0%nat * B 0%nat y + A x 1%nat * B 1%nat y). +Proof. +intros. lma'. +unfold WF_Matrix. +intros. +destruct H1. +repeat rewrite H. lca. 1,2: lia. +repeat rewrite H0. lca. 1,2: lia. +Qed. + +Lemma Mv_prod_21_explicit: forall (A: Square 2) (v : Vector 2), +WF_Matrix A -> WF_Matrix v -> +(A × v) = ((fun x y => +match (x,y) with +| (0,0) => (A 0 0)%nat * (v 0 0)%nat + (A 0 1)%nat * (v 1 0)%nat +| (1,0) => (A 1 0)%nat * (v 0 0)%nat + (A 1 1)%nat * (v 1 0)%nat +| _ => C0 +end): Square 2). +Proof. +intros. +lma'. +unfold WF_Matrix. +intros. +destruct H1. +destruct x as [|a]. contradict H. lia. +destruct a as [|x]. contradict H. lia. reflexivity. +destruct x as [|a]. destruct y as [|b]. contradict H. lia. +reflexivity. +destruct a as [|x]. destruct y as [|b]. contradict H. lia. reflexivity. reflexivity. +Qed. \ No newline at end of file diff --git a/OtherProperties.v b/OtherProperties.v index 7a3069c..843f794 100644 --- a/OtherProperties.v +++ b/OtherProperties.v @@ -167,7 +167,8 @@ do 2 rewrite Mplus_0_r in V3_way1. do 2 rewrite Mplus_assoc in V3_way1. rewrite Mplus_comm with (A:= ∣1⟩⟨1∣ ⊗ ((V2) † × (I 2 ⊗ (P1) †) × U1 × (V4) †)) in V3_way1. repeat rewrite <- Mplus_assoc in V3_way1. -assert (v3_decomp:= block_decomp_4 V3 WF_v3). +assert (ne20: 2%nat <> 0%nat). lia. +assert (v3_decomp:= @block_decomp_general 2 V3 ne20 WF_v3). destruct v3_decomp as [Q00 [Q01 [Q10 [Q11 [WF_Q00 [WF_Q01 [WF_Q10 [WF_Q11 v3_decomp]]]]]]]]. assert (V3_way2: acgate V3 = swapbc × abgate V3 × swapbc). unfold acgate. reflexivity. unfold abgate in V3_way2. diff --git a/QubitHelpers.v b/QubitHelpers.v index bd251a5..7ea7fbc 100644 --- a/QubitHelpers.v +++ b/QubitHelpers.v @@ -2,7 +2,6 @@ Require Import QuantumLib.Matrix. Require Import QuantumLib.Quantum. From Proof Require Import MatrixHelpers. From Proof Require Import AlgebraHelpers. -From Proof Require Import ExplicitDecompositions. Definition WF_Qubit {n} (q: Vector n) := (exists m: nat, (2 ^ m = n)%nat) /\ WF_Matrix q /\ ⟨ q, q ⟩ = 1. @@ -606,6 +605,59 @@ split. } Qed. +Lemma exists_unitary_mapping_qubit_to_1: forall (a : Vector 2), +WF_Qubit a -> exists (P : Square 2), WF_Unitary P /\ P × a = ∣1⟩. +Proof. +intros a a_qubit. +assert (temp: WF_Qubit a). assumption. +destruct temp as [_ [WF_a a_unit]]. +set (P := (fun x y => +match (x,y) with +| (0,0) => - (a 1%nat 0%nat) +| (0,1) => (a 0%nat 0%nat) +| (1,0) => (a 0%nat 0%nat)^* +| (1,1) => (a 1%nat 0%nat)^* +| _ => C0 +end) : Square 2). +assert (WF_P: WF_Matrix P). +{ + unfold WF_Matrix. + intros. + unfold P. + destruct H. + destruct x as [|b]. contradict H. lia. + destruct b as [|x]. contradict H. lia. reflexivity. + destruct x as [|b]. destruct y as [|c]. contradict H. lia. + destruct c as [|y]. contradict H. lia. reflexivity. + destruct b as [|x]. destruct y as [|c]. contradict H. lia. + destruct c as [|y]. contradict H. lia. + reflexivity. reflexivity. +} +exists P. +split. +{ + unfold WF_Unitary. + split. assumption. + lma'. + all: rewrite Mmult_square2_explicit. + 2,3,5,6,8,9,11,12: solve_WF_matrix. + all: repeat rewrite Madj_explicit_decomp. + all: unfold P,I. + all: simpl. + 2,3: lca. + all: rewrite <- a_unit. + all: lca. +} +{ + lma'. + all: rewrite Mv_prod_21_explicit. + 2,3,5,6: assumption. + all: unfold P. + lca. + rewrite <- a_unit. lca. +} +Qed. + Lemma orth_qubit_unitary: forall (a b: Vector 2), WF_Qubit a -> WF_Qubit b -> ⟨ a, b ⟩ = 0 -> WF_Unitary (a × ⟨0∣ .+ b × ⟨1∣). @@ -684,4 +736,51 @@ apply C1_neq_C0. rewrite <- H. rewrite <- q_unit. reflexivity. +Qed. + +Lemma qubit_not_0tens {n}: forall (x : Vector (2*n)), +n <> 0%nat -> WF_Matrix x -> +(exists i: nat, (n <= i)%nat /\ x i 0%nat <> 0) -> +forall (y : Vector n), WF_Matrix y -> x <> ∣0⟩ ⊗ y. +Proof. +intros x nn0 WF_x eln0 y. +destruct eln0 as [i [ibound x0]]. +unfold not. +intros. +apply x0. +rewrite H0. +unfold kron. +rewrite <- Nat.mul_1_r with (n:= n) in ibound. +apply Nat.div_le_lower_bound in ibound. 2: assumption. +assert (iub : (i < n * 2)%nat). +{ + destruct (le_lt_dec (n*2) i). + { + contradict x0. + rewrite WF_x. + reflexivity. + left. lia. + } + assumption. +} +apply Nat.div_lt_upper_bound in iub. 2: assumption. +assert (ind_val:= nat_tight_bound 1 (i/n)%nat ibound iub). +rewrite <- ind_val. +lca. +Qed. + +Lemma qubit_not_1tens {n}: forall (x : Vector (2*n)), +n <> 0%nat -> WF_Matrix x -> +(exists i: nat, (i < n)%nat /\ x i 0%nat <> 0) -> +forall (y : Vector n), WF_Matrix y -> x <> ∣1⟩ ⊗ y. +Proof. +intros x nn0 WF_x eln0 y. +destruct eln0 as [i [ibound x0]]. +unfold not. +intros. +apply x0. +rewrite H0. +unfold kron. +rewrite Nat.div_small. +lca. assumption. Qed. \ No newline at end of file diff --git a/TensorProducts.v b/TensorProducts.v index 55115a1..361af65 100644 --- a/TensorProducts.v +++ b/TensorProducts.v @@ -428,6 +428,171 @@ destruct (Classical_Prop.classic (TensorProd (U × (∣0⟩ ⊗ ∣0⟩)))). } Qed. +Lemma a21b: forall (U : Square 4), +WF_Unitary U -> exists (psi : Vector 2), +WF_Qubit psi /\ TensorProd (U × (∣1⟩ ⊗ psi)). +Proof. +intros U U_unitary. +destruct (Classical_Prop.classic (TensorProd (U × (∣1⟩ ⊗ ∣0⟩)))). +{ + exists ∣0⟩. split. apply qubit0_qubit. assumption. +} +{ + set (a00 := (U × (∣1⟩ ⊗ ∣0⟩)) 0%nat 0%nat). + set (a01 := (U × (∣1⟩ ⊗ ∣0⟩)) 1%nat 0%nat). + set (a10 := (U × (∣1⟩ ⊗ ∣0⟩)) 2%nat 0%nat). + set (a11 := (U × (∣1⟩ ⊗ ∣0⟩)) 3%nat 0%nat). + set (b00 := (U × (∣1⟩ ⊗ ∣1⟩)) 0%nat 0%nat). + set (b01 := (U × (∣1⟩ ⊗ ∣1⟩)) 1%nat 0%nat). + set (b10 := (U × (∣1⟩ ⊗ ∣1⟩)) 2%nat 0%nat). + set (b11 := (U × (∣1⟩ ⊗ ∣1⟩)) 3%nat 0%nat). + set (a := (a00 * a11 - a01 * a10)%C). + set (b := (a00 * b11 + a11 * b00 - a01 * b10 - a10 * b01)%C). + set (c := (b00 * b11 - b01 * b10)%C). + set (quad := Complex_sqrt (b * b - 4 * a * c)%C). + set (p0 := (/ (2 * a)%C * (-b + quad))%C). + set (c0 := 1 / √ ((Cmod p0)^2 + 1)%R). + set (psi0 := c0 * p0 .* ∣0⟩ .+ c0 .* ∣1⟩). + exists psi0. + assert (div_g0: 0 < Cmod p0 ^ 2 + 1). + { + rewrite <- Rplus_0_l with (r:= 0). + apply Rplus_le_lt_compat. 2: lra. + apply Rsqr_ge_0. + } + split. + { + unfold WF_Qubit. + split. exists (1%nat). trivial. + split. solve_WF_matrix. + rewrite vector2_inner_prod_decomp. + unfold psi0. + repeat rewrite Mplus_access. + repeat rewrite <- Mscale_access. + simpl. + repeat rewrite Cmult_0_r. + repeat rewrite Cmult_1_r. + repeat rewrite Cplus_0_l, Cplus_0_r. + rewrite Cconj_mult_distr. + rewrite <- Cmult_assoc. + rewrite Cmult_comm with (x := p0^*). + rewrite <- Cmult_assoc. rewrite Cmult_assoc at 1. + rewrite <- Cmult_1_r with (x:= c0 ^* * c0) at 2. + rewrite <- Cmult_plus_distr_l with (x:= c0 ^* * c0). + assert (expansion: c0^* * c0 = C1 / (Cmod p0 ^ 2 + 1)). + { + unfold c0. + repeat rewrite <- RtoC_div. + rewrite RtoC_conj. + rewrite <- RtoC_mult. + rewrite Rfrac_product with (a:= 1) . + rewrite sqrt_sqrt. + rewrite Rmult_1_l. + rewrite RtoC_div. + rewrite RtoC_plus. + rewrite RtoC_pow. + reflexivity. + 3,4,5: apply g0_sqn0. + apply Rgt_not_eq. + apply Rlt_gt. + 2: apply Rlt_le. + all: apply div_g0. + } + rewrite expansion. + rewrite Cmult_comm with (x:= p0). + rewrite <- Cmod_sqr. + unfold Cdiv. + rewrite Cmult_1_l. + apply Cinv_l. + unfold not. + intro. + apply complex_split in H0. + destruct H0. + apply eq_sym in H0. + revert H0. + rewrite RtoC_pow. + rewrite <- RtoC_plus. + unfold RtoC. + simpl. + apply Rlt_not_eq. + replace ((Cmod p0 * (Cmod p0 * 1))%R) with ((Cmod p0 ^ 2)%R) by lra. + assumption. + } + apply a20. solve_WF_matrix. apply U_unitary. + assert (psi0_def: psi0 = c0 * p0 .* ∣0⟩ .+ c0 .* ∣1⟩). unfold psi0. reflexivity. + assert (prod_decomp: U × (∣1⟩ ⊗ psi0) = U × (∣1⟩ ⊗ psi0)). reflexivity. + rewrite psi0_def in prod_decomp at 2. + rewrite kron_plus_distr_l in prod_decomp. + repeat rewrite Mscale_kron_dist_r in prod_decomp. + rewrite Mmult_plus_distr_l in prod_decomp. + repeat rewrite Mscale_mult_dist_r in prod_decomp. + assert (def0: (U × (∣1⟩ ⊗ psi0)) 0%nat 0%nat = c0 * p0 * a00 + c0 * b00). + { + rewrite prod_decomp. + rewrite Mplus_access. + repeat rewrite <- Mscale_access. + unfold a00, b00. + reflexivity. + } + assert (def1: (U × (∣1⟩ ⊗ psi0)) 1%nat 0%nat = c0 * p0 * a01 + c0 * b01). + { + rewrite prod_decomp. + rewrite Mplus_access. + repeat rewrite <- Mscale_access. + unfold a01, b01. + reflexivity. + } + assert (def2: (U × (∣1⟩ ⊗ psi0)) 2%nat 0%nat = c0 * p0 * a10 + c0 * b10). + { + rewrite prod_decomp. + rewrite Mplus_access. + repeat rewrite <- Mscale_access. + unfold a10, b10. + reflexivity. + } + assert (def3: (U × (∣1⟩ ⊗ psi0)) 3%nat 0%nat = c0 * p0 * a11 + c0 * b11). + { + rewrite prod_decomp. + rewrite Mplus_access. + repeat rewrite <- Mscale_access. + unfold a11, b11. + reflexivity. + } + rewrite def0, def1, def2, def3. + repeat rewrite <- Cmult_assoc. + repeat rewrite <- Cmult_plus_distr_l. + repeat rewrite <- Cmult_assoc. + rewrite Cmult_comm with (x := (p0 * a00 + b00)). + rewrite Cmult_comm with (x := (p0 * a01 + b01)). + rewrite <- Cmult_assoc. + rewrite Cmult_assoc with (y := c0). + rewrite <- Cmult_assoc with (y := (p0 * a10 + b10)). + rewrite Cmult_assoc with (y := c0). + apply Cmult_simplify. reflexivity. + rewrite <- Cplus_0_l with (x := (p0 * a11 + b11) * (p0 * a00 + b00)). + rewrite <- Cplus_0_r with (x := (p0 * a10 + b10) * (p0 * a01 + b01)). + rewrite <- Cplus_opp_r with (x := (p0 * a10 + b10) * (p0 * a01 + b01)) at 1. + rewrite <- Cplus_assoc. + apply Cplus_simplify. reflexivity. + assert (replace_helper: forall (p0 a10 b10 a01 b01 a11 b11 a00 b00: C), + - ((p0 * a10 + b10) * (p0 * a01 + b01)) + (p0 * a11 + b11) * (p0 * a00 + b00) = + p0 ^ 2 * (a00 * a11 - a01 * a10) + p0 * (a00 * b11 + a11 * b00 - a01 * b10 - a10 * b01) + + (b00 * b11 - b01 * b10)). intros. lca. + rewrite replace_helper. + fold a b c. + apply quadratic_formula. 2: unfold p0. 2: reflexivity. + (* follows from U00 not a tensor prod *) + unfold a. unfold not. intro. + apply H. + rewrite a20. 2: solve_WF_matrix. 2: apply U_unitary. + fold a00 a11 a01 a10. + apply (f_equal (fun f => f + a01 * a10)) in H0. + rewrite Cplus_0_l in H0. + rewrite <- H0. + lca. +} +Qed. + Lemma a22: forall (U: Square 4) (a b g psi : Vector 2) (phi : Vector 4), WF_Unitary U -> WF_Qubit a -> WF_Qubit b -> WF_Qubit g -> WF_Qubit psi -> WF_Qubit phi -> (acgate U) × (a ⊗ b ⊗ g) = psi ⊗ phi -> @@ -771,35 +936,256 @@ Qed. Lemma a24: forall (U V W00 W11 : Square 4), WF_Unitary U -> WF_Unitary V -> WF_Unitary W00 -> WF_Unitary W11 -> -acgate U × acgate V = ∣0⟩⟨0∣ ⊗ W00 .+ ∣1⟩⟨1∣ ⊗ W11 -> +acgate U × abgate V = ∣0⟩⟨0∣ ⊗ W00 .+ ∣1⟩⟨1∣ ⊗ W11 -> exists (P0 Q0 P1 Q1 : Square 2), WF_Unitary P0 /\ WF_Unitary Q0 /\ WF_Unitary P1 /\ WF_Unitary Q1 /\ -acgate U × acgate V = ∣0⟩⟨0∣ ⊗ P0 ⊗ Q0 .+ ∣1⟩⟨1∣ ⊗ P1 ⊗ Q1. +acgate U × abgate V = ∣0⟩⟨0∣ ⊗ P0 ⊗ Q0 .+ ∣1⟩⟨1∣ ⊗ P1 ⊗ Q1. Proof. intros U V W00 W11 U_unitary V_unitary W00_unitary W11_unitary acgate_mult. assert (temp: WF_Unitary V). assumption. destruct temp as [WF_V V_inv]. +assert (temp: WF_Unitary W00). assumption. +destruct temp as [WF_W00 W00_inv]. +assert (temp: WF_Unitary W11). assumption. +destruct temp as [WF_W11 W11_inv]. assert (temp:= a21 V V_unitary). -destruct temp as [psi [psi_qubit tens]]. -assert (temp: WF_Qubit psi). assumption. -destruct temp as [_ [WF_psi psi_unit]]. +destruct temp as [psi0 [psi0_qubit tens]]. +assert (temp: WF_Qubit psi0). assumption. +destruct temp as [_ [WF_psi0 psi0_unit]]. rewrite tensor_prod_of_qubit in tens. 2: { unfold WF_Qubit. split. exists 2%nat. trivial. split. solve_WF_matrix. rewrite <- unitary_preserves_inner_prod. 2: assumption. 2: solve_WF_matrix. - assert (kip_help: ⟨ ∣0⟩ ⊗ psi, ∣0⟩ ⊗ psi ⟩ = ⟨ ∣0⟩, ∣0⟩ ⟩ * ⟨ psi, psi ⟩). apply kron_inner_prod. + assert (kip_help: ⟨ ∣0⟩ ⊗ psi0, ∣0⟩ ⊗ psi0 ⟩ = ⟨ ∣0⟩, ∣0⟩ ⟩ * ⟨ psi0, psi0 ⟩). apply kron_inner_prod. rewrite kip_help at 1. clear kip_help. replace (⟨ ∣0⟩, ∣0⟩ ⟩) with (C1) by lca. - rewrite psi_unit. + rewrite psi0_unit. apply Cmult_1_l. } -assert (temp: WF_Matrix (V × (∣0⟩ ⊗ psi))). solve_WF_matrix. +assert (temp: WF_Matrix (V × (∣0⟩ ⊗ psi0))). solve_WF_matrix. unfold TensorProdQubit in tens. -apply tens in temp. -destruct temp as [a [b [a_qubit [b_qubit ab_decomp]]]]. -Admitted. +apply tens in temp. clear tens. +destruct temp as [a0 [b0 [a0_qubit [b0_qubit ab0_decomp]]]]. +destruct (exists_unitary_mapping_qubit_to_0 a0 a0_qubit) as [M0 [M0_unitary M0_prop]]. +assert (temp: WF_Unitary M0). assumption. +destruct temp as [WF_M0 M0_inv]. +assert (prod_decomp_0pass: acgate U × abgate V = acgate U × (M0† ⊗ I 2 ⊗ I 2) × (M0 ⊗ I 2 ⊗ I 2) × abgate V). +{ + rewrite Mmult_assoc. rewrite Mmult_assoc. + rewrite <- Mmult_assoc with (C:= abgate V). + assert (kron_mix_help: (M0) † ⊗ I 2 ⊗ I 2 × (M0 ⊗ I 2 ⊗ I 2) = ((M0) † ⊗ I 2 × (M0 ⊗ I 2)) ⊗ (I 2 × (I 2))). + apply kron_mixed_product. + rewrite kron_mix_help at 1. + rewrite kron_mixed_product. + rewrite Mmult_1_l. 2: solve_WF_matrix. + rewrite M0_inv. + rewrite id_kron. rewrite id_kron. rewrite Mmult_1_l. + reflexivity. + apply WF_abgate. assumption. +} +assert (ac_0pass: forall (y: Vector 2), WF_Qubit y -> +(exists (phi : Vector 4), WF_Matrix phi /\ acgate U × abgate V × (∣0⟩ ⊗ psi0 ⊗ y) = ∣0⟩ ⊗ phi)). +{ + intros y y_qubit. + destruct y_qubit as [_ [WF_y y_unit]]. + exists (W00 × (psi0 ⊗ y)). + split. solve_WF_matrix. + rewrite acgate_mult. + rewrite Mmult_plus_distr_r. + rewrite kron_assoc. 2,3,4: solve_WF_matrix. + repeat rewrite kron_mixed_product. + repeat rewrite Mmult_assoc. + rewrite Mmult10 at 1. + rewrite Mmult_0_r. rewrite kron_0_l. rewrite Mplus_0_r. + rewrite Mmult00 at 1. + rewrite Mmult_1_r. 2: solve_WF_matrix. + reflexivity. +} +rewrite prod_decomp_0pass in ac_0pass. +assert ((forall y : Vector 2, +WF_Qubit y -> exists phi : Vector 4, WF_Matrix phi /\ acgate U × ((M0) † ⊗ I 2 ⊗ I 2) + × (M0 ⊗ I 2 ⊗ I 2) × abgate V × (∣0⟩ ⊗ psi0 ⊗ y) = ∣0⟩ ⊗ phi) -> + (forall y : Vector 2, + WF_Qubit y -> exists phi : Vector 4, WF_Matrix phi /\ acgate U × ((M0) † ⊗ I 2 ⊗ I 2) + × (∣0⟩ ⊗ b0 ⊗ y) = ∣0⟩ ⊗ phi)). +{ + intros H y y_qubit. + specialize (H y y_qubit). + destruct H as [phi [WF_phi H]]. + exists phi. + split. assumption. + rewrite <- H. + repeat rewrite Mmult_assoc. + unfold abgate. + rewrite kron_mixed_product. + rewrite Mmult_1_l. 2: apply y_qubit. + rewrite ab0_decomp at 1. + rewrite kron_mixed_product. + rewrite Mmult_1_l. 2: apply y_qubit. + rewrite kron_mixed_product. + rewrite Mmult_1_l. 2: apply b0_qubit. + rewrite M0_prop. + reflexivity. +} +assert (ac_0pass_cor: forall y : Vector 2, WF_Qubit y -> +exists phi : Vector 4, WF_Matrix phi /\ + acgate U × ((M0) † ⊗ I 2 ⊗ I 2) + × (∣0⟩ ⊗ b0 ⊗ y) = ∣0⟩ ⊗ phi). apply H. assumption. +clear H ac_0pass. +assert (acgate_condense: acgate U × ((M0) † ⊗ I 2 ⊗ I 2) = acgate (U × ((M0) † ⊗ I 2))). +{ + unfold acgate at 2. + unfold abgate. + rewrite <- Mmult_1_l with (A:= I 2) at 4. 2: solve_WF_matrix. + rewrite <- kron_mixed_product. + rewrite <- Mmult_1_r with (A:= (U ⊗ I 2)). 2: solve_WF_matrix; apply U_unitary. + simpl. + rewrite <- swapbc_inverse. + unfold acgate. + unfold abgate. + repeat rewrite Mmult_assoc. + rewrite <- Mmult_assoc with (B := (M0) † ⊗ I 2 ⊗ I 2). + rewrite swapbc_3gate. 2,3,4: solve_WF_matrix. + reflexivity. +} +rewrite acgate_condense in ac_0pass_cor. +assert (ac_inner_unitary: WF_Unitary (U × ((M0) † ⊗ I 2))). +{ + apply Mmult_unitary. apply U_unitary. + apply kron_unitary. apply transpose_unitary. assumption. + apply id_unitary. +} +assert (acgate_diagblock_partial := acgate_diagblock (U × ((M0) † ⊗ I 2)) ac_inner_unitary). +assert (acgate_diag: exists TL BR : Square 4, WF_Unitary TL /\ WF_Unitary BR /\ + acgate (U × ((M0) † ⊗ I 2)) = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR). +{ + apply acgate_diagblock_partial. + exists b0. + split. assumption. + assumption. +} +clear acgate_diagblock_partial. +destruct acgate_diag as [acdiagTL [acdiagBR [acdiagTL_unitary [acdiagBR_unitary acgate_diag]]]]. +assert (acgate_2control_partial:= acgate_control (U × ((M0) † ⊗ I 2)) acdiagTL acdiagBR +ac_inner_unitary acdiagTL_unitary acdiagBR_unitary acgate_diag). +destruct (acgate_2control_partial) as [Q0 [Q1 [Q0_unitary [Q1_unitary acgate_inner_prop]]]]. +assert (abgate_0passthru_int : forall (y : Vector 2), WF_Qubit y -> forall (x: Vector 2), WF_Qubit x -> +(exists (phi : Vector 4), WF_Matrix phi /\ acgate U × abgate V × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi)). +{ + intros y y_qubit x x_qubit. + exists (W00 × (x ⊗ y)). + split. solve_WF_matrix. apply x_qubit. apply y_qubit. + rewrite acgate_mult. + rewrite Mmult_plus_distr_r. + rewrite kron_assoc. 4: apply y_qubit. 3: apply x_qubit. 2: solve_WF_matrix. + repeat rewrite kron_mixed_product. + repeat rewrite Mmult_assoc. + rewrite Mmult10 at 1. + rewrite Mmult_0_r. rewrite kron_0_l. rewrite Mplus_0_r. + rewrite Mmult00 at 1. + rewrite Mmult_1_r. 2: solve_WF_matrix. + reflexivity. +} +assert (abgate_condense: M0 ⊗ I 2 ⊗ I 2 × abgate V = abgate ((M0 ⊗ I 2) × V)). +{ + unfold abgate. + rewrite kron_mixed_product. + rewrite Mmult_1_l. 2: solve_WF_matrix. + reflexivity. +} +assert (abgate_0passthru: (exists (y: Vector 2), WF_Qubit y /\ +forall (x : Vector 2), WF_Qubit x -> (exists (phi: Vector 4), WF_Matrix phi /\ +(abgate ((M0 ⊗ I 2) × V)) × (∣0⟩ ⊗ x ⊗ y) = ∣0⟩ ⊗ phi))). +{ + exists ∣0⟩. + split. apply qubit0_qubit. + intros x x_qubit. + specialize (abgate_0passthru_int ∣0⟩ qubit0_qubit x x_qubit). + destruct abgate_0passthru_int as [phi [WF_phi abgate_0passthru_int]]. + rewrite prod_decomp_0pass in abgate_0passthru_int. + rewrite acgate_condense in abgate_0passthru_int. + apply (f_equal (fun f => (acgate (U × ((M0) † ⊗ I 2)))† × f)) in abgate_0passthru_int. + assert (acgate_condensed_unit: WF_Unitary (acgate (U × ((M0) † ⊗ I 2)))). + { + apply acgate_unitary. assumption. + } + destruct acgate_condensed_unit as [WF_condensed condensed_inv]. + repeat rewrite <- Mmult_assoc in abgate_0passthru_int. + rewrite condensed_inv in abgate_0passthru_int at 1. + rewrite Mmult_1_l in abgate_0passthru_int. 2: solve_WF_matrix. + rewrite abgate_condense in abgate_0passthru_int at 1. + rewrite acgate_diag in abgate_0passthru_int. + rewrite Mplus_adjoint in abgate_0passthru_int. + repeat rewrite kron_adjoint in abgate_0passthru_int. + rewrite adjoint00, adjoint11 in abgate_0passthru_int. + rewrite Mmult_plus_distr_r in abgate_0passthru_int. + rewrite kron_mixed_product in abgate_0passthru_int. + rewrite Mmult_assoc in abgate_0passthru_int. + rewrite Mmult00 in abgate_0passthru_int at 1. + rewrite Mmult_1_r in abgate_0passthru_int. 2: solve_WF_matrix. + rewrite kron_mixed_product in abgate_0passthru_int. + rewrite Mmult_assoc in abgate_0passthru_int. + rewrite Mmult10 in abgate_0passthru_int at 1. + rewrite Mmult_0_r in abgate_0passthru_int. + rewrite kron_0_l in abgate_0passthru_int. + rewrite Mplus_0_r in abgate_0passthru_int. + exists ((acdiagTL) † × phi). + split. solve_WF_matrix. apply acdiagTL_unitary. + assumption. +} +assert (ab_inner_unitary: WF_Unitary ((M0 ⊗ I 2) × V)). +{ + apply Mmult_unitary. + apply (@kron_unitary 2 2). assumption. + apply id_unitary. + assumption. +} +assert (abgate_diagblock_partial := abgate_diagblock (M0 ⊗ I 2 × V) ab_inner_unitary). +assert (abgate_diag: exists TL BR : Square 4, +WF_Unitary TL /\ WF_Unitary BR /\ +abgate (M0 ⊗ I 2 × V) = ∣0⟩⟨0∣ ⊗ TL .+ ∣1⟩⟨1∣ ⊗ BR). +{ + apply abgate_diagblock_partial. + assumption. +} +clear abgate_diagblock_partial. +destruct abgate_diag as [abdiagTL [abdiagBR [abdiagTL_unitary [abdiagBR_unitary abgate_diag]]]]. +assert (abgate_2control_partial:= abgate_control (M0 ⊗ I 2 × V) abdiagTL abdiagBR +ab_inner_unitary abdiagTL_unitary abdiagBR_unitary abgate_diag). +destruct (abgate_2control_partial) as [P0 [P1 [P0_unitary [P1_unitary abgate_inner_prop]]]]. +exists P0, Q0, P1, Q1. +split. assumption. +split. assumption. +split. assumption. +split. assumption. +rewrite prod_decomp_0pass. +rewrite acgate_condense. +rewrite Mmult_assoc. +rewrite abgate_condense. +rewrite acgate_inner_prop. +rewrite abgate_inner_prop. +rewrite Mmult_plus_distr_l. +repeat rewrite Mmult_plus_distr_r. +repeat rewrite kron_mixed_product. +repeat rewrite isolate_inner_mult. +rewrite Mmult00, Mmult01, Mmult10, Mmult11. +repeat rewrite Mmult_0_r. +repeat rewrite Mmult_0_l. +repeat rewrite kron_0_l. +rewrite Mplus_0_l. +rewrite Mplus_0_r. +repeat rewrite Mmult_1_r. +repeat rewrite Mmult_1_l. +reflexivity. +apply P1_unitary. +apply P0_unitary. +apply Q1_unitary. +solve_WF_matrix. +apply Q0_unitary. +solve_WF_matrix. +Qed. Lemma a25: forall (V : Square 4) (psi: Vector 2), WF_Unitary V -> WF_Qubit psi ->