From 64044e081c377aa05680b510d51461259611460a Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Fri, 1 Nov 2024 14:34:34 -0700
Subject: [PATCH 01/20] state lemma 0.1

---
 Helpers/Permutations.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index 2916793..9ecbc8a 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -12,6 +12,15 @@ Lemma perm_eigenvalues : forall {n} (U D D' : Square n),
 Proof.
 Admitted.
 
+Lemma char_poly_eigenvalue_perm : forall {n} (D E U : Square n),
+  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E ->
+  U × D × U† = E ->
+  exists (σ : nat -> nat),
+    permutation n σ /\
+    forall (i : nat), (i < n)%nat -> D i i = E (σ i) (σ i).
+Proof.
+Admitted.
+
 (* To equate the eigenvalues of two matrices, we often need equality of matrices
    up to some permutation. This lemma allows us to take the existence of a
    permutation on 4 elements and decompose it into the 24 possible cases. *)

From 21cf8c72b5178c4da8d0913bfcdb394c0701ef0a Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Tue, 17 Dec 2024 15:28:45 +0530
Subject: [PATCH 02/20] finish outlining lemma 0.1

---
 Helpers/DiagonalHelpers.v |  1 +
 Helpers/MatrixHelpers.v   |  3 ++
 Helpers/Permutations.v    | 76 +++++++++++++++++++++++++++++++++------
 3 files changed, 70 insertions(+), 10 deletions(-)

diff --git a/Helpers/DiagonalHelpers.v b/Helpers/DiagonalHelpers.v
index fc7c478..4fd49b6 100644
--- a/Helpers/DiagonalHelpers.v
+++ b/Helpers/DiagonalHelpers.v
@@ -1,4 +1,5 @@
 Require Import QuantumLib.Eigenvectors.
+Require Import QuantumLib.Matrix.
 Require Import MatrixHelpers.
 Require Import GateHelpers.
 
diff --git a/Helpers/MatrixHelpers.v b/Helpers/MatrixHelpers.v
index 73e00d6..65deaef 100644
--- a/Helpers/MatrixHelpers.v
+++ b/Helpers/MatrixHelpers.v
@@ -593,6 +593,9 @@ Proof.
   apply Coq.Logic.Classical_Prop.or_to_imply.
 Qed.
 
+Definition Mscale_id {n} (x : C) : Square n :=
+  fun i j => if i =? j then x else 0.
+
 Lemma Mscale_access {m n}: forall (a : C) (B : Matrix m n) (i j : nat),
 a * (B i j) = (a .* B) i j.
 Proof.
diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index 9ecbc8a..f03988c 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -4,23 +4,79 @@ Require Import QuantumLib.Eigenvectors.
 Require Import Coq.Sets.Ensembles.
 Require Import Coq.Logic.Classical_Pred_Type.
 Require Import Coq.Logic.Classical_Prop.
+Require Import DiagonalHelpers.
 
-Lemma perm_eigenvalues : forall {n} (U D D' : Square n),
-  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal D' -> U × D × U† = D' ->
-  exists (σ : nat -> nat),
-    permutation n σ /\ forall (i : nat), D i i = D' (σ i) (σ i).
+(* characteristic polynomial helpers *)
+(* Define a scaled identity matrix *)
+Definition scaled_identity (n : nat) (c : C) : Square n :=
+  fun x y =>
+    if (x =? y) then c else C0.
+
+(* Define the characteristic polynomial using scaled_identity and Mminus *)
+Definition char_poly {n} (A : Square n) (x : C) : C :=
+  Determinant (Mminus (scaled_identity n x) A).
+
+(* Conjugating a matrix with a unitary preserves the characteristic polynomial *)
+Lemma char_poly_similarity : forall {n} (A B U : Square n) x,
+  WF_Unitary U -> U × A × U† = B -> char_poly A x = char_poly B x.
 Proof.
 Admitted.
 
-Lemma char_poly_eigenvalue_perm : forall {n} (D E U : Square n),
-  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E ->
-  U × D × U† = E ->
-  exists (σ : nat -> nat),
-    permutation n σ /\
-    forall (i : nat), (i < n)%nat -> D i i = E (σ i) (σ i).
+Fixpoint prod_f (f : nat -> C) (n : nat) : C :=
+  match n with
+  | 0 => C1 (* The product over an empty range is 1 *)
+  | S n' => (f n') * (prod_f f n') (* Multiply the current value with the rest *)
+  end.
+
+Lemma char_poly_diagonal : forall {n} (D : Square n),
+  WF_Diagonal D -> forall x, char_poly D x = prod_f (fun i => x - D i i) n.
+Proof.
+Admitted.
+
+Lemma poly_roots_perm : forall {n} (f g : nat -> C),
+  (forall x, prod_f (fun i => x - f i) n = prod_f (fun i => x - g i) n) ->
+  exists (σ : nat -> nat), permutation n σ /\ forall (i : nat), f i = g (σ i).
 Proof.
 Admitted.
 
+Lemma perm_eigenvalues : forall {n} (D E U : Square n),
+  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E -> U × D × U† = E ->
+  exists (σ : nat -> nat),
+    permutation n σ /\ forall (i : nat), D i i = E (σ i) (σ i).
+Proof.
+  intros n D E U WF_U WF_D WF_E H_conj.
+  (* assert (H_conj' : U × D × U† = E).
+{ rewrite <- H_conj. reflexivity. } *)
+  (* Step 1: Show that D and E have the same characteristic polynomial. *)
+  assert (Hchar : forall x, char_poly D x = char_poly E x).
+  {
+    intros x.
+    apply (char_poly_similarity D E U x); assumption.
+  }
+  
+  assert (Hprod : forall x : C, prod_f (fun i => x - D i i) n = prod_f (fun i => x - E i i) n).
+  {
+    intros x.
+    rewrite <- (char_poly_diagonal D WF_D x).
+    rewrite <- (char_poly_diagonal E WF_E x).
+    apply Hchar.
+  }
+
+  apply poly_roots_perm in Hprod.
+  destruct Hprod as [σ [Hperm Heq]].
+  exists σ.
+  split. assumption.
+  intros i.
+  apply Heq.
+Qed.
+
+(* Lemma perm_eigenvalues : forall {n} (U D D' : Square n),
+  WF_Unitary U -> WF_Diagonal D -> WF_Diagonal D' -> U × D × U† = D' ->
+  exists (σ : nat -> nat),
+    permutation n σ /\ forall (i : nat), D i i = D' (σ i) (σ i).
+Proof.
+Admitted. *)
+
 (* To equate the eigenvalues of two matrices, we often need equality of matrices
    up to some permutation. This lemma allows us to take the existence of a
    permutation on 4 elements and decompose it into the 24 possible cases. *)

From 0ee9ab7bfb7220d78c01b926f75257e7571ddac9 Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Mon, 13 Jan 2025 16:21:37 -0800
Subject: [PATCH 03/20] prove equality of characteristic polynomials when
 matrix is conjugated with a unitary - Lemma char_poly_similarity: Conjugating
 a matrix with a unitary preserves the characteristic polynomial - Lemma
 scaled_identity_eq_scalar_times_identity: proves that scaled_identity is a
 complex constant times identity - Lemma WF_scaled_identity: shows
 well-formedness of scaled_identity matrices

---
 Helpers/Permutations.v | 153 ++++++++++++++++++++++++++++++++++++++---
 1 file changed, 145 insertions(+), 8 deletions(-)

diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index f03988c..4175c0f 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -5,22 +5,161 @@ Require Import Coq.Sets.Ensembles.
 Require Import Coq.Logic.Classical_Pred_Type.
 Require Import Coq.Logic.Classical_Prop.
 Require Import DiagonalHelpers.
+Require Import WFHelpers.
+Require Import UnitaryHelpers.
+Require Import Classical.
 
-(* characteristic polynomial helpers *)
-(* Define a scaled identity matrix *)
 Definition scaled_identity (n : nat) (c : C) : Square n :=
-  fun x y =>
-    if (x =? y) then c else C0.
+  fun x y => if (x <? n) && (y <? n) 
+             then (if (x =? y) then c else C0)
+             else C0.
 
 (* Define the characteristic polynomial using scaled_identity and Mminus *)
 Definition char_poly {n} (A : Square n) (x : C) : C :=
   Determinant (Mminus (scaled_identity n x) A).
 
+(* Lemma to show that scaled_identity is well-formed *)
+Lemma WF_scaled_identity : forall {n} (c : C), WF_Matrix (scaled_identity n c).
+Proof.
+  intros n c.
+  unfold WF_Matrix, scaled_identity.
+  intros.
+  destruct (x =? y).
+  destruct H.
+  - (* Case x >= n *)
+    assert (Hlt: (x <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    simpl.
+    reflexivity.
+  - (* Case y >= n *)
+    assert (Hlt: (y <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    rewrite andb_false_r.
+    reflexivity.
+  - destruct H.
+    assert (Hlt: (x <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    simpl.
+    reflexivity.
+    assert (Hlt: (y <? n) = false).
+    { apply Nat.ltb_ge. assumption. }
+    rewrite Hlt.
+    rewrite andb_false_r.
+    reflexivity.
+Qed.
+
+(* Lemma to show that scaled_identity is a complex scalar times the identity *)
+Lemma scaled_identity_eq_scalar_times_identity : forall {n} (x : C),
+  scaled_identity n x = x .* (I n).
+Proof.
+  intros n x.
+  unfold scaled_identity, I.
+  prep_matrix_equality.
+  simpl.
+  destruct ((x0 <? n) && (y <? n)) eqn:E1.
+  - (* Case where both indices are in bounds *)
+    destruct (x0 =? y) eqn:E2.
+    + (* Case where x0 = y *)
+      destruct ((x0 =? y) && (x0 <? n)) eqn:E3.
+      * (* Main case: x0 = y and both in bounds *)
+        unfold scale.
+        rewrite E3.
+        lca.
+      * (* Impossible case - we know x0 = y and x0 < n but E3 is false *)
+        apply andb_true_iff in E1. destruct E1 as [Hx0 Hy].
+        apply Nat.eqb_eq in E2. subst.
+        rewrite Hy in E3.
+        rewrite andb_true_r in E3.
+        rewrite Nat.eqb_refl in E3.
+        discriminate.
+    + (* Case where x0 <> y *)
+      destruct ((x0 =? y) && (x0 <? n)) eqn:E3.
+      * (* Impossible case - we know x0 ≠ y but E3 is true *)
+        apply andb_true_iff in E3.
+        destruct E3 as [Hx0 Hy].
+        rewrite E2 in Hx0.
+        discriminate.
+      * (* Case where indices are different *)
+        unfold scale.
+        rewrite E3.
+        lca.
+  - (* Case where at least one index is out of bounds *)
+    destruct ((x0 =? y) && (x0 <? n)) eqn:E2.
+    + (* Impossible case - we know one index is out but E3 is true *)
+      apply andb_true_iff in E2. destruct E2 as [Hx0 Hy].
+      apply andb_false_iff in E1. destruct E1 as [H1 | H2].
+      * rewrite Hy in H1.
+        discriminate.
+      * apply Nat.eqb_eq in Hx0. subst y.
+        rewrite Hy in H2.
+        discriminate.
+    + unfold scale.
+      rewrite E2.
+      lca.
+Qed.
+
 (* Conjugating a matrix with a unitary preserves the characteristic polynomial *)
 Lemma char_poly_similarity : forall {n} (A B U : Square n) x,
   WF_Unitary U -> U × A × U† = B -> char_poly A x = char_poly B x.
 Proof.
-Admitted.
+  intros n A B U x WF_U H_conj.
+  unfold char_poly.
+  assert (H_eq : Mminus(scaled_identity n x) B = 
+                 U × (Mminus (scaled_identity n x) A) × U†).
+{
+  unfold Mminus.
+  (* First show that U × (scaled_identity n x) = (scaled_identity n x) × U *)
+  assert (H_comm : U × (scaled_identity n x) = (scaled_identity n x) × U).
+  {
+    rewrite scaled_identity_eq_scalar_times_identity.
+    rewrite Mscale_mult_dist_r.
+    rewrite Mscale_mult_dist_l.
+    rewrite Mmult_1_r.
+    rewrite Mmult_1_l.
+    reflexivity.
+    solve_WF_matrix.
+    solve_WF_matrix.
+  }
+  (* Now use distributive properties *)
+  rewrite <- H_conj.
+  rewrite Mmult_plus_distr_l.
+  rewrite Mmult_plus_distr_r.
+  rewrite H_comm.
+  rewrite Mmult_assoc.
+  rewrite Mmult_assoc.
+  rewrite other_unitary_decomp.
+  Msimpl.
+  unfold Mopp at 1.
+  rewrite <- Mscale_mult_dist_r.
+  unfold Mopp.
+  rewrite <- Mscale_mult_dist_l.
+  rewrite Mmult_assoc.
+  reflexivity.
+  apply WF_scaled_identity.
+  assumption.
+}
+rewrite H_eq.
+rewrite <- Determinant_multiplicative.
+rewrite <- Determinant_multiplicative.
+rewrite <- Cmult_assoc.
+rewrite <- Cmult_comm.
+rewrite <- Cmult_assoc.
+assert (H_unit1: U × U† = I n) by (apply other_unitary_decomp; auto).
+assert (H_det: Determinant (U × U†) = Determinant (I n)) by (rewrite H_unit1; reflexivity).
+rewrite Determinant_multiplicative.
+assert (H_unit2: U† × U = I n).
+{
+  destruct WF_U as [WF_U unit_U].
+  apply unit_U.
+}
+rewrite H_unit2.
+rewrite Det_I.
+rewrite Cmult_1_r.
+reflexivity.
+Qed.
 
 Fixpoint prod_f (f : nat -> C) (n : nat) : C :=
   match n with
@@ -45,9 +184,7 @@ Lemma perm_eigenvalues : forall {n} (D E U : Square n),
     permutation n σ /\ forall (i : nat), D i i = E (σ i) (σ i).
 Proof.
   intros n D E U WF_U WF_D WF_E H_conj.
-  (* assert (H_conj' : U × D × U† = E).
-{ rewrite <- H_conj. reflexivity. } *)
-  (* Step 1: Show that D and E have the same characteristic polynomial. *)
+  
   assert (Hchar : forall x, char_poly D x = char_poly E x).
   {
     intros x.

From 64679e3cb007e1d0f74d4371d318c052c69a6c3d Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Sun, 19 Jan 2025 21:43:34 -0800
Subject: [PATCH 04/20] Add lemma for determinant of diag4

---
 Helpers/MatrixHelpers.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Helpers/MatrixHelpers.v b/Helpers/MatrixHelpers.v
index 65deaef..71ed94c 100644
--- a/Helpers/MatrixHelpers.v
+++ b/Helpers/MatrixHelpers.v
@@ -82,6 +82,12 @@ Proof.
   unfold diag2, Determinant, big_sum, parity, get_minor; lca.
 Qed.
 
+Lemma Det_diag4 : forall (c1 c2 c3 c4 : C), Determinant (diag4 c1 c2 c3 c4) = c1 * c2 * c3 * c4.
+Proof.
+  intros.
+  unfold diag4, Determinant, big_sum, parity, get_minor; lca.
+Qed.
+
 Lemma row_out_of_bounds: forall {m n} (A : Matrix m n) (i : nat),
   WF_Matrix A -> (i >= m)%nat -> forall (j : nat), A i j = C0.
 Proof.

From bb23b780e5f494df7456c8a09bb9e8d27a5a1b4c Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Sun, 19 Jan 2025 21:47:33 -0800
Subject: [PATCH 05/20] Prove Lemma char_poly_diagonal (Lemma perm_eigenvalues
 2/3) - modify char_poly definition to match math writeup - modify statement
 of perm_eigenvalues

---
 Helpers/Permutations.v | 173 +++++++++++++++++++++++++++++++++++------
 1 file changed, 151 insertions(+), 22 deletions(-)

diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index 4175c0f..835deb4 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -8,6 +8,7 @@ Require Import DiagonalHelpers.
 Require Import WFHelpers.
 Require Import UnitaryHelpers.
 Require Import Classical.
+Require Import MatrixHelpers.
 
 Definition scaled_identity (n : nat) (c : C) : Square n :=
   fun x y => if (x <? n) && (y <? n) 
@@ -16,7 +17,7 @@ Definition scaled_identity (n : nat) (c : C) : Square n :=
 
 (* Define the characteristic polynomial using scaled_identity and Mminus *)
 Definition char_poly {n} (A : Square n) (x : C) : C :=
-  Determinant (Mminus (scaled_identity n x) A).
+  Determinant (Mminus A (scaled_identity n x)).
 
 (* Lemma to show that scaled_identity is well-formed *)
 Lemma WF_scaled_identity : forall {n} (c : C), WF_Matrix (scaled_identity n c).
@@ -107,8 +108,8 @@ Lemma char_poly_similarity : forall {n} (A B U : Square n) x,
 Proof.
   intros n A B U x WF_U H_conj.
   unfold char_poly.
-  assert (H_eq : Mminus(scaled_identity n x) B = 
-                 U × (Mminus (scaled_identity n x) A) × U†).
+  assert (H_eq : Mminus B (scaled_identity n x) = 
+                 U × (Mminus A (scaled_identity n x)) × U†).
 {
   unfold Mminus.
   (* First show that U × (scaled_identity n x) = (scaled_identity n x) × U *)
@@ -127,19 +128,24 @@ Proof.
   rewrite <- H_conj.
   rewrite Mmult_plus_distr_l.
   rewrite Mmult_plus_distr_r.
-  rewrite H_comm.
+  assert (H_comm_mopp: U × Mopp(scaled_identity n x) = Mopp(scaled_identity n x) × U).
+  {
+    unfold Mopp.
+    rewrite Mscale_mult_dist_r.
+    rewrite Mscale_mult_dist_l.
+    rewrite H_comm.
+    reflexivity.
+  }
+  rewrite H_comm_mopp.
   rewrite Mmult_assoc.
   rewrite Mmult_assoc.
   rewrite other_unitary_decomp.
   Msimpl.
-  unfold Mopp at 1.
-  rewrite <- Mscale_mult_dist_r.
-  unfold Mopp.
-  rewrite <- Mscale_mult_dist_l.
-  rewrite Mmult_assoc.
   reflexivity.
-  apply WF_scaled_identity.
-  assumption.
+  - unfold Mopp at 1.
+    apply WF_scale.
+    apply WF_scaled_identity.
+  - solve_WF_matrix.
 }
 rewrite H_eq.
 rewrite <- Determinant_multiplicative.
@@ -167,23 +173,146 @@ Fixpoint prod_f (f : nat -> C) (n : nat) : C :=
   | S n' => (f n') * (prod_f f n') (* Multiply the current value with the rest *)
   end.
 
-Lemma char_poly_diagonal : forall {n} (D : Square n),
-  WF_Diagonal D -> forall x, char_poly D x = prod_f (fun i => x - D i i) n.
+(* Helper lemma: For diagonal matrices, off-diagonal entries are 0 *)
+(* Lemma diagonal_off_diag_zero : forall {n} (D : Square n),
+  WF_Diagonal D -> forall i j, i <> j -> D i j = C0.
 Proof.
-Admitted.
+  intros n D [WF_D D_diag] i j Hij.
+  apply D_diag.
+  assumption.
+Qed.
+
+(* Helper lemma: For diagonal matrices, diagonal entries are well-defined *)
+Lemma diagonal_diag_well_defined : forall {n} (D : Square n),
+  WF_Diagonal D -> forall i, (i < n)%nat -> exists c, D i i = c.
+Proof.
+  intros n D [WF_D D_diag] i Hi.
+  destruct (classic (D i i = C0)).
+  - exists C0. assumption.
+  - exists (D i i). reflexivity.
+Qed. *)
+
+(* Helper lemma: Product of diagonal entries equals determinant *)
+Lemma diagonal_det_prod : forall (D : Square 4),
+  WF_Diagonal D -> Determinant D = prod_f (fun i => D i i) 4.
+Proof.
+  intros D WF_D.
+  unfold prod_f.
+  Csimpl.
+  assert (H: exists c1 c2 c3 c4, D = diag4 c1 c2 c3 c4).
+  {
+    exists (D 0%nat 0%nat), (D 1%nat 1%nat), (D 2%nat 2%nat), (D 3%nat 3%nat).
+    destruct WF_D as [WF_D D_diag].
+    prep_matrix_equality.
+    destruct x, y; try reflexivity.
+    try (apply D_diag; lia).
+    Msimpl.
+    assert (H_neq: (S x) <> 0%nat).
+    { apply Nat.neq_succ_0. }
+    rewrite D_diag by auto.
+    unfold diag4.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    destruct x.
+    reflexivity.
+    reflexivity.
+    destruct x, y.
+    - simpl. unfold diag4. reflexivity.
+    - rewrite D_diag by auto.
+      unfold diag4.
+      reflexivity.
+    - rewrite D_diag by auto.
+      unfold diag4.
+      destruct x.
+      reflexivity.
+      destruct x.
+      reflexivity.
+      reflexivity.
+    - destruct x, y.
+      simpl. unfold diag4. reflexivity.
+      rewrite D_diag by lia.
+      unfold diag4.
+      reflexivity.
+      rewrite D_diag by lia.
+      unfold diag4.
+      destruct x.
+      reflexivity.
+      reflexivity.
+      destruct x, y; simpl.
+      reflexivity.
+      simpl.
+      unfold diag4.
+      rewrite D_diag by lia.
+      reflexivity.
+      unfold diag4.
+      rewrite D_diag by lia.
+      reflexivity.
+      simpl.
+      assert (H_bound: ((S (S (S (S x)))) >= 4)%nat) by lia.
+      rewrite (row_out_of_bounds D _).
+      unfold diag4.
+      reflexivity.
+      assumption.
+      assumption.
+  }
+  destruct H as [c1 [c2 [c3 [c4 D_eq]]]].
+  rewrite D_eq.
+  rewrite Det_diag4.
+  unfold diag4.
+  repeat rewrite Cmult_assoc.
+  lca.
+Qed.
+
+Lemma char_poly_diagonal : forall (D : Square 4),
+  WF_Diagonal D -> forall x, char_poly D x = prod_f (fun i => D i i - x) 4.
+Proof.
+intros D WF_D x.
+unfold char_poly.
+assert (H_diag: WF_Diagonal (Mminus D (scaled_identity 4 x))).
+{
+  rewrite scaled_identity_eq_scalar_times_identity.
+  unfold Mminus.
+  unfold Mopp.
+  unfold WF_Diagonal.
+  split. solve_WF_matrix.
+  destruct WF_D as [WF_D D_diag].
+  intros i j H_neq.
+  rewrite Mplus_access.
+  rewrite D_diag.
+  rewrite Cplus_0_l.
+  rewrite <- Mscale_access.
+  rewrite <- Mscale_access.
+  unfold I.
+  destruct (i =? j) eqn:Eij.
+  - apply Nat.eqb_eq in Eij.
+    contradiction.
+  - simpl.
+    lca.
+  - assumption.
+}
+rewrite (diagonal_det_prod (Mminus D (scaled_identity 4 x))); auto.
+rewrite scaled_identity_eq_scalar_times_identity.
+unfold Mminus.
+unfold Mopp.
+lca.
+Qed.
 
-Lemma poly_roots_perm : forall {n} (f g : nat -> C),
-  (forall x, prod_f (fun i => x - f i) n = prod_f (fun i => x - g i) n) ->
-  exists (σ : nat -> nat), permutation n σ /\ forall (i : nat), f i = g (σ i).
+Lemma poly_roots_perm : forall (f g : nat -> C),
+  (forall x, prod_f (fun i => f i - x) 4 = prod_f (fun i => g i - x) 4) ->
+  exists (σ : nat -> nat), permutation 4 σ /\ forall (i : nat), f i = g (σ i).
 Proof.
-Admitted.
+  Admitted.
 
-Lemma perm_eigenvalues : forall {n} (D E U : Square n),
+Lemma perm_eigenvalues : forall (U D E : Square 4),
   WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E -> U × D × U† = E ->
   exists (σ : nat -> nat),
-    permutation n σ /\ forall (i : nat), D i i = E (σ i) (σ i).
+    permutation 4 σ /\ forall (i : nat), D i i = E (σ i) (σ i).
 Proof.
-  intros n D E U WF_U WF_D WF_E H_conj.
+  intros U D E WF_U WF_D WF_E H_conj.
   
   assert (Hchar : forall x, char_poly D x = char_poly E x).
   {
@@ -191,7 +320,7 @@ Proof.
     apply (char_poly_similarity D E U x); assumption.
   }
   
-  assert (Hprod : forall x : C, prod_f (fun i => x - D i i) n = prod_f (fun i => x - E i i) n).
+  assert (Hprod : forall x : C, prod_f (fun i => D i i - x) 4 = prod_f (fun i => E i i - x) 4).
   {
     intros x.
     rewrite <- (char_poly_diagonal D WF_D x).

From 1837bd0748c61c374dc8f502402398b85a85d080 Mon Sep 17 00:00:00 2001
From: Arsh Malik <51771221+ArshMalik02@users.noreply.github.com>
Date: Sat, 5 Apr 2025 11:07:52 -0700
Subject: [PATCH 06/20] move to using QuantumLib Polynomials

---
 Helpers/Permutations.v      | 22 ++++++++++-
 Helpers/PolynomialHelpers.v | 76 +++++++++++++++++++++++++++++++++++++
 2 files changed, 97 insertions(+), 1 deletion(-)
 create mode 100644 Helpers/PolynomialHelpers.v

diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index 835deb4..b16791d 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -305,7 +305,27 @@ Lemma poly_roots_perm : forall (f g : nat -> C),
   (forall x, prod_f (fun i => f i - x) 4 = prod_f (fun i => g i - x) 4) ->
   exists (σ : nat -> nat), permutation 4 σ /\ forall (i : nat), f i = g (σ i).
 Proof.
-  Admitted.
+  intros f g H_prod.
+  assert (H_exists : forall i, (i < 4)%nat -> exists j, (j < 4)%nat /\ f i = g j).
+  {
+    admit.
+  }
+  (* For each i < 4, get the j that H_exists guarantees *)
+  destruct (H_exists 0%nat) as [j0 [H_j0 H_eq0]]. { auto. }
+  destruct (H_exists 1%nat) as [j1 [H_j1 H_eq1]]. { auto. }
+  destruct (H_exists 2%nat) as [j2 [H_j2 H_eq2]]. { auto. }
+  destruct (H_exists 3%nat) as [j3 [H_j3 H_eq3]]. { auto. }
+
+  (* Define our permutation σ *)
+  exists (fun i => match i with
+                  | 0 => j0
+                  | 1 => j1
+                  | 2 => j2
+                  | 3 => j3
+                  | _ => i
+                  end).
+  split.
+Admitted.
 
 Lemma perm_eigenvalues : forall (U D E : Square 4),
   WF_Unitary U -> WF_Diagonal D -> WF_Diagonal E -> U × D × U† = E ->
diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
new file mode 100644
index 0000000..4bfb97c
--- /dev/null
+++ b/Helpers/PolynomialHelpers.v
@@ -0,0 +1,76 @@
+Require Import QuantumLib.Complex.
+Require Import QuantumLib.Polynomial.
+Require Import QuantumLib.Matrix.
+Require Import QuantumLib.Quantum.
+Require Import QuantumLib.Eigenvectors.
+Require Import MatrixHelpers.
+Require Import DiagonalHelpers.
+Require Import UnitaryHelpers.
+Require Import Permutations.
+
+(* Open the polynomial scope *)
+Local Open Scope poly_scope.
+
+(* Define a notation for polynomial evaluation *)
+Notation "p @ x" := (Peval p x) (at level 10) : poly_scope.
+
+(* Define a function to create a polynomial with a root at a given point *)
+Definition linear_poly (c : C) : Polynomial := [- c; C1].
+
+(* Define a function to create a polynomial (x - c) *)
+Definition x_minus_c (c : C) : Polynomial := linear_poly c.
+
+(* Define a function to create a polynomial (c - x) *)
+Definition c_minus_x (c : C) : Polynomial := [c; -C1].
+
+Lemma Peval_nil : forall c, ([] @ c) = C0.
+Proof. 
+  intros.
+  reflexivity.
+Qed.
+
+(* Lemma to show that (x - c) evaluates to (a - c) at x = a *)
+Lemma x_minus_c_eval : forall (a c : C),
+  (x_minus_c c) @ a = a - c.
+Proof.
+  intros a c.
+  unfold x_minus_c, linear_poly.
+  simpl.
+  repeat rewrite cons_eval.
+  rewrite Peval_nil.
+  lca.
+Qed.
+
+(* Define a function to create a product of (x - c_i) terms *)
+Fixpoint prod_x_minus_c (cs : list C) : Polynomial :=
+  match cs with
+  | [] => [C1]  (* Empty product is 1 *)
+  | c :: cs' => (x_minus_c c) *, (prod_x_minus_c cs')
+  end.
+
+(* Define a function to create a product of (c_i - x) terms *)
+Fixpoint prod_c_minus_x (cs : list C) : Polynomial :=
+  match cs with
+  | [] => [C1]  (* Empty product is 1 *)
+  | c :: cs' => (c_minus_x c) *, (prod_c_minus_x cs')
+  end.
+
+(* Define a big product function for complex numbers *)
+Fixpoint big_prod (f : nat -> C) (n : nat) : C :=
+  match n with
+  | 0 => C1  (* Empty product is 1 *)
+  | S n' => (f n') * (big_prod f n')
+  end.
+
+(* Lemma 1.1 (Euclid's Lemma) *)
+Lemma euclid_lemma : forall (n : nat) (d e : C) (p r : Polynomial),
+  p *, c_minus_x d = r *, c_minus_x e  -> 
+  d = e \/ exists (q : Polynomial), q *, c_minus_x d = r.
+Proof.
+Admitted.
+
+(* Lemma poly_root_in_list : forall (n : nat) (d : C) (e_list : list C),
+  length e_list = n ->
+  (prod_x_minus_c e_list) @ d = C0 ->
+  exists k, nth k e_list C0 = d.
+Admitted. *)

From d22938a8ede17c329dd996cee413216c42df4577 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Sat, 5 Apr 2025 12:05:08 -0700
Subject: [PATCH 07/20] Add tags to gitignore

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.gitignore b/.gitignore
index a96c72e..681f2ed 100644
--- a/.gitignore
+++ b/.gitignore
@@ -35,3 +35,4 @@ nra.cache
 .DS_Store
 CoqMakefile
 CoqMakefile.conf
+tags

From a3af9759ecfe6ca63b550826eb959a10bba2c7ee Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Sat, 5 Apr 2025 12:05:08 -0700
Subject: [PATCH 08/20] Remove Peval notation in favor of library notation

---
 Helpers/PolynomialHelpers.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 4bfb97c..3bdc915 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -11,9 +11,6 @@ Require Import Permutations.
 (* Open the polynomial scope *)
 Local Open Scope poly_scope.
 
-(* Define a notation for polynomial evaluation *)
-Notation "p @ x" := (Peval p x) (at level 10) : poly_scope.
-
 (* Define a function to create a polynomial with a root at a given point *)
 Definition linear_poly (c : C) : Polynomial := [- c; C1].
 
@@ -23,7 +20,7 @@ Definition x_minus_c (c : C) : Polynomial := linear_poly c.
 (* Define a function to create a polynomial (c - x) *)
 Definition c_minus_x (c : C) : Polynomial := [c; -C1].
 
-Lemma Peval_nil : forall c, ([] @ c) = C0.
+Lemma Peval_nil : forall c, ([][[c]]) = C0.
 Proof. 
   intros.
   reflexivity.
@@ -31,7 +28,7 @@ Qed.
 
 (* Lemma to show that (x - c) evaluates to (a - c) at x = a *)
 Lemma x_minus_c_eval : forall (a c : C),
-  (x_minus_c c) @ a = a - c.
+  (x_minus_c c)[[a]] = a - c.
 Proof.
   intros a c.
   unfold x_minus_c, linear_poly.

From b4dba23a3671fef3874ba4de29f1936e9e8a1aee Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Sat, 5 Apr 2025 21:41:02 -0700
Subject: [PATCH 09/20] Prove a version of Euclid's lemma for complex
 polynomials

Must weaken "equals" to "Peq".
---
 Helpers/PolynomialHelpers.v | 43 +++++++++++++++++++++++++++++--------
 1 file changed, 34 insertions(+), 9 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 3bdc915..b243130 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -60,14 +60,39 @@ Fixpoint big_prod (f : nat -> C) (n : nat) : C :=
   end.
 
 (* Lemma 1.1 (Euclid's Lemma) *)
-Lemma euclid_lemma : forall (n : nat) (d e : C) (p r : Polynomial),
-  p *, c_minus_x d = r *, c_minus_x e  -> 
-  d = e \/ exists (q : Polynomial), q *, c_minus_x d = r.
+Lemma euclid_lemma : forall {d e : C} {p r : Polynomial},
+  p *, [d; -C1] ≅ r *, [e; -C1] ->
+  d = e \/ exists (q : Polynomial), q *, [d; -C1] ≅ r.
 Proof.
-Admitted.
+  (* TODO: the polynomial theorem names collide with Coq.PArith *)
 
-(* Lemma poly_root_in_list : forall (n : nat) (d : C) (e_list : list C),
-  length e_list = n ->
-  (prod_x_minus_c e_list) @ d = C0 ->
-  exists k, nth k e_list C0 = d.
-Admitted. *)
+  intros d e p r Heq.
+  destruct (Ceq_dec d e) as [| Hneq]; [auto | right].
+  apply Cminus_eq_contra in Hneq.
+
+  (* construct 1/(d - e) * (r - p) *)
+  exists ([/ (d - e)] *, (r +, -,p)).
+  rewrite Polynomial.Pmult_assoc.
+  rewrite Polynomial.Pmult_plus_distr_r.
+  unfold Popp.
+  rewrite Polynomial.Pmult_assoc, Heq.
+  rewrite <- Polynomial.Pmult_assoc.
+  rewrite (Polynomial.Pmult_comm ([-C1])).
+  rewrite Polynomial.Pmult_assoc.
+  rewrite <- (Polynomial.Pmult_plus_distr_l r).
+  simpl Polynomial.Pplus.
+  replace (d + (((- C1) * e) + 0)) with (d - e) by lca.
+  replace ((- C1) + ((- C1) * (- C1))) with C0 by lca.
+  rewrite (p_Peq_compactify_p [d - e; C0]).
+
+  unfold compactify.
+  simpl prune.
+  destruct (Ceq_dec 0 0); try easy.
+  destruct (Ceq_dec (d - e) 0); try easy.
+  simpl rev.
+
+  rewrite (Polynomial.Pmult_comm r), <- Polynomial.Pmult_assoc.
+  simpl Polynomial.Pmult at 2; rewrite Cplus_0_r.
+  rewrite (Cinv_l _ Hneq).
+  apply Pmult_1_l.
+Qed.

From 7e98af2822944f0cd4c6739a9186103a2721e883 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Thu, 17 Apr 2025 22:06:48 -0700
Subject: [PATCH 10/20] feat: Partially prove Lemma 1.2

It turns out the base case is difficult to prove and may require more
mathematical investigation.
---
 Helpers/PolynomialHelpers.v | 49 +++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index b243130..5b4a61d 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -7,6 +7,7 @@ Require Import MatrixHelpers.
 Require Import DiagonalHelpers.
 Require Import UnitaryHelpers.
 Require Import Permutations.
+Require Import Setoid.
 
 (* Open the polynomial scope *)
 Local Open Scope poly_scope.
@@ -20,6 +21,15 @@ Definition x_minus_c (c : C) : Polynomial := linear_poly c.
 (* Define a function to create a polynomial (c - x) *)
 Definition c_minus_x (c : C) : Polynomial := [c; -C1].
 
+(* A collection of linear factors *)
+Definition Factors := list C.
+
+Fixpoint poly_prod (c : Factors) : Polynomial :=
+  match c with
+  | nil    => [C1]
+  | h :: t => [h; -C1] *, poly_prod t
+  end.
+
 Lemma Peval_nil : forall c, ([][[c]]) = C0.
 Proof. 
   intros.
@@ -96,3 +106,42 @@ Proof.
   rewrite (Cinv_l _ Hneq).
   apply Pmult_1_l.
 Qed.
+
+Lemma poly_isolate_factor : forall (d : C) (facs : list C),
+    facs <> [] ->
+    (forall (p : Polynomial),
+      p *, [d; -C1] ≅ poly_prod facs ->
+      exists (k : nat), nth_error facs k = Some d).
+Proof.
+  intros d facs.
+  induction facs as [| f facs IH]; try contradiction.
+  destruct facs as [| f0 facs].
+  - (* singleton *)
+    intros _ p0 Heq. clear IH.
+    exists 0%nat.
+    simpl in *.
+    repeat rewrite Cplus_0_r in Heq.
+    repeat rewrite Cmult_1_r in Heq.
+    admit.
+  - intros _ p0 Heq.
+    assert (H0 : f0 :: facs <> []) by easy.
+    specialize (IH H0); clear H0.
+    setoid_replace
+      (poly_prod (f :: f0 :: facs)) with
+      ([f; -C1] *, poly_prod (f0 :: facs))
+      using relation Peq in Heq.
+    2: {
+      unfold poly_prod.
+      repeat rewrite <- Polynomial.Pmult_assoc.
+      reflexivity.
+    }
+    unfold poly_prod in *.
+    fold poly_prod in *.
+    rewrite (Polynomial.Pmult_comm [f; -C1]) in Heq.
+    destruct (euclid_lemma Heq) as [ Hdf | [q Hex] ].
+    + exists 0%nat.
+      subst. auto.
+    + destruct (IH q Hex) as [k Hk].
+      exists (S k).
+      auto.
+Admitted.

From 14a402fca744634c3dad0d9ecd0a14dd2bd41d37 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Thu, 24 Apr 2025 13:04:40 -0700
Subject: [PATCH 11/20] Add new Lemma 1.1; Prove 1.1-1.3

The new 1.3 is the old 1.2, we needed another helper lemma.
---
 Helpers/PolynomialHelpers.v | 71 ++++++++++++++++++++++++++++---------
 1 file changed, 55 insertions(+), 16 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 5b4a61d..04a7f15 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -9,6 +9,8 @@ Require Import UnitaryHelpers.
 Require Import Permutations.
 Require Import Setoid.
 
+Module P := Polynomial.
+
 (* Open the polynomial scope *)
 Local Open Scope poly_scope.
 
@@ -69,6 +71,39 @@ Fixpoint big_prod (f : nat -> C) (n : nat) : C :=
   | S n' => (f n') * (big_prod f n')
   end.
 
+Lemma complex_poly_degree : forall (q : Polynomial) (d : C),
+    Peval (q *, [d; -C1]) <> Peval [C1].
+Proof.
+  intros q d Heq'.
+  apply degree_mor in Heq' as Hdeg.
+  assert (Heq : (q *, [d; - C1]) ≅ [C1]) by apply Heq'.
+  unfold degree at 2 in Hdeg.
+  unfold compactify in Hdeg.
+  simpl in Hdeg.
+  destruct (Ceq_dec C1 C0) as [H01 | _]; try (inversion H01; lra).
+  simpl in Hdeg.
+  assert (H_nil_neq_1 : ~ ([] ≅ [C1])).
+  { intro H_nil_1.
+    assert ([][[0]] = [C1][[0]]) by now rewrite H_nil_1.
+    unfold Peval in H; simpl in H.
+    inversion H; lra.}
+  assert (Hq_neq_nil : ~ (q ≅ [])).
+  { intro H_qnil.
+    setoid_rewrite H_qnil in Heq.
+    now simpl in Heq.}
+  assert (Hdx_neq_nil : ~ ([d; - C1] ≅ [])).
+  { intro H_dxnil.
+    setoid_rewrite H_dxnil in Heq.
+    now rewrite P.Pmult_0_r in Heq.}
+  rewrite (Pmult_degree _ _ Hq_neq_nil Hdx_neq_nil) in Hdeg.
+
+  unfold degree at 2 in Hdeg.
+  unfold compactify in Hdeg.
+  simpl in Hdeg.
+  destruct (Ceq_dec (-C1) 0) as [H01 | _]; try (inversion H01; lra).
+  simpl in Hdeg. lia.
+Qed.
+
 (* Lemma 1.1 (Euclid's Lemma) *)
 Lemma euclid_lemma : forall {d e : C} {p r : Polynomial},
   p *, [d; -C1] ≅ r *, [e; -C1] ->
@@ -82,15 +117,15 @@ Proof.
 
   (* construct 1/(d - e) * (r - p) *)
   exists ([/ (d - e)] *, (r +, -,p)).
-  rewrite Polynomial.Pmult_assoc.
-  rewrite Polynomial.Pmult_plus_distr_r.
+  rewrite P.Pmult_assoc.
+  rewrite P.Pmult_plus_distr_r.
   unfold Popp.
-  rewrite Polynomial.Pmult_assoc, Heq.
-  rewrite <- Polynomial.Pmult_assoc.
-  rewrite (Polynomial.Pmult_comm ([-C1])).
-  rewrite Polynomial.Pmult_assoc.
-  rewrite <- (Polynomial.Pmult_plus_distr_l r).
-  simpl Polynomial.Pplus.
+  rewrite P.Pmult_assoc, Heq.
+  rewrite <- P.Pmult_assoc.
+  rewrite (P.Pmult_comm ([-C1])).
+  rewrite P.Pmult_assoc.
+  rewrite <- (P.Pmult_plus_distr_l r).
+  simpl P.Pplus.
   replace (d + (((- C1) * e) + 0)) with (d - e) by lca.
   replace ((- C1) + ((- C1) * (- C1))) with C0 by lca.
   rewrite (p_Peq_compactify_p [d - e; C0]).
@@ -101,8 +136,8 @@ Proof.
   destruct (Ceq_dec (d - e) 0); try easy.
   simpl rev.
 
-  rewrite (Polynomial.Pmult_comm r), <- Polynomial.Pmult_assoc.
-  simpl Polynomial.Pmult at 2; rewrite Cplus_0_r.
+  rewrite (P.Pmult_comm r), <- P.Pmult_assoc.
+  simpl P.Pmult at 2; rewrite Cplus_0_r.
   rewrite (Cinv_l _ Hneq).
   apply Pmult_1_l.
 Qed.
@@ -116,13 +151,18 @@ Proof.
   intros d facs.
   induction facs as [| f facs IH]; try contradiction.
   destruct facs as [| f0 facs].
-  - (* singleton *)
+  - (* singleton list *)
     intros _ p0 Heq. clear IH.
     exists 0%nat.
     simpl in *.
+
     repeat rewrite Cplus_0_r in Heq.
     repeat rewrite Cmult_1_r in Heq.
-    admit.
+
+    rewrite <- (Pmult_1_l [f; -C1]) in Heq.
+    destruct (euclid_lemma Heq) as [ Hdf | [q Hex] ]; try (subst; auto).
+    now apply complex_poly_degree in Hex.
+
   - intros _ p0 Heq.
     assert (H0 : f0 :: facs <> []) by easy.
     specialize (IH H0); clear H0.
@@ -132,16 +172,15 @@ Proof.
       using relation Peq in Heq.
     2: {
       unfold poly_prod.
-      repeat rewrite <- Polynomial.Pmult_assoc.
-      reflexivity.
+      now repeat rewrite <- P.Pmult_assoc.
     }
     unfold poly_prod in *.
     fold poly_prod in *.
-    rewrite (Polynomial.Pmult_comm [f; -C1]) in Heq.
+    rewrite (P.Pmult_comm [f; -C1]) in Heq.
     destruct (euclid_lemma Heq) as [ Hdf | [q Hex] ].
     + exists 0%nat.
       subst. auto.
     + destruct (IH q Hex) as [k Hk].
       exists (S k).
       auto.
-Admitted.
+Qed.

From ff967e8de688041e9813e9229a3cdac39312f8b6 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Fri, 16 May 2025 09:35:25 -0700
Subject: [PATCH 12/20] Remove trailing space

---
 Helpers/Permutations.v      | 2 +-
 Helpers/PolynomialHelpers.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Helpers/Permutations.v b/Helpers/Permutations.v
index b16791d..adf8ec3 100644
--- a/Helpers/Permutations.v
+++ b/Helpers/Permutations.v
@@ -11,7 +11,7 @@ Require Import Classical.
 Require Import MatrixHelpers.
 
 Definition scaled_identity (n : nat) (c : C) : Square n :=
-  fun x y => if (x <? n) && (y <? n) 
+  fun x y => if (x <? n) && (y <? n)
              then (if (x =? y) then c else C0)
              else C0.
 
diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 04a7f15..631adb5 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -33,7 +33,7 @@ Fixpoint poly_prod (c : Factors) : Polynomial :=
   end.
 
 Lemma Peval_nil : forall c, ([][[c]]) = C0.
-Proof. 
+Proof.
   intros.
   reflexivity.
 Qed.

From 4cf1180156cd23d7c44430b2ce5ecb192aa230c9 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Fri, 16 May 2025 09:35:59 -0700
Subject: [PATCH 13/20] Work on Lemma 1.4

---
 Helpers/PolynomialHelpers.v | 142 ++++++++++++++++++++++++++++++++----
 1 file changed, 129 insertions(+), 13 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 631adb5..db60e6c 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -3,6 +3,7 @@ Require Import QuantumLib.Polynomial.
 Require Import QuantumLib.Matrix.
 Require Import QuantumLib.Quantum.
 Require Import QuantumLib.Eigenvectors.
+Require Import QuantumLib.Permutations.
 Require Import MatrixHelpers.
 Require Import DiagonalHelpers.
 Require Import UnitaryHelpers.
@@ -11,6 +12,14 @@ Require Import Setoid.
 
 Module P := Polynomial.
 
+(* Given an assumption H : A -> B, prove A then specialize H with that proof, yielding H : B. *)
+Ltac forward H :=
+  match type of H with
+  | (?A -> ?B) =>
+    let H1 := fresh "H" in
+    assert (H1 : A); [ | specialize (H H1); clear H1]
+  end.
+
 (* Open the polynomial scope *)
 Local Open Scope poly_scope.
 
@@ -72,16 +81,16 @@ Fixpoint big_prod (f : nat -> C) (n : nat) : C :=
   end.
 
 Lemma complex_poly_degree : forall (q : Polynomial) (d : C),
-    Peval (q *, [d; -C1]) <> Peval [C1].
+    Peval ([d; -C1] *, q) <> Peval [C1].
 Proof.
   intros q d Heq'.
   apply degree_mor in Heq' as Hdeg.
-  assert (Heq : (q *, [d; - C1]) ≅ [C1]) by apply Heq'.
+  assert (Heq : ([d; - C1] *, q) ≅ [C1]) by apply Heq'.
   unfold degree at 2 in Hdeg.
   unfold compactify in Hdeg.
-  simpl in Hdeg.
+  simpl length in Hdeg.
   destruct (Ceq_dec C1 C0) as [H01 | _]; try (inversion H01; lra).
-  simpl in Hdeg.
+  simpl rev in Hdeg.
   assert (H_nil_neq_1 : ~ ([] ≅ [C1])).
   { intro H_nil_1.
     assert ([][[0]] = [C1][[0]]) by now rewrite H_nil_1.
@@ -90,14 +99,14 @@ Proof.
   assert (Hq_neq_nil : ~ (q ≅ [])).
   { intro H_qnil.
     setoid_rewrite H_qnil in Heq.
-    now simpl in Heq.}
+    now rewrite P.Pmult_0_r in Heq. }
   assert (Hdx_neq_nil : ~ ([d; - C1] ≅ [])).
   { intro H_dxnil.
     setoid_rewrite H_dxnil in Heq.
-    now rewrite P.Pmult_0_r in Heq.}
-  rewrite (Pmult_degree _ _ Hq_neq_nil Hdx_neq_nil) in Hdeg.
+    now simpl in Heq. }
+  rewrite (Pmult_degree _ _ Hdx_neq_nil Hq_neq_nil) in Hdeg.
 
-  unfold degree at 2 in Hdeg.
+  unfold degree at 1 in Hdeg.
   unfold compactify in Hdeg.
   simpl in Hdeg.
   destruct (Ceq_dec (-C1) 0) as [H01 | _]; try (inversion H01; lra).
@@ -106,8 +115,8 @@ Qed.
 
 (* Lemma 1.1 (Euclid's Lemma) *)
 Lemma euclid_lemma : forall {d e : C} {p r : Polynomial},
-  p *, [d; -C1] ≅ r *, [e; -C1] ->
-  d = e \/ exists (q : Polynomial), q *, [d; -C1] ≅ r.
+  [d; -C1] *, p ≅ r *, [e; -C1] ->
+  d = e \/ exists (q : Polynomial), [d; -C1] *, q ≅ r.
 Proof.
   (* TODO: the polynomial theorem names collide with Coq.PArith *)
 
@@ -117,8 +126,10 @@ Proof.
 
   (* construct 1/(d - e) * (r - p) *)
   exists ([/ (d - e)] *, (r +, -,p)).
+  rewrite P.Pmult_comm.
   rewrite P.Pmult_assoc.
   rewrite P.Pmult_plus_distr_r.
+  rewrite P.Pmult_comm in Heq.
   unfold Popp.
   rewrite P.Pmult_assoc, Heq.
   rewrite <- P.Pmult_assoc.
@@ -145,7 +156,7 @@ Qed.
 Lemma poly_isolate_factor : forall (d : C) (facs : list C),
     facs <> [] ->
     (forall (p : Polynomial),
-      p *, [d; -C1] ≅ poly_prod facs ->
+      [d; -C1] *, p ≅ poly_prod facs ->
       exists (k : nat), nth_error facs k = Some d).
 Proof.
   intros d facs.
@@ -164,8 +175,7 @@ Proof.
     now apply complex_poly_degree in Hex.
 
   - intros _ p0 Heq.
-    assert (H0 : f0 :: facs <> []) by easy.
-    specialize (IH H0); clear H0.
+    forward IH. { easy. }
     setoid_replace
       (poly_prod (f :: f0 :: facs)) with
       ([f; -C1] *, poly_prod (f0 :: facs))
@@ -184,3 +194,109 @@ Proof.
       exists (S k).
       auto.
 Qed.
+
+Lemma singleton_list : forall {T} {l : list T},
+  (length l = 1)%nat -> exists x, l = [x].
+Proof.
+  intros.
+  destruct l; try inversion H.
+  destruct l; try inversion H1.
+
+  now exists t.
+Qed.
+
+Lemma poly_prod_middle : forall (l1 l2 : Factors) (f : C), poly_prod (l1 ++ f :: l2) ≅ poly_prod (f :: l1 ++ l2).
+Proof.
+  intro l1.
+  induction l1; try reflexivity.
+  intros l2 f.
+  simpl app.
+  unfold poly_prod.
+  fold poly_prod.
+  rewrite IHl1.
+  unfold poly_prod.
+  fold poly_prod.
+  rewrite <- P.Pmult_assoc.
+  rewrite <- P.Pmult_assoc.
+  now rewrite (P.Pmult_comm [a; -C1] [f; -C1]).
+Qed.
+
+Lemma roots_equal_implies_permutation :
+  forall (n : nat),
+  (n > 0)%nat ->
+  forall (ds es: list C),
+  length ds = n -> length es = n ->
+  (poly_prod ds ≅ poly_prod es) ->
+  exists f, permutation n f /\ (forall i, ds !! i = es !! f i).
+Proof.
+  intros n.
+  induction n; try lia.
+  (* intros. *)
+  intros H ds es Hdlen Helen Hpeq.
+  destruct n as [| n].
+  - exists idn.
+    split.
+    + (* Permutation *)
+      apply idn_permutation.
+    + (* perm_pair_eq *)
+      destruct (singleton_list Hdlen) as [delem Hd].
+      destruct (singleton_list Helen) as [eelem He].
+      subst.
+      destruct i.
+      -- unfold poly_prod in Hpeq.
+         simpl; f_equal.
+         simpl in Hpeq.
+         apply Peq_head_eq in Hpeq.
+        (* Done, just dont wanna do manual math *)
+        admit.
+      -- easy.
+  - clear H.
+    forward IHn. { lia. }
+    destruct ds as [| d ds]; try easy.
+    assert (Heneqnil : es <> []).
+    { intro Hcontra.
+      subst. easy. }
+    destruct (poly_isolate_factor d es Heneqnil (poly_prod ds) Hpeq) as [k Hk].
+    clear Heneqnil.
+
+    (* break 'es' into multiple pieces *)
+    destruct (nth_error_split es k Hk) as [e1 [e2 [Hcombine Hidx] ] ].
+    rewrite Hcombine in Hpeq.
+
+    rewrite poly_prod_middle in Hpeq.
+    unfold poly_prod in Hpeq. fold poly_prod in Hpeq.
+
+    specialize (IHn ds (e1 ++ e2)).
+    forward IHn. { auto. }
+    forward IHn.
+    { rewrite Hcombine in Helen.
+      rewrite app_length in *.
+      simpl in Helen.
+      lia. }
+
+    (* We need rcancel_mul for polynomials *)
+    assert (Hpeq' : poly_prod ds ≅ poly_prod (e1 ++ e2)). { admit. }
+    clear Hpeq.
+    forward IHn. { easy. }
+    destruct IHn as [f [Hperm Hpermeq] ].
+
+    exists (fun i =>
+              if i =? 0 then k else
+                let i' := f i in
+                if k <=? i' then i'
+                  else (i' + 1)%nat).
+
+    (* need inverse of f0 *)
+    split. { admit. }
+
+    unfold permutation.
+    intros i.
+    destruct i as [| i']; try auto.
+    subst.
+    simpl.
+    rewrite Hpermeq.
+    bdestruct (length e1 <=? f (S i'))%nat.
+    + Search lt.
+    Search nth_error.
+    Check nth_error_app1.
+    rewrite (nth_error_app2 e1 (d :: e2) H).

From 860753c461815c33246d1f93ac7e52755f31e4be Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Fri, 16 May 2025 10:26:54 -0700
Subject: [PATCH 14/20] Prove main Lemma 1.4

There are still small unproved subgoals
---
 Helpers/PolynomialHelpers.v | 44 +++++++++++++++++++++++--------------
 1 file changed, 28 insertions(+), 16 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index db60e6c..8531d90 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -243,13 +243,15 @@ Proof.
       destruct (singleton_list Helen) as [eelem He].
       subst.
       destruct i.
-      -- unfold poly_prod in Hpeq.
-         simpl; f_equal.
-         simpl in Hpeq.
-         apply Peq_head_eq in Hpeq.
-        (* Done, just dont wanna do manual math *)
-        admit.
-      -- easy.
+      * unfold poly_prod in Hpeq.
+        simpl; f_equal.
+        simpl in Hpeq.
+        apply Peq_head_eq in Hpeq.
+        (* Why can't we use lca here? *)
+        repeat rewrite Cplus_0_r in Hpeq.
+        repeat rewrite Cmult_1_r in Hpeq.
+        auto.
+      * easy.
   - clear H.
     forward IHn. { lia. }
     destruct ds as [| d ds]; try easy.
@@ -281,10 +283,12 @@ Proof.
     destruct IHn as [f [Hperm Hpermeq] ].
 
     exists (fun i =>
-              if i =? 0 then k else
-                let i' := f i in
-                if k <=? i' then i'
-                  else (i' + 1)%nat).
+              match i with
+              | 0 => k
+              | S i' =>
+                  let j := f i' in
+                  if j <? k then j else S j
+              end).
 
     (* need inverse of f0 *)
     split. { admit. }
@@ -295,8 +299,16 @@ Proof.
     subst.
     simpl.
     rewrite Hpermeq.
-    bdestruct (length e1 <=? f (S i'))%nat.
-    + Search lt.
-    Search nth_error.
-    Check nth_error_app1.
-    rewrite (nth_error_app2 e1 (d :: e2) H).
+    bdestruct (f i' <? length e1)%nat.
+    + do 2 rewrite (nth_error_app1 _ _ H); reflexivity.
+    + replace (e1 ++ d :: e2) with ((e1 ++ [d]) ++ e2)
+        by ( rewrite <- app_assoc; auto ).
+      assert (Hsecond : (length (e1 ++ [d]) <= S (f i'))%nat).
+      { rewrite app_length. simpl. lia. }
+      rewrite (nth_error_app2 _ _ H).
+      rewrite (nth_error_app2 _ _ Hsecond).
+      rewrite app_length.
+      simpl length.
+      rewrite Nat.add_1_r.
+      auto.
+Admitted.

From 5a827cb262180d3aff37676c88a7b9cd033e41fb Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Tue, 27 May 2025 17:45:33 -0700
Subject: [PATCH 15/20] Lemma 1.4: proven except for Poly left cancel

---
 Helpers/PolynomialHelpers.v | 114 ++++++++++++++++++++++++++----------
 1 file changed, 82 insertions(+), 32 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 8531d90..1b3dc3c 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -12,14 +12,6 @@ Require Import Setoid.
 
 Module P := Polynomial.
 
-(* Given an assumption H : A -> B, prove A then specialize H with that proof, yielding H : B. *)
-Ltac forward H :=
-  match type of H with
-  | (?A -> ?B) =>
-    let H1 := fresh "H" in
-    assert (H1 : A); [ | specialize (H H1); clear H1]
-  end.
-
 (* Open the polynomial scope *)
 Local Open Scope poly_scope.
 
@@ -95,7 +87,7 @@ Proof.
   { intro H_nil_1.
     assert ([][[0]] = [C1][[0]]) by now rewrite H_nil_1.
     unfold Peval in H; simpl in H.
-    inversion H; lra.}
+    inversion H; lra. }
   assert (Hq_neq_nil : ~ (q ≅ [])).
   { intro H_qnil.
     setoid_rewrite H_qnil in Heq.
@@ -175,7 +167,7 @@ Proof.
     now apply complex_poly_degree in Hex.
 
   - intros _ p0 Heq.
-    forward IH. { easy. }
+    specialize (IH ltac:(easy)).
     setoid_replace
       (poly_prod (f :: f0 :: facs)) with
       ([f; -C1] *, poly_prod (f0 :: facs))
@@ -211,16 +203,23 @@ Proof.
   induction l1; try reflexivity.
   intros l2 f.
   simpl app.
-  unfold poly_prod.
-  fold poly_prod.
+  unfold poly_prod; fold poly_prod.
   rewrite IHl1.
-  unfold poly_prod.
-  fold poly_prod.
-  rewrite <- P.Pmult_assoc.
-  rewrite <- P.Pmult_assoc.
+  unfold poly_prod; fold poly_prod.
+  do 2 rewrite <- P.Pmult_assoc.
   now rewrite (P.Pmult_comm [a; -C1] [f; -C1]).
 Qed.
 
+Lemma Pfac_cancel_l : forall (d : C) (p1 p2 : Polynomial),
+    [d; -C1] *, p1 ≅ [d; -C1] *, p2 -> p1 ≅ p2.
+Proof.
+  intros d p1 p2 Hnil.
+  apply functional_extensionality; intros x.
+  unfold Peq in Hnil.
+  simpl in Hnil.
+  admit.
+Admitted.
+
 Lemma roots_equal_implies_permutation :
   forall (n : nat),
   (n > 0)%nat ->
@@ -252,13 +251,17 @@ Proof.
         repeat rewrite Cmult_1_r in Hpeq.
         auto.
       * easy.
-  - clear H.
-    forward IHn. { lia. }
+  - remember (S n) as N. clear H.
+    specialize (IHn ltac:(lia)).
     destruct ds as [| d ds]; try easy.
     assert (Heneqnil : es <> []).
     { intro Hcontra.
       subst. easy. }
     destruct (poly_isolate_factor d es Heneqnil (poly_prod ds) Hpeq) as [k Hk].
+    assert (Hk_le_n : (k < S N)%nat).
+    { rewrite <- Helen.
+      rewrite <- nth_error_Some.
+      now rewrite Hk. }
     clear Heneqnil.
 
     (* break 'es' into multiple pieces *)
@@ -268,30 +271,77 @@ Proof.
     rewrite poly_prod_middle in Hpeq.
     unfold poly_prod in Hpeq. fold poly_prod in Hpeq.
 
-    specialize (IHn ds (e1 ++ e2)).
-    forward IHn. { auto. }
-    forward IHn.
-    { rewrite Hcombine in Helen.
+    assert (Hleneq : length (e1 ++ e2) = N).
+    { subst.
       rewrite app_length in *.
-      simpl in Helen.
+      simpl in *.
       lia. }
 
+    specialize (IHn ds (e1 ++ e2) ltac:(auto) Hleneq).
     (* We need rcancel_mul for polynomials *)
-    assert (Hpeq' : poly_prod ds ≅ poly_prod (e1 ++ e2)). { admit. }
+    assert (Hpeq' : poly_prod ds ≅ poly_prod (e1 ++ e2)).
+    {
+      admit.
+    }
     clear Hpeq.
-    forward IHn. { easy. }
-    destruct IHn as [f [Hperm Hpermeq] ].
+    destruct (IHn ltac:(easy)) as [f' [Hperm Hpermeq] ].
 
-    exists (fun i =>
+    pose (f := fun i =>
               match i with
               | 0 => k
               | S i' =>
-                  let j := f i' in
+                  let j := f' i' in
                   if j <? k then j else S j
               end).
 
-    (* need inverse of f0 *)
-    split. { admit. }
+    exists f.
+
+    split.
+    { destruct Hperm as [f'inv Hf'inv].
+
+      pose (finv := fun j =>
+                if j =? k then 0%nat else
+                  if j <? k then S (f'inv j)
+                  else S (f'inv (pred j))).
+      exists finv.
+      intros x Hx.
+      repeat split.
+      - (* f x < S (S n) *)
+        destruct x.
+        + unfold f. subst.
+          rewrite app_length in Helen.
+          simpl in Helen.
+          lia.
+        + specialize (Hf'inv x ltac:(lia)).
+          simpl. destruct (f' x <? k) eqn:E; lia.
+      - (* finv x < S (S n) *)
+        unfold finv.
+        bdestruct_all; try (rewrite <- Nat.succ_lt_mono).
+        + (* k <= N *)
+          now destruct (Hf'inv x ltac:(lia)).
+        + lia.
+        + (* f'inv (pred x) < N *)
+          destruct x; simpl.
+          * now destruct (Hf'inv 0%nat ltac:(lia)).
+          * now destruct (Hf'inv x ltac:(lia)).
+      - (* finv (f x) = x *)
+        unfold finv, f.
+        destruct x.
+        + (* x = 0 *)
+          simpl.
+          bdestruct (k =? k); [ lia | easy ].
+        + bdestruct_all; simpl; destruct (Hf'inv x ltac:(lia)); lia.
+      - (* f (finv x) = x *)
+        unfold finv, f.
+        destruct x.
+        + bdestruct_all; try (destruct (Hf'inv 0%nat ltac:(lia))); lia.
+        + bdestruct_all.
+          * destruct (Hf'inv (S x) ltac:(lia)). lia.
+          * destruct (Hf'inv (S x) ltac:(lia)). lia.
+          * auto.
+          * simpl in *. destruct (Hf'inv x ltac:(lia)). lia.
+          * destruct (Hf'inv x ltac:(lia)). simpl. lia.
+    }
 
     unfold permutation.
     intros i.
@@ -299,11 +349,11 @@ Proof.
     subst.
     simpl.
     rewrite Hpermeq.
-    bdestruct (f i' <? length e1)%nat.
+    bdestruct (f' i' <? length e1)%nat.
     + do 2 rewrite (nth_error_app1 _ _ H); reflexivity.
     + replace (e1 ++ d :: e2) with ((e1 ++ [d]) ++ e2)
         by ( rewrite <- app_assoc; auto ).
-      assert (Hsecond : (length (e1 ++ [d]) <= S (f i'))%nat).
+      assert (Hsecond : (length (e1 ++ [d]) <= S (f' i'))%nat).
       { rewrite app_length. simpl. lia. }
       rewrite (nth_error_app2 _ _ H).
       rewrite (nth_error_app2 _ _ Hsecond).

From 2bd61a655820d1a803aa75f978544256326c0bc6 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Thu, 29 May 2025 11:42:07 -0700
Subject: [PATCH 16/20] Remove unused definitions

---
 Helpers/PolynomialHelpers.v | 39 -------------------------------------
 1 file changed, 39 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 1b3dc3c..c621958 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -33,45 +33,6 @@ Fixpoint poly_prod (c : Factors) : Polynomial :=
   | h :: t => [h; -C1] *, poly_prod t
   end.
 
-Lemma Peval_nil : forall c, ([][[c]]) = C0.
-Proof.
-  intros.
-  reflexivity.
-Qed.
-
-(* Lemma to show that (x - c) evaluates to (a - c) at x = a *)
-Lemma x_minus_c_eval : forall (a c : C),
-  (x_minus_c c)[[a]] = a - c.
-Proof.
-  intros a c.
-  unfold x_minus_c, linear_poly.
-  simpl.
-  repeat rewrite cons_eval.
-  rewrite Peval_nil.
-  lca.
-Qed.
-
-(* Define a function to create a product of (x - c_i) terms *)
-Fixpoint prod_x_minus_c (cs : list C) : Polynomial :=
-  match cs with
-  | [] => [C1]  (* Empty product is 1 *)
-  | c :: cs' => (x_minus_c c) *, (prod_x_minus_c cs')
-  end.
-
-(* Define a function to create a product of (c_i - x) terms *)
-Fixpoint prod_c_minus_x (cs : list C) : Polynomial :=
-  match cs with
-  | [] => [C1]  (* Empty product is 1 *)
-  | c :: cs' => (c_minus_x c) *, (prod_c_minus_x cs')
-  end.
-
-(* Define a big product function for complex numbers *)
-Fixpoint big_prod (f : nat -> C) (n : nat) : C :=
-  match n with
-  | 0 => C1  (* Empty product is 1 *)
-  | S n' => (f n') * (big_prod f n')
-  end.
-
 Lemma complex_poly_degree : forall (q : Polynomial) (d : C),
     Peval ([d; -C1] *, q) <> Peval [C1].
 Proof.

From 17212f4a9960437878e2d03ab56a4b92e32b8b25 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Thu, 29 May 2025 11:42:26 -0700
Subject: [PATCH 17/20] Formatting

---
 Helpers/PolynomialHelpers.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index c621958..b303d75 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -33,6 +33,7 @@ Fixpoint poly_prod (c : Factors) : Polynomial :=
   | h :: t => [h; -C1] *, poly_prod t
   end.
 
+(* Lemma 1.1 *)
 Lemma complex_poly_degree : forall (q : Polynomial) (d : C),
     Peval ([d; -C1] *, q) <> Peval [C1].
 Proof.
@@ -66,7 +67,7 @@ Proof.
   simpl in Hdeg. lia.
 Qed.
 
-(* Lemma 1.1 (Euclid's Lemma) *)
+(* Lemma 1.2 (Euclid's Lemma) *)
 Lemma euclid_lemma : forall {d e : C} {p r : Polynomial},
   [d; -C1] *, p ≅ r *, [e; -C1] ->
   d = e \/ exists (q : Polynomial), [d; -C1] *, q ≅ r.
@@ -106,6 +107,7 @@ Proof.
   apply Pmult_1_l.
 Qed.
 
+(* Lemma 1.3 *)
 Lemma poly_isolate_factor : forall (d : C) (facs : list C),
     facs <> [] ->
     (forall (p : Polynomial),
@@ -154,7 +156,6 @@ Proof.
   intros.
   destruct l; try inversion H.
   destruct l; try inversion H1.
-
   now exists t.
 Qed.
 
@@ -171,6 +172,7 @@ Proof.
   now rewrite (P.Pmult_comm [a; -C1] [f; -C1]).
 Qed.
 
+(* Lemma 1.4 *)
 Lemma Pfac_cancel_l : forall (d : C) (p1 p2 : Polynomial),
     [d; -C1] *, p1 ≅ [d; -C1] *, p2 -> p1 ≅ p2.
 Proof.
@@ -181,6 +183,7 @@ Proof.
   admit.
 Admitted.
 
+(* Lemma 1.5 *)
 Lemma roots_equal_implies_permutation :
   forall (n : nat),
   (n > 0)%nat ->

From 1c66e5c6814b1ef8081e856b23824b0916e978f8 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Thu, 29 May 2025 11:42:42 -0700
Subject: [PATCH 18/20] Move "Admitted" to helper lemma

---
 Helpers/PolynomialHelpers.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index b303d75..9824b38 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -242,12 +242,11 @@ Proof.
       lia. }
 
     specialize (IHn ds (e1 ++ e2) ltac:(auto) Hleneq).
-    (* We need rcancel_mul for polynomials *)
+
     assert (Hpeq' : poly_prod ds ≅ poly_prod (e1 ++ e2)).
-    {
-      admit.
-    }
+    { now apply Pfac_cancel_l in Hpeq. }
     clear Hpeq.
+
     destruct (IHn ltac:(easy)) as [f' [Hperm Hpermeq] ].
 
     pose (f := fun i =>
@@ -325,4 +324,4 @@ Proof.
       simpl length.
       rewrite Nat.add_1_r.
       auto.
-Admitted.
+Qed.

From 6f032bb00a9008bedc65f9a2ebf6d42678651c91 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Tue, 3 Jun 2025 15:49:55 -0700
Subject: [PATCH 19/20] Prove Lemma 1.4

---
 Helpers/PolynomialHelpers.v | 32 +++++++++++++++++++++++++++-----
 1 file changed, 27 insertions(+), 5 deletions(-)

diff --git a/Helpers/PolynomialHelpers.v b/Helpers/PolynomialHelpers.v
index 9824b38..64873c7 100644
--- a/Helpers/PolynomialHelpers.v
+++ b/Helpers/PolynomialHelpers.v
@@ -172,16 +172,38 @@ Proof.
   now rewrite (P.Pmult_comm [a; -C1] [f; -C1]).
 Qed.
 
+Lemma Pmult_0_factor : forall (p1 p2 : Polynomial),
+  (p1 *, p2) ≅ [] -> p1 ≅ [] \/ p2 ≅ [].
+Proof.
+  intros p1 p2 H.
+  destruct (Peq_0_dec p1), (Peq_0_dec p2); try auto.
+  destruct (Pmult_neq_0 _ _ n n0); auto.
+Qed.
+
 (* Lemma 1.4 *)
 Lemma Pfac_cancel_l : forall (d : C) (p1 p2 : Polynomial),
     [d; -C1] *, p1 ≅ [d; -C1] *, p2 -> p1 ≅ p2.
 Proof.
   intros d p1 p2 Hnil.
-  apply functional_extensionality; intros x.
-  unfold Peq in Hnil.
-  simpl in Hnil.
-  admit.
-Admitted.
+  pose proof (H := Pplus_mor _ _ Hnil ([d; -C1] *, -, p2) _ ltac:(reflexivity)).
+  rewrite <- P.Pmult_plus_distr_l in H.
+  unfold Popp in H.
+  rewrite <- P.Pmult_assoc in H.
+  rewrite (P.Pmult_comm [d; -C1] [- C1]) in H.
+  rewrite P.Pmult_assoc in H.
+  rewrite Pplus_opp_r in H.
+  destruct (Pmult_0_factor _ _ H).
+  - apply degree_mor in H0. unfold degree in H0.
+    unfold compactify in H0.
+    simpl in H0.
+    destruct (Ceq_dec (-C1) 0%R) as [H01 | _]; try (inversion H01; lra).
+    simpl in H0. lia.
+  - pose proof (H' := Pplus_mor _ _ H0 p2  _ ltac:(reflexivity)).
+    rewrite P.Pplus_assoc in H'.
+    setoid_replace ([-C1] *, p2 +, p2) with
+      ([] : Polynomial) in H' by now rewrite Pplus_opp_l.
+    simpl in H'. now rewrite P.Pplus_0_r in H'.
+Qed.
 
 (* Lemma 1.5 *)
 Lemma roots_equal_implies_permutation :

From 98b9cc3a422d2dedcfdccaf8f49e11c7cc963210 Mon Sep 17 00:00:00 2001
From: Michael Lan <michaellan202@gmail.com>
Date: Tue, 3 Jun 2025 17:16:51 -0700
Subject: [PATCH 20/20] CI: Bump QuantumLib to 1.6.0

---
 flake.nix | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/flake.nix b/flake.nix
index e3b1128..347bfb3 100644
--- a/flake.nix
+++ b/flake.nix
@@ -15,7 +15,7 @@
       system = "x86_64-linux";
       pkgs = nixpkgs.legacyPackages.${system};
       pkgs-unstable = nixpkgs-unstable.legacyPackages.${system};
-      coq-quantumlib-version = "v1.4.0";
+      coq-quantumlib-version = "v1.6.0";
     in
     let
       coq-quantumlib = pkgs.coqPackages.mkCoqDerivation {
@@ -25,8 +25,8 @@
 
         defaultVersion = coq-quantumlib-version;
         release.${coq-quantumlib-version} = {
-          rev = "80018571961e13968bfd80ea9cb061d9469b0817";
-          sha256 = "sha256-mx74GxIwF6mgmrELmNl0l3GiBBf/WrpouHfszylhTYQ=";
+          rev = "5e0e4da5e64fcf9b4390a274748079ed270c1965";
+          sha256 = "sha256-eKKYWUj6zDh48J5mahOr+HwWULgfn3K/3TY3oFhhYJA=";
         };
         useDune = true;
       };