diff --git a/.gitignore b/.gitignore index 810c196..90e8e55 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +<<<<<<< HEAD *.glob *.aux *~ @@ -13,3 +14,38 @@ extra/* .coqdeps.d CoqMakefile CoqMakefile.conf +======= +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.coq-native/ +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache +>>>>>>> QuantumLib/main diff --git a/Complex.v b/Complex.v index 59cd59f..40e3269 100644 --- a/Complex.v +++ b/Complex.v @@ -86,6 +86,11 @@ Notation "/ x" := (Cinv x) : C_scope. Infix "/" := Cdiv : C_scope. +<<<<<<< HEAD +======= + + +>>>>>>> QuantumLib/main (* Added exponentiation *) Fixpoint Cpow (c : C) (n : nat) : C := match n with @@ -206,6 +211,24 @@ Proof. apply Rsqr_le_abs_1 in H0 ; unfold pow; rewrite !Rmult_1_r; auto. Qed. +<<<<<<< HEAD +======= +(* some lemmas to help simplify addition/multiplication scenarios *) +Lemma Cplus_simplify : forall (a b c d : C), + a = b -> c = d -> (a + c = b + d)%C. +Proof. intros. + rewrite H, H0; easy. +Qed. + + +Lemma Cmult_simplify : forall (a b c d : C), + a = b -> c = d -> (a * c = b * d)%C. +Proof. intros. + rewrite H, H0; easy. +Qed. + + +>>>>>>> QuantumLib/main (** ** C is a field *) Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y. @@ -304,11 +327,16 @@ Proof. apply injective_projections ; simpl ; ring. Qed. +<<<<<<< HEAD <<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + + +>>>>>>> QuantumLib/main (* I'll be leaving out mixins and Canonical Structures : Definition C_AbelianGroup_mixin := AbelianGroup.Mixin _ _ _ _ Cplus_comm Cplus_assoc Cplus_0_r Cplus_opp_r. @@ -470,6 +498,7 @@ Proof. intros c. intros N E. apply N. rewrite E. reflexivity. Qed. Lemma RtoC_neq : forall (r : R), r <> 0 -> RtoC r <> 0. Proof. intros. apply C0_fst_neq. easy. Qed. +<<<<<<< HEAD <<<<<<< HEAD Lemma Copp_neq_0_compat: forall c : C, c <> 0 -> (- c)%C <> 0. Proof. @@ -484,6 +513,8 @@ Proof. Qed. ======= +======= +>>>>>>> QuantumLib/main Lemma C1_neq_C0 : C1 <> C0. Proof. apply C0_fst_neq. simpl. @@ -521,7 +552,10 @@ Proof. intros. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2. Proof. intros. @@ -631,6 +665,15 @@ Proof. lra. Qed. +<<<<<<< HEAD +======= +Lemma Cconj_simplify : forall (c1 c2 : C), c1^* = c2^* -> c1 = c2. +Proof. intros. + assert (H1 : c1 ^* ^* = c2 ^* ^*). { rewrite H; easy. } + do 2 rewrite Cconj_involutive in H1. + easy. +Qed. +>>>>>>> QuantumLib/main (******************) (** Square Roots **) @@ -728,6 +771,7 @@ Proof. field. Qed. +<<<<<<< HEAD <<<<<<< HEAD Lemma Cexp_plus_PI : forall x, Cexp (x + PI) = (- (Cexp x))%C. @@ -753,6 +797,8 @@ Qed. ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma Cexp_nonzero : forall θ, Cexp θ <> 0. Proof. intro θ. unfold Cexp. @@ -987,11 +1033,15 @@ Qed. Hint Rewrite Cexp_0 Cexp_PI Cexp_PI2 Cexp_2PI Cexp_3PI2 Cexp_PI4 Cexp_PIm4 Cexp_1PI4 Cexp_2PI4 Cexp_3PI4 Cexp_4PI4 Cexp_5PI4 Cexp_6PI4 Cexp_7PI4 Cexp_8PI4 +<<<<<<< HEAD <<<<<<< HEAD Cexp_add Cexp_neg Cexp_plus_PI Cexp_minus_PI : Cexp_db. ======= Cexp_add Cexp_neg : Cexp_db. >>>>>>> Heisenberg-Foundations/main +======= + Cexp_add Cexp_neg : Cexp_db. +>>>>>>> QuantumLib/main Opaque C. @@ -1005,6 +1055,7 @@ Lemma Cdiv_unfold : forall c1 c2, (c1 / c2 = c1 */ c2)%C. Proof. reflexivity. Qe (* For proving goals of the form x <> 0 or 0 < x *) Ltac nonzero := repeat split; +<<<<<<< HEAD <<<<<<< HEAD repeat match goal with @@ -1015,13 +1066,18 @@ Ltac nonzero := | |- not (@eq _ _ (RtoC (IZR Z0))) => apply RtoC_neq end; ======= +======= +>>>>>>> QuantumLib/main try match goal with | |- not (@eq _ _ (RtoC (IZR Z0))) => apply RtoC_neq | |- not (@eq _ (Cpow _ _) (RtoC (IZR Z0))) => apply Cpow_nonzero; try apply RtoC_neq | |- not (@eq _ Ci (RtoC (IZR Z0))) => apply C0_snd_neq; simpl | |- not (@eq _ (Cexp _) (RtoC (IZR Z0))) => apply Cexp_nonzero end; +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main repeat match goal with | |- not (@eq _ (sqrt (pow _ _)) (IZR Z0)) => rewrite sqrt_pow @@ -1035,6 +1091,7 @@ Ltac nonzero := | |- Rlt (IZR Z0) (Rmult _ _) => apply Rmult_lt_0_compat | |- Rlt (IZR Z0) (Rinv _) => apply Rinv_0_lt_compat | |- Rlt (IZR Z0) (pow _ _) => apply pow_lt +<<<<<<< HEAD <<<<<<< HEAD end; match goal with @@ -1043,12 +1100,17 @@ Ltac nonzero := | |- Rle _ _ => lra end. ======= +======= +>>>>>>> QuantumLib/main end; match goal with | |- not (@eq _ _ _) => lra | |- Rlt _ _ => lra | |- Rle _ _ => lra end. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Hint Rewrite Cminus_unfold Cdiv_unfold Ci2 Cconj_R Cconj_opp Cconj_rad2 Cinv_sqrt2_sqrt Cplus_div2 @@ -1069,12 +1131,15 @@ Hint Rewrite Cplus_0_l Cplus_0_r Cmult_0_l Cmult_0_r Copp_0 Hint Rewrite Cmult_plus_distr_l Cmult_plus_distr_r Copp_plus_distr Copp_mult_distr_l Copp_involutive : Cdist_db. +<<<<<<< HEAD <<<<<<< HEAD Hint Rewrite <- RtoC_opp RtoC_mult RtoC_plus : RtoC_db. Hint Rewrite <- RtoC_inv using nonzero : RtoC_db. Hint Rewrite RtoC_pow : RtoC_db. ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Ltac Csimpl := repeat match goal with diff --git a/Eigenvectors.v b/Eigenvectors.v index 190d3f8..c33edc2 100644 --- a/Eigenvectors.v +++ b/Eigenvectors.v @@ -1,3 +1,4 @@ +<<<<<<< HEAD Require Import List. Require Export Complex. Require Export Matrix. @@ -460,6 +461,20 @@ Qed. Hint Resolve WF_Phase WF_Phase' WF_Tgate WF_notc WF_ket WF_bra : wf_db. (* ran into problems with hadamard. Can probably make this more general. *) +======= +Require Import List. +Require Export Complex. +Require Export Quantum. +Require Export Polynomial. + + + +(****************************) +(* Proving some indentities *) +(****************************) + +(* little Ltac for helping with √ 2 *) +>>>>>>> QuantumLib/main Ltac Hhelper := unfold Mmult; unfold Csum; @@ -469,6 +484,7 @@ Ltac Hhelper := try lca; C_field. +<<<<<<< HEAD Lemma big_kron_app : forall {n m} (l1 l2 : list (Matrix n m)), (forall i, WF_Matrix (nth i l1 (@Zero n m))) -> @@ -502,6 +518,13 @@ Lemma H_eq_Hadjoint : hadamard† = hadamard. Proof. lma'. Qed. Hint Rewrite Y_eq_iXZ PEqP' H_eq_Hadjoint : id_db. +======= +Lemma Y_eq_iXZ : σy = Ci .* σx × σz. Proof. lma'. Qed. +Lemma H_eq_Hadjoint : hadamard† = hadamard. Proof. lma'. Qed. + + +Hint Rewrite Y_eq_iXZ H_eq_Hadjoint : id_db. +>>>>>>> QuantumLib/main Lemma ItimesIid : I 2 × I 2 = I 2. Proof. lma'. Qed. Lemma XtimesXid : σx × σx = I 2. Proof. lma'. Qed. @@ -513,15 +536,26 @@ Hint Resolve ItimesIid XtimesXid YtimesYid ZtimesZid HtimesHid : id_db. Lemma ZH_eq_HX : σz × hadamard = hadamard × σx. Proof. lma'. Qed. Lemma XH_eq_HZ : σx × hadamard = hadamard × σz. Proof. lma'. Qed. +<<<<<<< HEAD Lemma PX_eq_YP : Phase × σx = σy × Phase. Proof. rewrite PEqP'. lma'. Qed. Lemma PZ_eq_ZP : Phase × σz = σz × Phase. Proof. lma'. Qed. +======= +Lemma SX_eq_YS : Sgate × σx = σy × Sgate. Proof. lma'; unfold Mmult; + simpl; rewrite Cexp_PI2; lca. Qed. +Lemma SZ_eq_ZS : Sgate × σz = σz × Sgate. Proof. lma'; unfold Mmult; + simpl; rewrite Cexp_PI2; lca. Qed. +>>>>>>> QuantumLib/main Lemma cnotX1 : cnot × (σx ⊗ I 2) = (σx ⊗ σx) × cnot. Proof. lma'. Qed. Lemma cnotX2 : cnot × (I 2 ⊗ σx) = (I 2 ⊗ σx) × cnot. Proof. lma'. Qed. Lemma cnotZ1 : cnot × (σz ⊗ I 2) = (σz ⊗ I 2) × cnot. Proof. lma'. Qed. Lemma cnotZ2 : cnot × (I 2 ⊗ σz) = (σz ⊗ σz) × cnot. Proof. lma'. Qed. +<<<<<<< HEAD Hint Resolve ZH_eq_HX XH_eq_HZ PX_eq_YP PZ_eq_ZP cnotX1 cnotX2 cnotZ1 cnotZ2 : id_db. +======= +Hint Resolve ZH_eq_HX XH_eq_HZ SX_eq_YS SZ_eq_ZS cnotX1 cnotX2 cnotZ1 cnotZ2 : id_db. +>>>>>>> QuantumLib/main @@ -531,6 +565,11 @@ Hint Resolve ZH_eq_HX XH_eq_HZ PX_eq_YP PZ_eq_ZP cnotX1 cnotX2 cnotZ1 cnotZ2 : i (************************************************************************) +<<<<<<< HEAD +======= +Local Open Scope nat_scope. + +>>>>>>> QuantumLib/main Definition orthogonal {n m} (S : Matrix n m) : Prop := forall i j, i <> j -> inner_product (get_vec i S) (get_vec j S) = C0. @@ -566,6 +605,7 @@ Proof. intros. Qed. +<<<<<<< HEAD (***********************************************************) (* Defining and proving lemmas relating to the determinant *) (***********************************************************) @@ -1123,6 +1163,8 @@ Proof. induction n as [| n']. +======= +>>>>>>> QuantumLib/main (***************************************************) @@ -1142,7 +1184,11 @@ Proof. unfold good_M, I; intros. Qed. +<<<<<<< HEAD Lemma good_M_reduce : forall {n} (A : Square n) (x y : nat), +======= +Lemma good_M_reduce : forall {n} (A : Square (S n)) (x y : nat), +>>>>>>> QuantumLib/main good_M A -> good_M (reduce A x y). Proof. unfold good_M; intros. destruct H0 as [H0 H1]. @@ -1167,7 +1213,11 @@ Qed. Lemma connect : forall (n : nat) (A gM : Square (S n)), good_M gM -> +<<<<<<< HEAD exists (p : Polynomial (S n)), (forall c : C, Determinant (S n) (A .+ (-c .* gM)) = eval_P (S n) p c). +======= + exists (p : Polynomial (S n)), (forall c : C, Determinant (A .+ (-c .* gM)) = eval_P (S n) p c). +>>>>>>> QuantumLib/main Proof. induction n as [| n']. - intros. exists [A 0 0; - gM 0 0]. @@ -1190,7 +1240,11 @@ Proof. induction n as [| n']. Lemma connect2 : forall (n : nat) (A : Square (S n)), +<<<<<<< HEAD exists (c : C), Determinant (S n) (A .+ (-c .* I (S n))) = C0. +======= + exists (c : C), det_eq_c C0 (A .+ (-c .* I (S n))). +>>>>>>> QuantumLib/main Proof. intros. assert (H' : good_M (I (S n))). apply good_M_I. @@ -1199,7 +1253,13 @@ Proof. intros. assert (H0 : S n > 0). lia. apply (Fundamental_Theorem_Algebra p) in H0. destruct H0 as [c H0]. +<<<<<<< HEAD exists c. rewrite <- H0. +======= + exists c. + split; try easy. + rewrite <- H0. +>>>>>>> QuantumLib/main easy. Qed. @@ -1210,7 +1270,11 @@ Lemma exists_eigenvector : forall (n : nat) (A : Square (S n)), exists (c : C) (v : Vector (S n)), WF_Matrix v /\ v <> Zero /\ A × v = c.* v. Proof. intros. destruct (connect2 n A) as [c H0]. +<<<<<<< HEAD apply Det_0_lindep in H0. +======= + apply lin_dep_det_eq_0 in H0; auto with wf_db. +>>>>>>> QuantumLib/main destruct H0 as [v [H1 [H2 H3]]]. exists c, v. split; auto. @@ -1219,12 +1283,18 @@ Proof. intros. assert (H4 : A × v .+ (-c .* v) .+ (c .* v) = (c .* v)). { rewrite H3. lma. } rewrite Mplus_assoc in H4. +<<<<<<< HEAD Search (_ .* ?b .+ _ .* ?b). +======= +>>>>>>> QuantumLib/main rewrite <- Mscale_plus_distr_l in H4. replace (-c + c)%C with C0 in H4 by lca. rewrite <- H4. lma. +<<<<<<< HEAD auto with wf_db. +======= +>>>>>>> QuantumLib/main Qed. @@ -1285,10 +1355,18 @@ Lemma form_basis_ver : forall {n} (v : Vector n) (x : nat), linearly_independent (form_basis v x) /\ get_vec x (form_basis v x) = v. Proof. intros. destruct n; try lia. split. +<<<<<<< HEAD - apply (lin_indep_col_add_many_conv _ _ x _ (-C1 .* (make_row_zero x v))); try easy. unfold scale, make_row_zero. bdestruct (x =? x); try lia; lca. apply (lin_indep_scale_conv _ x (/ (v x 0))). +======= + - apply (mat_prop_col_add_many_conv _ _ x (-C1 .* (make_row_zero x v))); + try easy; auto with invr_db. + unfold scale, make_row_zero. + bdestruct (x =? x); try lia; lca. + apply (mat_prop_col_scale_conv _ _ x (/ (v x 0))); auto with invr_db. +>>>>>>> QuantumLib/main apply nonzero_div_nonzero; easy. assert (H' : forall A : Square (S n), A = I (S n) -> linearly_independent A). { intros. rewrite H3. @@ -1373,7 +1451,12 @@ Proof. intros. apply WF_col_swap; try lia; try easy. apply WF_form_basis; easy. split. +<<<<<<< HEAD + apply lin_indep_swap; try lia. +======= + + apply_mat_prop lin_indep_swap_invr. + apply H3; try lia. +>>>>>>> QuantumLib/main easy. + rewrite col_swap_diff_order. rewrite <- (col_swap_get_vec _ 0 x). @@ -1464,7 +1547,10 @@ Qed. (*****************************************************************************************) (* Defining and verifying the gram_schmidt algorythm and proving v can be part of an onb *) (*****************************************************************************************) +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main (* proj of v onto u *) @@ -1494,8 +1580,11 @@ Proof. intros. Qed. +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main Definition gram_schmidt_on_v (n m : nat) (v : Vector n) (S : Matrix n m) := v .+ (Msum m (fun i => (-C1) .* (proj (get_vec i S) v))). @@ -1537,7 +1626,11 @@ Proof. intros. do 2 rewrite Msum_Csum. rewrite Cplus_comm. rewrite <- Csum_extend_r. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main - apply Csum_eq_bounded. intros. unfold delta_T. @@ -1548,7 +1641,10 @@ Proof. intros. { prep_matrix_equality; unfold get_vec, reduce_col. bdestruct (x0 >>>>>> QuantumLib/main rewrite H'. unfold scale. lca. - unfold delta_T. bdestruct (m =? m); try lia. @@ -1622,11 +1718,15 @@ Proof. intros. rewrite (Msum_to_Mmult T (delta_T T)) in H0. unfold linearly_independent in H. apply H in H0. +<<<<<<< HEAD assert (H' : C1 <> C0). { apply C0_fst_neq. simpl. apply R1_neq_R0. } apply H'. +======= + apply C1_neq_C0. +>>>>>>> QuantumLib/main assert (H'' : f_to_vec (S m) (delta_T T) m 0 = C0). { rewrite H0. easy. } rewrite <- H''. @@ -1647,6 +1747,7 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma Cconj_simplify : forall (c1 c2 : C), c1^* = c2^* -> c1 = c2. Proof. intros. assert (H1 : c1 ^* ^* = c2 ^* ^*). { rewrite H; easy. } @@ -1658,13 +1759,19 @@ Qed. +======= +>>>>>>> QuantumLib/main Lemma get_vec_reduce_append_miss : forall {n m} (T : Matrix n (S m)) (v : Vector n) (i : nat), i < m -> get_vec i (col_append (reduce_col T m) v) = get_vec i T. Proof. intros. prep_matrix_equality. unfold get_vec, col_append, reduce_col. +<<<<<<< HEAD bdestruct (i =? S m - 1); bdestruct (i >>>>>> QuantumLib/main Qed. @@ -1674,8 +1781,12 @@ Proof. intros. unfold get_vec, col_append, reduce_col. prep_matrix_equality. bdestruct (y =? 0). +<<<<<<< HEAD - bdestruct (m =? S m - 1); try lia. rewrite H0; easy. +======= + - bdestruct_all; subst; easy. +>>>>>>> QuantumLib/main - rewrite H; try lia; easy. Qed. @@ -1686,14 +1797,22 @@ Lemma get_vec_reduce_append_over : forall {n m} (T : Matrix n (S m)) (v : Vector Proof. intros. prep_matrix_equality. unfold get_vec, col_append, reduce_col. +<<<<<<< HEAD bdestruct (i =? S m - 1); bdestruct (i >>>>>> QuantumLib/main right. lia. Qed. +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main Lemma extend_onb_ind_step_part1 : forall {n m} (T : Matrix n (S m)), WF_Matrix T -> linearly_independent T -> orthonormal (reduce_col T m) -> orthonormal (col_append (reduce_col T m) (normalize (gram_schmidt_on_T n m T))). @@ -1726,18 +1845,29 @@ Proof. intros. rewrite Cconj_involutive, Cconj_0. apply inner_product_zero_normalize. rewrite gram_schmidt_compare. +<<<<<<< HEAD rewrite easy_sub in *. apply (gram_schmidt_orthogonal (get_vec m T) _ j) in H1; try lia. assert (H9 := (@get_vec_reduce_col n (S m) j m T)). rewrite easy_sub in *. rewrite H9 in H1; try lia. +======= + apply (gram_schmidt_orthogonal (get_vec m T) _ j) in H1; try lia. + rewrite (@get_vec_reduce_col n m j m T) in H1; try lia. +>>>>>>> QuantumLib/main apply H1. assert (H' : WF_Matrix (get_vec m T)). { apply WF_get_vec; easy. } apply inner_product_zero_iff_zero in H'. destruct (Ceq_dec (inner_product (get_vec m T) (get_vec m T)) C0); try easy. apply H' in e. +<<<<<<< HEAD apply lin_indep_nonzero_cols in e; try lia; try easy. +======= + apply_mat_prop lin_indep_pzf. + apply H10 in H0; try easy. + exists m; split; try lia; easy. +>>>>>>> QuantumLib/main unfold normalize. apply WF_scale. apply WF_gs_on_T; easy. @@ -1747,18 +1877,29 @@ Proof. intros. rewrite get_vec_reduce_append_miss; try easy. apply inner_product_zero_normalize. rewrite gram_schmidt_compare. +<<<<<<< HEAD rewrite easy_sub in *. apply (gram_schmidt_orthogonal (get_vec m T) _ i) in H1; try lia. assert (H9 := (@get_vec_reduce_col n (S m) i m T)). rewrite easy_sub in *. rewrite H9 in H1; try lia. +======= + apply (gram_schmidt_orthogonal (get_vec m T) _ i) in H1; try lia. + rewrite (@get_vec_reduce_col n m i m T) in H1; try lia. +>>>>>>> QuantumLib/main apply H1. assert (H' : WF_Matrix (get_vec m T)). { apply WF_get_vec; easy. } apply inner_product_zero_iff_zero in H'. destruct (Ceq_dec (inner_product (get_vec m T) (get_vec m T)) C0); try easy. apply H' in e. +<<<<<<< HEAD apply lin_indep_nonzero_cols in e; try lia; try easy. +======= + apply_mat_prop lin_indep_pzf. + apply H10 in H0; try easy. + exists m; split; try lia; easy. +>>>>>>> QuantumLib/main unfold normalize. apply WF_scale. apply WF_gs_on_T; easy. @@ -1768,9 +1909,14 @@ Proof. intros. unfold orthonormal in H1. destruct H1 as [H1 _]. unfold orthogonal in H1. +<<<<<<< HEAD apply (@get_vec_reduce_col n (S m) i m T) in H7. apply (@get_vec_reduce_col n (S m) j m T) in H8. rewrite easy_sub in *. +======= + apply (@get_vec_reduce_col n m i m T) in H7. + apply (@get_vec_reduce_col n m j m T) in H8. +>>>>>>> QuantumLib/main apply H1 in H2. rewrite H7, H8 in H2; easy. - intros. @@ -1788,9 +1934,14 @@ Proof. intros. apply WF_scale. apply WF_gs_on_T; easy. + destruct H1 as [_ H1]. +<<<<<<< HEAD rewrite get_vec_reduce_append_miss; try lia. assert (H' := (@get_vec_reduce_col n (S m) i m T)). rewrite <- H'; try lia. +======= + rewrite get_vec_reduce_append_miss; try lia. + rewrite <- (@get_vec_reduce_col n m i m T); try lia. +>>>>>>> QuantumLib/main apply H1; lia. Qed. @@ -1815,7 +1966,11 @@ Proof. intros. rewrite <- Csum_extend_r. bdestruct (m1 =? m1); bdestruct (0 =? 0); try lia. rewrite Cplus_comm. +<<<<<<< HEAD apply Csum_simplify; try lca. +======= + apply Cplus_simplify; try lca. +>>>>>>> QuantumLib/main unfold get_vec. assert (p : S m1 + m2 = m1 + (S m2)). lia. rewrite p. @@ -1852,11 +2007,17 @@ Lemma extend_onb_ind_step_part2 : forall {n m1 m2} (T1 : Matrix n m1) (T2 : Matr (normalize (gram_schmidt_on_T n m1 (col_append T1 v)))) T2). Proof. intros. rewrite smash_scale. +<<<<<<< HEAD apply lin_indep_scale. +======= + apply_mat_prop lin_indep_scale_invr. + apply H5. +>>>>>>> QuantumLib/main unfold not; intros. assert (H4' : (norm (gram_schmidt_on_T n m1 (col_append T1 v)) * / norm (gram_schmidt_on_T n m1 (col_append T1 v)) = norm (gram_schmidt_on_T n m1 (col_append T1 v)) * C0)%C). +<<<<<<< HEAD { rewrite H4; easy. } rewrite Cmult_0_r, Cinv_r in H4'. assert (H5 : C1 <> C0). @@ -1864,20 +2025,39 @@ Proof. intros. simpl. apply R1_neq_R0. } apply H5; easy. +======= + { rewrite H6; easy. } + rewrite Cmult_0_r, Cinv_r in H4'. + apply C1_neq_C0; easy. +>>>>>>> QuantumLib/main unfold not; intros. assert (H5' : WF_Matrix (gram_schmidt_on_T n m1 (col_append T1 v))). { apply WF_gs_on_T. apply WF_col_append; easy. } apply norm_zero_iff_zero in H5'. +<<<<<<< HEAD apply RtoC_inj in H5. rewrite H5 in H5'. +======= + apply RtoC_inj in H7. + rewrite H7 in H5'. +>>>>>>> QuantumLib/main apply (gram_schmidt_non_zero (col_append T1 v)). apply lin_indep_smash in H3; easy. apply H5'; lra. rewrite gs_on_T_cols_add; try easy. +<<<<<<< HEAD apply lin_indep_col_add_many; try lia; try easy. unfold f_to_vec, delta_T'. bdestruct (m1 >>>>>> QuantumLib/main Qed. @@ -1904,11 +2084,15 @@ Proof. intros. bdestruct (1 + y =? m1); try lia; try easy. all : rewrite H; try lia; rewrite H; try lia; lca. } rewrite H' in H4. +<<<<<<< HEAD rewrite easy_sub in *. +======= +>>>>>>> QuantumLib/main apply H4; try easy. apply WF_col_append; easy. - apply extend_onb_ind_step_part2; try easy. apply lin_indep_smash in H2. +<<<<<<< HEAD assert (H4 := @lin_indep_nonzero_cols n (S m1) (col_append T1 v)). assert (H' : get_vec m1 (col_append T1 v) = v). { prep_matrix_equality. @@ -1918,6 +2102,19 @@ Proof. intros. rewrite H1; try lca; lia. } rewrite <- H'. apply H4; try lia; easy. +======= + apply_mat_prop lin_indep_pzf. + unfold not; intros. + assert (H' : ~ linearly_independent (col_append T1 v)). + { apply H5. + exists m1. + split; try lia. + rewrite <- H6. + prep_matrix_equality. + unfold get_vec, col_append. + bdestruct (y =? 0); bdestruct (m1 =? m1); subst; try easy; try lia. } + easy. +>>>>>>> QuantumLib/main Qed. @@ -1936,7 +2133,10 @@ Proof. induction m2 as [| m2']. - intros. rewrite (split T2) in *. assert (H3 := (smash_assoc T1 (get_vec 0 T2) (reduce_col T2 0))). +<<<<<<< HEAD rewrite easy_sub in *. +======= +>>>>>>> QuantumLib/main simpl in *. rewrite <- H3 in H1. rewrite <- smash_append in H1; try easy. @@ -1947,7 +2147,10 @@ Proof. induction m2 as [| m2']. rewrite (split T2). easy. apply WF_get_vec. rewrite (split T2). easy. +<<<<<<< HEAD rewrite easy_sub in *. +======= +>>>>>>> QuantumLib/main assert (add1 : S (m1 + S m2') = S (S m1) + m2'). { lia. } assert (add2 : S (m1 + 1) = S (S m1)). { lia. } rewrite add1, add2 in H1. @@ -1955,6 +2158,7 @@ Proof. induction m2 as [| m2']. destruct H4 as [v [H4 [H5 H6]]]. assert (H7 : exists T2' : Matrix n m2', WF_Matrix T2' /\ orthonormal (smash (smash T1 v) T2')). +<<<<<<< HEAD { apply (IHm2' _ (smash T1 v) (reduce_col T2 0)). assert (H' : Nat.add m1 (S O) = S m1). lia. unfold Nat.add in H'. @@ -1971,12 +2175,28 @@ Proof. induction m2 as [| m2']. lia. rewrite (split T2). easy. +======= + { assert (H'' := (@WF_smash n (S m1) (S O) T1 v)). + assert (H''' : Nat.add (S m1) (S O) = S (S m1)). lia. + apply (IHm2' _ (smash T1 v) (reduce_col T2 0)); try easy. + assert (H' : Nat.add m1 (S O) = S m1). lia. + unfold Nat.add in H'. + rewrite H'. + rewrite H''' in *. + apply H''. + easy. easy. + apply (WF_reduce_col 0 T2); try lia. + rewrite (split T2); easy. +>>>>>>> QuantumLib/main assert (add1 : S (Nat.add m1 (S m2')) = S (Nat.add (Nat.add m1 (S O)) m2')). lia. rewrite add1 in H1. unfold Nat.add in H1. unfold Nat.add. rewrite <- smash_append; try easy. +<<<<<<< HEAD rewrite easy_sub in *. +======= +>>>>>>> QuantumLib/main assert (add2 : Nat.add (S (S m1)) m2' = S (Nat.add (Nat.add m1 (S O)) m2')). lia. assert (add3 : (S (S m1)) = S (Nat.add m1 (S O))). lia. rewrite add2, add3 in H6. @@ -2074,9 +2294,13 @@ Proof. intros. apply WF_get_vec; easy. easy. apply WF_get_vec; easy. +<<<<<<< HEAD apply (WF_reduce_col 0) in H1. rewrite easy_sub in *; easy. lia. +======= + apply (WF_reduce_col 0) in H1; try easy; lia. +>>>>>>> QuantumLib/main rewrite H3; apply orthonormal_normalize_v; easy. unfold not; intros; apply H0. prep_matrix_equality. @@ -2109,6 +2333,7 @@ Qed. (********************************************************************) +<<<<<<< HEAD Lemma P_unitary : WF_Unitary Phase. Proof. apply phase_unitary. Qed. Lemma T_unitary : WF_Unitary Tgate. Proof. unfold WF_Unitary. @@ -2121,6 +2346,10 @@ Proof. unfold WF_Unitary. rewrite H1 in H; rewrite H. rewrite Cexp_mul_neg_l. lca. Qed. +======= +Lemma P_unitary : WF_Unitary Sgate. Proof. apply phase_unitary. Qed. +Lemma T_unitary : WF_Unitary Tgate. Proof. apply phase_unitary. Qed. +>>>>>>> QuantumLib/main Lemma notc_unitary : WF_Unitary notc. @@ -2198,6 +2427,10 @@ Proof. intros n U. split. bdestruct (i =? j); bdestruct (i >>>>>> QuantumLib/main apply sqrt_1_unique in H0. unfold RtoC. apply c_proj_eq. @@ -2575,7 +2808,11 @@ Proof. Qed. +<<<<<<< HEAD Lemma up_tri_reduce_0 : forall {n : nat} (A : Square n), +======= +Lemma up_tri_reduce_0 : forall {n : nat} (A : Square (S n)), +>>>>>>> QuantumLib/main upper_triangular A -> upper_triangular (reduce A 0 0). Proof. unfold upper_triangular, reduce. @@ -2588,7 +2825,11 @@ Qed. Lemma det_up_tri_diags : forall {n : nat} (A : Square n), upper_triangular A -> +<<<<<<< HEAD Determinant n A = Cprod (fun i => A i i) n. +======= + Determinant A = Cprod (fun i => A i i) n. +>>>>>>> QuantumLib/main Proof. induction n as [| n']. - easy. - intros. simpl. @@ -2603,14 +2844,22 @@ Proof. induction n as [| n']. rewrite <- Csum_extend_l. rewrite <- Cplus_0_r. rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main simpl parity. rewrite IHn'; try lca. apply up_tri_reduce_0; easy. unfold upper_triangular in H. rewrite H; try lia. rewrite <- Cplus_0_r. +<<<<<<< HEAD apply Csum_simplify; try lca. +======= + apply Cplus_simplify; try lca. +>>>>>>> QuantumLib/main apply Csum_0_bounded. intros. rewrite H; try lia; lca. @@ -2618,6 +2867,7 @@ Qed. +<<<<<<< HEAD Lemma det_multiplicative_up_tri : forall {n} (A B : Square n), upper_triangular A -> upper_triangular B -> (Determinant n A * Determinant n B)%C = Determinant n (A × B). @@ -2638,6 +2888,8 @@ Qed. +======= +>>>>>>> QuantumLib/main (**************************************************) (* Defining eignestates to be used in type system *) (**************************************************) @@ -2669,9 +2921,17 @@ Proof. unfold WF_Diagonal, Eigenpair, e_i. intros. - intros. simpl. bdestruct (x' =? i); try lia; lca. Qed. +<<<<<<< HEAD Lemma eigen_scale : forall {n} (A : Square n) (v : Vector n) (c1 c2 : C), Eigenpair A (v, c1) -> Eigenpair (c2 .* A) (v, Cmult c1 c2). +======= +Local Close Scope nat_scope. + + +Lemma eigen_scale : forall {n} (A : Square n) (v : Vector n) (c1 c2 : C), + Eigenpair A (v, c1) -> Eigenpair (c2 .* A) (v, c1 * c2). +>>>>>>> QuantumLib/main Proof. intros. unfold Eigenpair in *; simpl in *. rewrite Mscale_mult_dist_l. @@ -2742,9 +3002,15 @@ Proof. intros. destruct H0 as [v [H0 [H1 H2]]]. rewrite Mscale_mult_dist_r in H4. rewrite Mscale_mult_dist_l in H4. rewrite Mscale_assoc in H4. +<<<<<<< HEAD assert (H' : ((v) † × v) 0 0 = (c * c ^* .* ((v) † × v)) 0 0). rewrite <- H4; easy. assert (H'' : ((v) † × v) 0 0 = inner_product v v). easy. +======= + assert (H' : ((v) † × v) O O = (c * c ^* .* ((v) † × v)) O O). + rewrite <- H4; easy. + assert (H'' : ((v) † × v) O O = inner_product v v). easy. +>>>>>>> QuantumLib/main unfold scale in H'. rewrite H'' in H'. apply (Cmult_simplify (inner_product v v) (c * c ^* * inner_product v v) @@ -2819,7 +3085,11 @@ Proof. intros n A [Hwf Hu]. apply H; easy. Qed. +<<<<<<< HEAD +======= +Local Open Scope nat_scope. +>>>>>>> QuantumLib/main (* this proof is horribly long and I feel like theres probably a better way to show this *) (* TODO : make this better *) Lemma unitary_reduction_step2 : forall {n} (A : Square (S n)), @@ -2848,6 +3118,10 @@ Proof. intros n A H [c H0] i j H1. assert (H4 : norm (get_vec 0 A†) = 1%R). { apply Hn; lia. } unfold norm in H4. +<<<<<<< HEAD +======= + apply eq_sym in H4. +>>>>>>> QuantumLib/main apply sqrt_1_unique in H4. replace 1%R with (fst C1) in H4 by easy. apply (c_proj_eq (((get_vec 0 A†) † × get_vec 0 A†) 0 0) C1) in H4. @@ -2922,11 +3196,16 @@ Proof. intros n A [Hwf Hu]. assert (H' : WF_Matrix (reduce A 0 0)). { apply WF_reduce; try lia; easy. } split. split. +<<<<<<< HEAD rewrite easy_sub in *. apply H'. apply mat_equiv_eq; auto with wf_db. apply WF_mult; try apply WF_adjoint. all : rewrite easy_sub in *; try easy. +======= + apply H'. + apply mat_equiv_eq; auto with wf_db. +>>>>>>> QuantumLib/main unfold mat_equiv; intros. assert (H2 : ((A) † × A) (S i) (S j) = (I n) i j). { rewrite Hu. @@ -2995,7 +3274,12 @@ Proof. induction n as [| n']. { do 2 try apply Mmult_unitary. apply transpose_unitary. all : easy. } +<<<<<<< HEAD assert (H4 : (forall (i j : nat), (i = 0 \/ j = 0) /\ i <> j -> ((X) † × A × X) i j = C0)). +======= + assert (H4 : (forall (i j : nat), (i = 0 \/ j = 0) /\ i <> j -> + ((X) † × A × X) i j = C0)). +>>>>>>> QuantumLib/main { apply unitary_reduction_step2; try easy. exists c. easy. } apply unitary_reduction_step3 in H3; try easy. diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..905b725 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2021 INQWIRE + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/Matrix.v b/Matrix.v index 48ad1c2..173c41e 100644 --- a/Matrix.v +++ b/Matrix.v @@ -1,4 +1,8 @@ +<<<<<<< HEAD Require Import Psatz. +======= +Require Import Psatz. +>>>>>>> QuantumLib/main Require Import String. Require Import Program. Require Export Complex. @@ -8,6 +12,7 @@ Require Import List. (* TODO: Use matrix equality everywhere, declare equivalence relation *) (* TODO: Make all nat arguments to matrix lemmas implicit *) +<<<<<<< HEAD <<<<<<< HEAD ======= Local Open Scope nat_scope. @@ -38,6 +43,8 @@ Qed. >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (*******************************************) (** Matrix Definitions and Infrastructure **) (*******************************************) @@ -172,9 +179,12 @@ Definition I (n : nat) : Square n := (* Optional coercion to scalar (should be limited to 1 × 1 matrices): Definition to_scalar (m n : nat) (A: Matrix m n) : C := A 0 0. <<<<<<< HEAD +<<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Coercion to_scalar : Matrix >-> C. *) @@ -289,7 +299,10 @@ Ltac lma := lca. <<<<<<< HEAD +<<<<<<< HEAD +======= ======= +>>>>>>> QuantumLib/main Ltac solve_end := @@ -319,7 +332,21 @@ Ltac lma' := +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +(* lemmas which are useful for simplifying proofs involving Mmult or kron *) +Lemma kron_simplify : forall (n m o p : nat) (a b : Matrix n m) (c d : Matrix o p), + a = b -> c = d -> a ⊗ c = b ⊗ d. +Proof. intros; subst; easy. +Qed. + +Lemma Mmult_simplify : forall (n m o : nat) (a b : Matrix n m) (c d : Matrix m o), + a = b -> c = d -> a × c = b × d. +Proof. intros; subst; easy. +Qed. + +>>>>>>> QuantumLib/main (******************************) (** Proofs about finite sums **) (******************************) @@ -522,8 +549,11 @@ Proof. apply Rplus_le_compat; easy. Qed. +<<<<<<< HEAD <<<<<<< HEAD ======= +======= +>>>>>>> QuantumLib/main Lemma Csum_gt_0 : forall f n, (forall x, 0 <= fst (f x)) -> (exists y : nat, (y < n)%nat /\ 0 < fst (f y)) -> @@ -543,7 +573,10 @@ Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma Csum_member_le : forall (f : nat -> C) (n : nat), (forall x, 0 <= fst (f x)) -> (forall x, (x < n)%nat -> fst (f x) <= fst (Csum f n)). Proof. @@ -565,11 +598,14 @@ Proof. apply Csum_ge_0; easy. lra. <<<<<<< HEAD +<<<<<<< HEAD Qed. ======= +======= +>>>>>>> QuantumLib/main Qed. Lemma Csum_squeeze : forall (f : nat -> C) (n : nat), @@ -628,7 +664,11 @@ Proof. induction m as [| m']. - rewrite Nat.mul_succ_r. rewrite <- Csum_extend_r. rewrite Csum_sum. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main apply Csum_eq_bounded; intros. rewrite mult_comm. rewrite Nat.div_add_l; try lia. @@ -651,7 +691,11 @@ Proof. intros. assert (H' : forall a b c d, (a + b + c + d = (a + c) + (b + d))%C). { intros. lca. } rewrite H'. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main rewrite <- Csum_plus. apply Csum_eq_bounded; intros. easy. @@ -669,7 +713,11 @@ Proof. induction n as [| n']. rewrite (IHn' f g); try easy. repeat rewrite Cmult_plus_distr_l. repeat rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main assert (H' : forall a b c, (a + (b + c) = (a + c) + b)%C). intros. lca. do 2 rewrite H'. @@ -677,22 +725,33 @@ Proof. induction n as [| n']. do 2 rewrite Csum_extend_r. do 2 rewrite Csum_mult_l. rewrite Cplus_comm. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main all : apply Csum_eq_bounded; intros. apply H; lia. apply H0; lia. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (**********************************) (** Proofs about Well-Formedness **) (**********************************) +<<<<<<< HEAD <<<<<<< HEAD Local Open Scope nat_scope. ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Lemma WF_Matrix_dim_change : forall (m n m' n' : nat) (A : Matrix m n), m = m' -> @@ -825,6 +884,22 @@ Proof. apply IHl. intros i. apply (H (S i)). Qed. +<<<<<<< HEAD +======= +(* alternate version that uses In instead of nth *) +Lemma WF_big_kron' : forall n m (l : list (Matrix m n)), + (forall A, In A l -> WF_Matrix A) -> + WF_Matrix (⨂ l). +Proof. + intros n m l H. + induction l. + - simpl. apply WF_I. + - simpl. apply WF_kron; trivial. apply H; left; easy. + apply IHl. intros A' H0. apply H; right; easy. +Qed. + + +>>>>>>> QuantumLib/main Lemma WF_Mmult_n : forall n {m} (A : Square m), WF_Matrix A -> WF_Matrix (Mmult_n n A). Proof. @@ -1014,10 +1089,14 @@ Proof. lia. Qed. +<<<<<<< HEAD <<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Lemma Mmult_1_l: forall (m n : nat) (A : Matrix m n), WF_Matrix A -> I m × A = A. Proof. @@ -1346,7 +1425,10 @@ Proof. Qed. <<<<<<< HEAD +<<<<<<< HEAD +======= ======= +>>>>>>> QuantumLib/main Lemma Mscale_div : forall {n m} (c : C) (A B : Matrix n m), c <> C0 -> c .* A = c .* B -> A = B. @@ -1360,7 +1442,10 @@ Proof. intros. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma Mscale_plus_distr_l : forall (m n : nat) (x y : C) (A : Matrix m n), (x + y) .* A = x .* A .+ y .* A. Proof. @@ -1429,17 +1514,22 @@ Proof. reflexivity. Qed. Lemma Mscale_adj : forall (m n : nat) (x : C) (A : Matrix m n), (x .* A)† = x^* .* A†. Proof. +<<<<<<< HEAD <<<<<<< HEAD intros m n x A. ======= intros m n xtranspose A. >>>>>>> Heisenberg-Foundations/main +======= + intros m n xtranspose A. +>>>>>>> QuantumLib/main unfold scale, adjoint. prep_matrix_equality. rewrite Cconj_mult_distr. reflexivity. Qed. +<<<<<<< HEAD <<<<<<< HEAD (* Inverses of square matrices *) @@ -1478,11 +1568,114 @@ Proof. unfold Minv. split; trivial. apply Minv_flip. assumption. +======= + +Lemma Mplus_transpose : forall (m n : nat) (A : Matrix m n) (B : Matrix m n), + (A .+ B)⊤ = A⊤ .+ B⊤. +Proof. reflexivity. Qed. + +Lemma Mmult_transpose : forall (m n o : nat) (A : Matrix m n) (B : Matrix n o), + (A × B)⊤ = B⊤ × A⊤. +Proof. + intros m n o A B. + unfold Mmult, transpose. + prep_matrix_equality. + apply Csum_eq. + apply functional_extensionality. intros z. + rewrite Cmult_comm. + reflexivity. +Qed. + +Lemma kron_transpose : forall (m n o p : nat) (A : Matrix m n) (B : Matrix o p ), + (A ⊗ B)⊤ = A⊤ ⊗ B⊤. +Proof. reflexivity. Qed. + + +Lemma Mplus_adjoint : forall (m n : nat) (A : Matrix m n) (B : Matrix m n), + (A .+ B)† = A† .+ B†. +Proof. + intros m n A B. + unfold Mplus, adjoint. + prep_matrix_equality. + rewrite Cconj_plus_distr. + reflexivity. +Qed. + +Lemma Mmult_adjoint : forall {m n o : nat} (A : Matrix m n) (B : Matrix n o), + (A × B)† = B† × A†. +Proof. + intros m n o A B. + unfold Mmult, adjoint. + prep_matrix_equality. + rewrite Csum_conj_distr. + apply Csum_eq. + apply functional_extensionality. intros z. + rewrite Cconj_mult_distr. + rewrite Cmult_comm. + reflexivity. +Qed. + +Lemma kron_adjoint : forall {m n o p : nat} (A : Matrix m n) (B : Matrix o p), + (A ⊗ B)† = A† ⊗ B†. +Proof. + intros. unfold adjoint, kron. + prep_matrix_equality. + rewrite Cconj_mult_distr. + reflexivity. +Qed. + +Lemma id_kron : forall (m n : nat), I m ⊗ I n = I (m * n). +Proof. + intros. + unfold I, kron. + prep_matrix_equality. + bdestruct (x =? y); rename H into Eq; subst. + + repeat rewrite <- beq_nat_refl; simpl. + destruct n. + - simpl. + rewrite mult_0_r. + bdestruct (y >>>>>> QuantumLib/main Qed. Local Open Scope nat_scope. +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main Lemma div_mod : forall (x y z : nat), (x / y) mod z = (x mod (y * z)) / y. Proof. intros. bdestruct (y =? 0). subst. simpl. @@ -1555,6 +1748,10 @@ Proof. apply kron_assoc_mat_equiv. Qed. +<<<<<<< HEAD +======= + +>>>>>>> QuantumLib/main Lemma kron_mixed_product : forall {m n o p q r : nat} (A : Matrix m n) (B : Matrix p q ) (C : Matrix n o) (D : Matrix q r), (A ⊗ B) × (C ⊗ D) = (A × C) ⊗ (B × D). Proof. @@ -1576,7 +1773,11 @@ Qed. (* Arguments kron_mixed_product [m n o p q r]. *) +<<<<<<< HEAD (* +======= + +>>>>>>> QuantumLib/main (* A more explicit version, for when typechecking fails *) Lemma kron_mixed_product' : forall (m n n' o p q q' r mp nq or: nat) (A : Matrix m n) (B : Matrix p q) (C : Matrix n' o) (D : Matrix q' r), @@ -1585,6 +1786,7 @@ Lemma kron_mixed_product' : forall (m n n' o p q q' r mp nq or: nat) (@Mmult mp nq or (@kron m n p q A B) (@kron n' o q' r C D)) = (@kron m o p r (@Mmult m n o A C) (@Mmult p q r B D)). Proof. intros. subst. apply kron_mixed_product. Qed. +<<<<<<< HEAD *) Lemma Mplus_tranpose : forall (m n : nat) (A : Matrix m n) (B : Matrix m n), @@ -1695,6 +1897,10 @@ Proof. Qed. <<<<<<< HEAD +======= + + +>>>>>>> QuantumLib/main Lemma outer_product_eq : forall m (φ ψ : Matrix m 1), φ = ψ -> outer_product φ φ = outer_product ψ ψ. Proof. congruence. Qed. @@ -1710,6 +1916,27 @@ Proof. reflexivity. Qed. +<<<<<<< HEAD +======= +Lemma big_kron_app : forall {n m} (l1 l2 : list (Matrix n m)), + (forall i, WF_Matrix (nth i l1 (@Zero n m))) -> + (forall i, WF_Matrix (nth i l2 (@Zero n m))) -> + ⨂ (l1 ++ l2) = (⨂ l1) ⊗ (⨂ l2). +Proof. induction l1. + - intros. simpl. rewrite (kron_1_l _ _ (⨂ l2)); try easy. + apply (WF_big_kron _ _ _ (@Zero n m)); easy. + - intros. simpl. rewrite IHl1. + rewrite kron_assoc. + do 2 (rewrite <- Nat.pow_add_r). + rewrite app_length. + reflexivity. + assert (H' := H 0); simpl in H'; easy. + all : try apply (WF_big_kron _ _ _ (@Zero n m)); try easy. + all : intros. + all : assert (H' := H (S i)); simpl in H'; easy. +Qed. + +>>>>>>> QuantumLib/main Lemma kron_n_assoc : forall n {m1 m2} (A : Matrix m1 m2), WF_Matrix A -> (S n) ⨂ A = A ⊗ (n ⨂ A). Proof. @@ -1750,17 +1977,202 @@ Proof. reflexivity. Qed. -Lemma kron_n_mult : forall {m1 m2 m3} n (A : Matrix m1 m2) (B : Matrix m2 m3), - n ⨂ A × n ⨂ B = n ⨂ (A × B). +Lemma kron_n_mult : forall {m1 m2 m3} n (A : Matrix m1 m2) (B : Matrix m2 m3), + n ⨂ A × n ⨂ B = n ⨂ (A × B). +Proof. + intros. + induction n; simpl. + rewrite Mmult_1_l. reflexivity. + apply WF_I. + replace (m1 * m1 ^ n) with (m1 ^ n * m1) by apply Nat.mul_comm. +<<<<<<< HEAD +======= + +(* this was origionally with the other Msum stuff, but I needed it earlier... *) +Lemma Msum_Csum : forall {d1 d2} n (f : nat -> Matrix d1 d2) i j, + Msum n f i j = Csum (fun x => f x i j) n. +Proof. + intros. + induction n; simpl. + reflexivity. + unfold Mplus. + rewrite IHn. + reflexivity. +Qed. + + + +(*****************************************************) +(* Defining matrix altering/col operations functions *) +(*****************************************************) + +Local Open Scope nat_scope. +======= + replace (m2 * m2 ^ n) with (m2 ^ n * m2) by apply Nat.mul_comm. + replace (m3 * m3 ^ n) with (m3 ^ n * m3) by apply Nat.mul_comm. + rewrite kron_mixed_product. + rewrite IHn. + reflexivity. +Qed. + +Lemma kron_n_I : forall n, n ⨂ I 2 = I (2 ^ n). +Proof. + intros. + induction n; simpl. + reflexivity. + rewrite IHn. + rewrite id_kron. + apply f_equal. + lia. +Qed. + +Lemma Mmult_n_kron_distr_l : forall {m n} i (A : Square m) (B : Square n), + i ⨉ (A ⊗ B) = (i ⨉ A) ⊗ (i ⨉ B). +Proof. + intros m n i A B. + induction i; simpl. + rewrite id_kron; reflexivity. + rewrite IHi. + rewrite kron_mixed_product. + reflexivity. +Qed. + +Lemma Mmult_n_1_l : forall {n} (A : Square n), + WF_Matrix A -> + 1 ⨉ A = A. +Proof. intros n A WF. simpl. rewrite Mmult_1_r; auto. Qed. + +Lemma Mmult_n_1_r : forall n i, + i ⨉ (I n) = I n. +Proof. + intros n i. + induction i; simpl. + reflexivity. + rewrite IHi. + rewrite Mmult_1_l; auto with wf_db. +Qed. + +Lemma Mmult_n_eigenvector : forall {n} (A : Square n) (ψ : Vector n) λ i, + WF_Matrix ψ -> A × ψ = λ .* ψ -> + i ⨉ A × ψ = (λ ^ i) .* ψ. +Proof. + intros n A ψ λ i WF H. + induction i; simpl. + rewrite Mmult_1_l; auto. + rewrite Mscale_1_l; auto. + rewrite Mmult_assoc. + rewrite IHi. + rewrite Mscale_mult_dist_r. + rewrite H. + rewrite Mscale_assoc. + rewrite Cmult_comm. + reflexivity. +Qed. + +Lemma Msum_eq_bounded : forall {d1 d2} n (f f' : nat -> Matrix d1 d2), + (forall i, (i < n)%nat -> f i = f' i) -> Msum n f = Msum n f'. +Proof. + intros d1 d2 n f f' Heq. + induction n; simpl. + reflexivity. + rewrite Heq by lia. + rewrite IHn. reflexivity. + intros. apply Heq. lia. +Qed. + +Lemma kron_Msum_distr_l : + forall {d1 d2 d3 d4} n (f : nat -> Matrix d1 d2) (A : Matrix d3 d4), + A ⊗ Msum n f = Msum n (fun i => A ⊗ f i). +Proof. + intros. + induction n; simpl. lma. + rewrite kron_plus_distr_l, IHn. reflexivity. +Qed. + +Lemma kron_Msum_distr_r : + forall {d1 d2 d3 d4} n (f : nat -> Matrix d1 d2) (A : Matrix d3 d4), + Msum n f ⊗ A = Msum n (fun i => f i ⊗ A). +Proof. + intros. + induction n; simpl. lma. + rewrite kron_plus_distr_r, IHn. reflexivity. +Qed. + +Lemma Mmult_Msum_distr_l : forall {d1 d2 m} n (f : nat -> Matrix d1 d2) (A : Matrix m d1), + A × Msum n f = Msum n (fun i => A × f i). +Proof. + intros. + induction n; simpl. + rewrite Mmult_0_r. reflexivity. + rewrite Mmult_plus_distr_l, IHn. reflexivity. +Qed. + +Lemma Mmult_Msum_distr_r : forall {d1 d2 m} n (f : nat -> Matrix d1 d2) (A : Matrix d2 m), + Msum n f × A = Msum n (fun i => f i × A). +Proof. + intros. + induction n; simpl. + rewrite Mmult_0_l. reflexivity. + rewrite Mmult_plus_distr_r, IHn. reflexivity. +Qed. + +Lemma Mscale_Msum_distr_r : forall {d1 d2} x n (f : nat -> Matrix d1 d2), + x .* Msum n f = Msum n (fun i => x .* f i). +Proof. + intros d1 d2 x n f. + induction n; simpl. lma. + rewrite Mscale_plus_distr_r, IHn. reflexivity. +Qed. + +Lemma Mscale_Msum_distr_l : forall {d1 d2} n (f : nat -> C) (A : Matrix d1 d2), + Msum n (fun i => (f i) .* A) = Csum f n .* A. +Proof. + intros d1 d2 n f A. + induction n; simpl. lma. + rewrite Mscale_plus_distr_l, IHn. reflexivity. +Qed. + +Lemma Msum_0 : forall {d1 d2} n (f : nat -> Matrix d1 d2), + (forall x, x < n -> f x = Zero) -> Msum n f = Zero. +Proof. + intros d1 d2 n f Hf. + induction n; simpl. reflexivity. + rewrite IHn, Hf. lma. + lia. intros. apply Hf. lia. +Qed. + +Lemma Msum_constant : forall {d1 d2} n (A : Matrix d1 d2), Msum n (fun _ => A) = INR n .* A. +Proof. + intros. + induction n. + simpl. lma. + simpl Msum. + rewrite IHn. + replace (S n) with (n + 1)%nat by lia. + rewrite plus_INR; simpl. + rewrite RtoC_plus. + rewrite Mscale_plus_distr_l. + lma. +Qed. + +Lemma Msum_plus : forall {d1 d2} n (f1 f2 : nat -> Matrix d1 d2), + Msum n (fun i => (f1 i) .+ (f2 i)) = Msum n f1 .+ Msum n f2. +Proof. + intros d1 d2 n f1 f2. + induction n; simpl. lma. + rewrite IHn. lma. +Qed. + +Lemma Msum_adjoint : forall {d1 d2} n (f : nat -> Matrix d1 d2), + (Msum n f)† = Msum n (fun i => (f i)†). Proof. intros. induction n; simpl. - rewrite Mmult_1_l. reflexivity. - apply WF_I. - replace (m1 * m1 ^ n) with (m1 ^ n * m1) by apply Nat.mul_comm. -======= + lma. + rewrite Mplus_adjoint, IHn. + reflexivity. +Qed. -(* this was origionally with the other Msum stuff, but I needed it earlier... *) Lemma Msum_Csum : forall {d1 d2} n (f : nat -> Matrix d1 d2) i j, Msum n f i j = Csum (fun x => f x i j) n. Proof. @@ -1772,13 +2184,40 @@ Proof. reflexivity. Qed. +Lemma Msum_unique : forall {d1 d2} n (f : nat -> Matrix d1 d2) (A : Matrix d1 d2), + (exists i, i < n /\ f i = A /\ (forall j, j < n -> j <> i -> f j = Zero)) -> + Msum n f = A. +Proof. + intros d1 d2 n f A H. + destruct H as [i [? [? H]]]. + induction n; try lia. + simpl. + bdestruct (n =? i). + rewrite (Msum_eq_bounded _ _ (fun _ : nat => Zero)). + rewrite Msum_0. subst. lma. reflexivity. + intros x ?. apply H; lia. + rewrite IHn; try lia. + rewrite H by lia. lma. + intros. apply H; lia. +Qed. + +Lemma Msum_diagonal : + forall {d1 d2} n (f : nat -> nat -> Matrix d1 d2), + (forall i j, (i < n)%nat -> (j < n)%nat -> (i <> j)%nat -> f i j = Zero) -> + Msum n (fun i => Msum n (fun j => f i j)) = Msum n (fun i => f i i). +Proof. + intros. apply Msum_eq_bounded. intros. + apply Msum_unique. + exists i. auto. +Qed. + (*****************************************************) (* Defining matrix altering/col operations functions *) (*****************************************************) -Local Open Scope nat_scope. +>>>>>>> QuantumLib/main Definition get_vec {n m} (i : nat) (S : Matrix n m) : Vector n := fun x y => (if (y =? 0) then S x i else C0). @@ -1788,26 +2227,43 @@ Definition get_row {n m} (i : nat) (S : Matrix n m) : Matrix 1 m := fun x y => (if (x =? 0) then S i y else C0). +<<<<<<< HEAD Definition reduce_row {n m} (A : Matrix n m) (row : nat) : Matrix (n - 1) m := +======= +Definition reduce_row {n m} (A : Matrix (S n) m) (row : nat) : Matrix n m := +>>>>>>> QuantumLib/main fun x y => if x >>>>>> QuantumLib/main fun x y => if y if x if x >>>>>> QuantumLib/main then v x y else v (1 + x) y. (* More specific form for squares *) +<<<<<<< HEAD Definition reduce {n} (A : Square n) (row col : nat) : Square (n - 1) := +======= +Definition reduce {n} (A : Square (S n)) (row col : nat) : Square n := +>>>>>>> QuantumLib/main fun x y => (if x WF_Matrix A -> WF_Matrix (reduce_row A row). +======= +Lemma WF_reduce_row : forall {n m} (row : nat) (A : Matrix (S n) m), + row < (S n) -> WF_Matrix A -> WF_Matrix (reduce_row A row). +>>>>>>> QuantumLib/main Proof. unfold WF_Matrix, reduce_row. intros. bdestruct (x b < c -> 1 + a < c). { lia. } +<<<<<<< HEAD apply (nibzo x row n) in H2. +======= + apply (nibzo x row (S n)) in H2. +>>>>>>> QuantumLib/main simpl in H2. lia. apply H. + apply H0; auto. - apply H0. destruct H1. @@ -1962,15 +2427,24 @@ Proof. unfold WF_Matrix, reduce_row. intros. Qed. +<<<<<<< HEAD Lemma WF_reduce_col : forall {n m} (col : nat) (A : Matrix n m), col < m -> WF_Matrix A -> WF_Matrix (reduce_col A col). +======= +Lemma WF_reduce_col : forall {n m} (col : nat) (A : Matrix n (S m)), + col < (S m) -> WF_Matrix A -> WF_Matrix (reduce_col A col). +>>>>>>> QuantumLib/main Proof. unfold WF_Matrix, reduce_col. intros. bdestruct (y b < c -> 1 + a < c). { lia. } +<<<<<<< HEAD apply (nibzo y col m) in H2. +======= + apply (nibzo y col (S m)) in H2. +>>>>>>> QuantumLib/main simpl in H2. lia. apply H. - apply H0. destruct H1. + left. apply H1. @@ -1978,23 +2452,38 @@ Proof. unfold WF_Matrix, reduce_col. intros. Qed. +<<<<<<< HEAD Lemma rvn_is_rr_n : forall {n : nat} (v : Vector n), reduce_vecn v = reduce_row v (n - 1). +======= +Lemma rvn_is_rr_n : forall {n : nat} (v : Vector (S n)), + reduce_vecn v = reduce_row v n. +>>>>>>> QuantumLib/main Proof. intros. prep_matrix_equality. unfold reduce_row, reduce_vecn. easy. Qed. +<<<<<<< HEAD Lemma WF_reduce_vecn : forall {n} (v : Vector n), n <> 0 -> WF_Matrix v -> WF_Matrix (reduce_vecn v). Proof. intros. +======= +Lemma WF_reduce_vecn : forall {n} (v : Vector (S n)), + n <> 0 -> WF_Matrix v -> WF_Matrix (reduce_vecn v). +Proof. intros. +>>>>>>> QuantumLib/main rewrite rvn_is_rr_n. apply WF_reduce_row; try lia; try easy. Qed. +<<<<<<< HEAD Lemma reduce_is_redrow_redcol : forall {n} (A : Square n) (row col : nat), +======= +Lemma reduce_is_redrow_redcol : forall {n} (A : Square (S n)) (row col : nat), +>>>>>>> QuantumLib/main reduce A row col = reduce_col (reduce_row A row) col. Proof. intros. prep_matrix_equality. @@ -2003,7 +2492,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma reduce_is_redcol_redrow : forall {n} (A : Square n) (row col : nat), +======= +Lemma reduce_is_redcol_redrow : forall {n} (A : Square (S n)) (row col : nat), +>>>>>>> QuantumLib/main reduce A row col = reduce_row (reduce_col A col) row. Proof. intros. prep_matrix_equality. @@ -2012,8 +2505,13 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma WF_reduce : forall {n} (A : Square n) (row col : nat), n <> 0 -> row < n -> col < n -> WF_Matrix A -> WF_Matrix (reduce A row col). +======= +Lemma WF_reduce : forall {n} (A : Square (S n)) (row col : nat), + row < S n -> col < S n -> WF_Matrix A -> WF_Matrix (reduce A row col). +>>>>>>> QuantumLib/main Proof. intros. rewrite reduce_is_redrow_redcol. apply WF_reduce_col; try easy. @@ -2236,10 +2734,17 @@ Hint Resolve WF_get_vec WF_get_row WF_reduce_row WF_reduce_col WF_reduce_vecn WF Hint Resolve WF_col_swap WF_row_swap WF_col_scale WF_row_scale WF_col_add WF_row_add : wf_db. Hint Resolve WF_gen_new_vec WF_gen_new_row WF_col_add_many WF_row_add_many : wf_db. Hint Resolve WF_col_append WF_row_append WF_row_wedge WF_col_wedge WF_smash : wf_db. +<<<<<<< HEAD Hint Resolve WF_col_add_each WF_row_add_each WF_make_col_zero WF_make_row_zero : wf_db. Lemma get_vec_reduce_col : forall {n m} (i col : nat) (A : Matrix n m), +======= +Hint Resolve WF_col_add_each WF_row_add_each WF_make_col_zero WF_make_row_zero WF_make_WF : wf_db. +Hint Extern 1 (Nat.lt _ _) => lia : wf_db. + +Lemma get_vec_reduce_col : forall {n m} (i col : nat) (A : Matrix n (S m)), +>>>>>>> QuantumLib/main i < col -> get_vec i (reduce_col A col) = get_vec i A. Proof. intros. prep_matrix_equality. @@ -2277,7 +2782,11 @@ Proof. intros. prep_matrix_equality. Qed. +<<<<<<< HEAD Lemma col_scale_reduce_col_same : forall {n m} (T : Matrix n m) (y col : nat) (a : C), +======= +Lemma col_scale_reduce_col_same : forall {n m} (T : Matrix n (S m)) (y col : nat) (a : C), +>>>>>>> QuantumLib/main y = col -> reduce_col (col_scale T col a) y = reduce_col T y. Proof. intros. prep_matrix_equality. @@ -2286,7 +2795,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_swap_reduce_before : forall {n : nat} (T : Square n) (row col c1 c2 : nat), +======= +Lemma col_swap_reduce_before : forall {n : nat} (T : Square (S n)) (row col c1 c2 : nat), +>>>>>>> QuantumLib/main col < (S c1) -> col < (S c2) -> reduce (col_swap T (S c1) (S c2)) row col = col_swap (reduce T row col) c1 c2. Proof. intros. @@ -2299,7 +2812,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_scale_reduce_before : forall {n : nat} (T : Square n) (x y col : nat) (a : C), +======= +Lemma col_scale_reduce_before : forall {n : nat} (T : Square (S n)) (x y col : nat) (a : C), +>>>>>>> QuantumLib/main y < col -> reduce (col_scale T col a) x y = col_scale (reduce T x y) (col - 1) a. Proof. intros. prep_matrix_equality. @@ -2311,7 +2828,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_scale_reduce_same : forall {n : nat} (T : Square n) (x y col : nat) (a : C), +======= +Lemma col_scale_reduce_same : forall {n : nat} (T : Square (S n)) (x y col : nat) (a : C), +>>>>>>> QuantumLib/main y = col -> reduce (col_scale T col a) x y = reduce T x y. Proof. intros. prep_matrix_equality. @@ -2321,7 +2842,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_scale_reduce_after : forall {n : nat} (T : Square n) (x y col : nat) (a : C), +======= +Lemma col_scale_reduce_after : forall {n : nat} (T : Square (S n)) (x y col : nat) (a : C), +>>>>>>> QuantumLib/main y > col -> reduce (col_scale T col a) x y = col_scale (reduce T x y) col a. Proof. intros. prep_matrix_equality. @@ -2331,7 +2856,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma mcz_reduce_col_same : forall {n m} (T : Matrix n m) (col : nat), +======= +Lemma mcz_reduce_col_same : forall {n m} (T : Matrix n (S m)) (col : nat), +>>>>>>> QuantumLib/main reduce_col (make_col_zero col T) col = reduce_col T col. Proof. intros. prep_matrix_equality. @@ -2340,7 +2869,11 @@ Proof. intros. bdestruct (y =? col); bdestruct (1 + y =? col); try lia; easy. Qed. +<<<<<<< HEAD Lemma mrz_reduce_row_same : forall {n m} (T : Matrix n m) (row : nat), +======= +Lemma mrz_reduce_row_same : forall {n m} (T : Matrix (S n) m) (row : nat), +>>>>>>> QuantumLib/main reduce_row (make_row_zero row T) row = reduce_row T row. Proof. intros. prep_matrix_equality. @@ -2349,7 +2882,12 @@ Proof. intros. bdestruct (x =? row); bdestruct (1 + x =? row); try lia; easy. Qed. +<<<<<<< HEAD Lemma col_add_many_reduce_col_same : forall {n m} (T : Matrix n m) (v : Vector m) (col : nat), +======= +Lemma col_add_many_reduce_col_same : forall {n m} (T : Matrix n (S m)) (v : Vector (S m)) + (col : nat), +>>>>>>> QuantumLib/main reduce_col (col_add_many col v T) col = reduce_col T col. Proof. intros. unfold reduce_col, col_add_many. @@ -2358,7 +2896,12 @@ Proof. intros. bdestruct (y =? col); bdestruct (1 + y =? col); try lia; easy. Qed. +<<<<<<< HEAD Lemma row_add_many_reduce_row_same : forall {n m} (T : Matrix n m) (v : Matrix 1 n) (row : nat), +======= +Lemma row_add_many_reduce_row_same : forall {n m} (T : Matrix (S n) m) (v : Matrix 1 (S n)) + (row : nat), +>>>>>>> QuantumLib/main reduce_row (row_add_many row v T) row = reduce_row T row. Proof. intros. unfold reduce_row, row_add_many. @@ -2367,7 +2910,12 @@ Proof. intros. bdestruct (x =? row); bdestruct (1 + x =? row); try lia; easy. Qed. +<<<<<<< HEAD Lemma col_wedge_reduce_col_same : forall {n m} (T : Matrix n m) (v : Vector m) (col : nat), +======= +Lemma col_wedge_reduce_col_same : forall {n m} (T : Matrix n m) (v : Vector m) + (col : nat), +>>>>>>> QuantumLib/main reduce_col (col_wedge T v col) col = T. Proof. intros. prep_matrix_equality. @@ -2378,7 +2926,12 @@ Proof. intros. all : rewrite p; easy. Qed. +<<<<<<< HEAD Lemma row_wedge_reduce_row_same : forall {n m} (T : Matrix n m) (v : Matrix 1 n) (row : nat), +======= +Lemma row_wedge_reduce_row_same : forall {n m} (T : Matrix n m) (v : Matrix 1 n) + (row : nat), +>>>>>>> QuantumLib/main reduce_row (row_wedge T v row) row = T. Proof. intros. prep_matrix_equality. @@ -2389,18 +2942,30 @@ Proof. intros. all : rewrite p; easy. Qed. +<<<<<<< HEAD Lemma col_add_many_reduce_row : forall {n m} (T : Matrix n m) (v : Vector m) (col row : nat), +======= +Lemma col_add_many_reduce_row : forall {n m} (T : Matrix (S n) m) (v : Vector m) (col row : nat), +>>>>>>> QuantumLib/main col_add_many col v (reduce_row T row) = reduce_row (col_add_many col v T) row. Proof. intros. prep_matrix_equality. unfold col_add_many, reduce_row, gen_new_vec, scale, get_vec. bdestruct (y =? col); try lia; try easy. bdestruct (x >>>>>> QuantumLib/main do 2 rewrite Msum_Csum. apply Csum_eq_bounded; intros. bdestruct (x >>>>>> QuantumLib/main reduce_col (reduce_row A i) j = reduce_row (reduce_col A j) i. Proof. intros. prep_matrix_equality. unfold reduce_col, reduce_row. bdestruct (y >>>>>> QuantumLib/main reduce_col (reduce_col (col_swap A 0 1) 0) 0 = reduce_col (reduce_col A 0) 0. Proof. intros. prep_matrix_equality. @@ -2511,7 +3084,11 @@ Proof. intros. easy. Qed. +<<<<<<< HEAD Lemma reduce_reduce_0 : forall {n} (A : Square n) (x y : nat), +======= +Lemma reduce_reduce_0 : forall {n} (A : Square (S (S n))) (x y : nat), +>>>>>>> QuantumLib/main x <= y -> (reduce (reduce A x 0) y 0) = (reduce (reduce A (S y) 0) x 0). Proof. intros. @@ -2524,7 +3101,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_add_split : forall {n} (A : Square n) (i : nat) (c : C), +======= +Lemma col_add_split : forall {n} (A : Square (S n)) (i : nat) (c : C), +>>>>>>> QuantumLib/main col_add A 0 i c = col_wedge (reduce_col A 0) (get_vec 0 A .+ c.* get_vec i A) 0. Proof. intros. prep_matrix_equality. @@ -2576,7 +3157,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_swap_reduce_row : forall {n m : nat} (S : Matrix n m) (x y row : nat), +======= +Lemma col_swap_reduce_row : forall {n m : nat} (S : Matrix (S n) m) (x y row : nat), +>>>>>>> QuantumLib/main col_swap (reduce_row S row) x y = reduce_row (col_swap S x y) row. Proof. intros. prep_matrix_equality. @@ -2642,8 +3227,12 @@ Lemma row_add_swap : forall {n m : nat} (S : Matrix n m) (x y : nat) (a : C), Proof. intros. prep_matrix_equality. unfold row_swap, row_add. +<<<<<<< HEAD bdestruct (x0 =? x); bdestruct (y =? x); bdestruct (x0 =? y); bdestruct (x =? x); try lia; easy. +======= + bdestruct_all; easy. +>>>>>>> QuantumLib/main Qed. @@ -2665,14 +3254,62 @@ Proof. intros. lca. easy. Qed. +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main Lemma mat_equiv_make_WF : forall {n m} (T : Matrix n m), T == make_WF T. Proof. unfold make_WF, mat_equiv; intros. bdestruct (i T = make_WF T. +Proof. intros. + apply mat_equiv_eq; auto with wf_db. + apply mat_equiv_make_WF. +Qed. + + +Lemma col_swap_make_WF : forall {n m} (T : Matrix n m) (x y : nat), + x < m -> y < m -> col_swap (make_WF T) x y = make_WF (col_swap T x y). +Proof. intros. + unfold make_WF, col_swap. + prep_matrix_equality. + bdestruct_all; try easy. +Qed. + +Lemma col_scale_make_WF : forall {n m} (T : Matrix n m) (x : nat) (c : C), + col_scale (make_WF T) x c = make_WF (col_scale T x c). +Proof. intros. + unfold make_WF, col_scale. + prep_matrix_equality. + bdestruct_all; try easy; lca. +Qed. + +Lemma col_add_make_WF : forall {n m} (T : Matrix n m) (x y : nat) (c : C), + x < m -> y < m -> col_add (make_WF T) x y c = make_WF (col_add T x y c). +Proof. intros. + unfold make_WF, col_add. + prep_matrix_equality. + bdestruct_all; try easy; lca. +Qed. + +Lemma Mmult_make_WF : forall {n m o} (A : Matrix n m) (B : Matrix m o), + make_WF A × make_WF B = make_WF (A × B). +Proof. intros. + apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; intros. + unfold make_WF, Mmult. + bdestruct (i >>>>>> QuantumLib/main Lemma gen_new_vec_0 : forall {n m} (T : Matrix n m) (as' : Vector m), as' == Zero -> gen_new_vec n m T as' = Zero. @@ -2714,7 +3351,11 @@ Lemma row_add_many_0 : forall {n m} (row : nat) (T : Matrix n m) (as' : Matrix 1 as' == Zero -> T = row_add_many row as' T. Proof. intros. unfold row_add_many in *. +<<<<<<< HEAD prep_matrix_equality. +======= + prep_matrix_equality. +>>>>>>> QuantumLib/main bdestruct (x =? row); try easy. rewrite gen_new_row_0; try easy. unfold Zero; lca. @@ -2788,14 +3429,22 @@ Proof. intros. bdestruct (y =? col); try easy. bdestruct (e =? col); try lia. rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main assert (H' : m = e + (m - e)). lia. rewrite H'. do 2 rewrite Msum_Csum. rewrite Csum_sum. rewrite Csum_sum. rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main apply Csum_eq_bounded; intros. unfold make_row_zero. bdestruct (x0 =? e); try lia; easy. @@ -2806,7 +3455,11 @@ Proof. intros. unfold scale. rewrite Cmult_0_l, Cplus_0_l. rewrite Cplus_comm. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main apply Csum_eq_bounded; intros. bdestruct (e + S x0 =? e); try lia; easy. unfold get_vec. simpl. @@ -2814,17 +3467,26 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_add_many_cancel : forall {n m} (T : Matrix n m) (as' : Vector m) (col : nat), col < m -> as' col 0 = C0 -> (reduce_col T col) × (reduce_row as' col) = -C1 .* (get_vec col T) -> (forall i : nat, (col_add_many col as' T) i col = C0). Proof. intros. destruct m; try lia. +======= +Lemma col_add_many_cancel : forall {n m} (T : Matrix n (S m)) (as' : Vector (S m)) (col : nat), + col < (S m) -> as' col 0 = C0 -> + (reduce_col T col) × (reduce_row as' col) = -C1 .* (get_vec col T) -> + (forall i : nat, (col_add_many col as' T) i col = C0). +Proof. intros. +>>>>>>> QuantumLib/main unfold col_add_many, gen_new_vec. bdestruct (col =? col); try lia. rewrite Msum_Csum. assert (H' : (Csum (fun x : nat => (as' x 0 .* get_vec x T) i 0) (S m) = (@Mmult n m 1 (reduce_col T col) (reduce_row as' col)) i 0)%C). +<<<<<<< HEAD { unfold Mmult. assert (p : S m = col + (S (m - col))). lia. assert (p1 : m = col + (m - col)). lia. @@ -2836,15 +3498,29 @@ Proof. intros. bdestruct (x >>>>>> QuantumLib/main unfold scale; rewrite Cmult_0_l, Cplus_0_l. apply Csum_eq_bounded; intros. unfold get_vec, scale, reduce_col, reduce_row. bdestruct (col + x >>>>>> QuantumLib/main unfold scale, get_vec. bdestruct (0 =? 0); try lia. lca. @@ -2859,7 +3535,11 @@ Proof. intros. bdestruct (y =? col); try easy. rewrite <- (Cplus_0_r (S x y)). rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify; try lca. +======= + apply Cplus_simplify; try lca. +>>>>>>> QuantumLib/main do 2 rewrite Msum_Csum. rewrite <- Csum_plus. rewrite Csum_0_bounded; try lca. @@ -2992,7 +3672,11 @@ Proof. intros. prep_matrix_equality. unfold row_add_many, col_add_many, transpose. bdestruct (x =? col); try easy. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main unfold gen_new_vec, gen_new_row, get_vec, get_row, scale. do 2 rewrite Msum_Csum. apply Csum_eq_bounded; intros. @@ -3005,7 +3689,11 @@ Proof. intros. prep_matrix_equality. unfold row_add_many, col_add_many, transpose. bdestruct (y =? row); try easy. +<<<<<<< HEAD apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main unfold gen_new_vec, gen_new_row, get_vec, get_row, scale. do 2 rewrite Msum_Csum. apply Csum_eq_bounded; intros. @@ -3040,7 +3728,11 @@ Proof. intros. bdestruct (x >>>>>> QuantumLib/main apply Csum_eq_bounded. intros. unfold col_swap, row_swap. @@ -3053,7 +3745,11 @@ Proof. intros. rewrite (le_plus_minus (y - x - 1) x'); try lia. do 2 rewrite Csum_sum. do 2 rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main apply Csum_eq_bounded. intros. unfold col_swap, row_swap. @@ -3063,7 +3759,11 @@ Proof. intros. rewrite Cplus_comm. rewrite (Cplus_comm _ (col_swap A x y x0 (x + 0)%nat * row_swap B x y (x + 0)%nat y0)%C). do 2 rewrite Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main do 2 rewrite <- plus_n_O. unfold col_swap, row_swap. bdestruct (x + S (y - x - 1) =? x); bdestruct (x + S (y - x - 1) =? y); @@ -3103,7 +3803,11 @@ Proof. intros. Qed. +<<<<<<< HEAD Lemma col_add_preserves_mul_lt : forall {n m o} (A : Matrix n m) (B : Matrix m o) +======= +Lemma add_preserves_mul_lt : forall {n m o} (A : Matrix n m) (B : Matrix m o) +>>>>>>> QuantumLib/main (x y : nat) (a : C), x < y -> x < m -> y < m -> A × (row_add B y x a) = (col_add A x y a) × B. Proof. intros. @@ -3112,7 +3816,11 @@ Proof. intros. bdestruct (x >>>>>> QuantumLib/main apply Csum_eq_bounded. intros. unfold row_add, col_add. @@ -3125,7 +3833,11 @@ Proof. intros. rewrite (le_plus_minus (y - x - 1) x'); try lia. do 2 rewrite Csum_sum. do 2 rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main apply Csum_eq_bounded. intros. unfold row_add, col_add. @@ -3135,7 +3847,11 @@ Proof. intros. rewrite Cplus_comm. rewrite (Cplus_comm _ (col_add A x y a x0 (x + 0)%nat * B (x + 0)%nat y0)%C). do 2 rewrite Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify. +======= + apply Cplus_simplify. +>>>>>>> QuantumLib/main unfold row_add, col_add. do 2 rewrite <- plus_n_O. bdestruct (x =? y); bdestruct (x =? x); @@ -3148,11 +3864,19 @@ Proof. intros. bdestruct (x + S (y - x - 1 + S x1) =? x); try lia; easy. Qed. +<<<<<<< HEAD Lemma col_add_preserves_mul : forall {n m o} (A : Matrix n m) (B : Matrix m o) (x y : nat) (a : C), x < m -> y < m -> A × (row_add B y x a) = (col_add A x y a) × B. Proof. intros. bdestruct (x y < m -> A × (row_add B y x a) = (col_add A x y a) × B. +Proof. intros. bdestruct (x >>>>>> QuantumLib/main - destruct H1. + rewrite col_add_double, row_add_double. apply scale_preserves_mul. @@ -3162,7 +3886,11 @@ Proof. intros. bdestruct (x >>>>>> QuantumLib/main Qed. @@ -3202,10 +3930,17 @@ Proof. intros. unfold col_add, col_add_many. bdestruct (y =? col); try lia; try easy. repeat rewrite <- Cplus_assoc. +<<<<<<< HEAD apply Csum_simplify; try easy. bdestruct (to_add =? col); try lia. rewrite Cplus_comm. apply Csum_simplify; try easy. +======= + apply Cplus_simplify; try easy. + bdestruct (to_add =? col); try lia. + rewrite Cplus_comm. + apply Cplus_simplify; try easy. +>>>>>>> QuantumLib/main unfold gen_new_vec. do 2 rewrite Msum_Csum. apply Csum_eq_bounded; intros. @@ -3228,7 +3963,11 @@ Proof. induction e as [| e]. rewrite <- (col_add_many_0 col A (make_row_zero (skip_count col 0) v)). rewrite (row_add_each_row_add col (skip_count col 0) _ _); try easy. rewrite <- (row_add_each_0 col B (make_row_zero (skip_count col 0) v)). +<<<<<<< HEAD apply col_add_preserves_mul; try easy. +======= + apply add_preserves_mul; try easy. +>>>>>>> QuantumLib/main apply mat_equiv_eq; auto with wf_db. unfold mat_equiv; intros. destruct j; try lia. @@ -3255,7 +3994,11 @@ Proof. induction e as [| e]. destruct m; try easy. rewrite (col_add_many_col_add col (skip_count col (S e)) _ _); try easy. rewrite (row_add_each_row_add col (skip_count col (S e)) _ _); try easy. +<<<<<<< HEAD rewrite col_add_preserves_mul; try easy. +======= + rewrite add_preserves_mul; try easy. +>>>>>>> QuantumLib/main rewrite cam_ca_switch. rewrite IHe; try easy; auto with wf_db. assert (p : e < S e). lia. @@ -3345,6 +4088,16 @@ Proof. intros. rewrite Mmult_1_r; auto with wf_db. Qed. +<<<<<<< HEAD +======= +Lemma col_add_mult_r : forall {n} (A : Square n) (x y : nat) (a : C), + x < n -> y < n -> WF_Matrix A -> + col_add A x y a = A × (row_add (I n) y x a). +Proof. intros. + rewrite add_preserves_mul; auto. + rewrite Mmult_1_r; auto with wf_db. +Qed. +>>>>>>> QuantumLib/main Lemma col_add_many_mult_r : forall {n} (A : Square n) (v : Vector n) (col : nat), WF_Matrix A -> WF_Matrix v -> col < n -> v col 0 = C0 -> @@ -3364,15 +4117,64 @@ Proof. intros. Qed. +<<<<<<< HEAD +======= +(* now we prove facts about the ops on (I n) *) +Lemma col_row_swap_invr_I : forall (n x y : nat), + x < n -> y < n -> col_swap (I n) x y = row_swap (I n) x y. +Proof. intros. + prep_matrix_equality. + unfold col_swap, row_swap, I. + bdestruct_all; try easy. +Qed. + +Lemma col_row_scale_invr_I : forall (n x : nat) (c : C), + col_scale (I n) x c = row_scale (I n) x c. +Proof. intros. + prep_matrix_equality. + unfold col_scale, row_scale, I. + bdestruct_all; try easy; lca. +Qed. + +Lemma col_row_add_invr_I : forall (n x y : nat) (c : C), + x < n -> y < n -> col_add (I n) x y c = row_add (I n) y x c. +Proof. intros. + prep_matrix_equality. + unfold col_add, row_add, I. + bdestruct_all; try easy; try lca. +Qed. + + +Lemma row_each_col_many_invr_I : forall (n col : nat) (v : Vector n), + WF_Matrix v -> col < n -> v col 0 = C0 -> + row_add_each col v (I n) = col_add_many col v (I n). +Proof. intros. + rewrite <- Mmult_1_r, <- col_add_many_preserves_mul, Mmult_1_l; auto with wf_db. +Qed. + + +Lemma row_many_col_each_invr_I : forall (n col : nat) (v : Matrix 1 n), + WF_Matrix v -> col < n -> v 0 col = C0 -> + row_add_many col v (I n) = col_add_each col v (I n). +Proof. intros. + rewrite <- Mmult_1_r, <- col_add_each_preserves_mul, Mmult_1_l; auto with wf_db. +Qed. + +>>>>>>> QuantumLib/main Lemma reduce_append_split : forall {n m} (T : Matrix n (S m)), WF_Matrix T -> T = col_append (reduce_col T m) (get_vec m T). Proof. intros. prep_matrix_equality. unfold col_append, get_vec, reduce_col. +<<<<<<< HEAD bdestruct (y =? S m - 1); bdestruct (0 =? 0); bdestruct (y >>>>>> QuantumLib/main Qed. @@ -3451,12 +4253,18 @@ Proof. induction n as [| n']. rewrite H1. destruct j. apply e. lia. +<<<<<<< HEAD apply (m i j) in H0. unfold reduce_vecn in H0. assert (H' : i >>>>>> QuantumLib/main * right. unfold not. intros. unfold mat_equiv in H. apply n. apply H; lia. @@ -3465,9 +4273,13 @@ Proof. induction n as [| n']. intros. apply n. unfold mat_equiv in *. intros. unfold reduce_vecn. +<<<<<<< HEAD assert (H' : i >>>>>> QuantumLib/main apply H; lia. Qed. @@ -3506,11 +4318,19 @@ Qed. (* we can also now prove some useful lemmas about nonzero vectors *) +<<<<<<< HEAD Lemma last_zero_simplification : forall {n : nat} (v : Vector n), WF_Matrix v -> v (n - 1) 0 = C0 -> v = reduce_vecn v. Proof. intros. unfold reduce_vecn. prep_matrix_equality. bdestruct (x v n 0 = C0 -> v = reduce_vecn v. +Proof. intros. unfold reduce_vecn. + prep_matrix_equality. + bdestruct (x >>>>>> QuantumLib/main - easy. - unfold WF_Matrix in H. destruct H1. @@ -3576,23 +4396,32 @@ Proof. induction n as [| n']. easy. } easy. * assert (H1 : exists x, (reduce_row v n') x 0 <> C0). +<<<<<<< HEAD { apply IHn'. assert (H1' := (@WF_reduce_row (S n') 1 n')). rewrite easy_sub in *. apply H1'; try lia; try easy. +======= + { apply IHn'; auto with wf_db. +>>>>>>> QuantumLib/main unfold not in *. intros. apply n. rewrite H1. easy. } destruct H1. exists x. +<<<<<<< HEAD rewrite (last_zero_simplification v); try easy. rewrite rvn_is_rr_n. all : rewrite easy_sub. apply H1. apply e. +======= + rewrite (last_zero_simplification v); try easy. +>>>>>>> QuantumLib/main + exists n'. apply n. Qed. +<<<<<<< HEAD (***********************************************************) (* Defining linear independence, and proving lemmas etc... *) (***********************************************************) @@ -5511,6 +6340,21 @@ Qed. (*******************************) (* Restoring Matrix Dimensions *) (*******************************) +======= + + +(* Note on "using [tactics]": Most generated subgoals will be of the form + WF_Matrix M, where auto with wf_db will work. + Occasionally WF_Matrix M will rely on rewriting to match an assumption in the + context, here we recursively autorewrite (which adds time). + kron_1_l requires proofs of (n > 0)%nat, here we use lia. *) + +(* *) + +(*******************************) +(* Restoring Matrix Dimensions *) +(*******************************) +>>>>>>> QuantumLib/main (** Restoring Matrix dimensions *) Ltac is_nat n := match type of n with nat => idtac end. @@ -5594,11 +6438,15 @@ Ltac restore_dims_rec A := | Matrix ?m'' ?n'' => constr:(@Mplus m' n' A' B') end end +<<<<<<< HEAD <<<<<<< HEAD | ?c .* ?A => let A' := restore_dims_rec A in ======= | ?c .* ?AA => let A' := restore_dims_rec A in >>>>>>> Heisenberg-Foundations/main +======= + | ?c .* ?AA => let A' := restore_dims_rec A in +>>>>>>> QuantumLib/main match type of A' with | Matrix ?m' ?n' => constr:(@scale m' n' c A') end @@ -5893,8 +6741,11 @@ Ltac solve_matrix := assoc_least; Eg: ((..×..×..)⊗(..×..×..)⊗(..×..×..)) .+ ((..×..)⊗(..×..)) *) +<<<<<<< HEAD Local Open Scope nat_scope. +======= +>>>>>>> QuantumLib/main Lemma repad_lemma1_l : forall (a b d : nat), a < b -> d = (b - a - 1) -> b = a + 1 + d. Proof. intros. subst. lia. Qed. @@ -5919,6 +6770,7 @@ Proof. intros. exists (b - a - 1). lia. Qed. Lemma lt_ex_diff_r : forall a b, a < b -> exists d, b = a + 1 + d. Proof. intros. exists (b - a - 1). lia. Qed. +<<<<<<< HEAD <<<<<<< HEAD ======= Ltac bdestruct_all := @@ -5929,6 +6781,8 @@ Ltac bdestruct_all := end; try (exfalso; lia). >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (* Remove _ < _ from hyps, remove _ - _ from goal *) Ltac remember_differences := repeat match goal with diff --git a/Prelim.v b/Prelim.v index bc4fe07..de47708 100644 --- a/Prelim.v +++ b/Prelim.v @@ -7,10 +7,30 @@ Require Export List. Export ListNotations. +<<<<<<< HEAD <<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +(* Some more than basic nat lemmas that are useful to have *) + +Lemma easy_sub : forall (n : nat), S n - 1 = n. Proof. lia. Qed. + +Lemma easy_sub3 : forall (n k : nat), n <> 0 -> n + k - 0 - 1 = n - 0 - 1 + k. +Proof. intros. + destruct n as [| n]. + - easy. + - simpl. lia. +Qed. + +Lemma easy_sub6 : forall (a c b : nat), + b < c -> a < b -> c = (a + S (b - a) + (c - b - 1)). +Proof. intros. lia. Qed. + + +>>>>>>> QuantumLib/main (* Boolean notations, lemmas *) Notation "¬ b" := (negb b) (at level 10). @@ -58,14 +78,21 @@ Ltac bdestruct X := Ltac bdestructΩ X := bdestruct X; simpl; try lia. <<<<<<< HEAD +<<<<<<< HEAD +======= +>>>>>>> QuantumLib/main Ltac bdestruct_all := repeat match goal with | |- context[?a bdestruct (a bdestruct (a <=? b) | |- context[?a =? ?b] => bdestruct (a =? b) end; try (exfalso; lia). +<<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main (* Distribute functions over lists *) @@ -229,6 +256,7 @@ Definition maybe {A} (o : option A) (default : A) : A := end. +<<<<<<< HEAD <<<<<<< HEAD (* Why are we defining this from scratch??? *) Fixpoint inb (a : nat) (ls : list nat) : bool := @@ -329,6 +357,8 @@ Proof. Qed. ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (************************************) (* Helpful, general purpose tactics *) @@ -417,7 +447,10 @@ Ltac unify_pows_two := | [ |- (2^?x = 2^?y)%nat ] => apply pow_components; try lia end. <<<<<<< HEAD +<<<<<<< HEAD +======= ======= +>>>>>>> QuantumLib/main @@ -515,6 +548,339 @@ Proof. intros X l1 l2 l3. Qed. +<<<<<<< HEAD Hint Resolve subset_concat_l subset_concat_r subset_self subsets_add subset_trans : sub_db. >>>>>>> Heisenberg-Foundations/main +======= +Hint Resolve subset_concat_l subset_concat_r subset_self subsets_add subset_trans : sub_db. + + +Lemma firstn_subset : forall {X : Type} (n : nat) (ls : list X), + firstn n ls ⊆ ls. +Proof. induction n as [| n']. + - easy. + - intros. destruct ls. + easy. simpl. + unfold subset_gen in *. + intros. + destruct H as [H | H]. + left; easy. + right; apply IHn'; apply H. +Qed. + +Lemma skipn_subset : forall {X : Type} (n : nat) (ls : list X), + skipn n ls ⊆ ls. +Proof. induction n as [| n']. + - easy. + - intros. destruct ls. + easy. simpl. + unfold subset_gen in *. + intros. + right; apply IHn'; apply H. +Qed. + + +Hint Resolve firstn_subset skipn_subset : sub_db. + +(******************************) +(* Some more basic list stuff *) +(******************************) + + +Definition zipWith {X Y Z: Type} (f : X -> Y -> Z) (As : list X) (Bs : list Y) : list Z := + map (uncurry f) (combine As Bs). + + +Lemma zipWith_len_pres : forall {X Y Z : Type} (f : X -> Y -> Z) (n : nat) + (As : list X) (Bs : list Y), + length As = n -> length Bs = n -> length (zipWith f As Bs) = n. +Proof. intros. + unfold zipWith. + rewrite map_length. + rewrite combine_length. + rewrite H, H0; lia. +Qed. + + +Lemma zipWith_app_product : forall {X Y Z: Type} (f : X -> Y -> Z) (n : nat) + (l0s l2s : list X) (l1s l3s : list Y), + length l0s = n -> length l1s = n -> + (zipWith f l0s l1s) ++ (zipWith f l2s l3s) = zipWith f (l0s ++ l2s) (l1s ++ l3s). +Proof. induction n as [| n']. + - intros. destruct l0s; destruct l1s; easy. + - intros. destruct l0s; destruct l1s; try easy. + unfold zipWith in *. + simpl in *. + rewrite <- IHn'; try nia. + reflexivity. +Qed. + + +Lemma zipWith_cons : forall {X Y Z : Type} (f : X -> Y -> Z) (a : X) (b : Y) (A : list X) (B : list Y), + zipWith f (a :: A) (b :: B) = (f a b) :: (zipWith f A B). +Proof. intros. + unfold zipWith. simpl. + unfold uncurry. + simpl. easy. +Qed. + + +Fixpoint first_n (n : nat) : list nat := + match n with + | 0 => [0] + | S n' => n :: first_n n' + end. + +Lemma first_n_contains : forall (n i : nat), + i <= n <-> In i (first_n n). +Proof. split. + - induction n as [| n']. + * intros. bdestruct (i =? 0). + + rewrite H0. simpl. left. easy. + + apply le_n_0_eq in H. rewrite H in H0. easy. + * intros. simpl. bdestruct (i =? S n'). + + left. rewrite H0. easy. + + right. apply IHn'. + apply le_lt_eq_dec in H. destruct H. + ** apply Nat.lt_succ_r. apply l. + ** rewrite e in H0. easy. + - induction n as [| n']. + * intros [H | F]. + + rewrite H. easy. + + simpl in F. easy. + * intros. simpl in H. destruct H. + + rewrite H. easy. + + apply IHn' in H. + apply le_n_S in H. apply le_Sn_le. + apply H. +Qed. + + +(* defining switch and many lemmas having to do with switch and nth *) + +Fixpoint switch {X : Type} (ls : list X) (x : X) (n : nat) := + match ls with + | [] => [] + | (h :: ls') => + match n with + | 0 => x :: ls' + | S n' => h :: (switch ls' x n') + end + end. + +Lemma switch_len : forall {X : Type} (n : nat) (ls : list X) (x : X), + length (switch ls x n) = length ls. +Proof. induction n as [| n']. + - destruct ls. easy. easy. + - intros. destruct ls. + easy. simpl. + rewrite IHn'. + reflexivity. +Qed. + + +Lemma switch_map : forall {X Y : Type} (n : nat) (ls : list X) (x : X) (f : X -> Y), + map f (switch ls x n) = switch (map f ls) (f x) n. +Proof. induction n as [| n']. + - intros. destruct ls; easy. + - intros. destruct ls. easy. + simpl. rewrite IHn'. easy. +Qed. + +Lemma switch_switch_diff : forall {X : Type} (n m : nat) (ls : list X) (a b : X), + n <> m -> + switch (switch ls a n) b m = switch (switch ls b m) a n. +Proof. induction n as [| n']. + - intros. + destruct m; destruct ls; easy. + - intros. + destruct m; try (destruct ls; easy). + destruct ls; try easy. + simpl. + rewrite IHn'; try easy. + bdestruct (n' =? m); lia. +Qed. + +Lemma switch_base : forall {X : Type} (ls : list X) (x : X), + ls <> [] -> switch ls x 0 = x :: (skipn 1 ls). +Proof. intros. + destruct ls. + easy. + reflexivity. +Qed. + + + +Lemma nth_switch_hit : forall {X : Type} (n : nat) (ls : list X) (x def : X), + n < length ls -> + nth n (switch ls x n) def = x. +Proof. induction n as [| n']. + - destruct ls; easy. + - intros. + destruct ls; try easy. + apply IHn'. + simpl in H. + nia. +Qed. + + + +Lemma nth_switch_miss : forall {X : Type} (sn n : nat) (ls : list X) (x def : X), + n <> sn -> + nth n (switch ls x sn) def = nth n ls def. +Proof. induction sn as [| sn']. + - destruct ls. + easy. + destruct n; easy. + - intros. + destruct n. + + destruct ls; easy. + + assert (H' : n <> sn'). { nia. } + destruct ls. + easy. simpl. + apply IHsn'. + apply H'. +Qed. + + +Lemma switch_inc_helper : forall {X : Type} (n : nat) (l1 l2 : list X) (x : X), + length l1 = n -> + switch (l1 ++ l2) x n = l1 ++ switch l2 x 0. +Proof. induction n as [| n']. + - destruct l1. + reflexivity. + easy. + - intros. destruct l1. + easy. + simpl. + rewrite <- IHn'. + reflexivity. + simpl in H. + injection H. + easy. +Qed. + + +Lemma switch_inc_helper2 : forall {X : Type} (n : nat) (ls : list X) (x : X), + n < length ls -> switch ls x n = (firstn n ls) ++ switch (skipn n ls) x 0. +Proof. intros. + assert (H' : switch ls x n = switch (firstn n ls ++ skipn n ls) x n). + { rewrite (firstn_skipn n ls). reflexivity. } + rewrite H'. + rewrite switch_inc_helper. + reflexivity. + rewrite firstn_length_le. + reflexivity. + nia. +Qed. + + + +Lemma skipn_nil_length : forall {X : Type} (n : nat) (ls : list X), + skipn n ls = [] -> length ls <= n. +Proof. intros. + rewrite <- (firstn_skipn n ls). + rewrite H. + rewrite <- app_nil_end. + apply firstn_le_length. +Qed. + + +Lemma skipskip : forall {X : Type} (ls : list X) (n : nat), + skipn (S n) ls = skipn 1 (skipn n ls). +Proof. induction ls as [| h]. + - destruct n. easy. easy. + - destruct n. easy. + assert (H : skipn (S n) (h :: ls) = skipn n ls). + { reflexivity. } + rewrite H. + rewrite <- IHls. + reflexivity. +Qed. + + +Lemma switch_inc_helper3 : forall {X : Type} (n : nat) (ls : list X) (x : X), + n < length ls -> switch (skipn n ls) x 0 = [x] ++ (skipn (S n) ls). +Proof. intros. destruct (skipn n ls) as [| h] eqn:E. + - apply skipn_nil_length in E. nia. + - assert (H' : skipn (S n) ls = l). + { rewrite skipskip. + rewrite E. + reflexivity. } + rewrite H'. + reflexivity. +Qed. + + +Lemma switch_inc : forall {X : Type} (n : nat) (ls : list X) (x : X), + n < length ls -> switch ls x n = (firstn n ls) ++ [x] ++ (skipn (S n) ls). +Proof. intros. + rewrite switch_inc_helper2. + rewrite switch_inc_helper3. + reflexivity. + apply H. apply H. +Qed. + + +Lemma nth_base : forall {X : Type} (ls : list X) (x : X), + ls <> [] -> ls = (nth 0 ls x) :: (skipn 1 ls). +Proof. intros. + destruct ls. + easy. + reflexivity. +Qed. + + +Lemma nth_helper : forall {X : Type} (n : nat) (ls : list X) (x : X), + n < length ls -> skipn n ls = [nth n ls x] ++ skipn (S n) ls. +Proof. induction n as [| n']. + - destruct ls. easy. easy. + - intros. destruct ls. + assert (H' : forall (n : nat), S n < 0 -> False). { nia. } + apply H' in H. easy. + rewrite skipn_cons. + assert (H'' : nth (S n') (x0 :: ls) x = nth n' ls x). { easy. } + rewrite H''. + rewrite (IHn' ls x). + easy. + simpl in H. + assert (H''' : forall (n m : nat), S m < S n -> m < n). { nia. } + apply H''' in H. + easy. +Qed. + + + +Lemma nth_inc : forall {X : Type} (n : nat) (ls : list X) (x : X), + n < length ls -> ls = (firstn n ls) ++ [nth n ls x] ++ (skipn (S n) ls). +Proof. intros. + rewrite <- nth_helper. + rewrite (firstn_skipn n ls). + reflexivity. easy. +Qed. + + + +Lemma length_change : forall {X : Type} (A B : list X) (x : X), + 2 ^ (length (A ++ [x] ++ B)) = (2 ^ (length A)) * (2 * (2 ^ (length B))). +Proof. intros. + do 2 (rewrite app_length). + simpl length. + rewrite Nat.pow_add_r. + easy. +Qed. + + + + +(* a similar lemma to the one defined by Coq, but better for our purposes *) +Lemma skipn_length' : forall {X : Type} (n : nat) (ls : list X), + length (skipn (S n) ls) = length ls - n - 1. +Proof. intros. + rewrite skipn_length. + nia. +Qed. + + +>>>>>>> QuantumLib/main diff --git a/Quantum.v b/Quantum.v index 2fc1688..cdda6dc 100644 --- a/Quantum.v +++ b/Quantum.v @@ -1,4 +1,5 @@ <<<<<<< HEAD +<<<<<<< HEAD Require Import Psatz. ======= Require Import Psatz. @@ -13,11 +14,21 @@ Require Export Matrix. (* Using our (complex, unbounded) matrices, their complex numbers *) ======= +======= +Require Import Psatz. +Require Import Reals. + +Require Export VecSet. + +>>>>>>> QuantumLib/main (* Using our (complex, unbounded) matrices, their complex numbers *) +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (*******************************************) (** * Quantum basis states *) (*******************************************) @@ -148,6 +159,7 @@ Definition σz : Matrix 2 2 := | _, _ => C0 end. <<<<<<< HEAD +<<<<<<< HEAD Definition sqrtx : Matrix 2 2 := fun x y => match x, y with @@ -169,6 +181,9 @@ Qed. ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Definition control {n : nat} (A : Matrix n n) : Matrix (2*n) (2*n) := fun x y => if (x >>>>>> QuantumLib/main Lemma x_rotation_pi : x_rotation PI = -Ci .* σx. Proof. unfold σx, x_rotation, scale. @@ -352,11 +376,14 @@ Proof. lra. Qed. +<<<<<<< HEAD <<<<<<< HEAD (* sqrtx as a (x-)rotation? *) ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma Rx_rotation : forall θ, rotation θ (3*PI/2) (PI/2) = x_rotation θ. Proof. intros. @@ -405,6 +432,7 @@ Qed. (* Lemmas *) +<<<<<<< HEAD <<<<<<< HEAD Lemma sqrtx_decompose: sqrtx = hadamard × phase_shift (PI/2) × hadamard. Proof. @@ -414,6 +442,8 @@ Qed. ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (* Additional tactics for ∣0⟩, ∣1⟩, cnot and σx. *) Lemma Mmult00 : ⟨0∣ × ∣0⟩ = I 1. Proof. solve_matrix. Qed. @@ -580,7 +610,10 @@ Lemma WF_qubit1 : WF_Matrix ∣1⟩. Proof. show_wf. Qed. Lemma WF_braqubit0 : WF_Matrix ∣0⟩⟨0∣. Proof. show_wf. Qed. Lemma WF_braqubit1 : WF_Matrix ∣1⟩⟨1∣. Proof. show_wf. Qed. <<<<<<< HEAD +<<<<<<< HEAD ======= +======= +>>>>>>> QuantumLib/main Lemma WF_bra : forall (x : nat), WF_Matrix (bra x). Proof. intros x. unfold bra. destruct (x =? 0). show_wf. show_wf. @@ -590,7 +623,10 @@ Lemma WF_ket : forall (x : nat), WF_Matrix (ket x). Proof. intros x. unfold ket. destruct (x =? 0). show_wf. show_wf. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma WF_bool_to_ket : forall b, WF_Matrix (bool_to_ket b). Proof. destruct b; show_wf. Qed. Lemma WF_bool_to_matrix : forall b, WF_Matrix (bool_to_matrix b). @@ -598,6 +634,7 @@ Proof. destruct b; show_wf. Qed. Lemma WF_bool_to_matrix' : forall b, WF_Matrix (bool_to_matrix' b). Proof. destruct b; show_wf. Qed. +<<<<<<< HEAD <<<<<<< HEAD Lemma WF_ket : forall n, WF_Matrix (ket n). Proof. destruct n; simpl; show_wf. Qed. @@ -606,6 +643,8 @@ Proof. destruct n; simpl; show_wf. Qed. ======= >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma WF_bools_to_matrix : forall l, @WF_Matrix (2^(length l)) (2^(length l)) (bools_to_matrix l). Proof. @@ -616,6 +655,7 @@ Proof. apply IHl. Qed. +<<<<<<< HEAD <<<<<<< HEAD Hint Resolve WF_bra0 WF_bra1 WF_qubit0 WF_qubit1 WF_braqubit0 WF_braqubit1 : wf_db. Hint Resolve WF_bool_to_ket WF_bool_to_matrix WF_bool_to_matrix' : wf_db. @@ -625,17 +665,31 @@ Hint Resolve WF_bra0 WF_bra1 WF_qubit0 WF_qubit1 WF_bra WF_ket WF_braqubit0 WF_b Hint Resolve WF_bool_to_ket WF_bool_to_matrix WF_bool_to_matrix' : wf_db. Hint Resolve WF_bools_to_matrix : wf_db. >>>>>>> Heisenberg-Foundations/main +======= +Hint Resolve WF_bra0 WF_bra1 WF_qubit0 WF_qubit1 WF_bra WF_ket WF_braqubit0 WF_braqubit1 : wf_db. +Hint Resolve WF_bool_to_ket WF_bool_to_matrix WF_bool_to_matrix' : wf_db. +Hint Resolve WF_bools_to_matrix : wf_db. +>>>>>>> QuantumLib/main Lemma WF_hadamard : WF_Matrix hadamard. Proof. show_wf. Qed. Lemma WF_σx : WF_Matrix σx. Proof. show_wf. Qed. Lemma WF_σy : WF_Matrix σy. Proof. show_wf. Qed. Lemma WF_σz : WF_Matrix σz. Proof. show_wf. Qed. Lemma WF_cnot : WF_Matrix cnot. Proof. show_wf. Qed. +<<<<<<< HEAD +======= +Lemma WF_notc : WF_Matrix notc. Proof. show_wf. Qed. +>>>>>>> QuantumLib/main Lemma WF_swap : WF_Matrix swap. Proof. show_wf. Qed. Lemma WF_rotation : forall θ ϕ λ, WF_Matrix (rotation θ ϕ λ). Proof. intros. show_wf. Qed. Lemma WF_phase : forall ϕ, WF_Matrix (phase_shift ϕ). Proof. intros. show_wf. Qed. +<<<<<<< HEAD +======= +Lemma WF_Sgate : WF_Matrix Sgate. Proof. show_wf. Qed. +Lemma WF_Tgate: WF_Matrix Tgate. Proof. show_wf. Qed. +>>>>>>> QuantumLib/main Lemma WF_control : forall (n : nat) (U : Matrix n n), WF_Matrix U -> WF_Matrix (control U). @@ -648,8 +702,13 @@ Proof. all: rewrite WFU; [reflexivity|lia]. Qed. +<<<<<<< HEAD Hint Resolve WF_hadamard WF_σx WF_σy WF_σz WF_cnot WF_swap WF_phase : wf_db. Hint Resolve WF_rotation : wf_db. +======= +Hint Resolve WF_hadamard WF_σx WF_σy WF_σz WF_cnot WF_notc WF_swap : wf_db. +Hint Resolve WF_phase WF_Sgate WF_Tgate WF_rotation : wf_db. +>>>>>>> QuantumLib/main Hint Extern 2 (WF_Matrix (phase_shift _)) => apply WF_phase : wf_db. Hint Extern 2 (WF_Matrix (control _)) => apply WF_control : wf_db. @@ -808,6 +867,7 @@ Proof. intros. rewrite <- Rx_rotation. apply rotation_unitary. Qed. Lemma y_rotation_unitary : forall θ, @WF_Unitary 2 (y_rotation θ). Proof. intros. rewrite <- Ry_rotation. apply rotation_unitary. Qed. +<<<<<<< HEAD <<<<<<< HEAD Lemma control_unitary : forall n (A : Matrix n n), ======= @@ -815,6 +875,11 @@ Lemma control_unitary : forall n (A : Matrix n n), Lemma control_unitary : forall n (A : Matrix n n), >>>>>>> Heisenberg-Foundations/main +======= +(* caused errors so commenting out for now: + + Lemma control_unitary : forall n (A : Matrix n n), +>>>>>>> QuantumLib/main WF_Unitary A -> WF_Unitary (control A). Proof. intros n A H. @@ -823,6 +888,7 @@ Proof. unfold control, adjoint, Mmult, I. prep_matrix_equality. simpl. +<<<<<<< HEAD <<<<<<< HEAD bdestructΩ (x =? y). - subst; simpl. @@ -830,12 +896,17 @@ Proof. bdestructΩ (y >>>>>> QuantumLib/main bdestruct (x =? y). - subst; simpl. rewrite Csum_sum. bdestruct (y >>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main * rewrite Csum_0_bounded. Csimpl. rewrite (Csum_eq _ (fun x => A x (y - n)%nat ^* * A x (y - n)%nat)). ++ unfold control, adjoint, Mmult, I in U. @@ -844,6 +915,7 @@ Proof. eapply (equal_f) in U. rewrite U. rewrite Nat.eqb_refl. simpl. +<<<<<<< HEAD <<<<<<< HEAD bdestructΩ (y - n >>>>>> QuantumLib/main bdestruct (y - n >>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main rewrite andb_false_r. bdestructΩ (n <=? x). simpl. lca. @@ -873,11 +950,15 @@ Proof. ++ lca. ++ intros. rewrite andb_false_r. +<<<<<<< HEAD <<<<<<< HEAD bdestructΩ (n + x >>>>>> Heisenberg-Foundations/main +======= + bdestruct (n + x >>>>>> QuantumLib/main simpl. lca. ++ exists y. @@ -888,11 +969,15 @@ Proof. bdestructΩ (y >>>>>> Heisenberg-Foundations/main +======= + bdestruct (y =? x ). +>>>>>>> QuantumLib/main repeat rewrite andb_false_r. lca. + rewrite 2 Csum_0_bounded; [lca| |]. @@ -969,10 +1054,14 @@ Proof. rewrite (WF _ (y-n)%nat) by (right; lia). destruct ((n <=? z) && (n <=? y)); lca. <<<<<<< HEAD +<<<<<<< HEAD Qed. ======= Qed. *) >>>>>>> Heisenberg-Foundations/main +======= +Qed. *) +>>>>>>> QuantumLib/main Lemma transpose_unitary : forall n (A : Matrix n n), WF_Unitary A -> WF_Unitary (A†). Proof. @@ -982,6 +1071,7 @@ Proof. + destruct H; auto with wf_db. + unfold WF_Unitary in *. rewrite adjoint_involutive. +<<<<<<< HEAD <<<<<<< HEAD destruct H as [_ H]. apply Minv_left in H as [_ S]. (* NB: admitted lemma *) @@ -989,12 +1079,17 @@ Proof. Qed. ======= +======= +>>>>>>> QuantumLib/main destruct H as [H H0]. apply Minv_left in H0 as [_ S]; auto with wf_db. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma cnot_unitary : WF_Unitary cnot. Proof. split. @@ -1312,19 +1407,27 @@ Inductive Mixed_State {n} : Matrix n n -> Prop := | Mix_S : forall (p : R) ρ1 ρ2, 0 < p < 1 -> Mixed_State ρ1 -> Mixed_State ρ2 -> Mixed_State (p .* ρ1 .+ (1-p)%R .* ρ2). <<<<<<< HEAD +<<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Lemma WF_Pure : forall {n} (ρ : Density n), Pure_State ρ -> WF_Matrix ρ. Proof. intros. destruct H as [φ [[WFφ IP1] Eρ]]. rewrite Eρ. auto with wf_db. Qed. Hint Resolve WF_Pure : wf_db. +<<<<<<< HEAD <<<<<<< HEAD Lemma WF_Mixed : forall {n} (ρ : Density n), Mixed_State ρ -> WF_Matrix ρ. ======= Lemma WF_Mixed : forall {n} (ρ : Density n), Mixed_State ρ -> WF_Matrix ρ. >>>>>>> Heisenberg-Foundations/main +======= +Lemma WF_Mixed : forall {n} (ρ : Density n), Mixed_State ρ -> WF_Matrix ρ. +>>>>>>> QuantumLib/main Proof. induction 1; auto with wf_db. Qed. Hint Resolve WF_Mixed : wf_db. @@ -1339,16 +1442,22 @@ Proof. exists (I 1). split. split. auto with wf_db. solve_matrix. solve_matrix. Lemma pure_dim1 : forall (ρ : Square 1), Pure_State ρ -> ρ = I 1. Proof. +<<<<<<< HEAD <<<<<<< HEAD intros ρ [φ [[WFφ IP1] Eρ]]. apply Minv_flip in IP1. ======= +======= +>>>>>>> QuantumLib/main intros. assert (H' := H). apply WF_Pure in H'. destruct H as [φ [[WFφ IP1] Eρ]]. apply Minv_flip in IP1; auto with wf_db. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main rewrite Eρ; easy. Qed. @@ -1492,6 +1601,7 @@ Proof. + apply pure_dim1; trivial. + rewrite IHMixed_State1, IHMixed_State2. prep_matrix_equality. +<<<<<<< HEAD <<<<<<< HEAD lca. Qed. @@ -1499,17 +1609,24 @@ Qed. lca. Qed. >>>>>>> Heisenberg-Foundations/main +======= + lca. +Qed. +>>>>>>> QuantumLib/main (* Useful to be able to normalize vectors *) Definition norm {n} (ψ : Vector n) : R := sqrt (fst ((ψ† × ψ) O O)). +<<<<<<< HEAD <<<<<<< HEAD Definition normalize {n} (ψ : Vector n) := / (norm ψ) .* ψ. ======= +======= +>>>>>>> QuantumLib/main Lemma norm_real : forall {n} (v : Vector n), snd ((v† × v) 0%nat 0%nat) = 0%R. @@ -1526,7 +1643,10 @@ Definition normalize {n} (ψ : Vector n) := / (norm ψ) .* ψ. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Lemma inner_product_ge_0 : forall {d} (ψ : Vector d), 0 <= fst ((ψ† × ψ) O O). Proof. @@ -1540,10 +1660,14 @@ Proof. apply Rmult_le_pos; apply Cmod_ge_0. Qed. +<<<<<<< HEAD <<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Lemma norm_scale : forall {n} c (v : Vector n), norm (c .* v) = ((Cmod c) * norm v)%R. Proof. intros n c v. @@ -1563,7 +1687,10 @@ Proof. Qed. <<<<<<< HEAD +<<<<<<< HEAD +======= ======= +>>>>>>> QuantumLib/main Lemma div_real : forall (c : C), snd c = 0 -> snd (/ c) = 0. @@ -1623,7 +1750,10 @@ Proof. intros. Qed. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main (** Density matrices and superoperators **) Definition Superoperator m n := Density m -> Density n. @@ -1835,6 +1965,7 @@ Proof. simpl. rewrite Mmult_assoc. repeat rewrite Mmult_assoc. +<<<<<<< HEAD <<<<<<< HEAD rewrite (kron_assoc q0 q1) by auto with wf_db. Qsimpl. replace 4%nat with (2*2)%nat by reflexivity. @@ -1846,6 +1977,8 @@ Proof. repeat rewrite <- kron_assoc by auto with wf_db. reflexivity. ======= +======= +>>>>>>> QuantumLib/main rewrite (kron_assoc q0 q1). Qsimpl. replace 4%nat with (2*2)%nat by reflexivity. repeat rewrite kron_assoc. @@ -1856,7 +1989,10 @@ Proof. repeat rewrite <- kron_assoc. reflexivity. all : auto with wf_db. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Qed. Lemma swap_two_base : swap_two 2 1 0 = swap. @@ -1902,15 +2038,20 @@ Proof. intros q0 q1 q2 q3 WF0 WF1 WF2 WF3. unfold move_to_0, move_to_0_aux. repeat rewrite Mmult_assoc. +<<<<<<< HEAD <<<<<<< HEAD rewrite (kron_assoc q0 q1) by auto with wf_db. ======= rewrite (kron_assoc q0 q1). >>>>>>> Heisenberg-Foundations/main +======= + rewrite (kron_assoc q0 q1). +>>>>>>> QuantumLib/main simpl. restore_dims. replace 4%nat with (2*2)%nat by reflexivity. Qsimpl. +<<<<<<< HEAD <<<<<<< HEAD rewrite <- kron_assoc by auto with wf_db. restore_dims. @@ -1918,13 +2059,18 @@ Proof. Qsimpl. reflexivity. ======= +======= +>>>>>>> QuantumLib/main rewrite <- kron_assoc. restore_dims. repeat rewrite (kron_assoc _ q1). Qsimpl. reflexivity. all : auto with wf_db. +<<<<<<< HEAD >>>>>>> Heisenberg-Foundations/main +======= +>>>>>>> QuantumLib/main Qed. (* *) diff --git a/README.md b/README.md index 0c912a1..020953c 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ <<<<<<< HEAD +<<<<<<< HEAD # QWIRE This is a Coq implementation of the QWIRE quantum programming language, described in the following papers by Jennifer Paykin, Robert Rand, Dong-Ho Lee and Steve Zdancewic: @@ -72,3 +73,6 @@ Files in this repository # Heisenberg-Foundations The basics of the Heisenberg representation of quantum computing >>>>>>> Heisenberg-Foundations/main +======= +# QuantumLib +>>>>>>> QuantumLib/main diff --git a/RealAux.v b/RealAux.v index 03d91ac..a15a087 100644 --- a/RealAux.v +++ b/RealAux.v @@ -1,18 +1,26 @@ Require Export Reals. <<<<<<< HEAD +<<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Require Import Psatz. (******************************************) (** Relevant lemmas from Rcomplements.v. **) (******************************************) +<<<<<<< HEAD <<<<<<< HEAD ======= >>>>>>> Heisenberg-Foundations/main +======= + +>>>>>>> QuantumLib/main Open Scope R_scope. Lemma Rle_minus_l : forall a b c,(a - c <= b <-> a <= b + c). Proof. intros. lra. Qed. @@ -151,6 +159,15 @@ Proof. apply sqrt_neq_0_compat; lra. Qed. +<<<<<<< HEAD +======= +Lemma sqrt_1_unique : forall x, 1 = √ x -> x = 1. +Proof. intros. assert (H' := H). unfold sqrt in H. destruct (Rcase_abs x). + - apply R1_neq_R0 in H; easy. + - rewrite <- (sqrt_def x); try rewrite <- H'; lra. +Qed. + +>>>>>>> QuantumLib/main (* Automation *) Ltac R_field_simplify := repeat field_simplify_eq [pow2_sqrt2 sqrt2_inv]. Ltac R_field := R_field_simplify; easy. diff --git a/VecSet.v b/VecSet.v new file mode 100644 index 0000000..7755173 --- /dev/null +++ b/VecSet.v @@ -0,0 +1,2667 @@ +Require Import Psatz. +Require Import Reals. + +Require Export Matrix. + + +(************************************) +(* some preliminary defs and lemmas *) +(************************************) + +Local Open Scope nat_scope. + + +Definition e_i {n : nat} (i : nat) : Vector n := + fun x y => (if (x =? i) && (x WF_Matrix (pad A c). +Proof. unfold WF_Matrix, pad. split. + - intros. + unfold col_wedge, row_wedge, e_i, scale. + bdestruct (y (reduce A 0 0) × (reduce_row v 0) = reduce_row (A × v) 0. +Proof. intros. + prep_matrix_equality. + unfold Mmult, reduce, reduce_row. + bdestruct (x (reduce A n n) × (reduce_row v n) = reduce_row (A × v) n. +Proof. intros. + prep_matrix_equality. + unfold Mmult, reduce, reduce_row. + assert (H' : S n - 1 = n). { lia. } + bdestruct (x (reduce A x x) × (reduce_row v x) = reduce_row (A × v) x. +Proof. *) + + +(* similar lemma for append *) +Lemma append_mul : forall {n m} (A : Matrix n m) (v : Vector n) (a : Vector m), + (col_append A v) × (row_append a (@Zero 1 1)) = A × a. +Proof. intros. + prep_matrix_equality. + unfold Mmult. + simpl. + assert (H' : (col_append A v x m * row_append a Zero m y = C0)%C). + { unfold col_append, row_append. + bdestruct (m =? m); try lia; lca. } + rewrite H'. + rewrite Cplus_0_r. + apply Csum_eq_bounded. + intros. + unfold col_append, row_append. + bdestruct (x0 =? m); try lia; try easy. +Qed. + +Lemma matrix_by_basis : forall {n m} (T : Matrix n m) (i : nat), + i < m -> get_vec i T = T × e_i i. +Proof. intros. unfold get_vec, e_i, Mmult. + prep_matrix_equality. + bdestruct (y =? 0). + - rewrite (Csum_unique (T x i) _ m); try easy. + exists i. split. + apply H. split. + bdestruct (i =? i); bdestruct (i j -> A i j = C0) -> A 0 0 = c -> + exists a : Matrix n m, pad a c = A. +Proof. intros. + exists (reduce_col (reduce_row A 0) 0). + unfold pad, reduce_row, reduce_col, col_wedge, row_wedge, e_i, scale. + prep_matrix_equality. + bdestruct (y Prop) -> Prop := +| invr_swap : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m x y : nat) (T : Matrix n m), x < m -> y < m -> P n m T -> P n m (col_swap T x y)) + -> invr_col_swap P. + +Inductive invr_col_scale : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| invr_scale : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m x : nat) (T : Matrix n m) (c : C), c <> C0 -> P n m T -> P n m (col_scale T x c)) + -> invr_col_scale P. + +Inductive invr_col_add : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| invr_add : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m x y : nat) (T : Matrix n m) (c : C), + x <> y -> x < m -> y < m -> P n m T -> P n m (col_add T x y c)) + -> invr_col_add P. + +Inductive invr_col_add_many : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| invr_add_many : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m col : nat) (T : Matrix n m) (as' : Vector m), + col < m -> as' col 0 = C0 -> P n m T -> P n m (col_add_many col as' T)) + -> invr_col_add_many P. + +Inductive invr_col_add_each : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| invr_add_each : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m col : nat) (T : Matrix n m) (as' : Matrix 1 m), + col < m -> WF_Matrix as' -> P n m T -> P n m (col_add_each col (make_col_zero col as') T)) + -> invr_col_add_each P. + +Inductive invr_pad : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| invr_p : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m : nat) (T : Matrix n m) (c : C), c <> C0 -> P (S n) (S m) (pad T c) -> P n m T) + -> invr_pad P. + +Inductive prop_zero_true : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| PZT : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m : nat) (T : Matrix n m), (exists i, i < m /\ get_vec i T = Zero) -> P n m T) -> + prop_zero_true P. + +Inductive prop_zero_false : (forall n m : nat, Matrix n m -> Prop) -> Prop := +| PZF : forall (P : (forall n m : nat, Matrix n m -> Prop)), + (forall (n m : nat) (T : Matrix n m), (exists i, i < m /\ get_vec i T = Zero) -> ~ (P n m T)) -> + prop_zero_false P. + +(* Ltac to help apply these properties of (Mat -> Prop)s *) +Ltac apply_mat_prop tac := + let H := fresh "H" in + assert (H := tac); inversion H; subst; try apply H. + +Lemma mat_prop_col_add_many_some : forall (e n m col : nat) (P : forall n m : nat, Matrix n m -> Prop) + (T : Matrix n m) (as' : Vector m), + (skip_count col e) < m -> col < m -> + (forall i : nat, (skip_count col e) < i -> as' i 0 = C0) -> as' col 0 = C0 -> + invr_col_add P -> + P n m T -> P n m (col_add_many col as' T). +Proof. induction e as [| e]. + - intros. + inversion H3; subst. + rewrite (col_add_many_col_add _ (skip_count col 0)); + try lia; try easy. + apply H5; try lia. + apply skip_count_not_skip. + assert (H' : (col_add_many col (make_row_zero (skip_count col 0) as') T) = T). + { prep_matrix_equality. + unfold col_add_many, make_row_zero, skip_count, gen_new_vec, scale in *. + bdestruct (y =? col); try lia; try easy. + rewrite <- Cplus_0_l. + rewrite Cplus_comm. + apply Cplus_simplify; try easy. + rewrite Msum_Csum. + apply Csum_0_bounded; intros. + destruct col; simpl in *. + bdestruct (x0 =? 1); try lca. + destruct x0; try rewrite H2; try rewrite H1; try lca; try lia. + destruct x0; try lca; rewrite H1; try lca; lia. } + rewrite H'; easy. + apply skip_count_not_skip. + - intros. + inversion H3; subst. + rewrite (col_add_many_col_add _ (skip_count col (S e))); + try lia; try easy. + apply H5; try lia. + apply skip_count_not_skip. + apply IHe; try lia; try easy; auto with wf_db. + assert (H' : e < S e). lia. + apply (skip_count_mono col) in H'. + lia. + intros. + unfold skip_count, make_row_zero in *. + bdestruct (e Prop), + invr_col_add P -> invr_col_add_many P. +Proof. intros. + inversion H; subst. + apply invr_add_many; intros. + destruct m; try lia. + destruct m. + - assert (H' : as' == Zero). + { unfold mat_equiv; intros. + destruct col; destruct i; destruct j; try lia. + easy. } + rewrite <- col_add_many_0; easy. + - rewrite (col_add_many_mat_equiv _ _ _ (make_WF as')); + try apply mat_equiv_make_WF. + bdestruct (col =? S m). + + apply (mat_prop_col_add_many_some m); try lia; try easy. + unfold skip_count. bdestruct (m Prop) + (as' : Matrix 1 m) (T : Matrix n m), + WF_Matrix as' -> (skip_count col e) < m -> col < m -> + (forall i : nat, (skip_count col e) < i -> as' 0 i = C0) -> as' 0 col = C0 -> + invr_col_add P -> + P n m T -> P n m (col_add_each col as' T). +Proof. induction e as [| e]. + - intros. + inversion H4; subst. + rewrite (col_add_each_col_add _ (skip_count col 0)); try lia. + apply H6; try lia. + assert (H' := skip_count_not_skip col 0). auto. + assert (H' : (make_col_zero (skip_count col 0) as') = Zero). + { apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; intros. + unfold make_col_zero, skip_count in *. + destruct i; try lia. + destruct col; simpl in *. + all : destruct j; try easy; simpl. + destruct j; try easy; simpl. + all : apply H2; lia. } + rewrite H'. + rewrite <- col_add_each_0; easy. + apply skip_count_not_skip. + intros x. destruct x; try easy. + apply H; lia. + - intros. + inversion H4; subst. + rewrite (col_add_each_col_add _ (skip_count col (S e))); try lia. + apply H6; try lia. + assert (H' := skip_count_not_skip col (S e)). auto. + apply IHe; try lia; try easy; auto with wf_db. + assert (H' : e < S e). lia. + apply (skip_count_mono col) in H'. + lia. + intros. + unfold skip_count, make_col_zero in *. + bdestruct (e Prop), + invr_col_add P -> invr_col_add_each P. +Proof. intros. + inversion H; subst. + apply invr_add_each; intros. + destruct m; try lia. + destruct m. + - assert (H' : make_col_zero col as' = Zero). + { apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; intros. + destruct col; destruct i; destruct j; try lia. + unfold make_col_zero. + easy. } + rewrite H'. + rewrite <- col_add_each_0; easy. + - bdestruct (col =? S m). + + apply (mat_prop_col_add_each_some m); try lia; try easy; auto with wf_db. + unfold skip_count. bdestruct (m Prop) (T : Matrix n m) (x y : nat), + invr_col_swap P -> + x < m -> y < m -> + P n m (col_swap T x y) -> P n m T. +Proof. intros. + inversion H; subst. + rewrite (col_swap_inv T x y). + apply H3; easy. +Qed. + +Lemma mat_prop_col_scale_conv : forall {n m} (P : forall n m : nat, Matrix n m -> Prop) + (T : Matrix n m) (x : nat) (c : C), + invr_col_scale P -> + c <> C0 -> + P n m (col_scale T x c) -> P n m T. +Proof. intros. + inversion H; subst. + rewrite (col_scale_inv T x c); try easy. + apply H2; try apply nonzero_div_nonzero; easy. +Qed. + +Lemma mat_prop_col_add_conv : forall {n m} (P : forall n m : nat, Matrix n m -> Prop) + (T : Matrix n m) (x y : nat) (c : C), + invr_col_add P -> + x <> y -> x < m -> y < m -> + P n m (col_add T x y c) -> P n m T. +Proof. intros. + inversion H; subst. + rewrite (col_add_inv T x y c); try easy. + apply H4; try easy. +Qed. + +Lemma mat_prop_col_add_many_conv : forall {n m} (P : forall n m : nat, Matrix n m -> Prop) + (T : Matrix n m) (col : nat) (as' : Vector m), + invr_col_add P -> + col < m -> as' col 0 = C0 -> + P n m (col_add_many col as' T) -> P n m T. +Proof. intros. + apply invr_col_add_col_add_many in H. + inversion H; subst. + rewrite (col_add_many_inv T col as'); try easy. + apply H3; try easy. + unfold scale; rewrite H1. + lca. +Qed. + +Lemma mat_prop_col_add_each_conv : forall {n m} (P : forall n m : nat, Matrix n m -> Prop) + (T : Matrix n m) (col : nat) (as' : Matrix 1 m), + invr_col_add P -> + col < m -> WF_Matrix as' -> + P n m (col_add_each col (make_col_zero col as') T) -> P n m T. +Proof. intros. + apply invr_col_add_col_add_each in H. + inversion H; subst. + rewrite (col_add_each_inv col as'); try easy. + apply H3; try easy. + auto with wf_db. +Qed. + +(***********************************************************) +(* Defining and proving lemmas relating to the determinant *) +(***********************************************************) + + +Fixpoint parity (n : nat) : C := + match n with + | 0 => C1 + | S 0 => -C1 + | S (S n) => parity n + end. + + +Lemma parity_S : forall (n : nat), + (parity (S n) = -C1 * parity n)%C. +Proof. intros. + induction n as [| n']; try lca. + rewrite IHn'. + simpl. lca. +Qed. + + +Fixpoint Determinant (n : nat) (A : Square n) : C := + match n with + | 0 => C1 + | S 0 => A 0 0 + | S n' => (Csum (fun i => (parity i) * (A i 0) * (Determinant n' (reduce A i 0)))%C n) + end. + +Arguments Determinant {n}. + +Lemma Det_simplify : forall {n} (A : Square (S (S n))), + Determinant A = + (Csum (fun i => (parity i) * (A i 0) * (Determinant (reduce A i 0)))%C (S (S n))). +Proof. intros. easy. Qed. + + +Lemma Det_simplify_fun : forall {n} (A : Square (S (S (S n)))), + (fun i : nat => parity i * A i 0 * Determinant (reduce A i 0))%C = + (fun i : nat => (Csum (fun j => + (parity i) * (A i 0) * (parity j) * ((reduce A i 0) j 0) * + (Determinant (reduce (reduce A i 0) j 0)))%C (S (S n))))%C. +Proof. intros. + apply functional_extensionality; intros. + rewrite Det_simplify. + rewrite Csum_mult_l. + apply Csum_eq_bounded; intros. + lca. +Qed. + + +Lemma reduce_I : forall (n : nat), reduce (I (S n)) 0 0 = I n. +Proof. intros. + apply mat_equiv_eq. + apply WF_reduce; try lia; auto with wf_db. + apply WF_I. + unfold mat_equiv; intros. + unfold reduce, I. + bdestruct (i + match (x, y) with + | (0, 0) => 1%R + | (0, 1) => 2%R + | (1, 0) => 4%R + | (1, 1) => 5%R + | _ => C0 + end. + + +Lemma Det_M22 : (Determinant M22) = (Copp (3%R,0%R))%C. +Proof. lca. Qed. + + +Lemma Determinant_scale : forall {n} (A : Square n) (c : C) (col : nat), + col < n -> Determinant (col_scale A col c) = (c * Determinant A)%C. +Proof. induction n. + + intros. easy. + + intros. simpl. + destruct n. + - simpl. unfold col_scale. + bdestruct (0 =? col); try lia; easy. + - rewrite Cmult_plus_distr_l. + apply Cplus_simplify. + * rewrite Csum_mult_l. + apply Csum_eq_bounded. + intros. + destruct col. + rewrite col_scale_reduce_same; try lia. + unfold col_scale. bdestruct (0 =? 0); try lia. + lca. + rewrite col_scale_reduce_before; try lia. + rewrite easy_sub. + rewrite IHn; try lia. + unfold col_scale. + bdestruct (0 =? S col); try lia; lca. + * destruct col. + rewrite col_scale_reduce_same; try lia. + unfold col_scale. bdestruct (0 =? 0); try lia. + lca. + rewrite col_scale_reduce_before; try lia. + rewrite easy_sub. + rewrite IHn; try lia. + unfold col_scale. + bdestruct (0 =? S col); try lia; lca. +Qed. + + +(* some helper lemmas *) +Lemma Det_diff_1 : forall {n} (A : Square (S (S (S n)))), + Determinant (col_swap A 0 1) = + Csum (fun i => (Csum (fun j => ((A i 1) * (A (skip_count i j) 0) * (parity i) * (parity j) * + Determinant (reduce (reduce A i 0) j 0))%C) + (S (S n)))) (S (S (S n))). +Proof. intros. + rewrite Det_simplify. + rewrite Det_simplify_fun. + apply Csum_eq_bounded; intros. + apply Csum_eq_bounded; intros. + replace (col_swap A 0 1 x 0) with (A x 1) by easy. + assert (H' : @reduce (S (S n)) (col_swap A 0 1) x 0 x0 0 = A (skip_count x x0) 0). + { unfold reduce, col_swap, skip_count. + simpl. bdestruct (x0 (Csum (fun j => ((A i 0) * (A (skip_count i j) 1) * (parity i) * (parity j) * + Determinant (reduce (reduce A i 0) j 0))%C) + (S (S n)))) (S (S (S n))). +Proof. intros. + rewrite Det_simplify. + rewrite Det_simplify_fun. + apply Csum_eq_bounded; intros. + apply Csum_eq_bounded; intros. + apply Cmult_simplify; try easy. + assert (H' : @reduce (S (S n)) A x 0 x0 0 = A (skip_count x x0) 1). + { unfold reduce, col_swap, skip_count. + simpl. bdestruct (x0 Determinant (col_swap A 0 1) = (-C1 * (Determinant A))%C. +Proof. intros. + destruct n; try lia. + destruct n; try lia. + destruct n. + - simpl. unfold col_swap, reduce. lca. + - rewrite Det_diff_1, Det_diff_2. + apply Csum_rearrange; intros. + + unfold skip_count. + bdestruct (x Determinant (col_swap A i (S i)) = (-C1 * (Determinant A))%C. +Proof. induction n as [| n']. + - easy. + - intros. + destruct i. + + apply Determinant_swap_01; easy. + + simpl. destruct n'; try lia. + do 2 rewrite Csum_extend_r. + rewrite Csum_mult_l. + apply Csum_eq_bounded; intros. + rewrite col_swap_reduce_before; try lia. + rewrite IHn'; try lia. + replace (col_swap A (S i) (S (S i)) x 0) with (A x 0) by easy. + lca. +Qed. + + +Lemma Determinant_swap_ik : forall {n} (k i : nat) (A : Square n), + i + (S k) < n -> Determinant (col_swap A i (i + (S k))) = (-C1 * (Determinant A))%C. +Proof. induction k as [| k']. + - intros. + replace (i + 1) with (S i) by lia. + rewrite Determinant_swap_adj; try lia; lca. + - intros. + rewrite (col_swap_three A i (i + (S k')) (i + (S (S k')))); try lia. + rewrite IHk'; try lia. + replace (i + (S (S k'))) with (S (i + (S k'))) by lia. + rewrite Determinant_swap_adj; try lia. + rewrite IHk'; try lia. + lca. +Qed. + +Lemma Determinant_swap : forall {n} (A : Square n) (i j : nat), + i < n -> j < n -> i <> j -> + Determinant (col_swap A i j) = (-C1 * (Determinant A))%C. +Proof. intros. + bdestruct (i Determinant A = C0. +Proof. intros n A [i [H H0]]. + destruct n; try easy. + destruct n. + destruct i; try lia. + replace C0 with (@Zero 1 1 0 0) by easy. + rewrite <- H0. easy. + destruct i. + - rewrite Det_simplify. + apply Csum_0_bounded; intros. + replace (A x 0) with (@Zero (S (S n)) 1 x 0) by (rewrite <- H0; easy). + unfold Zero; lca. + - rewrite (col_swap_inv _ 0 (S i)). + rewrite Determinant_swap; try lia. + rewrite Det_simplify. + rewrite Csum_mult_l. + apply Csum_0_bounded; intros. + replace (col_swap A 0 (S i) x 0) with + (@Zero (S (S n)) 1 x 0) by (rewrite <- H0; easy). + unfold Zero; lca. +Qed. + + +Lemma col_same_Det_0 : forall {n} (A : Square n) (i j : nat), + i < n -> j < n -> i <> j -> + get_vec i A = get_vec j A -> + Determinant A = C0. +Proof. intros. + apply eq_neg_implies_0. + rewrite <- (Determinant_swap _ i j); try easy. + rewrite (det_by_get_vec (col_swap A i j) A); try easy; intros. + prep_matrix_equality. + destruct y; try easy. + bdestruct (i0 =? i); bdestruct (i0 =? j); try lia. + - rewrite H3, <- col_swap_get_vec, H2; easy. + - rewrite H4, col_swap_diff_order, <- col_swap_get_vec, H2; easy. + - unfold col_swap, get_vec. simpl. + bdestruct (i0 =? i); bdestruct (i0 =? j); try lia; easy. +Qed. + +Lemma col_scale_same_Det_0 : forall {n} (A : Square n) (i j : nat) (c : C), + i < n -> j < n -> i <> j -> + get_vec i A = c .* (get_vec j A) -> + Determinant A = C0. +Proof. intros. + destruct (Ceq_dec c C0). + - apply col_0_Det_0. + exists i. + split; try easy. + rewrite H2, e. + apply Mscale_0_l. + - rewrite (col_scale_inv A j c); try easy. + rewrite Determinant_scale; try easy. + assert (H3 : Determinant (col_scale A j c) = C0). + { apply (col_same_Det_0 _ i j); try easy. + prep_matrix_equality. + unfold get_vec, col_scale. + bdestruct (y =? 0); try easy. + bdestruct (i =? j); bdestruct (j =? j); try lia. + rewrite <- get_vec_conv. + rewrite H2. + unfold scale. + rewrite get_vec_conv. + easy. } + rewrite H3. + lca. +Qed. + + +Lemma Det_col_add_comm : forall {n} (T : Matrix (S n) n) (v1 v2 : Vector (S n)), + (Determinant (col_wedge T v1 0) + Determinant (col_wedge T v2 0) = + Determinant (col_wedge T (v1 .+ v2) 0))%C. +Proof. intros. + destruct n; try easy. + do 3 rewrite Det_simplify. + rewrite <- Csum_plus. + apply Csum_eq_bounded; intros. + repeat rewrite reduce_is_redcol_redrow. + repeat rewrite col_wedge_reduce_col_same. + unfold col_wedge, Mplus. + bdestruct (0 i <> 0 -> Determinant (col_add A 0 i c) = Determinant A. +Proof. intros. + destruct n; try easy. + rewrite col_add_split. + assert (H' := (@Det_col_add_comm n (reduce_col A 0) (get_vec 0 A) (c .* get_vec i A))). + rewrite <- H'. + rewrite <- Cplus_0_r. + apply Cplus_simplify. + assert (H1 : col_wedge (reduce_col A 0) (get_vec 0 A) 0 = A). + { prep_matrix_equality. + unfold col_wedge, reduce_col, get_vec. + destruct y; try easy; simpl. + replace (y - 0) with y by lia; easy. } + rewrite H1; easy. + apply (col_scale_same_Det_0 _ 0 i c); try lia. + prep_matrix_equality. + unfold get_vec, col_wedge, reduce_col, scale; simpl. + bdestruct (y =? 0); bdestruct (i =? 0); try lca; try lia. + replace (S (i - 1)) with i by lia. + easy. +Qed. + + +Lemma Determinant_col_add : forall {n} (A : Square n) (i j : nat) (c : C), + i < n -> j < n -> i <> j -> Determinant (col_add A i j c) = Determinant A. +Proof. intros. + destruct j. + - rewrite <- col_swap_col_add_0. + rewrite Determinant_swap. + rewrite Determinant_col_add0i. + rewrite Determinant_swap. + lca. + all : easy. + - destruct i. + rewrite Determinant_col_add0i; try easy. + rewrite <- col_swap_col_add_Si. + rewrite Determinant_swap. + rewrite Determinant_col_add0i. + rewrite Determinant_swap. + lca. + all : try easy; try lia. +Qed. + +(* We can now define some invariants for Determinant *) +Definition det_neq_0 {n m : nat} (A : Matrix n m) : Prop := + n = m /\ @Determinant n A <> C0. + +Definition det_eq_c (c : C) {n m : nat} (A : Matrix n m) : Prop := + n = m /\ @Determinant n A = c. + + +Lemma det_neq_0_swap_invr : invr_col_swap (@det_neq_0). +Proof. apply invr_swap; intros. + destruct H1; subst. + split; auto. + bdestruct (x =? y); subst. + - rewrite col_swap_same. + easy. + - rewrite Determinant_swap; auto. + unfold not; intros. + apply H2. + rewrite <- (Cmult_1_l _). + replace C1 with ((-C1) * (-C1))%C by lca. + rewrite <- Cmult_assoc, H3. + lca. +Qed. + +Lemma det_neq_0_scale_invr : invr_col_scale (@det_neq_0). +Proof. apply invr_scale; intros. + destruct H0; subst. + split; auto. + bdestruct (x as' col 0 = C0 -> + Determinant A = Determinant (col_add_many col as' A). +Proof. intros. + assert (H' := det_c_add_invr (Determinant A)). + apply invr_col_add_col_add_many in H'. + inversion H'; subst. + apply (H1 n n col A as') in H; try easy. + unfold det_eq_c in *. + destruct H; easy. +Qed. + + +Lemma Determinant_col_add_each : forall (n col : nat) (as' : Matrix 1 n) + (A : Square n), + col < n -> WF_Matrix as' -> as' 0 col = C0 -> + Determinant A = Determinant (col_add_each col as' A). +Proof. intros. + assert (H' := det_c_add_invr (Determinant A)). + apply invr_col_add_col_add_each in H'. + inversion H'; subst. + apply (H2 n n col A as') in H; try easy. + unfold det_eq_c in *. + destruct H; rewrite <- H3. + assert (H4 : (make_col_zero col as') = as'). + { apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; intros. + unfold make_col_zero. + destruct i; try lia. + bdestruct_all; subst; easy. } + rewrite H4; easy. +Qed. + + +(***********************************************************) +(* Defining linear independence, and proving lemmas etc... *) +(***********************************************************) + + +Definition linearly_independent {n m} (T : Matrix n m) : Prop := + forall (a : Vector m), WF_Matrix a -> @Mmult n m 1 T a = Zero -> a = Zero. + + +Definition linearly_dependent {n m} (T : Matrix n m) : Prop := + exists (a : Vector m), WF_Matrix a /\ a <> Zero /\ @Mmult n m 1 T a = Zero. + + +Lemma lindep_implies_not_linindep : forall {n m} (T : Matrix n m), + linearly_dependent T -> ~ (linearly_independent T). +Proof. unfold not, linearly_dependent, linearly_independent in *. + intros. + destruct H as [a [H1 [H2 H3]]]. + apply H0 in H1; easy. +Qed. + +Lemma not_lindep_implies_linindep : forall {n m} (T : Matrix n m), + not (linearly_dependent T) -> linearly_independent T. +Proof. unfold not, linearly_dependent, linearly_independent in *. + intros. + destruct (vec_equiv_dec a Zero). + - apply mat_equiv_eq; auto with wf_db. + - assert (H2 : (exists a : Vector m, WF_Matrix a /\ a <> Zero /\ T × a = Zero)). + { exists a. + split; auto. + split; try easy. + unfold not; intros. + apply n0. + rewrite H2. + easy. } + apply H in H2. + easy. +Qed. + + +Lemma lin_indep_vec : forall {n} (v : Vector n), + WF_Matrix v -> v <> Zero -> linearly_independent v. +Proof. intros. + unfold linearly_independent. + intros. + assert (H' : v × a = (a 0 0) .* v). + { apply mat_equiv_eq; auto with wf_db. + unfold Mmult, scale, mat_equiv. + intros. simpl. + destruct j; try lia; lca. } + assert (H1' := H). + apply nonzero_vec_nonzero_elem in H1'; try easy. + destruct H1' as [x H1']. + destruct (Ceq_dec (a 0 0) C0). + + prep_matrix_equality. + destruct x0. destruct y. + rewrite e; easy. + all : apply H1; lia. + + assert (H'' : ((a 0 0) .* v) x 0 = C0). + { rewrite <- H'. rewrite H2; easy. } + unfold scale in H''. + assert (H3 : (a 0 0 * v x 0)%C <> C0). + { apply Cmult_neq_0; easy. } + easy. +Qed. + + +Lemma invertible_l_implies_linind : forall {n} (A B : Square n), + A × B = I n -> linearly_independent B. +Proof. intros. + unfold linearly_independent. intros. + rewrite <- (Mmult_1_l _ _ a); try easy. + rewrite <- H. + rewrite Mmult_assoc, H1. + rewrite Mmult_0_r. + reflexivity. +Qed. + +Lemma lin_indep_col_reduce_n : forall {n m} (A : Matrix n (S m)), + linearly_independent A -> linearly_independent (reduce_col A m). +Proof. intros. + unfold linearly_independent in *. + intros. + assert (H' : row_append a Zero = Zero). + { apply H. + apply WF_row_append; try easy. + prep_matrix_equality. + unfold Mmult, row_append, Zero. + rewrite <- Csum_extend_r. + bdestruct (m =? m); try lia. + autorewrite with C_db. + assert (H' : (reduce_col A m × a) x y = C0). + { rewrite H1; easy. } + rewrite <- H'. + unfold Mmult. + apply Csum_eq_bounded. + intros. + unfold reduce_col. + bdestruct (x0 =? m); bdestruct (x0 linearly_independent A1. +Proof. induction m2 as [| m2']. + - intros. + unfold linearly_independent in *. + intros. assert (H' : m1 + 0 = m1). lia. + rewrite H' in *. + apply H; try easy. + rewrite <- H1. + unfold smash, Mmult. + prep_matrix_equality. + apply Csum_eq_bounded. + intros. + bdestruct (x0 linearly_dependent (A × B). +Proof. intros. + unfold linearly_dependent in *. + destruct H as [a [H [H0 H1]]]. + exists a. + repeat split; auto. + rewrite Mmult_assoc, H1, Mmult_0_r; easy. +Qed. + +Lemma lin_dep_col_append_n : forall {n m} (A : Matrix n m) (v : Vector n), + linearly_dependent A -> linearly_dependent (col_append A v). +Proof. intros. + unfold linearly_dependent in *. + destruct H as [a [H [H1 H2]]]. + exists (row_append a (@Zero 1 1)). + split; auto with wf_db. + split. unfold not; intros; apply H1. + prep_matrix_equality. + assert (H' : row_append a Zero x y = C0). + { rewrite H0. easy. } + unfold row_append in H'. + bdestruct (x =? m). + rewrite H; try easy; lia. + rewrite H'; easy. + rewrite append_mul. + easy. +Qed. + + +(* proving invr properties *) + + +Lemma lin_indep_swap_invr : invr_col_swap (@linearly_independent). +Proof. apply invr_swap; intros. + unfold linearly_independent in *. + intros. + rewrite (row_swap_inv a x y) in H3. + rewrite <- (swap_preserves_mul T (row_swap a x y) x y) in H3; try easy. + apply H1 in H3. + rewrite (row_swap_inv a x y). + rewrite H3. + prep_matrix_equality. + unfold row_swap. + bdestruct (x0 =? x); bdestruct (x0 =? y); easy. + apply WF_row_swap; easy. +Qed. + +Lemma lin_indep_scale_invr : invr_col_scale (@linearly_independent). +Proof. apply invr_scale; intros. + unfold linearly_independent in *. + intros. + rewrite <- scale_preserves_mul in H2. + apply H0 in H2. + rewrite (row_scale_inv _ x c); try easy. + rewrite H2. + prep_matrix_equality. + unfold row_scale. + bdestruct (x0 =? x); + lca. + apply WF_row_scale; easy. +Qed. + +Lemma lin_indep_add_invr : invr_col_add (@linearly_independent). +Proof. apply invr_add; intros. + unfold linearly_independent in *. + intros. + rewrite <- add_preserves_mul in H4; try easy. + apply H2 in H4. + rewrite (row_add_inv a y x c); try lia. + rewrite H4. + prep_matrix_equality. + unfold row_add. + bdestruct (x0 =? y); + lca. + apply WF_row_add; easy. +Qed. + +Lemma lin_indep_pad_invr : invr_pad (@linearly_independent). +Proof. apply invr_p; intros. + unfold linearly_independent in *. + intros. + assert (H3 : @Mmult (S n) (S m) 1 (pad T c) (row_wedge a Zero 0) = Zero). + { prep_matrix_equality. + destruct x. unfold Mmult. + unfold Zero. apply Csum_0_bounded. + intros. + unfold pad, row_wedge, col_wedge, e_i, scale. + bdestruct (x linearly_dependent T -> + (exists i, i < (S m) /\ + (exists v : Vector m, WF_Matrix v /\ + @Mmult n m 1 (reduce_col T i) v = (-C1) .* (get_vec i T))). +Proof. intros. + unfold linearly_dependent in H. + destruct H0 as [a [H1 [H2 H3]]]. + assert (H4 := H1). + apply nonzero_vec_nonzero_elem in H4; try easy. + destruct H4 as [x H4]. + exists x. + bdestruct (x reduce_col T x i y * reduce_row a x y j) m + + (a x 0) * get_vec x T i j = @Zero n 1 i j)%C). + { rewrite <- H3. unfold Mmult. + assert (H'' : m = x + (m - x)). lia. + rewrite H''. + rewrite Csum_sum. + rewrite <- H''. + assert (H2' : S m = x + S (m - x)). lia. + rewrite H2'. + rewrite Csum_sum. + rewrite <- Csum_extend_l. + rewrite <- Cplus_assoc. + apply Cplus_simplify. + apply Csum_eq_bounded. + intros. unfold reduce_col, reduce_row. + bdestruct (x0 reduce_col T x i y * reduce_row a x y j) m + + (a x 0) * get_vec x T i j + (a x 0) * (- (get_vec x T i j)) = + (- (a x 0)) * get_vec x T i j)%C). + { rewrite H'. lca. } + rewrite <- Cplus_assoc in H1'. + rewrite <- Cmult_plus_distr_l in H1'. + rewrite Cplus_opp_r in H1'. + rewrite Cmult_0_r, Cplus_0_r in H1'. + rewrite H1'. + rewrite Cmult_assoc. + rewrite <- Copp_mult_distr_r. + rewrite Cinv_l; easy. + - assert (H' : a x 0 = C0). + apply H1; try lia. + easy. +Qed. + + +Lemma gt_dim_lindep_ind_step1 : forall {n m} (T : Matrix (S n) (S m)) (col : nat), + WF_Matrix T -> col <= m -> get_vec col T = @e_i (S n) 0 -> + linearly_dependent (reduce_row (reduce_col T col) 0) -> linearly_dependent T. +Proof. intros. + apply (mat_prop_col_add_each_conv _ _ col (-C1 .* (get_row 0 T))); + auto with wf_db; try lia. + apply lin_dep_add_invr. + unfold linearly_dependent in *. + destruct H2 as [a [H3 [H4 H5]]]. + repeat rewrite easy_sub in *. + exists (row_wedge a (@Zero 1 1) col). + split; auto with wf_db. + split. + + unfold not in *. + intros. apply H4. + prep_matrix_equality. + bdestruct (x col < S m -> v col 0 = C0 -> + reduce_col (reduce_row T 0) col × (reduce_row v col) = + - C1 .* get_vec col (reduce_row T 0) -> + linearly_dependent (reduce_row (reduce_col T col) 0) -> linearly_dependent T. +Proof. intros. + assert (H' := @col_add_many_cancel n m (reduce_row T 0) v col). + assert (H0' : forall i : nat, @col_add_many n (S m) col v (reduce_row T 0) i col = C0). + { apply H'; try easy. } + apply (mat_prop_col_add_many_conv _ _ col v); try easy. + apply lin_dep_add_invr. + destruct (Ceq_dec ((col_add_many col v T) 0 col) C0). + - apply_mat_prop (@lin_dep_pzt). + apply H5; exists col. + split; auto. + prep_matrix_equality. unfold get_vec. + destruct y; try easy; simpl. + destruct x; try easy. unfold Zero. + rewrite <- (H0' x). + unfold col_add_many, reduce_row. + bdestruct (col =? col); bdestruct (x WF_Matrix T -> linearly_dependent T. +Proof. induction m as [| m']. + - intros; lia. + - intros. + destruct n as [| n']. + + exists (e_i 0). + split. apply WF_e_i. + split. unfold not; intros. + assert (H' : (@e_i (S m') 0) 0 0 = C0). + { rewrite H1; easy. } + unfold e_i in H'; simpl in H'. + apply C1_neq_C0; easy. + assert (H' : T = Zero). + { prep_matrix_equality. + rewrite H0; try easy; try lia. } + rewrite H'. apply Mmult_0_l. + + bdestruct (n' Prop := +| otI_I: op_to_I (I n) +| otI_swap : forall (A : Square n) (x y : nat), x < n -> y < n -> + op_to_I A -> op_to_I (col_swap A x y) +| otI_scale : forall (A : Square n) (x : nat) (c : C), x < n -> c <> C0 -> + op_to_I A -> op_to_I (col_scale A x c) +| otI_add : forall (A : Square n) (x y : nat) (c : C), x < n -> y < n -> x <> y -> + op_to_I A -> op_to_I (col_add A x y c). + + + +Lemma op_to_I_WF : forall {n} (A : Square n), + op_to_I A -> WF_Matrix A. +Proof. intros. + apply op_to_I_ind; auto with wf_db. +Qed. + +Hint Resolve op_to_I_WF : wf_db. + + +Definition otI_multiplicative {n} (A : Square n) : Prop := + forall (B : Square n), (op_to_I B -> op_to_I (B × A)). + + +Lemma otI_implies_otI_multiplicative : forall {n} (A : Square n), + op_to_I A -> otI_multiplicative A. +Proof. intros. + apply op_to_I_ind; auto. + - unfold otI_multiplicative; intros. + rewrite Mmult_1_r; auto with wf_db. + - unfold otI_multiplicative; intros. + rewrite col_swap_mult_r; auto with wf_db. + rewrite <- Mmult_assoc. + rewrite <- col_swap_mult_r; auto with wf_db. + apply otI_swap; auto with wf_db. + - unfold otI_multiplicative; intros. + rewrite col_scale_mult_r; auto with wf_db. + rewrite <- Mmult_assoc. + rewrite <- col_scale_mult_r; auto with wf_db. + apply otI_scale; auto with wf_db. + - unfold otI_multiplicative; intros. + rewrite col_add_mult_r; auto with wf_db. + rewrite <- Mmult_assoc. + rewrite <- col_add_mult_r; auto with wf_db. + apply otI_add; auto with wf_db. +Qed. + + +Lemma otI_Mmult : forall {n} (A B : Square n), + op_to_I A -> op_to_I B -> + op_to_I (A × B). +Proof. intros. + apply otI_implies_otI_multiplicative in H0. + unfold otI_multiplicative in H0. + apply H0; easy. +Qed. + +Definition otI_padded {n} (A : Square n) : Prop := + forall (c : C), (c <> C0 -> op_to_I (pad A c)). + +Lemma otI_implies_otI_padded : forall {n} (A : Square n), + op_to_I A -> otI_padded A. +Proof. intros. + apply op_to_I_ind; auto. + - unfold otI_padded; intros. + assert (H' : (pad (I n) c) = col_scale (I (S n)) 0 c). + { apply mat_equiv_eq; auto with wf_db. + apply WF_pad; apply WF_I. + unfold mat_equiv; intros. + unfold pad, col_scale, col_wedge, row_wedge, e_i, scale, I. + bdestruct_all; easy. } + rewrite H'. + apply otI_scale; auto; try lia. + apply otI_I. + - intros. + unfold otI_padded in *; intros. + rewrite pad_col_swap. + apply otI_swap; try lia. + apply H3; easy. + - intros. + unfold otI_padded in *; intros. + rewrite pad_col_scale. + apply otI_scale; try lia; try easy. + apply H3; easy. + - intros. + unfold otI_padded in *; intros. + rewrite pad_col_add. + apply otI_add; try lia; try easy. + apply H4; easy. +Qed. + +Lemma otI_pad : forall {n} (A : Square n) (c : C), + c <> C0 -> op_to_I A -> + op_to_I (pad A c). +Proof. intros. + apply otI_implies_otI_padded in H0. + unfold otI_padded in H0. + apply H0; easy. +Qed. + + +Lemma otI_lin_indep : forall {n} (A : Square n), + op_to_I A -> linearly_independent A. +Proof. intros. + apply op_to_I_ind; auto. + - unfold linearly_independent; intros. + rewrite Mmult_1_l in H1; auto with wf_db. + - intros. + apply_mat_prop lin_indep_swap_invr. + apply H5; auto. + - intros. + apply_mat_prop lin_indep_scale_invr. + apply H5; auto. + - intros. + apply_mat_prop lin_indep_add_invr. + apply H6; auto. +Qed. + + +(* need alternate def to deal with broader n <> m case *) +Definition op_to_I' {n m : nat} (A : Matrix n m) := + n = m /\ @op_to_I n A. + +Lemma otI_equiv_otI' : forall {n} (A : Square n), + op_to_I' A <-> op_to_I A. +Proof. intros. split. + - intros. + destruct H; easy. + - intros. + split; easy. +Qed. + +Lemma otI'_add_invr : invr_col_add (@op_to_I'). +Proof. apply invr_add; intros. + destruct H2; split; try easy; subst. + apply otI_add; easy. +Qed. + + +Lemma otI_col_add_many : forall (n col : nat) (A : Square n) (as' : Vector n), + col < n -> as' col 0 = C0 -> + op_to_I A -> op_to_I (col_add_many col as' A). +Proof. intros. + assert (H' := otI'_add_invr). + apply invr_col_add_col_add_many in H'. + inversion H'; subst. + apply (H2 n n col A as') in H; try easy. + destruct H; easy. +Qed. + + +Lemma otI_col_add_each : forall (n col : nat) (A : Square n) (as' : Matrix 1 n), + col < n -> WF_Matrix as' -> as' 0 col = C0 -> + op_to_I A -> op_to_I (col_add_each col as' A). +Proof. intros. + assert (H' := otI'_add_invr). + apply invr_col_add_col_add_each in H'. + inversion H'; subst. + apply (H3 n n col A as') in H; try easy. + assert (H4 : (make_col_zero col as') = as'). + { apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; intros. + unfold make_col_zero. + destruct i; try lia. + bdestruct_all; subst; easy. } + rewrite H4 in *. + destruct H; easy. +Qed. + + + +(**********************************************) +(* Now we prove more properties of invariants *) +(**********************************************) + + +(* a case for when we consider (Mat -> Prop)s that are the same as lin_indep, invertible, + etc... these props will satisfy 'prop_zero_false P' *) +Lemma mpr_step1_pzf_P : forall {n} (A : Square (S n)) (P : forall m o, Matrix m o -> Prop), + invr_col_add P -> invr_col_scale P -> + prop_zero_false P -> + WF_Matrix A -> P (S n) (S n) A -> + (exists B : Square (S n), op_to_I B /\ P (S n) (S n) (A × B) /\ + (exists i, i < (S n) /\ get_vec i (A × B) = e_i 0)). +Proof. intros. + assert (H4 : WF_Matrix (reduce_row A 0)). + { apply WF_reduce_row; try lia; easy. } + assert (H5 : linearly_dependent (reduce_row A 0)). + { apply gt_dim_lindep; try lia. + apply H4. } + apply lin_dep_gen_elem in H4; try easy. + destruct H4 as [i [H6 H4]]. + destruct H4 as [v [H4 H7]]. + apply invr_col_add_col_add_many in H. + inversion H; subst. + assert (H9 : P (S n) (S n) (col_add_many i (row_wedge v Zero i) A)). + apply H8; auto. + unfold row_wedge; bdestruct_all; easy. + destruct (Ceq_dec ((col_add_many i (row_wedge v Zero i) A) 0 i) C0). + - assert (H10 : forall i0 : nat, + col_add_many i (row_wedge v Zero i) (reduce_row A 0) i0 i = C0). + apply (col_add_many_cancel (reduce_row A 0) (row_wedge v Zero i) i); try easy. + unfold row_wedge. + bdestruct (i Prop)s that are + the same as lin_indep, invertible, etc... *) +Lemma mrp_step1_pzt_P0 : forall {n} (A : Square (S n)) (P P0: forall m o, Matrix m o -> Prop), + invr_col_add P -> invr_col_scale P -> + invr_col_add P0 -> prop_zero_true P0 -> + WF_Matrix A -> P (S n) (S n) A -> + (exists B : Square (S n), op_to_I B /\ P (S n) (S n) (A × B) /\ + (exists i, i < (S n) /\ get_vec i (A × B) = e_i 0)) \/ P0 (S n) (S n) A. +Proof. intros. + assert (H5 : WF_Matrix (reduce_row A 0)). + { apply WF_reduce_row; try lia; easy. } + assert (H6 : linearly_dependent (reduce_row A 0)). + { apply gt_dim_lindep; try lia. + apply H5. } + apply lin_dep_gen_elem in H5; try easy. + destruct H5 as [i [H7 H5]]. + destruct H5 as [v [H5 H8]]. + apply invr_col_add_col_add_many in H. + inversion H; subst. + assert (H10 : P (S n) (S n) (col_add_many i (row_wedge v Zero i) A)). + apply H9; auto. + unfold row_wedge; bdestruct_all; easy. + destruct (Ceq_dec ((col_add_many i (row_wedge v Zero i) A) 0 i) C0). + - right. + assert (H11 : forall i0 : nat, + col_add_many i (row_wedge v Zero i) (reduce_row A 0) i0 i = C0). + apply (col_add_many_cancel (reduce_row A 0) (row_wedge v Zero i) i); try easy. + unfold row_wedge. + bdestruct (i Prop), + invr_col_add P -> invr_col_swap P -> + WF_Matrix A -> P (S n) (S n) A -> + (exists i, i < (S n) /\ get_vec i A = e_i 0) -> + (exists B : Square (S n), op_to_I B /\ P (S n) (S n) (A × B) /\ + (exists a : Square n, pad a C1 = (A × B))). +Proof. intros. + destruct H3 as [i [H3 H4]]. + inversion H0; subst. + apply (H5 _ _ 0 i A) in H2; try lia; try easy. + apply invr_col_add_col_add_each in H. + inversion H; subst. + assert (H3' : 0 < S n). lia. + apply (H6 _ _ 0 (col_swap A 0 i) (-C1 .* (get_row 0 (col_swap A 0 i)))) in H3'; try lia. + exists ((row_swap (I (S n)) 0 i) × (row_add_many 0 + (make_col_zero 0 (-C1 .* (get_row 0 (col_swap A 0 i)))) + (I (S n)))). + split. + apply otI_Mmult. + rewrite <- col_row_swap_invr_I; try lia. + apply otI_swap; try lia; apply otI_I. + rewrite row_many_col_each_invr_I; try lia; auto. + apply otI_col_add_each; try lia; auto with wf_db. + all : try (apply WF_make_col_zero; apply WF_scale; + apply WF_get_row; apply WF_col_swap; try lia; auto). + apply otI_I. + rewrite <- Mmult_assoc. + rewrite <- col_swap_mult_r; try lia; try easy. + rewrite <- col_add_each_mult_r; try lia; try easy. + split; try easy. + apply padded; intros. + 4 : apply WF_make_col_zero. + all : try (apply WF_scale; apply WF_get_row). + all : try (apply WF_col_swap; try lia; easy). + destruct H7 as [H7 H8]. + destruct H7. + + unfold col_add_each, make_col_zero, get_row, col_swap, + Mplus, Mmult, get_vec, scale. + rewrite H7 in *. + bdestruct (j =? 0); try lia. + assert (H' : (get_vec i A) 0 0 = C1). + { rewrite H4. easy. } + simpl. bdestruct (j =? i); try lia. + all : unfold get_vec in H'; simpl in H'. + all : rewrite H'; lca. + + unfold col_add_each, make_col_zero, get_row, col_swap, + Mplus, Mmult, get_vec, scale. + rewrite H7 in *; simpl. + destruct i0; try lia. + assert (H' : (get_vec i A) (S i0) 0 = C0). + { rewrite H4. easy. } + unfold get_vec in H'; simpl in H'. + rewrite H'; lca. + + unfold col_add_each, make_col_zero, get_row, col_swap, + Mplus, Mmult, get_vec, scale; simpl. + assert (H' : (get_vec i A) 0 0 = C1). + { rewrite H4. easy. } + unfold get_vec in H'; simpl in H'. + rewrite H'; lca. + + easy. +Qed. + + +(* these two lemmas allow us to reduce our study of Square (S n) to Square n, allowing + us to induct on n. Then, 'invr_pad P' allows us to jump from the n case to (S n) *) +Lemma mat_prop_reduce_pzf_P : forall {n} (A : Square (S n)) (P P0 : forall m o, Matrix m o -> Prop), + invr_col_swap P -> invr_col_scale P -> + invr_col_add P -> prop_zero_false P -> + invr_pad P -> + WF_Matrix A -> P (S n) (S n) A -> + (exists B : Square (S n), op_to_I B /\ P (S n) (S n) (A × B) /\ + (exists a : Square n, pad a C1 = (A × B))). +Proof. intros. + apply (mpr_step1_pzf_P A P) in H5; auto. + destruct H5 as [B [H5 [H6 [i [H7 H8]]]]]. + apply (mpr_step2 (A × B) P) in H1; auto with wf_db. + destruct H1 as [B0 [H10 [H11 H12]]]. + exists (B × B0); split. + apply otI_Mmult; auto. + split; rewrite <- Mmult_assoc; easy. + exists i. split; easy. +Qed. + +Lemma mat_prop_reduce_pzt_P0 : forall {n} (A : Square (S n)) (P P0 : forall m o, Matrix m o -> Prop), + invr_col_swap P -> invr_col_scale P -> + invr_col_add P -> + invr_pad P -> + invr_col_add P0 -> prop_zero_true P0 -> + WF_Matrix A -> P (S n) (S n) A -> + (exists B : Square (S n), op_to_I B /\ P (S n) (S n) (A × B) /\ + (exists a : Square n, pad a C1 = (A × B))) \/ P0 (S n) (S n) A. +Proof. intros. + apply (mrp_step1_pzt_P0 A P P0) in H6; auto. + destruct H6. + - left. + destruct H6 as [B [H6 [H7 [i [H8 H9]]]]]. + apply (mpr_step2 (A × B) P) in H1; auto with wf_db. + destruct H1 as [B0 [H10 [H11 H12]]]. + exists (B × B0); split. + apply otI_Mmult; auto. + split; rewrite <- Mmult_assoc; easy. + exists i. split; easy. + - right; easy. +Qed. + + +(* now, we prove some theorems with these powerful lemmas *) +Theorem invr_P_implies_invertible_r : forall {n} (A : Square n) (P : forall m o, Matrix m o -> Prop), + invr_col_swap P -> invr_col_scale P -> + invr_col_add P -> prop_zero_false P -> + invr_pad P -> + WF_Matrix A -> P n n A -> + (exists B, op_to_I B /\ A × B = I n). +Proof. induction n as [| n']. + - intros. + exists (I 0). split. + apply otI_I. + assert (H' : I 0 = Zero). + prep_matrix_equality. + unfold I; bdestruct_all; easy. + rewrite H', Mmult_0_r. + apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv. lia. + - intros. + apply mat_prop_reduce_pzf_P in H5; auto. + destruct H5 as [B [H5 [H6 [a H7]]]]. + rewrite <- H7 in H6. + inversion H3; subst. + apply H8 in H6. + apply IHn' in H6; auto. + destruct H6 as [B0 [H9 H10]]. + exists (B × (pad B0 C1)). + split. + apply otI_Mmult; auto. + apply otI_pad; auto. + all : try apply C1_neq_C0. + rewrite <- Mmult_assoc, <- H7. + rewrite <- pad_mult, H10, Cmult_1_l, pad_I; easy. + apply (WF_pad a C1). + rewrite H7; auto with wf_db. +Qed. + + +Corollary lin_ind_implies_invertible_r : forall {n} (A : Square n), + WF_Matrix A -> + linearly_independent A -> + (exists B, op_to_I B /\ A × B = I n). +Proof. intros. + apply (invr_P_implies_invertible_r _ (@linearly_independent)); + auto with invr_db. +Qed. + + +(*******************************) +(* Inverses of square matrices *) +(*******************************) + +Definition Minv {n : nat} (A B : Square n) : Prop := A × B = I n /\ B × A = I n. + + +Definition invertible {n : nat} (A : Square n) : Prop := + exists B, Minv A B. + + +Lemma Minv_unique : forall (n : nat) (A B C : Square n), + WF_Matrix A -> WF_Matrix B -> WF_Matrix C -> + Minv A B -> Minv A C -> B = C. +Proof. + intros n A B C WFA WFB WFC [HAB HBA] [HAC HCA]. + replace B with (B × I n) by (apply Mmult_1_r; assumption). + rewrite <- HAC. + replace C with (I n × C) at 2 by (apply Mmult_1_l; assumption). + rewrite <- HBA. + rewrite Mmult_assoc. + reflexivity. +Qed. + +Lemma Minv_symm : forall (n : nat) (A B : Square n), Minv A B -> Minv B A. +Proof. unfold Minv; intuition. Qed. + +(* The left inverse of a square matrix is also its right inverse *) +Lemma Minv_flip : forall (n : nat) (A B : Square n), + WF_Matrix A -> WF_Matrix B -> + A × B = I n -> B × A = I n. +Proof. intros. + assert (H3 := H1). + apply invertible_l_implies_linind in H1. + apply lin_ind_implies_invertible_r in H1; try easy. + destruct H1 as [A' [H2 H4]]. + assert (H' : (A × B) × A' = A'). + { rewrite H3. apply Mmult_1_l; auto with wf_db. } + rewrite Mmult_assoc in H'. + rewrite H4 in H'. + rewrite Mmult_1_r in H'; try easy. + rewrite H'; easy. +Qed. + +Lemma Minv_left : forall (n : nat) (A B : Square n), + WF_Matrix A -> WF_Matrix B -> + A × B = I n -> Minv A B. +Proof. + intros n A B H H0 H1. + unfold Minv. split; trivial. + apply Minv_flip; + assumption. +Qed. + +Lemma Minv_right : forall (n : nat) (A B : Square n), + WF_Matrix A -> WF_Matrix B -> + B × A = I n -> Minv A B. +Proof. + intros n A B H H0. + unfold Minv. split; trivial. + apply Minv_flip; + assumption. +Qed. + + +Corollary lin_indep_invertible : forall (n : nat) (A : Square n), + WF_Matrix A -> (linearly_independent A <-> invertible A). +Proof. intros; split. + - intros. + assert (H1 := H). + apply lin_ind_implies_invertible_r in H; try easy. + destruct H as [B [H H2]]. + unfold invertible. + exists B. unfold Minv. + split; try easy. + apply Minv_flip in H2; auto with wf_db. + - intros. + destruct H0 as [B [H1 H2]]. + apply invertible_l_implies_linind in H2. + easy. +Qed. + +Lemma Minv_otI_l : forall (n : nat) (A B : Square n), + WF_Matrix A -> WF_Matrix B -> + Minv A B -> + op_to_I A. +Proof. intros. + assert (H2 := lin_indep_invertible). + assert (H3 : invertible B). + { exists A. apply Minv_symm; easy. } + apply H2 in H3; auto. + apply lin_ind_implies_invertible_r in H3; auto. + destruct H3 as [B' [H3 H4]]. + apply Minv_left in H4; auto with wf_db. + apply Minv_symm in H1. + apply (Minv_unique _ B A B') in H4; auto with wf_db; subst. + easy. +Qed. + + +(*********************************************) +(* We finish proving lemmas about invarients *) +(*********************************************) + +(* Finally, we show that if all 6 nice properties are true about two (Mat -> Prop)s, then + they are equivalent on well formed matrices *) +Theorem invr_P_equiv_otI : forall {n} (A : Square n) (P : forall m o, Matrix m o -> Prop), + invr_col_swap P -> invr_col_scale P -> + invr_col_add P -> prop_zero_false P -> + invr_pad P -> P n n (I n) -> + WF_Matrix A -> + (P n n A <-> op_to_I A). +Proof. intros. split. + - intros. + apply invr_P_implies_invertible_r in H6; auto. + destruct H6 as [B [H6 H7]]. + apply (Minv_otI_l _ A B); auto with wf_db. + apply Minv_left; auto with wf_db. + - intros. + apply op_to_I_ind; auto; intros. + + inversion H; subst. + apply H11; easy. + + inversion H0; subst. + apply H11; easy. + + inversion H1; subst. + apply H12; easy. +Qed. + +Corollary lin_indep_det_neq_0 : forall {n} (A : Square n), + WF_Matrix A -> (linearly_independent A <-> det_neq_0 A). +Proof. intros. split. + - intros. + apply invr_P_equiv_otI in H0; auto with invr_db. + apply invr_P_equiv_otI; auto with invr_db. + split; auto. + rewrite Det_I; apply C1_neq_C0. + unfold linearly_independent; intros. + rewrite Mmult_1_l in H3; auto. + - intros. + apply invr_P_equiv_otI in H0; auto with invr_db. + apply invr_P_equiv_otI; auto with invr_db. + unfold linearly_independent; intros. + rewrite Mmult_1_l in H2; auto. + split; auto. + rewrite Det_I; apply C1_neq_C0. +Qed. + +Corollary lin_dep_det_eq_0 : forall {n} (A : Square n), + WF_Matrix A -> (linearly_dependent A <-> det_eq_c C0 A). +Proof. induction n as [| n']. + - intros. split; intros. + destruct H0 as [v [H0 [H1 H2]]]. + assert (H' : v = Zero). + { apply mat_equiv_eq; auto with wf_db. + unfold mat_equiv; easy. } + easy. + destruct H0. + unfold Determinant in H1. + assert (H2 := C1_neq_C0). + easy. + - intros. + split; intros. + + split; try easy. + apply lindep_implies_not_linindep in H0. + assert (H' : ~ (det_neq_0 A)). + unfold not; intros; apply H0. + apply lin_indep_det_neq_0; auto. + unfold not in H'. + destruct (Ceq_dec (Determinant A) C0); try easy. + assert (H'' : False). apply H'. + split; easy. + easy. + + apply (mat_prop_reduce_pzt_P0 _ _ (@linearly_dependent)) in H0; + auto with invr_db. + destruct H0; try easy. + destruct H0 as [B [H0 [H1 [a H2]]]]. + assert (H' : linearly_dependent a). + { apply IHn'. + apply <- (@WF_pad n' n' a C1). + rewrite H2; auto with wf_db. + apply_mat_prop det_0_pad_invr. + apply (H4 n' n' a C1). + apply C1_neq_C0. + rewrite H2; easy. } + unfold linearly_dependent in *. + destruct H' as [v [H3 [H4 H5]]]. + exists (B × (row_wedge v Zero 0)); split. + apply WF_mult; auto with wf_db. + apply WF_row_wedge; try lia; auto with wf_db. split. + unfold not; intros; apply H4. + assert (H7 := H0); apply otI_lin_indep in H7. + apply lin_indep_invertible in H7; auto with wf_db. + destruct H7 as [B0 H7]. + assert (H8 : B0 × (B × row_wedge v Zero 0) = Zero). { rewrite H6, Mmult_0_r; easy. } + destruct H7. + rewrite <- Mmult_assoc, H9, Mmult_1_l in H8. + prep_matrix_equality. + assert (H' : row_wedge v Zero 0 (S x) y = C0). { rewrite H8; easy. } + unfold Zero; rewrite <- H'. + unfold row_wedge; bdestruct_all. + rewrite easy_sub; easy. + apply WF_row_wedge; try lia; auto with wf_db. + rewrite <- Mmult_assoc, <- H2. + rewrite pad_row_wedge_mult, H5. + prep_matrix_equality. + unfold row_wedge. + bdestruct_all; easy. +Qed. + + +Corollary lin_dep_indep_dec : forall {n} (A : Square n), + WF_Matrix A -> { linearly_independent A } + { linearly_dependent A }. +Proof. intros. + destruct (Ceq_dec (Determinant A) C0). + - right. + apply lin_dep_det_eq_0; auto. + split; easy. + - left. + apply lin_indep_det_neq_0; auto. + split; easy. +Qed. + +(*************************************************************************************) +(* we define another set of invariants to help show that Det A × Det B = Det (A × B) *) +(*************************************************************************************) + +Definition Det_mult_comm_l (n m : nat) (A : Matrix n m) := + n = m /\ (forall (B : Square n), (Determinant B) * (@Determinant n A) = (@Determinant n (B × A)))%C. + + +Lemma Dmc_I : forall {n}, Det_mult_comm_l n n (I n). +Proof. intros. + unfold Det_mult_comm_l; split; auto. + intros. + rewrite Det_I, Det_make_WF, (Det_make_WF _ (B × I n)). + rewrite <- Mmult_make_WF. + rewrite <- (eq_make_WF (I n)); auto with wf_db. + rewrite Mmult_1_r; auto with wf_db. + lca. +Qed. + +Lemma Dmc_make_WF : forall {n} (A : Square n), + Det_mult_comm_l n n (make_WF A) <-> Det_mult_comm_l n n A. +Proof. intros; split; intros. + - destruct H; subst. + split; auto; intros. + rewrite (Det_make_WF _ A), H0. + rewrite <- Det_Mmult_make_WF_r; easy. + - destruct H; subst. + split; auto; intros. + rewrite <- Det_make_WF. + rewrite <- Det_Mmult_make_WF_r; easy. +Qed. + +Lemma Dmc_Mmult : forall {n} (A B : Square n), + Det_mult_comm_l n n A -> Det_mult_comm_l n n B -> + Det_mult_comm_l n n (A × B). +Proof. intros. + destruct H; destruct H0; subst. + split; auto. + intros. + rewrite <- H2, Cmult_assoc, H1, H2, Mmult_assoc; easy. +Qed. + + +Lemma Dmc_swap_I : forall (n x y : nat), + x < n -> y < n -> + Det_mult_comm_l n n (row_swap (I n) x y). +Proof. intros. + bdestruct (x =? y); subst. + - rewrite row_swap_same. + apply Dmc_I. + - split; auto; intros. + rewrite Det_Mmult_make_WF_l. + rewrite <- col_swap_mult_r; auto with wf_db. + rewrite <- col_row_swap_invr_I; auto. + rewrite Determinant_swap, Det_I, Determinant_swap; auto. + rewrite Det_make_WF; lca. +Qed. + +Lemma Dmc_scale_I : forall (n x : nat) (c : C), + Det_mult_comm_l n n (row_scale (I n) x c). +Proof. intros. + split; auto; intros. + rewrite Det_Mmult_make_WF_l. + rewrite <- col_scale_mult_r; auto with wf_db. + rewrite <- col_row_scale_invr_I; auto. + bdestruct (x y -> x < n -> y < n -> Det_mult_comm_l n n (row_add (I n) x y c). +Proof. intros. + split; auto; intros. + rewrite Det_Mmult_make_WF_l. + rewrite <- col_add_mult_r; auto with wf_db. + rewrite <- col_row_add_invr_I; auto. + rewrite Determinant_col_add, Det_I, Determinant_col_add; auto. + rewrite Det_make_WF; lca. +Qed. + +(* proving Dmc invariants *) +Lemma Dmc_swap_invr : invr_col_swap (Det_mult_comm_l). +Proof. apply invr_swap; intros. + bdestruct (x =? y); subst. + - rewrite col_swap_same; easy. + - bdestruct (n =? m); subst; try (destruct H1; easy). + apply Dmc_make_WF. + rewrite <- col_swap_make_WF; auto. + rewrite col_swap_mult_r; auto with wf_db. + apply Dmc_Mmult. + apply Dmc_make_WF; easy. + apply Dmc_swap_I; auto. +Qed. + +Lemma Dmc_scale_invr : invr_col_scale (Det_mult_comm_l). +Proof. apply invr_scale; intros. + bdestruct (n =? m); subst; try (destruct H0; easy). + apply Dmc_make_WF. + rewrite <- col_scale_make_WF; auto. + rewrite col_scale_mult_r; auto with wf_db. + apply Dmc_Mmult. + apply Dmc_make_WF; easy. + apply Dmc_scale_I; auto. +Qed. + +Lemma Dmc_add_invr : invr_col_add (Det_mult_comm_l). +Proof. apply invr_add; intros. + bdestruct (n =? m); subst; try (destruct H2; easy). + apply Dmc_make_WF. + rewrite <- col_add_make_WF; auto. + rewrite col_add_mult_r; auto with wf_db. + apply Dmc_Mmult. + apply Dmc_make_WF; easy. + apply Dmc_add_I; auto. +Qed. + +Local Close Scope nat_scope. + +Lemma otI_Dmc : forall {n} (A : Square n), + op_to_I A -> Det_mult_comm_l n n A. +Proof. intros. + apply op_to_I_ind; auto. + - apply Dmc_I. + - intros. + apply_mat_prop Dmc_swap_invr. + apply H5; easy. + - intros. + apply_mat_prop Dmc_scale_invr. + apply H5; easy. + - intros. + apply_mat_prop Dmc_add_invr. + apply H6; easy. +Qed. + + +Lemma Determinant_multiplicative_WF : forall {n} (A B : Square n), + WF_Matrix A -> WF_Matrix B -> + (Determinant A) * (Determinant B) = Determinant (A × B). +Proof. intros. + destruct (lin_dep_indep_dec B); auto. + - apply invr_P_equiv_otI in l; auto with invr_db. + apply otI_Dmc in l; destruct l. + apply H2. + unfold linearly_independent; intros. + rewrite <- H3, Mmult_1_l; easy. + - assert (H' : linearly_dependent (A × B)). + { apply lin_dep_mult_r; easy. } + apply lin_dep_det_eq_0 in l; + apply lin_dep_det_eq_0 in H'; auto with wf_db. + destruct l; destruct H'. + rewrite H2, H4; lca. +Qed. + + +Theorem Determinant_multiplicative : forall {n} (A B : Square n), + (Determinant A) * (Determinant B) = Determinant (A × B). +Proof. intros. + rewrite Det_make_WF, (Det_make_WF _ B), Determinant_multiplicative_WF; + auto with wf_db. + rewrite <- Det_Mmult_make_WF_l, <- Det_Mmult_make_WF_r; easy. +Qed. + diff --git a/_CoqProject b/_CoqProject index 31d93bb..41f6e28 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,5 +1,6 @@ -R . Top +<<<<<<< HEAD <<<<<<< HEAD Ancilla.v Complex.v @@ -27,6 +28,10 @@ UnitarySemantics.v Complex.v Eigenvectors.v Heisenberg.v +======= +Complex.v +Eigenvectors.v +>>>>>>> QuantumLib/main Matrix.v Monad.v Monoid.v @@ -34,6 +39,11 @@ Polynomial.v Prelim.v Quantum.v RealAux.v +<<<<<<< HEAD Types.v >>>>>>> Heisenberg-Foundations/main +======= +VecSet.v + +>>>>>>> QuantumLib/main