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

kylechui · web-flow · commit c06e964a54f5 · 2024-05-20T21:55:36.000-07:00
diff --git a/Main.v b/Main.v
@@ -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)).
     {
@@ -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.
@@ -554,7 +553,7 @@ Proof.
         }
         {
           unfold scale, I; simpl.
-          rewrite H1; lca.
+          rewrite H0; lca.
         }
         {
           unfold scale, I; simpl.
@@ -572,7 +571,7 @@ Proof.
         }
         {
           unfold scale, I; simpl.
-          rewrite H2; lca.
+          rewrite H1; lca.
         }
       }
       assert (DPD_dI : DPD = d0 .* I 2).
@@ -583,7 +582,7 @@ Proof.
         }
         {
           unfold scale, I; simpl.
-          rewrite H3; lca.
+          rewrite H2; lca.
         }
         {
           destruct Diagonal_DPD as [_ DPD_0].
@@ -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.
@@ -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).
     {
@@ -660,7 +684,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H2; reflexivity.
+          rewrite H0; reflexivity.
         }
         {
           destruct Diagonal_DP as [_ DP_0].
@@ -674,7 +698,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H3; reflexivity.
+          rewrite H1; reflexivity.
         }
       }
       assert (DPD_diag : DPD = diag2 c0 d0).
@@ -685,7 +709,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H4; reflexivity.
+          rewrite H2; reflexivity.
         }
         {
           destruct Diagonal_DPD as [_ DPD_0].
@@ -699,7 +723,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H5; reflexivity.
+          rewrite H3; reflexivity.
         }
       }
       rewrite DP_diag in P_decomp; clear DP_diag.
@@ -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).
     {
@@ -746,7 +774,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H2; reflexivity.
+          rewrite H0; reflexivity.
         }
         {
           destruct Diagonal_DP as [_ DP_0].
@@ -760,7 +788,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H3; reflexivity.
+          rewrite H1; reflexivity.
         }
       }
       assert (DPD_diag : DPD = diag2 d0 c0).
@@ -771,7 +799,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H4; reflexivity.
+          rewrite H2; reflexivity.
         }
         {
           destruct Diagonal_DPD as [_ DPD_0].
@@ -785,7 +813,7 @@ Proof.
         }
         {
           unfold diag2; simpl.
-          rewrite H5; reflexivity.
+          rewrite H3; reflexivity.
         }
       }
       rewrite DP_diag in P_decomp; clear DP_diag.
@@ -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.
     }
 
@@ -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.
     }
@@ -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.

Original file line number	Diff line number	Diff line change
`@@ -491,15 +491,14 @@ Lemma m3_3 : forall (u0 u1 : C),`
`491`	`491`	`Cmod u0 = 1 -> Cmod u1 = 1 ->`
`492`	`492`	`(exists (P : Square 2), WF_Unitary P /\`
`493`	`493`	`exists (U : Square 4), WF_Unitary U /\`
`494`		`- exists (c d : C), c <> C0 /\ d <> C0 /\`
`495`		`- ((I 2) ⊗ P) × control (diag2 u0 u1) = U × diag4 c c d d × U†)`
	`494`	`+ exists (c d : C), ((I 2) ⊗ P) × control (diag2 u0 u1) = U × diag4 c c d d × U†)`
`496`	`495`	`<-> u0 = u1 \/ u0 * u1 = C1.`
`497`	`496`	`Proof.`
`498`	`497`	`intros u0 u1 unit_u0 unit_u1.`
`499`	`498`	`split.`
`500`	`499`	`{`
`501`	`500`	`intro.`
`502`		`- destruct H as [P [Unitary_P [U [Unitary_U [c [d [c_neq_0 [d_neq_0 H]]]]]]]].`
	`501`	`+ destruct H as [P [Unitary_P [U [Unitary_U [c [d H]]]]]].`
`503`	`502`	`set (PD := P × diag2 u0 u1).`
`504`	`503`	`assert (Unitary_PD : WF_Unitary (P × diag2 u0 u1)).`
`505`	`504`	`{`
`@@ -542,7 +541,7 @@ Proof.`
`542`	`541`	`all: specialize (step3 2%nat) as eigen2.`
`543`	`542`	`all: specialize (step3 3%nat) as eigen3.`
`544`	`543`
`545`		`- assert (case_A : forall (c d : C), (c <> C0 -> DP 0 0 = c -> DP 1 1 = c ->`
	`544`	`+ assert (case_A : forall (c d : C), (DP 0 0 = c -> DP 1 1 = c ->`
`546`	`545`	`DPD 0 0 = d -> DPD 1 1 = d -> u0 = u1)%nat).`
`547`	`546`	`{`
`548`	`547`	`intros.`
`@@ -554,7 +553,7 @@ Proof.`
`554`	`553`	`}`
`555`	`554`	`{`
`556`	`555`	`unfold scale, I; simpl.`
`557`		`- rewrite H1; lca.`
	`556`	`+ rewrite H0; lca.`
`558`	`557`	`}`
`559`	`558`	`{`
`560`	`559`	`unfold scale, I; simpl.`
`@@ -572,7 +571,7 @@ Proof.`
`572`	`571`	`}`
`573`	`572`	`{`
`574`	`573`	`unfold scale, I; simpl.`
`575`		`- rewrite H2; lca.`
	`574`	`+ rewrite H1; lca.`
`576`	`575`	`}`
`577`	`576`	`}`
`578`	`577`	`assert (DPD_dI : DPD = d0 .* I 2).`
`@@ -583,7 +582,7 @@ Proof.`
`583`	`582`	`}`
`584`	`583`	`{`
`585`	`584`	`unfold scale, I; simpl.`
`586`		`- rewrite H3; lca.`
	`585`	`+ rewrite H2; lca.`
`587`	`586`	`}`
`588`	`587`	`{`
`589`	`588`	`destruct Diagonal_DPD as [_ DPD_0].`
`@@ -599,8 +598,33 @@ Proof.`
`599`	`598`	`}`
`600`	`599`	`{`
`601`	`600`	`unfold scale, I; simpl.`
`602`		`- rewrite H4; lca.`
	`601`	`+ rewrite H3; lca.`
	`602`	`+ }`
	`603`	`+ }`
	`604`	`+ assert (c0_neq_C0 : c0 <> C0).`
	`605`	`+ {`
	`606`	`+ assert (det_P : Determinant P = c0 * c0).`
	`607`	`+ {`
	`608`	`+ assert (VP_u : WF_Unitary (VP†)).`
	`609`	`+ {`
	`610`	`+ apply adjoint_unitary; assumption.`
	`611`	`+ }`
	`612`	`+ rewrite P_decomp, DP_cI.`
	`613`	`+ replace (c0 .* I 2) with (diag2 c0 c0).`
	`614`	`+ repeat rewrite <- Determinant_multiplicative.`
	`615`	`+ rewrite Cmult_comm, Cmult_assoc.`
	`616`	`+ rewrite Determinant_multiplicative.`
	`617`	`+ destruct Unitary_VP as [_ Unitary_VP].`
	`618`	`+ rewrite Unitary_VP, Det_I, Cmult_1_l.`
	`619`	`+ apply Det_diag2.`
	`620`	`+ lma'.`
	`621`	`+ all: unfold diag2, I, scale; simpl; lca.`
`603`	`622`	`}`
	`623`	`+ pose proof (unit_det_neq_0 P Unitary_P).`
	`624`	`+ rewrite det_P in H4; clear det_P.`
	`625`	`+ intro.`
	`626`	`+ contradict H4.`
	`627`	`+ rewrite H5; lca.`
`604`	`628`	`}`
`605`	`629`	`rewrite DP_cI in P_decomp; clear DP_cI.`
`606`	`630`	`rewrite DPD_dI in PD_decomp; clear DPD_dI.`
`@@ -644,10 +668,10 @@ Proof.`
`644`	`668`	`unfold scale, diag2, I in PD_dI; simpl in PD_dI.`
`645`	`669`	`rewrite PD_dI; lca.`
`646`	`670`	`}`
`647`		`- apply (Cmult_cancel_l c0); try apply H0.`
	`671`	`+ apply (Cmult_cancel_l c0); try apply H0; auto.`
`648`	`672`	`rewrite cu0_d, cu1_d; reflexivity.`
`649`	`673`	`}`
`650`		`- assert (case_B : forall (c d : C), c <> C0 -> d <> C0 ->`
	`674`	`+ assert (case_B : forall (c d : C),`
`651`	`675`	`(DP 0 0)%nat = c -> (DP 1 1)%nat = d ->`
`652`	`676`	`(DPD 0 0)%nat = c -> (DPD 1 1)%nat = d -> u0 * u1 = C1).`
`653`	`677`	`{`
`@@ -660,7 +684,7 @@ Proof.`
`660`	`684`	`}`
`661`	`685`	`{`
`662`	`686`	`unfold diag2; simpl.`
`663`		`- rewrite H2; reflexivity.`
	`687`	`+ rewrite H0; reflexivity.`
`664`	`688`	`}`
`665`	`689`	`{`
`666`	`690`	`destruct Diagonal_DP as [_ DP_0].`
`@@ -674,7 +698,7 @@ Proof.`
`674`	`698`	`}`
`675`	`699`	`{`
`676`	`700`	`unfold diag2; simpl.`
`677`		`- rewrite H3; reflexivity.`
	`701`	`+ rewrite H1; reflexivity.`
`678`	`702`	`}`
`679`	`703`	`}`
`680`	`704`	`assert (DPD_diag : DPD = diag2 c0 d0).`
`@@ -685,7 +709,7 @@ Proof.`
`685`	`709`	`}`
`686`	`710`	`{`
`687`	`711`	`unfold diag2; simpl.`
`688`		`- rewrite H4; reflexivity.`
	`712`	`+ rewrite H2; reflexivity.`
`689`	`713`	`}`
`690`	`714`	`{`
`691`	`715`	`destruct Diagonal_DPD as [_ DPD_0].`
`@@ -699,7 +723,7 @@ Proof.`
`699`	`723`	`}`
`700`	`724`	`{`
`701`	`725`	`unfold diag2; simpl.`
`702`		`- rewrite H5; reflexivity.`
	`726`	`+ rewrite H3; reflexivity.`
`703`	`727`	`}`
`704`	`728`	`}`
`705`	`729`	`rewrite DP_diag in P_decomp; clear DP_diag.`
`@@ -726,14 +750,18 @@ Proof.`
`726`	`750`	`rewrite Det_I, Cmult_1_l.`
`727`	`751`	`rewrite Det_diag2; reflexivity.`
`728`	`752`	`}`
	`753`	`+ assert (c0d0_neq_C0 : c0 * d0 <> C0).`
	`754`	`+ {`
	`755`	`+ rewrite <- detP.`
	`756`	`+ apply unit_det_neq_0; auto.`
	`757`	`+ }`
`729`	`758`	`unfold PD in detPD.`
`730`	`759`	`rewrite a1 in detPD.`
`731`	`760`	`rewrite detP, Det_diag2 in detPD.`
`732`		`- apply (Cmult_cancel_l (c0 * d0)).`
`733`		`- apply Cmult_nonzero; auto.`
	`761`	`+ apply (Cmult_cancel_l (c0 * d0)); auto.`
`734`	`762`	`rewrite detPD; lca.`
`735`	`763`	`}`
`736`		`- assert (case_C : forall (c d : C), c <> C0 -> d <> C0 ->`
	`764`	`+ assert (case_C : forall (c d : C),`
`737`	`765`	`(DP 0 0)%nat = c -> (DP 1 1)%nat = d ->`
`738`	`766`	`(DPD 0 0)%nat = d -> (DPD 1 1)%nat = c -> u0 * u1 = C1).`
`739`	`767`	`{`
`@@ -746,7 +774,7 @@ Proof.`
`746`	`774`	`}`
`747`	`775`	`{`
`748`	`776`	`unfold diag2; simpl.`
`749`		`- rewrite H2; reflexivity.`
	`777`	`+ rewrite H0; reflexivity.`
`750`	`778`	`}`
`751`	`779`	`{`
`752`	`780`	`destruct Diagonal_DP as [_ DP_0].`
`@@ -760,7 +788,7 @@ Proof.`
`760`	`788`	`}`
`761`	`789`	`{`
`762`	`790`	`unfold diag2; simpl.`
`763`		`- rewrite H3; reflexivity.`
	`791`	`+ rewrite H1; reflexivity.`
`764`	`792`	`}`
`765`	`793`	`}`
`766`	`794`	`assert (DPD_diag : DPD = diag2 d0 c0).`
`@@ -771,7 +799,7 @@ Proof.`
`771`	`799`	`}`
`772`	`800`	`{`
`773`	`801`	`unfold diag2; simpl.`
`774`		`- rewrite H4; reflexivity.`
	`802`	`+ rewrite H2; reflexivity.`
`775`	`803`	`}`
`776`	`804`	`{`
`777`	`805`	`destruct Diagonal_DPD as [_ DPD_0].`
`@@ -785,7 +813,7 @@ Proof.`
`785`	`813`	`}`
`786`	`814`	`{`
`787`	`815`	`unfold diag2; simpl.`
`788`		`- rewrite H5; reflexivity.`
	`816`	`+ rewrite H3; reflexivity.`
`789`	`817`	`}`
`790`	`818`	`}`
`791`	`819`	`rewrite DP_diag in P_decomp; clear DP_diag.`
`@@ -814,11 +842,15 @@ Proof.`
`814`	`842`	`rewrite Det_I, Cmult_1_l.`
`815`	`843`	`rewrite Det_diag2, Cmult_comm; reflexivity.`
`816`	`844`	`}`
	`845`	`+ assert (c0d0_neq_C0 : c0 * d0 <> C0).`
	`846`	`+ {`
	`847`	`+ rewrite <- detP.`
	`848`	`+ apply unit_det_neq_0; auto.`
	`849`	`+ }`
`817`	`850`	`unfold PD in detPD.`
`818`	`851`	`rewrite a1 in detPD.`
`819`	`852`	`rewrite detP, Det_diag2 in detPD.`
`820`		`- apply (Cmult_cancel_l (c0 * d0)).`
`821`		`- apply Cmult_nonzero; auto.`
	`853`	`+ apply (Cmult_cancel_l (c0 * d0)); auto.`
`822`	`854`	`rewrite detPD; lca.`
`823`	`855`	`}`
`824`	`856`
`@@ -936,8 +968,6 @@ Proof.`
`936`	`968`	`exists (I 4).`
`937`	`969`	`split; try apply id_unitary.`
`938`	`970`	`exists C1, u0.`
`939`		`- split; try apply C1_neq_C0.`
`940`		`- split. rewrite Cmod_gt_0, unit_u0; lra.`
`941`	`971`	`rewrite id_kron; Msimpl_light.`
`942`	`972`	`lma'; solve_WF_matrix.`
`943`	`973`	`}`
`@@ -956,8 +986,6 @@ Proof.`
`956`	`986`	`}`
`957`	`987`	`{`
`958`	`988`	`exists C1, u0.`
`959`		`- split; try apply C1_neq_C0.`
`960`		`- split; try rewrite Cmod_gt_0, unit_u0; try lra.`
`961`	`989`	`assert (H : I 2 ⊗ diag2 C1 u0 × control (diag2 u0 u1) = diag4 C1 u0 u0 (u0 * u1)).`
`962`	`990`	`{`
`963`	`991`	`lma'; solve_WF_matrix.`