merge 2

.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

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