Improve permutations, much small proof repair and improvement, includ…

…ing to use new ZXperm machinery
inQWIRE · Aug 20, 2024 · 676d80b · 676d80b
1 parent 451871c
commit 676d80b
Show file tree

Hide file tree

Showing 33 changed files with 1,630 additions and 11,553 deletions.
diff --git a/src/CoreData/QlibTemp.v b/src/CoreData/QlibTemp.v
diff --git a/src/CoreData/SemanticCore.v b/src/CoreData/SemanticCore.v
diff --git a/src/CoreData/ZXCore.v b/src/CoreData/ZXCore.v
@@ -1,9 +1,9 @@
 Require Import QuantumLib.Quantum.
 Require Import QuantumLib.Proportional.
 Require Import QuantumLib.VectorStates.
+Require Import QuantumLib.Kronecker.
 
 Require Export SemanticCore.
-Require Export QlibTemp.
 
 (* 
 Base constructions for the ZX calculus, lets us build every diagram inductively.
@@ -99,7 +99,9 @@ Proof.
   apply cast_semantics.
 Qed.
 
-Tactic Notation "simpl_cast_semantics" := try repeat rewrite cast_semantics; try repeat (rewrite cast_semantics_dim; unfold cast_semantics_dim_eqn).
+Ltac simpl_cast_semantics := 
+  try repeat rewrite cast_semantics; 
+  try repeat (rewrite cast_semantics_dim; unfold cast_semantics_dim_eqn).
 (* @nocheck name *)
 
 Fixpoint ZX_dirac_sem {n m} (zx : ZX n m) : 
@@ -246,8 +248,8 @@ Lemma semantics_transpose_comm {nIn nOut} : forall (zx : ZX nIn nOut),
 Proof.
   induction zx.
   - Msimpl; reflexivity.
-  - simpl; solve_matrix.
-  - simpl; solve_matrix.
+  - lma'.
+  - lma'.
   - simpl; lma.
   - simpl; rewrite id_transpose_eq; reflexivity.
   - simpl; rewrite hadamard_st; reflexivity.
@@ -264,8 +266,8 @@ Proof.
   intros.
   induction zx.
   - simpl; Msimpl; reflexivity.
-  - simpl; solve_matrix.
-  - simpl; solve_matrix.
+  - lma'. 
+  - lma'. 
   - simpl; lma.
   - simpl; Msimpl; reflexivity.
   - simpl; lma.
@@ -295,11 +297,34 @@ Lemma semantics_colorswap_comm {nIn nOut} : forall (zx : ZX nIn nOut),
 Proof.
   induction zx.
   - simpl; Msimpl; reflexivity.
-  - solve_matrix.
-  - solve_matrix.
-  - simpl.
+  - cbn.
+    apply mat_equiv_eq; 
+    [auto using show_WF_list2D_to_matrix with wf_db..|].
+    rewrite kron_1_l_mat_equiv.
+    rewrite Mmult_assoc, Mmult_1_r by now apply show_WF_list2D_to_matrix.
+    compute_matrix (hadamard ⊗ hadamard).
+    group_radicals.
+    rewrite make_WF_equiv.
+    unfold Mmult.
+    by_cell; lca.
+  - cbn.
+    apply mat_equiv_eq; 
+    [auto using show_WF_list2D_to_matrix with wf_db..|].
+    rewrite kron_1_l_mat_equiv.
+    rewrite Mmult_1_l by now apply show_WF_list2D_to_matrix.
+    compute_matrix (hadamard ⊗ hadamard).
+    group_radicals.
+    rewrite make_WF_equiv.
+    unfold Mmult.
+    by_cell; lca.
+  - cbn.
     Msimpl.
-    solve_matrix.
+    restore_dims.
+    rewrite swap_eq_kron_comm.
+    rewrite kron_comm_commutes_r by auto_wf.
+    rewrite Mmult_assoc.
+    rewrite kron_mixed_product, MmultHH, id_kron.
+    now rewrite Mmult_1_r by auto_wf.
   - simpl; Msimpl; restore_dims; rewrite MmultHH; reflexivity.
   - simpl; Msimpl; restore_dims; rewrite MmultHH; Msimpl; reflexivity.
   - simpl. unfold X_semantics.
@@ -377,14 +402,20 @@ Qed.
 
 Lemma z_1_1_pi_σz :
 	⟦ Z 1 1 PI ⟧ = σz.
-Proof. solve_matrix. autorewrite with Cexp_db. lca. Qed.
+Proof. lma'. autorewrite with Cexp_db. lca. Qed.
 
 Lemma x_1_1_pi_σx :
 	⟦ X 1 1 PI ⟧ = σx.
-Proof. 
-	simpl. 
-	unfold X_semantics. simpl; Msimpl. solve_matrix; autorewrite with Cexp_db. 
-	all: C_field_simplify; [lca | C_field].
+Proof.
+  prep_matrix_equivalence.
+  cbn [ZX_semantics].
+  unfold X_semantics.
+  rewrite kron_n_1 by auto_wf.
+  simpl_rewrite z_1_1_pi_σz.
+  restore_dims.
+  compute_matrix (hadamard × σz × hadamard).
+  autorewrite with C_db.
+  by_cell; reflexivity.
 Qed.
 
 Definition zx_triangle : ZX 1 1 :=

diff --git a/src/CoreRules/CapCupRules.v b/src/CoreRules/CapCupRules.v
@@ -9,17 +9,17 @@ Require Import CoreAutomation.
 Lemma cup_Z : ⊃ ∝ Z 2 0 0.
 Proof.
   prop_exists_nonzero 1.
-  Msimpl; simpl.
-  solve_matrix.
-  autorewrite with Cexp_db; easy.
+  rewrite Mscale_1_l.
+  lma'.
+  now rewrite Cexp_0.
 Qed.
 
 Lemma cap_Z : ⊂ ∝ Z 0 2 0.
 Proof.
   prop_exists_nonzero 1.
-  Msimpl; simpl.
-  solve_matrix.
-  autorewrite with Cexp_db; easy.
+  rewrite Mscale_1_l.
+  lma'.
+  now rewrite Cexp_0.
 Qed.
 
 Lemma cup_X : ⊃ ∝ X 2 0 0.
@@ -31,23 +31,19 @@ Proof. colorswap_of cap_Z. Qed.
 Lemma n_cup_0_empty : n_cup 0 ∝ ⦰.
 Proof.
   unfold n_cup.
-  repeat (simpl;
-  cleanup_zx;
-  simpl_casts).
-  easy.
+  cbn.
+  cleanup_zx.
+  apply cast_id.
 Qed.
 
 Lemma n_cup_1_cup : n_cup 1 ∝ ⊃.
 Proof.
   unfold n_cup.
-  simpl.
-  simpl_casts.
-  simpl.
-  cleanup_zx.
-  simpl_casts.
-  bundle_wires.
+  cbn.
+  rewrite cast_id.
   cleanup_zx.
-  easy.
+  rewrite !cast_id.
+  now rewrite wire_to_n_wire, n_wire_stack, 2!nwire_removal_l.
 Qed.
 
 Opaque n_cup.
@@ -78,23 +74,21 @@ Proof.
   intros.
   induction n.
   - simpl.
-    simpl_casts.
-    cleanup_zx.
-    simpl_casts.
-    bundle_wires.
+    rewrite !cast_id.
     cleanup_zx.
-    easy.
+    rewrite !cast_id.
+    now rewrite wire_to_n_wire, n_wire_stack, nwire_removal_l.
   - simpl.
     simpl in IHn.
     rewrite IHn at 1.
     simpl_casts.
     rewrite stack_wire_distribute_l.
     rewrite stack_wire_distribute_r.
-    bundle_wires.
-    erewrite <- (@cast_n_wire (n + 1) (1 + n)).
+    change (— ↕ n_wire n) with (n_wire (1 + n)).
+    rewrite <- (@cast_n_wire (n + 1) (1 + n)).
     rewrite <- ComposeRules.compose_assoc.
     apply compose_simplify; [ | easy].
-    erewrite (cast_compose_mid (S (n + S n))).
+    rewrite (cast_compose_mid (S (n + S n))).
     rewrite cast_compose_distribute.
     repeat rewrite cast_contract.
     apply compose_simplify; [ | apply cast_simplify; easy].
@@ -103,13 +97,13 @@ Proof.
     simpl_casts.
     rewrite 3 stack_assoc_back.
     simpl_casts.
-    erewrite <- (@cast_n_wire (n + 1) (1 + n)) at 2.
+    rewrite <- (@cast_n_wire (n + 1) (1 + n)) at 2.
     rewrite cast_stack_r.
     simpl.
-    rewrite (stack_assoc (— ↕ n_wire n ↕ ⊃) (n_wire n) —). 
-    bundle_wires.
+    rewrite (stack_assoc (— ↕ n_wire n ↕ ⊃) (n_wire n) —).
+    rewrite <- n_wire_stack.
     simpl_casts.
-    easy.
+    now rewrite <- wire_to_n_wire.
 Unshelve.
   all: lia.
 Qed.

diff --git a/src/CoreRules/CastRules.v b/src/CoreRules/CastRules.v
@@ -26,14 +26,30 @@ Proof.
   congruence.
 Qed.
 
-Tactic Notation "cast_irrelevance" := 
+Ltac cast_irrelevance := 
   apply cast_simplify; try easy.
 
-Tactic Notation "auto_cast_eqn" tactic3(tac) := unshelve tac; try lia; shelve_unifiable.
+Ltac auto_cast_eqn tac := 
+  unshelve tac; try lia; shelve_unifiable.
+
+Tactic Notation "auto_cast_eqn" tactic3(tac) := 
+  unshelve tac; try lia; shelve_unifiable.
+
+Create HintDb cast_simpl_db.
 
 #[export] Hint Rewrite @cast_id : cast_simpl_db.
-Tactic Notation "simpl_casts" := auto_cast_eqn (autorewrite with cast_simpl_db); repeat cast_irrelevance.
-Tactic Notation "simpl_casts_in" hyp(H) := auto_cast_eqn (autorewrite with cast_simpl_db in H); repeat (apply cast_simplify in H).
+
+Ltac simpl_casts := 
+  auto_cast_eqn (autorewrite with cast_simpl_db); 
+  repeat cast_irrelevance.
+
+Ltac simpl_casts_in H := 
+  auto_cast_eqn (autorewrite with cast_simpl_db in H); 
+  repeat (apply cast_simplify in H).
+
+Tactic Notation "simpl_casts_in" hyp(H) := 
+  auto_cast_eqn (autorewrite with cast_simpl_db in H); 
+  repeat (apply cast_simplify in H).
 
 
 Lemma cast_stack_l : forall {nTop nTop' mTop mTop' nBot mBot} prfnTop prfmTop prfn prfm
@@ -325,6 +341,26 @@ Qed.
 
 #[export] Hint Rewrite @cast_Z @cast_X: cast_simpl_db.
 
+Lemma cast_Z_to_refl_r n m α {m' o' o} (zx : ZX m' o') Hm Ho : 
+	Z n m α ⟷ cast m o Hm Ho zx = 
+	Z n m' α ⟷ cast m' o eq_refl Ho zx.
+Proof. now subst. Qed.
+
+Lemma cast_X_to_refl_r n m α {m' o' o} (zx : ZX m' o') Hm Ho : 
+	X n m α ⟷ cast m o Hm Ho zx = 
+	X n m' α ⟷ cast m' o eq_refl Ho zx.
+Proof. now subst. Qed.
+
+Lemma cast_Z_contract_r n m α {m' o' o} (zx : ZX m' o') Hm Ho : 
+	Z n m α ⟷ cast m o Hm Ho zx = 
+	cast n o eq_refl Ho (Z n m' α ⟷ zx).
+Proof. now subst. Qed.
+
+Lemma cast_X_contract_r n m α {m' o' o} (zx : ZX m' o') Hm Ho : 
+	X n m α ⟷ cast m o Hm Ho zx = 
+	cast n o eq_refl Ho (X n m' α ⟷ zx).
+Proof. now subst. Qed.
+
 Lemma cast_n_stack1 : forall {n n'} prfn prfm (zx : ZX 1 1),
   cast n' n' prfn prfm (n ↑ zx) ∝ n' ↑ zx.
 Proof.

diff --git a/src/CoreRules/CoreAutomation.v b/src/CoreRules/CoreAutomation.v
@@ -20,9 +20,10 @@ match goal with
   | [ |- ?zx1 ∝ ?zx2] => try (wire_to_n_wire_safe_aux zx1); try (wire_to_n_wire_safe_aux zx2); repeat rewrite n_stack_n_wire_1_n_wire
 end.
 
-Tactic Notation "bundle_wires" := wire_to_n_wire_safe; (* change wires to n_wires *)
-                                  repeat rewrite n_wire_stack; (* stack n_wire *)
-                                  repeat rewrite <- wire_to_n_wire. (* restore *)
+Ltac bundle_wires := 
+  wire_to_n_wire_safe; (* change wires to n_wires *)
+  repeat rewrite n_wire_stack; (* stack n_wire *)
+  repeat rewrite <- wire_to_n_wire. (* restore *)
 
 #[export] Hint Rewrite 
   (fun n => @compose_empty_l n)
@@ -39,7 +40,7 @@ Tactic Notation "bundle_wires" := wire_to_n_wire_safe; (* change wires to n_wire
   (fun n m o p => @nwire_stack_compose_topleft n m o p)
   (fun n m o p => @nwire_stack_compose_botleft n m o p)
   : cleanup_zx_db.
-Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db).
+Ltac cleanup_zx := auto_cast_eqn (autorewrite with cleanup_zx_db).
 
 #[export] Hint Rewrite
   (fun n m o p => @cast_colorswap n m o p)