diff --git a/src/CoreData/QlibTemp.v b/src/CoreData/QlibTemp.v new file mode 100644 index 0000000..d415a25 --- /dev/null +++ b/src/CoreData/QlibTemp.v @@ -0,0 +1,48 @@ +Require Import QuantumLib.VectorStates. +Require Import QuantumLib.Permutations. + +Local Open Scope nat_scope. + +Lemma kron_f_to_vec_eq {n m p q : nat} (A : Matrix (2^n) (2^m)) + (B : Matrix (2^p) (2^q)) (f : nat -> bool) : WF_Matrix A -> WF_Matrix B -> + A ⊗ B × f_to_vec (m + q) f + = A × f_to_vec m f ⊗ (B × f_to_vec q (fun k : nat => f (m + k))). +Proof. + intros. + prep_matrix_equivalence. + apply kron_f_to_vec. +Qed. + +Lemma equal_on_basis_states_implies_equal' : (* FIXME: Replace + equal_on_basis_states_implies_equal with this *) + forall {m dim : nat} (A B : Matrix m (2 ^ dim)), + WF_Matrix A -> WF_Matrix B -> + (forall f : nat -> bool, A × f_to_vec dim f = B × f_to_vec dim f) -> + A = B. +Proof. + intros m dim A B HA HB HAB. + prep_matrix_equivalence. + intros i j Hi Hj. + rewrite 2!(get_entry_with_e_i _ i j) by lia. + rewrite 2!Mmult_assoc. + rewrite <- (basis_vector_eq_e_i _ j) by assumption. + rewrite basis_f_to_vec_alt by assumption. + now rewrite HAB. +Qed. + +Lemma equal_on_conj_basis_states_implies_equal {n m} + (A B : Matrix (2 ^ n) (2 ^ m)) : WF_Matrix A -> WF_Matrix B -> + (forall f g, (f_to_vec n g) ⊤%M × (A × f_to_vec m f) = + (f_to_vec n g) ⊤%M × (B × f_to_vec m f)) -> A = B. +Proof. + intros HA HB HAB. + apply equal_on_basis_states_implies_equal'; [auto..|]. + intros f. + apply transpose_matrices. + apply equal_on_basis_states_implies_equal'; [auto_wf..|]. + intros g. + apply transpose_matrices. + rewrite Mmult_transpose, transpose_involutive, HAB. + rewrite Mmult_transpose, transpose_involutive. + reflexivity. +Qed. \ No newline at end of file diff --git a/src/CoreData/SemanticCore.v b/src/CoreData/SemanticCore.v index cdcb150..a1a2144 100644 --- a/src/CoreData/SemanticCore.v +++ b/src/CoreData/SemanticCore.v @@ -3,10 +3,11 @@ Contains the definitions for Z and X spider semantics, their equivalence, and well formedness *) +Require Export QuantumLib.Modulus. Require Export QuantumLib.Quantum. Require Import QuantumLib.Proportional. Require Export QuantumLib.VectorStates. - +Require Export QlibTemp. (* Sparse Matrix Definition *) diff --git a/src/CoreRules/CapCupRules.v b/src/CoreRules/CapCupRules.v index 42ca8c7..49a4a64 100644 --- a/src/CoreRules/CapCupRules.v +++ b/src/CoreRules/CapCupRules.v @@ -4,7 +4,9 @@ Require Import CastRules. Require Import WireRules. Require Import StackRules. Require Import SwapRules. +Require Import ZXpermFacts. Require Import CoreAutomation. +Require Import StackComposeRules. Lemma cup_Z : ⊃ ∝ Z 2 0 0. Proof. @@ -46,24 +48,519 @@ Proof. now rewrite wire_to_n_wire, n_wire_stack, 2!nwire_removal_l. Qed. -Opaque n_cup. - Lemma n_cap_0_empty : n_cap 0 ∝ ⦰. Proof. - apply transpose_diagrams. - simpl. + unfold n_cap. rewrite n_cup_0_empty. easy. Qed. Lemma n_cap_1_cap : n_cap 1 ∝ ⊂. Proof. + unfold n_cap. + rewrite n_cup_1_cup. + easy. +Qed. + +Local Open Scope nat_scope. + +Lemma cap_f_to_vec f : + ⟦ ⊃ ⟧ × f_to_vec 2 f = + b2R (eqb (f 0) ((f 1))) .* I (2 ^ 0). +Proof. + prep_matrix_equivalence. + unfold scale, kron. + by_cell; + destruct (f 0), (f 1); cbv; lca. +Qed. + +Lemma n_cup_unswapped_f_to_vec n f : + ⟦ n_cup_unswapped n ⟧ × f_to_vec (n + n) f = + b2R (forallb (fun k => eqb (f k) ( f (n + n - S k))) (seq 0 n)) .* I (2 ^ 0). +Proof. + revert f; + induction n; intros f. + - cbn. Csimpl. now Msimpl_light. + - cbn [n_cup_unswapped]. + rewrite zx_compose_spec. + simpl_cast_semantics. + rewrite 2!zx_stack_spec. + replace (S n + S n) with (1 + (n + n) + 1) by lia. + rewrite Mmult_assoc. + restore_dims. + rewrite (@kron_f_to_vec_eq (1 + 0) (1 + (n + n)) 1 1) by auto_wf. + rewrite (@kron_f_to_vec_eq 1 1 0 (n + n)) by auto_wf. + rewrite IHn. + cbn -[f_to_vec seq]. + rewrite Mmult_1_l, Mmult_1_comm by apply (f_to_vec_WF 1). + rewrite (kron_split_diag (f_to_vec 1 f)) by auto_wf. + rewrite <- kron_mixed_product, kron_1_r. + restore_dims. + rewrite f_to_vec_merge. + rewrite <- Mmult_assoc. + rewrite cap_f_to_vec. + cbn [Nat.ltb Nat.leb]. + rewrite Nat.sub_diag, Nat.add_0_r. + rewrite kron_1_l, kron_1_r by auto_wf. + cbn -[seq]. + restore_dims. + distribute_scale. + Msimpl_light. + f_equal. + unfold b2R. + rewrite !(if_dist _ _ _ RtoC). + rewrite Cmult_if_if_1_l. + apply f_equal_if; [|easy..]. + cbn. + f_equal; [repeat f_equal; lia|]. + apply eq_iff_eq_true. + rewrite forallb_seq0, forallb_seq. + setoid_rewrite eqb_true_iff. + apply forall_iff. + intros s. + apply impl_iff; intros Hs. + rewrite 2!(Nat.add_comm _ 1). + cbn. + replace (S (n + n - S s)) with (n + n - s) by lia. + reflexivity. +Qed. + +Lemma n_cup_f_to_vec n f : + ⟦ n_cup n ⟧ × f_to_vec (n + n) f = + b2R (forallb (fun k => eqb (f k) ( f (n + k))) (seq 0 n)) .* I (2 ^ 0). +Proof. + unfold n_cup. + rewrite zx_compose_spec, zx_stack_spec. + rewrite n_wire_semantics. + rewrite perm_of_zx_permutation_semantics by auto with zxperm_db. + rewrite perm_of_n_swap. + rewrite Mmult_assoc. + restore_dims. + rewrite kron_f_to_vec_eq by auto_wf. + rewrite perm_to_matrix_permutes_qubits by cleanup_perm. + rewrite Mmult_1_l by auto_wf. + rewrite f_to_vec_merge. + rewrite n_cup_unswapped_f_to_vec. + f_equal. + f_equal. + f_equal. + apply eq_iff_eq_true. + rewrite 2!forallb_seq0. + setoid_rewrite eqb_true_iff. + split. + - intros Hf. + intros s Hs. + generalize (Hf (n - S s) ltac:(lia)). + do 2 simplify_bools_lia_one_kernel. + rewrite reflect_perm_defn by lia. + rewrite sub_S_sub_S by lia. + intros ->. + f_equal; lia. + - intros Hf. + intros s Hs. + generalize (Hf (n - S s) ltac:(lia)). + do 2 simplify_bools_lia_one_kernel. + rewrite reflect_perm_defn by lia. + intros ->. + f_equal; lia. +Qed. + +Lemma f_to_vec_transpose_f_to_vec n f g : + transpose (f_to_vec n f) × f_to_vec n g = + b2R (forallb (fun k => eqb (f k) (g k)) (seq 0 n)) .* I 1. +Proof. + prep_matrix_equivalence. + intros [] []; [|lia..]; intros _ _. + rewrite 2!basis_f_to_vec. + rewrite basis_trans_basis. + simplify_bools_moddy_lia_one_kernel. + unfold scale. + cbn. + rewrite Cmult_1_r. + unfold b2R. + rewrite (if_dist _ _ _ RtoC). + apply f_equal_if; [|easy..]. + apply eq_iff_eq_true. + rewrite Nat.eqb_eq, forallb_seq0, <- funbool_to_nat_eq_iff. + now setoid_rewrite eqb_true_iff. +Qed. + +Lemma f_to_vec_transpose_f_to_vec' n f g : + transpose (f_to_vec n f) × f_to_vec n g = + (if funbool_to_nat n f =? funbool_to_nat n g then + C1 else C0) .* I 1. +Proof. + rewrite f_to_vec_transpose_f_to_vec. + f_equal. + unfold b2R. + rewrite (if_dist R C). + apply f_equal_if; [|easy..]. + apply eq_iff_eq_true. + rewrite forallb_seq0, Nat.eqb_eq. + setoid_rewrite eqb_true_iff. + apply funbool_to_nat_eq_iff. +Qed. + +Lemma f_to_vec_transpose_self n f : + transpose (f_to_vec n f) × f_to_vec n f = + I 1. +Proof. + rewrite f_to_vec_transpose_f_to_vec', Nat.eqb_refl. + now Msimpl_light. +Qed. + + +Lemma n_cup_f_to_vec_pullthrough_bot n f : + @Mmult _ (2^(n + n)) (2^n) (⟦ n_cup n ⟧) (I (2 ^ n) ⊗ f_to_vec n f) = + (f_to_vec n f) ⊤%M. +Proof. + unify_pows_two. + apply equal_on_basis_states_implies_equal'; + [auto_wf.. |]. + intros g. + rewrite <- (kron_1_r _ _ (f_to_vec n g)) at 1. + rewrite Mmult_assoc. + restore_dims. + rewrite kron_mixed_product, Mmult_1_l, Mmult_1_r by auto_wf. + rewrite f_to_vec_transpose_f_to_vec. + rewrite f_to_vec_merge. + rewrite n_cup_f_to_vec. + do 3 f_equal. + apply eq_iff_eq_true. + rewrite 2!forallb_seq0. + apply forall_iff; intros s. + apply impl_iff; intros Hs. + do 2 simplify_bools_lia_one_kernel. + rewrite add_sub'. + rewrite 2!eqb_true_iff. + easy. +Qed. + +Lemma n_cup_f_to_vec_pullthrough_top n f : + @Mmult _ (2^(n + n)) (2^n) (⟦ n_cup n ⟧) (f_to_vec n f ⊗ I (2 ^ n)) = + (f_to_vec n f) ⊤%M. +Proof. + unify_pows_two. + apply equal_on_basis_states_implies_equal'; + [auto_wf.. |]. + intros g. + rewrite <- (kron_1_l _ _ (f_to_vec n g)) at 1 by auto_wf. + rewrite Mmult_assoc. + restore_dims. + rewrite kron_mixed_product, Mmult_1_l, Mmult_1_r by auto_wf. + rewrite f_to_vec_transpose_f_to_vec. + rewrite f_to_vec_merge. + rewrite n_cup_f_to_vec. + do 3 f_equal. + apply eq_iff_eq_true. + rewrite 2!forallb_seq0. + apply forall_iff; intros s. + apply impl_iff; intros Hs. + do 2 simplify_bools_lia_one_kernel. + now rewrite add_sub'. +Qed. + +Lemma n_cap_f_to_vec_pullthrough_bot n f : + @Mmult (2^n) (2^(n + n)) _ (I (2 ^ n) ⊗ (f_to_vec n f) ⊤%M) (⟦ n_cap n ⟧) = + f_to_vec n f. +Proof. + apply transpose_matrices. + rewrite Mmult_transpose. + restore_dims. + rewrite Nat.pow_add_r. + change (@transpose (2 ^ n)) with (@transpose (2^n * 2^0)). + rewrite (kron_transpose). + unfold n_cap. + rewrite semantics_transpose_comm. + change (transpose (transpose ?x)) with x. + rewrite id_transpose_eq. + unify_pows_two. + apply n_cup_f_to_vec_pullthrough_bot. +Qed. + +Lemma n_cap_f_to_vec_pullthrough_top n f : + @Mmult (2^n) (2^(n + n)) _ ((f_to_vec n f) ⊤%M ⊗ I (2 ^ n)) (⟦ n_cap n ⟧) = + f_to_vec n f. +Proof. + apply transpose_matrices. + rewrite Mmult_transpose. + restore_dims. + rewrite Nat.pow_add_r. + change (@transpose (2 ^ n)) with (@transpose (2^0 * 2^n)). + rewrite (kron_transpose). + unfold n_cap. + rewrite semantics_transpose_comm. + change (transpose (transpose ?x)) with x. + rewrite id_transpose_eq. + unify_pows_two. + apply n_cup_f_to_vec_pullthrough_top. +Qed. + +Lemma Mmult_vec_comm {n} (v u : Vector n) : WF_Matrix u -> WF_Matrix v -> + v ⊤%M × u = u ⊤%M × v. +Proof. + intros Hu Hv. + prep_matrix_equivalence. + by_cell. + apply big_sum_eq_bounded. + intros k Hk. + unfold transpose. + lca. +Qed. + +Lemma n_cup_matrix_pullthrough_top n m (A : Matrix (2 ^ n) (2 ^ m)) + (HA : WF_Matrix A) : + @Mmult _ (2^(n + n)) (2^(m + n)) (⟦ n_cup n ⟧) (A ⊗ I (2 ^ n)) = + @Mmult _ (2^(m + m)) (2^(m + n)) (⟦ n_cup m ⟧) (I (2 ^ m) ⊗ A ⊤%M). +Proof. + unify_pows_two. + apply equal_on_basis_states_implies_equal'; + [auto_wf..|]. + intros f. + rewrite 2!Mmult_assoc. + restore_dims. + rewrite 2!kron_f_to_vec_eq by auto_wf. + rewrite 2!Mmult_1_l, kron_split_antidiag by auto_wf. + restore_dims. + unify_pows_two. + rewrite <- Mmult_assoc. + rewrite n_cup_f_to_vec_pullthrough_bot. + symmetry. + rewrite kron_split_diag by auto_wf. + unify_pows_two. + rewrite <- Mmult_assoc. + rewrite n_cup_f_to_vec_pullthrough_top. + rewrite kron_1_l, kron_1_r by auto_wf. + rewrite <- Mmult_assoc. + rewrite Mmult_vec_comm, Mmult_transpose by auto_wf. + easy. +Qed. + +Lemma n_cup_matrix_pullthrough_bot n m (A : Matrix (2 ^ n) (2 ^ m)) + (HA : WF_Matrix A) : + @Mmult _ (2^(n + n)) (2^(n + m)) (⟦ n_cup n ⟧) (I (2 ^ n) ⊗ A) = + @Mmult _ (2^(m + m)) (2^(n + m)) (⟦ n_cup m ⟧) (A ⊤%M ⊗ I (2 ^ m)). +Proof. + now rewrite n_cup_matrix_pullthrough_top, + transpose_involutive by auto_wf. +Qed. + +Open Scope ZX_scope. + +Lemma n_cup_pullthrough_top {n m} (zx : ZX n m) : + zx ↕ n_wire m ⟷ n_cup m ∝ + n_wire n ↕ zx ⊤ ⟷ n_cup n. +Proof. + prop_exists_nonzero 1%R. + rewrite Mscale_1_l. + cbn [ZX_semantics]. + rewrite semantics_transpose_comm, 2!n_wire_semantics. + apply n_cup_matrix_pullthrough_top. + auto_wf. +Qed. + +Lemma n_cup_pullthrough_bot {n m} (zx : ZX n m) : + n_wire m ↕ zx ⟷ n_cup m ∝ + zx ⊤ ↕ n_wire n ⟷ n_cup n. +Proof. + rewrite n_cup_pullthrough_top, Proportional.transpose_involutive. + easy. +Qed. + +Lemma n_cap_pullthrough_top {n m} (zx : ZX n m) : + n_cap n ⟷ (zx ↕ n_wire n) ∝ + n_cap m ⟷ (n_wire m ↕ zx ⊤). +Proof. apply transpose_diagrams. - simpl. - rewrite <- n_cup_1_cup. + cbn -[n_cup]. + unfold n_cap. + rewrite !Proportional.transpose_involutive, !n_wire_transpose. + now rewrite n_cup_pullthrough_bot. +Qed. + +Lemma n_cap_pullthrough_bot {n m} (zx : ZX n m) : + n_cap n ⟷ (n_wire n ↕ zx) ∝ + n_cap m ⟷ (zx ⊤ ↕ n_wire m). +Proof. + now rewrite n_cap_pullthrough_top, Proportional.transpose_involutive. +Qed. + +Lemma n_cup_inv_n_swap_n_wire : forall n, n_cup n ∝ n_wire n ↕ n_swap n ⟷ n_cup_unswapped n. +Proof. + intros n. + rewrite compose_zxperm_l' by auto_zxperm. + cbn. + rewrite n_wire_transpose. + rewrite n_cup_pullthrough_bot, n_swap_transpose. + rewrite compose_zxperm_l by auto_zxperm. + cbn. + rewrite n_wire_transpose. + now rewrite 2!n_swap_transpose. +Qed. + +Lemma n_cup_unswapped_to_n_cup_n_swap_top n : + n_cup_unswapped n ∝ + n_swap n ↕ n_wire n ⟷ n_cup n. +Proof. + rewrite compose_zxperm_l' by auto_zxperm. + now rewrite stack_transpose, n_swap_transpose, n_wire_transpose. +Qed. + +Lemma n_cup_unswapped_pullthrough_top {n m} (zx : ZX n m) : + zx ↕ n_wire m ⟷ n_cup_unswapped m ∝ + n_wire n ↕ (n_swap m ⟷ zx ⊤ ⟷ n_swap n) ⟷ n_cup_unswapped n. +Proof. + rewrite n_cup_unswapped_to_n_cup_n_swap_top. + rewrite n_cup_pullthrough_top. + rewrite <- compose_assoc, <- stack_compose_distr, + nwire_removal_l, nwire_removal_r, n_swap_transpose. + rewrite stack_split_antidiag, compose_assoc, n_cup_pullthrough_top. + rewrite n_cup_inv_n_swap_n_wire. + now rewrite !stack_nwire_distribute_l, !compose_assoc. +Qed. + +Lemma n_cup_unswapped_pullthrough_bot {n m} (zx : ZX n m) : + n_wire m ↕ zx ⟷ n_cup_unswapped m ∝ + (n_swap m ⟷ zx ⊤ ⟷ n_swap n) ↕ n_wire n ⟷ n_cup_unswapped n. +Proof. + rewrite n_cup_unswapped_to_n_cup_n_swap_top. + (* rewrite n_cup_pullthrough_top. *) + rewrite <- compose_assoc, <- stack_compose_distr, + nwire_removal_l, nwire_removal_r. + rewrite stack_split_diag, compose_assoc, n_cup_pullthrough_bot. + now rewrite !stack_nwire_distribute_r, !compose_assoc. +Qed. + +Lemma big_yank_l n prf0 prf1 : + (n_cap n ↕ n_wire n) ⟷ + cast _ _ prf0 prf1 + (n_wire n ↕ n_cup n) ∝ n_wire n. +Proof. + prop_exists_nonzero 1%R. + cbn -[n_cup n_cap]. + simpl_cast_semantics. + cbn -[n_cup n_cap]. + rewrite Mscale_1_l, n_wire_semantics. + apply equal_on_basis_states_implies_equal; [auto_wf..|]. + intros f. + rewrite Mmult_1_l by auto_wf. + rewrite Mmult_assoc. + rewrite <- (kron_1_l _ _ (f_to_vec n f)) by auto_wf. + restore_dims. + rewrite kron_mixed_product, Mmult_1_l, Mmult_1_r by auto_wf. + rewrite (kron_split_antidiag _ (f_to_vec n f)) by auto_wf. + rewrite Nat.pow_add_r, <- id_kron. + rewrite kron_assoc by auto_wf. + restore_dims. + unify_pows_two. + rewrite <- Mmult_assoc. + restore_dims. + rewrite kron_mixed_product' by unify_pows_two. + unify_pows_two. + rewrite n_cup_f_to_vec_pullthrough_bot. + rewrite Mmult_1_l, kron_1_r by auto_wf. + rewrite n_cap_f_to_vec_pullthrough_bot. + now rewrite kron_1_l by auto_wf. +Qed. + +Lemma big_yank_r n prf0 prf1 prf2 : + (n_wire n ↕ n_cap n) ⟷ + cast _ _ prf0 prf1 + (n_cup n ↕ n_wire n) ∝ cast _ _ prf2 eq_refl (n_wire n). +Proof. + apply transpose_diagrams. + cbn [ZXCore.transpose]. + rewrite 2!cast_transpose. + cbn [ZXCore.transpose]. unfold n_cap. rewrite Proportional.transpose_involutive. - easy. + fold (n_cap n). + rewrite n_wire_transpose. + rewrite cast_compose_l. + clean_eqns eapply (cast_diagrams n n). + clean_eqns rewrite cast_contract, + cast_compose_distribute, cast_contract, cast_id. + rewrite (big_yank_l n). + now clean_eqns rewrite cast_contract, cast_id. +Qed. + +Lemma n_cap_n_cup_matrix_pullthrough n m (A : Matrix (2 ^ n) (2 ^ m)) + (HA : WF_Matrix A) : + I (2 ^ m) ⊗ (⟦ n_cup n ⟧) × (I (2 ^ m) ⊗ A ⊗ I (2 ^ n)) × + (⟦ n_cap m ⟧ ⊗ I (2 ^ n)) = + A ⊤%M. +Proof. + apply equal_on_basis_states_implies_equal'; + [auto_wf..|]. + intros f. + rewrite <- (kron_1_l _ _ (f_to_vec n f)) at 1 by auto_wf. + rewrite Mmult_assoc; + restore_dims. + rewrite Mmult_assoc, kron_mixed_product' by unify_pows_two. + restore_dims. + rewrite kron_mixed_product. + rewrite !Mmult_1_l, Mmult_1_r by auto_wf. + rewrite (kron_split_antidiag (_ × _)), <- id_kron, kron_assoc by auto_wf. + rewrite kron_1_r. + restore_dims. + unify_pows_two. + + rewrite <- Mmult_assoc. + restore_dims. + rewrite kron_mixed_product' by unify_pows_two. + rewrite Mmult_1_r by auto_wf. + unify_pows_two. + rewrite n_cup_f_to_vec_pullthrough_bot, <- Mmult_assoc. + restore_dims. + rewrite kron_mixed_product, Mmult_1_r by auto_wf. + apply transpose_matrices. + rewrite !Mmult_transpose. + change (transpose (?A ⊗ ?B)) with ((transpose A) ⊗ (transpose B)). + rewrite Mmult_transpose, transpose_involutive. + unfold n_cap. + rewrite semantics_transpose_comm. + change (transpose (transpose ?x)) with x. + rewrite id_transpose_eq. + unify_pows_two. + apply equal_on_basis_states_implies_equal'; + [auto_wf..|]. + intros g. + rewrite Mmult_assoc. + rewrite <- (kron_1_r _ _ (f_to_vec m g)). + restore_dims. + rewrite kron_mixed_product. + rewrite kron_1_r. + rewrite Mmult_1_l, Mmult_1_r by auto_wf. + rewrite (kron_split_diag (f_to_vec _ _)) by auto_wf. + unify_pows_two. + rewrite <- Mmult_assoc. + rewrite n_cup_f_to_vec_pullthrough_top. + rewrite kron_1_l by auto_wf. + now rewrite Mmult_vec_comm by auto_wf. +Qed. + +Lemma n_cap_n_cup_pullthrough n m (A : ZX m n) prf1 prf2 : + (n_cap m ↕ n_wire n) ⟷ + (n_wire m ↕ A ↕ n_wire n) ⟷ + cast _ _ prf1 prf2 (n_wire m ↕ n_cup n) ∝ + A ⊤. +Proof. + rewrite <- stack_nwire_distribute_r. + rewrite n_cap_pullthrough_bot. + rewrite stack_nwire_distribute_r, compose_assoc. + clean_eqns rewrite stack_assoc. + clean_eqns rewrite cast_compose_l, cast_contract. + rewrite (cast_compose_r _ _ (A ⊤ ↕ _)), cast_id. + rewrite <- stack_compose_distr. + rewrite n_wire_stack, nwire_removal_l, nwire_removal_r. + rewrite (stack_split_antidiag (A ⊤)). + clean_eqns rewrite stack_empty_r, + (cast_compose_r _ _ (n_wire n ↕ _)), !cast_contract. + clean_eqns rewrite cast_compose_distribute, + cast_contract, cast_id. + rewrite <- compose_assoc. + rewrite big_yank_l. + now cleanup_zx. Qed. Global Open Scope ZX_scope. @@ -81,12 +578,11 @@ Proof. - simpl. simpl in IHn. rewrite IHn at 1. - simpl_casts. rewrite stack_wire_distribute_l. rewrite stack_wire_distribute_r. change (— ↕ n_wire n) with (n_wire (1 + n)). rewrite <- (@cast_n_wire (n + 1) (1 + n)). - rewrite <- ComposeRules.compose_assoc. + rewrite <- compose_assoc. apply compose_simplify; [ | easy]. rewrite (cast_compose_mid (S (n + S n))). rewrite cast_compose_distribute. @@ -108,15 +604,6 @@ Unshelve. all: lia. Qed. -Lemma n_cup_inv_n_swap_n_wire : forall n, n_cup n ∝ n_wire n ↕ n_swap n ⟷ n_cup_unswapped n. -Proof. - intros. - strong induction n. - destruct n; [ | destruct n]. - - simpl. rewrite n_cup_0_empty. cleanup_zx. simpl_casts. easy. - - simpl. rewrite n_cup_1_cup. cleanup_zx. simpl_casts. bundle_wires. cleanup_zx. easy. -Admitted. (*TODO*) - Lemma n_cup_unswapped_colorswap : forall n, ⊙ (n_cup_unswapped n) ∝ n_cup_unswapped n. Proof. intros. @@ -132,7 +619,6 @@ Qed. Lemma n_cup_colorswap : forall n, ⊙ (n_cup n) ∝ n_cup n. Proof. intros. -Local Transparent n_cup. unfold n_cup. simpl. rewrite n_wire_colorswap. diff --git a/src/CoreRules/StackComposeRules.v b/src/CoreRules/StackComposeRules.v index d1bbb4c..f3286b4 100644 --- a/src/CoreRules/StackComposeRules.v +++ b/src/CoreRules/StackComposeRules.v @@ -12,11 +12,7 @@ Lemma nwire_stack_compose_topleft : forall {topIn botIn topOut botOut} (zx1 ↕ zx0). Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite n_wire_semantics. - Msimpl. - easy. + now rewrite <- stack_compose_distr, nwire_removal_l, nwire_removal_r. Qed. Lemma nwire_stack_compose_botleft : forall {topIn botIn topOut botOut} @@ -25,11 +21,19 @@ Lemma nwire_stack_compose_botleft : forall {topIn botIn topOut botOut} (zx0 ↕ zx1). Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite n_wire_semantics. - Msimpl. - easy. + now rewrite <- stack_compose_distr, nwire_removal_l, nwire_removal_r. +Qed. + +Lemma stack_split_diag {n m o p} (zx0 : ZX n m) (zx1 : ZX o p) : + zx0 ↕ zx1 ∝ zx0 ↕ n_wire o ⟷ (n_wire m ↕ zx1). +Proof. + now rewrite <- stack_compose_distr, nwire_removal_l, nwire_removal_r. +Qed. + +Lemma stack_split_antidiag {n m o p} (zx0 : ZX n m) (zx1 : ZX o p) : + zx0 ↕ zx1 ∝ (n_wire n ↕ zx1) ⟷ (zx0 ↕ n_wire p). +Proof. + now rewrite <- stack_compose_distr, nwire_removal_l, nwire_removal_r. Qed. Lemma push_out_top : forall {nIn nOut nOutAppendix} (appendix : ZX 0 nOutAppendix) (zx : ZX nIn nOut), diff --git a/src/CoreRules/SwapRules.v b/src/CoreRules/SwapRules.v index f168597..3a72ef0 100644 --- a/src/CoreRules/SwapRules.v +++ b/src/CoreRules/SwapRules.v @@ -226,58 +226,37 @@ Qed. Lemma a_swap_semantics_ind : forall n, a_swap_semantics (S (S (S n))) = swap ⊗ (I (2 ^ (S n))) × (I 2 ⊗ a_swap_semantics (S (S n))) × (swap ⊗ (I (2 ^ (S n)))). Proof. - intros. - rewrite <- 2 a_swap_correct. - simpl. - repeat rewrite kron_id_dist_l by shelve. - restore_dims. - rewrite <- 2 (kron_assoc (I 2) (I 2) (_)) by shelve. - repeat rewrite id_kron. - replace ((2 ^ n + (2 ^ n + 0)))%nat with (2 ^ (S n))%nat by (simpl; lia). - restore_dims. - repeat rewrite <- Mmult_assoc. - restore_dims. - rewrite (kron_mixed_product swap (I _) (I (2 * 2)) (_)). - Msimpl. - repeat rewrite Mmult_assoc. - restore_dims. - repeat rewrite Mmult_assoc. - remember (⟦ (top_to_bottom_helper n) ⊤%ZX ⟧) as ZX_tb_t. - remember (⟦ top_to_bottom_helper n ⟧) as ZX_tb. - restore_dims. - rewrite (kron_mixed_product (I (2 * 2)) ZX_tb_t swap (I (2 ^ (S n)))) . - Msimpl; [ | shelve]. - rewrite <- (Mmult_1_r _ _ (swap ⊗ ZX_tb)) by shelve. - rewrite n_wire_transpose. - rewrite n_wire_semantics. - rewrite <- 2 kron_assoc by shelve. - restore_dims. - repeat rewrite <- Mmult_assoc by shelve. - rewrite <- 2 kron_id_dist_r by shelve. - rewrite a_swap_3_order_indep. - rewrite 2 kron_id_dist_r by shelve. - repeat rewrite <- Mmult_assoc by shelve. - restore_dims. - rewrite (kron_assoc _ (I 2) (I (2 ^ n))) by shelve. - rewrite id_kron. - replace (2 * (2 ^ n))%nat with (2 ^ (S n))%nat by (simpl; lia). - restore_dims. - repeat rewrite <- Mmult_assoc by shelve. - rewrite kron_mixed_product. - Msimpl. - 2,3: shelve. - restore_dims. - repeat rewrite Mmult_assoc by shelve. + intros n. + rewrite <- a_swap_correct. + rewrite <- n_wire_semantics. + change (I 2) with (⟦ — ⟧). + rewrite <- a_swap_correct. + change (swap ⊗ ⟦n_wire (S n)⟧) with + (⟦ ⨉ ↕ n_wire (S n)⟧). restore_dims. - rewrite kron_mixed_product. - Msimpl; [ | shelve]. - easy. -Unshelve. -all: subst; auto with wf_db. -all: try (apply WF_kron; try lia; replace (2 ^ n + (2 ^ n + 0))%nat with (2 ^ (S n))%nat by (simpl; lia); auto with wf_db). - apply WF_mult. - auto with wf_db. - apply WF_kron; try lia; replace (2 ^ n + (2 ^ n + 0))%nat with (2 ^ (S n))%nat by (simpl; lia); auto with wf_db. + change (⟦ a_swap (S (S (S n))) ⟧ = ⟦ + (⨉ ↕ n_wire (S n)) ⟷ ((— ↕ a_swap (S (S n))) + ⟷ (⨉ ↕ n_wire (S n))) ⟧). + rewrite 2!perm_of_zx_permutation_semantics by auto_zxperm. + apply perm_to_matrix_eq_of_perm_eq. + cbn [perm_of_zx]. + rewrite perm_of_n_wire, 2!perm_of_a_swap. + rewrite swap_perm_defn by lia. + rewrite stack_perms_idn_f, stack_perms_WF_idn by auto_perm. + unfold swap_2_perm. + intros k Hk. + rewrite <- Combinators.compose_assoc. + unfold compose at 1. + bdestruct (k =? 0); + [unfold swap_perm; bdestructΩ'; + unfold compose; bdestructΩ'|]. + bdestruct (k =? 1); + [unfold swap_perm; bdestructΩ'; + unfold compose; bdestructΩ'|]. + unfold swap_perm. + simplify_bools_lia_one_kernel. + unfold compose. + bdestructΩ'. Qed. Lemma a_swap_transpose : forall n, diff --git a/src/CoreRules/XRules.v b/src/CoreRules/XRules.v index 9a32713..b36d19d 100644 --- a/src/CoreRules/XRules.v +++ b/src/CoreRules/XRules.v @@ -81,6 +81,14 @@ Lemma X_absolute_fusion : forall {n m o} α β, X n o (α + β). Proof. intros. colorswap_of (@Z_absolute_fusion n m o). Qed. +Lemma X_split_left : forall n m α, + X n m α ∝ X n 1 α ⟷ X 1 m 0. +Proof. intros n m α. colorswap_of (Z_split_left n m α). Qed. + +Lemma X_split_right : forall n m α, + X n m α ∝ X n 1 0 ⟷ X 1 m α. +Proof. intros n m α. colorswap_of (Z_split_right n m α). Qed. + Lemma dominated_X_spider_fusion_top_right : forall n m0 m1 o α β, (X n (S m0) α ↕ n_wire m1 ⟷ X (S m0 + m1) o β) ∝ X (n + m1) o (α + β). diff --git a/src/CoreRules/ZRules.v b/src/CoreRules/ZRules.v index fc869a6..31a1be6 100644 --- a/src/CoreRules/ZRules.v +++ b/src/CoreRules/ZRules.v @@ -316,6 +316,22 @@ Proof. apply IHm. Qed. +Lemma Z_split_left : forall n m α, + Z n m α ∝ Z n 1 α ⟷ Z 1 m 0. +Proof. + intros n m α. + rewrite Z_absolute_fusion. + now rewrite Rplus_0_r. +Qed. + +Lemma Z_split_right : forall n m α, + Z n m α ∝ Z n 1 0 ⟷ Z 1 m α. +Proof. + intros n m α. + rewrite Z_absolute_fusion. + now rewrite Rplus_0_l. +Qed. + Lemma dominated_Z_spider_fusion_top_right : forall n m0 m1 o α β, (Z n (S m0) α ↕ n_wire m1 ⟷ Z (S m0 + m1) o β) ∝ Z (n + m1) o (α + β). @@ -434,16 +450,11 @@ Qed. Lemma Z_self_cap_absorbtion_base : forall {n} α, Z n 2%nat α ⟷ ⊃ ∝ Z n 0%nat α. Proof. intros. + rewrite (Z_split_left n 0 α), Z_split_left. + rewrite compose_assoc. + apply compose_simplify; [easy|]. prop_exists_nonzero 1. - Msimpl. - prep_matrix_equivalence. - intros i j Hi Hj. - destruct i as [|[]]; [..|cbn in Hi; lia]; - cbn; [|lca]. - destruct j; [destruct n; cbn -[Nat.eqb]; - [cbn|pose proof (Modulus.pow2_nonzero n); - Modulus.bdestructΩ']; lca|]. - Modulus.bdestructΩ'; lca. + lma'. Qed. Lemma Z_self_cap_absorbtion_top : forall {n m α}, (Z) n (S (S m)) α ⟷ (⊃ ↕ n_wire m) ∝ Z n m α. @@ -820,72 +831,18 @@ Qed. Lemma Z_n_wrap_under_r_base_unswapped : forall n m α, Z (n + m) 0 α ∝ (Z n m α ↕ n_wire m) ⟷ n_cup_unswapped m. Proof. - intros. - generalize dependent n. - generalize dependent α. - induction m; intros; [simpl; cleanup_zx; simpl_casts; subst; easy | ]. - remember (Z (n + (S m)) _ _) as LHS. - rewrite n_cup_unswapped_grow_l. - rewrite <- (@cast_Z n _ (m + 1)). - rewrite Z_add_r_base_rot. - simpl_casts. - rewrite <- compose_assoc. - simpl. - rewrite cast_compose_r. - simpl_casts. - rewrite (cast_compose_l _ _ (Z n 2 α ⟷ (Z 1 m 0 ↕ Z 1 1 0) ↕ n_wire S m)). - simpl_casts. - rewrite stack_assoc. - rewrite stack_nwire_distribute_r. - rewrite (stack_assoc (Z 1 m 0) _ (n_wire (S m))). - simpl_casts. - rewrite compose_assoc. - simpl. - rewrite (stack_assoc_back (Z 1 1 0) — (n_wire m)). - simpl_casts. - erewrite <- cast_compose_mid_contract. - simpl_casts. - erewrite <- (@cast_id (2 + m) (2 + m) _ _ (Z 1 1 0 ↕ — ↕ (n_wire m))). - rewrite <- (stack_compose_distr (Z 1 m 0) (n_wire m) _ (⊃ ↕ n_wire m)). - simpl_casts. - cleanup_zx. - rewrite <- (stack_compose_distr (— ↕ —) ⊃ (n_wire m) (n_wire m)). - bundle_wires. - cleanup_zx. - rewrite cast_compose_r. - simpl_casts. - simpl. - rewrite (stack_assoc_back _ —). - rewrite (stack_assoc_back _ ⊃ (n_wire m)). - rewrite <- cast_compose_mid_contract. - rewrite <- stack_nwire_distribute_r. - rewrite <- (nwire_stack_compose_botleft (Z 1 m 0) ⊃). - simpl. - cleanup_zx; simpl_casts. - rewrite <- compose_assoc. - rewrite stack_assoc_back. - simpl_casts. - rewrite cast_compose_r. - simpl_casts. - rewrite <- stack_wire_distribute_r. - rewrite <- Z_0_is_wire at 1. - rewrite <- Z_add_r_base_rot. - erewrite (cast_compose_l _ _ (Z _ _ _ ↕ —)). - erewrite (cast_compose_partial_contract_r _ _ _ m _ _ _ _ _ _ _ (n_wire m ↕ ⊃)). - rewrite <- (@Z_wrap_under_bot_right n m α). - simpl_casts. - eapply (cast_diagrams (n + 1 + m) 0). - erewrite <- (@cast_Z (n + 1) _ (m) (m + 0)). - rewrite cast_stack_l. - rewrite (cast_compose_mid (m + m)). - rewrite 2 cast_contract. - rewrite <- cast_compose_mid_contract. - rewrite <- IHm. - rewrite HeqLHS. - simpl_casts. - easy. -Unshelve. - all: lia. + intros n m α. + rewrite (Z_split_left n m), stack_nwire_distribute_r. + rewrite compose_assoc, n_cup_unswapped_pullthrough_top. + cbn [ZXCore.transpose]. + rewrite Z_zxperm_absorbtion_left, Z_zxperm_absorbtion_right by auto_zxperm. + rewrite <- compose_assoc, <- stack_compose_distr. + rewrite nwire_removal_l, nwire_removal_r. + unfold n_cup_unswapped. + rewrite cup_Z. + rewrite Z_zxperm_absorbtion_left by auto_zxperm. + rewrite <- Z_add_l. + now rewrite 2!Rplus_0_r. Qed. Lemma Z_n_wrap_under_r_base : forall n m α, Z (n + m) 0 α ∝ (Z n m α ↕ n_wire m) ⟷ n_cup m. @@ -901,59 +858,12 @@ Qed. Lemma Z_n_wrap_over_r_base_unswapped : forall n m α, Z (m + n) 0 α ∝ (n_wire m ↕ Z n m α) ⟷ n_cup_unswapped m. Proof. - intros. - generalize dependent n. - generalize dependent α. - induction m; intros; [simpl; cleanup_zx; simpl_casts; subst; easy | ]. - remember (Z (S m + n) 0 α) as LHS. - rewrite n_cup_unswapped_grow_l. - rewrite <- (@cast_Z n _ (1 + m)). - rewrite Z_add_r_base_rot. - simpl_casts. - rewrite stack_nwire_distribute_l. (* TODO: rename *) - rewrite n_wire_grow_r at 2. - rewrite <- compose_assoc. - rewrite (compose_assoc (n_wire (S m) ↕ Z n 2 α)). - rewrite cast_stack_l. - rewrite 2 stack_assoc. - simpl_casts. - erewrite <- (cast_compose_mid_contract (S m + 2) (S m + S m) (m + m) _ _ _ _ _ _ (n_wire m ↕ (— ↕ (Z 1 1 0 ↕ Z 1 m 0))) (n_wire m ↕ (⊃ ↕ n_wire m))). - rewrite <- stack_nwire_distribute_l. - rewrite stack_assoc_back. - simpl_casts. - rewrite <- (stack_compose_distr (— ↕ (Z 1 1 0)) ⊃ (Z 1 m 0)). - rewrite (stack_empty_r_rev ⊃). - simpl_casts. - replace ⦰ with (n_wire 0) by easy. - rewrite <- (Z_wrap_over_top_left 1 0). - cleanup_zx. - rewrite Z_2_0_0_is_cap. - rewrite n_wire_grow_r. - rewrite cast_stack_l. - rewrite stack_assoc. - simpl_casts. - erewrite (cast_compose_mid (m + 3) _ _ (cast _ _ _ _ _) (cast _ _ _ _ (n_wire m ↕ (⊃ ↕ Z 1 m 0)))). - rewrite cast_contract. - rewrite cast_contract. - rewrite <- cast_compose_mid_contract. - rewrite <- stack_compose_distr. - cleanup_zx. - rewrite <- (nwire_stack_compose_botleft ⊃ (Z 1 m 0)). - rewrite <- compose_assoc. - rewrite <- (Z_wrap_over_top_left n 1). - simpl. - cleanup_zx. - rewrite Z_spider_1_1_fusion. - eapply (cast_diagrams (m + (S n)) 0). - rewrite cast_compose_l. - simpl_casts. - rewrite <- IHm. - replace (α + 0)%R with α by lra. - rewrite HeqLHS. - simpl_casts. - easy. -Unshelve. - all: lia. + intros n m α. + rewrite Z_n_wrap_under_r_base_unswapped. + rewrite n_cup_unswapped_pullthrough_top. + cbn [ZXCore.transpose]. + now rewrite Z_zxperm_absorbtion_left, + Z_zxperm_absorbtion_right by auto_zxperm. Qed. Lemma Z_n_wrap_over_r_base : forall n m α, Z (m + n) 0 α ∝ (n_wire m ↕ Z n m α) ⟷ n_cup m. diff --git a/src/Permutations/ZXpermAutomation.v b/src/Permutations/ZXpermAutomation.v index 08a5881..0090635 100644 --- a/src/Permutations/ZXpermAutomation.v +++ b/src/Permutations/ZXpermAutomation.v @@ -2,6 +2,9 @@ Require Import ZXCore. Require CastRules ComposeRules. Require Export ZXperm. +#[export] Hint Extern 100 (WF_Matrix _) => + apply WF_Matrix_dim_change : wf_db. + Create HintDb perm_of_zx_cleanup_db. Create HintDb zxperm_db. #[export] Hint Constructors ZXperm : zxperm_db. diff --git a/src/Permutations/ZXpermFacts.v b/src/Permutations/ZXpermFacts.v index b70c932..f726c11 100644 --- a/src/Permutations/ZXpermFacts.v +++ b/src/Permutations/ZXpermFacts.v @@ -490,8 +490,9 @@ Qed. Lemma compose_zxperm_l' {n m o} (zxp : ZX n m) (zx0 : ZX m o) zx1 (H : ZXperm zxp) : - zxp ⊤ ⟷ zx1 ∝ zx0 <-> zx1 ∝ zxp ⟷ zx0. + zx1 ∝ zxp ⟷ zx0 <-> zxp ⊤ ⟷ zx1 ∝ zx0. Proof. + symmetry. split; [intros <- | intros ->]; rewrite <- compose_assoc, ?zxperm_transpose_left_inverse, ?zxperm_transpose_right_inverse @@ -512,8 +513,9 @@ Qed. Lemma compose_zxperm_r' {n m o} (zxp : ZX m o) (zx0 : ZX n m) zx1 (H : ZXperm zxp) : - zx1 ⟷ zxp ⊤ ∝ zx0 <-> zx1 ∝ zx0 ⟷ zxp. + zx1 ∝ zx0 ⟷ zxp <-> zx1 ⟷ zxp ⊤ ∝ zx0. Proof. + symmetry. split; [intros <- | intros ->]; rewrite compose_assoc, ?zxperm_transpose_left_inverse, ?zxperm_transpose_right_inverse