QuantumLib.Proportional

Require Export Matrix.
Require Import Setoid.

Relation for equality up to a global phase.

Definition proportional {m n : nat} (A B : Matrix m n) :=
  ∃ θ , A = Cexp θ .* B.
Infix "∝" := proportional (at level 70).

Lemma proportional_refl : ∀ {m n} (A : Matrix m n), A ∝ A.

Lemma proportional_symm : ∀ {m n} (A B : Matrix m n), A ∝ B → B ∝ A.

Lemma proportional_trans : ∀ {m n} (A B C : Matrix m n),
  A ∝ B → B ∝ C → A ∝ C.

Lemma Mmult_proportional_compat : ∀ {m n o} (A A' : Matrix m n) (B B' : Matrix n o),
  A ∝ A' → B ∝ B' → A × B ∝ A' × B'.

Add Parametric Relation (m n : nat) : (Matrix m n) (@proportional m n)
  reflexivity proved by proportional_refl
  symmetry proved by proportional_symm
  transitivity proved by proportional_trans
  as uc_equiv_rel.

Add Parametric Morphism (m n o : nat) : (@Mmult m n o)
  with signature (@proportional m n ) ==> (@proportional n o ) ==>
                                     (@proportional m o ) as Mmult_mor.