reverting files to most updated versions

.gitignore

@@ -1,4 +1,3 @@
-<<<<<<< HEAD
 *.glob
 *.aux
 *~
@@ -14,38 +13,3 @@ 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,11 +86,8 @@ 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
@@ -211,8 +208,6 @@ 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.
@@ -228,7 +223,6 @@ Proof. intros.
 Qed.
 
 
->>>>>>> QuantumLib/main
 (** ** C is a field *)
 
 Lemma RtoC_plus (x y : R) : RtoC (x + y) = RtoC x + RtoC y.
@@ -327,16 +321,8 @@ 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.
@@ -498,23 +484,6 @@ 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.
- intros c H.
- apply C0_imp in H as [H | H].
- apply C0_fst_neq.
- apply Ropp_neq_0_compat.
- assumption.
- apply C0_snd_neq.
- apply Ropp_neq_0_compat.
- assumption.
-Qed.
-
-=======
-=======
->>>>>>> QuantumLib/main
 Lemma C1_neq_C0 : C1 <> C0.
 Proof. apply C0_fst_neq.
        simpl. 
@@ -552,10 +521,6 @@ 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.
@@ -665,15 +630,12 @@ 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 **)
@@ -771,34 +733,6 @@ Proof.
     field.
 Qed.
 
-<<<<<<< HEAD
-<<<<<<< HEAD
-Lemma Cexp_plus_PI : forall x,
-  Cexp (x + PI) = (- (Cexp x))%C.
-Proof.
-  intros.
-  unfold Cexp.
-  rewrite neg_cos, neg_sin.
-  lca.
-Qed.
-
-Lemma Cexp_minus_PI: forall x : R, Cexp (x - PI) = (- Cexp x)%C.
-Proof.
-  intros x.
-  unfold Cexp.
-  rewrite cos_sym.
-  rewrite Ropp_minus_distr.
-  rewrite Rtrigo_facts.cos_pi_minus.
-  rewrite <- Ropp_minus_distr.
-  rewrite sin_antisym.
-  rewrite Rtrigo_facts.sin_pi_minus.
-  lca.
-Qed.
-
-=======
->>>>>>> Heisenberg-Foundations/main
-=======
->>>>>>> QuantumLib/main
 Lemma Cexp_nonzero : forall θ, Cexp θ <> 0.
 Proof. 
   intro θ. unfold Cexp.
@@ -1033,15 +967,7 @@ 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.
 
@@ -1055,29 +981,12 @@ 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
-    | |- not (@eq _ (Copp _) (RtoC (IZR Z0))) => apply Copp_neq_0_compat
-    | |- not (@eq _ (Cpow _ _) (RtoC (IZR Z0))) => apply Cpow_nonzero
-    | |- not (@eq _ Ci (RtoC (IZR Z0))) => apply C0_snd_neq; simpl
-    | |- not (@eq _ (Cexp _) (RtoC (IZR Z0))) => apply Cexp_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
@@ -1091,26 +1000,11 @@ 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
-  | |- not (@eq _ _ _) => lra
-  | |- Rlt _ _ => lra
-  | |- 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
@@ -1131,15 +1025,6 @@ 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