moved lemmas to correct files.

removed references to swapproperty file

Author: nvaishampayan517

GateHelpers.v

@@ -3,7 +3,6 @@ Require Import QuantumLib.Eigenvectors.
 From Proof Require Import AlgebraHelpers.
 From Proof Require Import MatrixHelpers. 
 From Proof Require Import SwapHelpers.
-From Proof Require Import SwapProperty.
 From Proof Require Import QubitHelpers.
 From Proof Require Import WFHelpers.
 

MatrixHelpers.v

@@ -2426,3 +2426,20 @@ Proof.
     }
   }
 Qed.
+
+Lemma Mmult88_explicit_decomp: forall (A B: Square 8), 
+WF_Matrix A -> WF_Matrix B -> 
+A × B = ((fun x y => 
+A x 0%nat * B 0%nat y + A x 1%nat * B 1%nat y
++ A x 2%nat * B 2%nat y + A x 3%nat * B 3%nat y
++ A x 4%nat * B 4%nat y + A x 5%nat * B 5%nat y
++ A x 6%nat * B 6%nat y + A x 7%nat * B 7%nat y) : Square 8).
+Proof.
+intros.
+lma'.
+unfold WF_Matrix.
+intros.
+destruct H1.
+repeat rewrite H. lca. 1,2,3,4,5,6,7,8: lia.
+repeat rewrite H0. lca. all: lia.
+Qed.

README.md

@@ -13,7 +13,6 @@ Helper Files:
 - MatrixHelpers - Helper lemmas for matrix calculations. 
 - QubitHelpers - Helper lemmas for unit vectors.
 - SwapHelpers - Helper lemmas for properties of swaps.
-- SwapProperty - Particular swap property that takes a long time to compile.
 - PartialTraceDefinitions - Adding the functions for tracing out qubits, and properties of the function.
 - TraceoutHelpers - Contains helper lemmas for tracing out qubits.
 

SwapHelpers.v

@@ -191,24 +191,6 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma Mmult88_explicit_decomp: forall (A B: Square 8), 
-WF_Matrix A -> WF_Matrix B -> 
-A × B = ((fun x y => 
-A x 0%nat * B 0%nat y + A x 1%nat * B 1%nat y
-+ A x 2%nat * B 2%nat y + A x 3%nat * B 3%nat y
-+ A x 4%nat * B 4%nat y + A x 5%nat * B 5%nat y
-+ A x 6%nat * B 6%nat y + A x 7%nat * B 7%nat y) : Square 8).
-Proof.
-intros.
-lma'.
-unfold WF_Matrix.
-intros.
-destruct H1.
-repeat rewrite H. lca. 1,2,3,4,5,6,7,8: lia.
-repeat rewrite H0. lca. all: lia.
-Qed.
-
-
 Property swap_helper : forall (U : Square 4),
   WF_Matrix U -> 
   swapbc × (U ⊗ I 2) × swapbc = swapab × (I 2 ⊗ U) × swapab.

Swaps.v

@@ -2,7 +2,6 @@ Require Import QuantumLib.Quantum.
 From Proof Require Import SwapHelpers.
 From Proof Require Import GateHelpers.
 From Proof Require Import MatrixHelpers.
-From Proof Require Import SwapProperty.
 From Proof Require Import WFHelpers.
 Lemma a10 : forall (a b : Vector 2),
   WF_Matrix a -> WF_Matrix b ->