Skip to content

feat(M3.3): Remove c, d <> C0 stipulation. #41

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
kylechui merged 1 commit into from
May 21, 2024
Merged

feat(M3.3): Remove c, d <> C0 stipulation. #41

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
feat(M3.3): Remove c, d <> C0 stipulation.
  • Loading branch information
@kylechui
kylechui committed May 21, 2024
commit bd3251db57fe79f9b1927aa61246b1e619608b64
82 changes: 55 additions & 27 deletions Main.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -491,15 +491,14 @@ Lemma m3_3 : forall (u0 u1 : C),
Cmod u0 = 1 -> Cmod u1 = 1 ->
(exists (P : Square 2), WF_Unitary P /\
exists (U : Square 4), WF_Unitary U /\
exists (c d : C), c <> C0 /\ d <> C0 /\
((I 2) ⊗ P) × control (diag2 u0 u1) = U × diag4 c c d d × U†)
exists (c d : C), ((I 2) ⊗ P) × control (diag2 u0 u1) = U × diag4 c c d d × U†)
<-> u0 = u1 \/ u0 * u1 = C1.
Proof.
intros u0 u1 unit_u0 unit_u1.
split.
{
intro.
destruct H as [P [Unitary_P [U [Unitary_U [c [d [c_neq_0 [d_neq_0 H]]]]]]]].
destruct H as [P [Unitary_P [U [Unitary_U [c [d H]]]]]].
set (PD := P × diag2 u0 u1).
assert (Unitary_PD : WF_Unitary (P × diag2 u0 u1)).
{
Expand Down Expand Up @@ -542,7 +541,7 @@ Proof.
all: specialize (step3 2%nat) as eigen2.
all: specialize (step3 3%nat) as eigen3.

assert (case_A : forall (c d : C), (c <> C0 -> DP 0 0 = c -> DP 1 1 = c ->
assert (case_A : forall (c d : C), (DP 0 0 = c -> DP 1 1 = c ->
DPD 0 0 = d -> DPD 1 1 = d -> u0 = u1)%nat).
{
intros.
Expand All @@ -554,7 +553,7 @@ Proof.
}
{
unfold scale, I; simpl.
rewrite H1; lca.
rewrite H0; lca.
}
{
unfold scale, I; simpl.
Expand All @@ -572,7 +571,7 @@ Proof.
}
{
unfold scale, I; simpl.
rewrite H2; lca.
rewrite H1; lca.
}
}
assert (DPD_dI : DPD = d0 .* I 2).
Expand All @@ -583,7 +582,7 @@ Proof.
}
{
unfold scale, I; simpl.
rewrite H3; lca.
rewrite H2; lca.
}
{
destruct Diagonal_DPD as [_ DPD_0].
Expand All @@ -599,8 +598,33 @@ Proof.
}
{
unfold scale, I; simpl.
rewrite H4; lca.
rewrite H3; lca.
}
}
assert (c0_neq_C0 : c0 <> C0).
{
assert (det_P : Determinant P = c0 * c0).
{
assert (VP_u : WF_Unitary (VP†)).
{
apply adjoint_unitary; assumption.
}
rewrite P_decomp, DP_cI.
replace (c0 .* I 2) with (diag2 c0 c0).
repeat rewrite <- Determinant_multiplicative.
rewrite Cmult_comm, Cmult_assoc.
rewrite Determinant_multiplicative.
destruct Unitary_VP as [_ Unitary_VP].
rewrite Unitary_VP, Det_I, Cmult_1_l.
apply Det_diag2.
lma'.
all: unfold diag2, I, scale; simpl; lca.
}
pose proof (unit_det_neq_0 P Unitary_P).
rewrite det_P in H4; clear det_P.
intro.
contradict H4.
rewrite H5; lca.
}
rewrite DP_cI in P_decomp; clear DP_cI.
rewrite DPD_dI in PD_decomp; clear DPD_dI.
Expand Down Expand Up @@ -644,10 +668,10 @@ Proof.
unfold scale, diag2, I in PD_dI; simpl in PD_dI.
rewrite PD_dI; lca.
}
apply (Cmult_cancel_l c0); try apply H0.
apply (Cmult_cancel_l c0); try apply H0; auto.
rewrite cu0_d, cu1_d; reflexivity.
}
assert (case_B : forall (c d : C), c <> C0 -> d <> C0 ->
assert (case_B : forall (c d : C),
(DP 0 0)%nat = c -> (DP 1 1)%nat = d ->
(DPD 0 0)%nat = c -> (DPD 1 1)%nat = d -> u0 * u1 = C1).
{
Expand All @@ -660,7 +684,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H2; reflexivity.
rewrite H0; reflexivity.
}
{
destruct Diagonal_DP as [_ DP_0].
Expand All @@ -674,7 +698,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H3; reflexivity.
rewrite H1; reflexivity.
}
}
assert (DPD_diag : DPD = diag2 c0 d0).
Expand All @@ -685,7 +709,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H4; reflexivity.
rewrite H2; reflexivity.
}
{
destruct Diagonal_DPD as [_ DPD_0].
Expand All @@ -699,7 +723,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H5; reflexivity.
rewrite H3; reflexivity.
}
}
rewrite DP_diag in P_decomp; clear DP_diag.
Expand All @@ -726,14 +750,18 @@ Proof.
rewrite Det_I, Cmult_1_l.
rewrite Det_diag2; reflexivity.
}
assert (c0d0_neq_C0 : c0 * d0 <> C0).
{
rewrite <- detP.
apply unit_det_neq_0; auto.
}
unfold PD in detPD.
rewrite a1 in detPD.
rewrite detP, Det_diag2 in detPD.
apply (Cmult_cancel_l (c0 * d0)).
apply Cmult_nonzero; auto.
apply (Cmult_cancel_l (c0 * d0)); auto.
rewrite detPD; lca.
}
assert (case_C : forall (c d : C), c <> C0 -> d <> C0 ->
assert (case_C : forall (c d : C),
(DP 0 0)%nat = c -> (DP 1 1)%nat = d ->
(DPD 0 0)%nat = d -> (DPD 1 1)%nat = c -> u0 * u1 = C1).
{
Expand All @@ -746,7 +774,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H2; reflexivity.
rewrite H0; reflexivity.
}
{
destruct Diagonal_DP as [_ DP_0].
Expand All @@ -760,7 +788,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H3; reflexivity.
rewrite H1; reflexivity.
}
}
assert (DPD_diag : DPD = diag2 d0 c0).
Expand All @@ -771,7 +799,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H4; reflexivity.
rewrite H2; reflexivity.
}
{
destruct Diagonal_DPD as [_ DPD_0].
Expand All @@ -785,7 +813,7 @@ Proof.
}
{
unfold diag2; simpl.
rewrite H5; reflexivity.
rewrite H3; reflexivity.
}
}
rewrite DP_diag in P_decomp; clear DP_diag.
Expand Down Expand Up @@ -814,11 +842,15 @@ Proof.
rewrite Det_I, Cmult_1_l.
rewrite Det_diag2, Cmult_comm; reflexivity.
}
assert (c0d0_neq_C0 : c0 * d0 <> C0).
{
rewrite <- detP.
apply unit_det_neq_0; auto.
}
unfold PD in detPD.
rewrite a1 in detPD.
rewrite detP, Det_diag2 in detPD.
apply (Cmult_cancel_l (c0 * d0)).
apply Cmult_nonzero; auto.
apply (Cmult_cancel_l (c0 * d0)); auto.
rewrite detPD; lca.
}

Expand Down Expand Up @@ -936,8 +968,6 @@ Proof.
exists (I 4).
split; try apply id_unitary.
exists C1, u0.
split; try apply C1_neq_C0.
split. rewrite Cmod_gt_0, unit_u0; lra.
rewrite id_kron; Msimpl_light.
lma'; solve_WF_matrix.
}
Expand All @@ -956,8 +986,6 @@ Proof.
}
{
exists C1, u0.
split; try apply C1_neq_C0.
split; try rewrite Cmod_gt_0, unit_u0; try lra.
assert (H : I 2 ⊗ diag2 C1 u0 × control (diag2 u0 u1) = diag4 C1 u0 u0 (u0 * u1)).
{
lma'; solve_WF_matrix.
Expand Down