cleanup

DiscreteProb.v

@@ -1501,7 +1501,6 @@ Proof.
     rewrite <- le_plus_minus in H0.
     rewrite plus_comm in H0.
     assumption.
-    Search (?a <= _ * ?a)%nat.
     destruct (mult_O_le (2^k) (2^n))%nat; auto.
     assert (2 <> 0)%nat by lia.
     apply (pow_positive 2 n) in H2.

FTA.v

@@ -2,114 +2,6 @@ Require Import Polar.
 Require Export Ctopology.
 Require Import Setoid.
 
-
-(* defining Rsum and some lemmas (does this exist already??) *)
-
-(*
-Fixpoint Rsum (f : nat -> R) (n : nat) : R := 
-  match n with
-  | 0 => 0
-  | S n' => (Rsum f n' +  f n')%R
-  end.
-
-Lemma Rsum_eq : forall f g n, f = g -> Rsum f n = Rsum g n.
-Proof. intros f g n H. subst. reflexivity. Qed.
-
-Lemma Rsum_0_bounded : forall f n, (forall x, (x < n)%nat -> f x = 0) -> Rsum f n = 0. 
-Proof.
-  intros.
-  induction n.
-  - reflexivity.
-  - simpl.
-    rewrite IHn, H. 
-    lra.
-    lia.
-    intros.
-    apply H.
-    lia.
-Qed.
-
-Lemma Rsum_eq_bounded : forall f g n, (forall x, (x < n)%nat -> f x = g x) -> Rsum f n = Rsum g n.
-Proof. 
-  intros f g n H. 
-  induction n.
-  + simpl. reflexivity.
-  + simpl. 
-    rewrite H by lia.
-    rewrite IHn by (intros; apply H; lia).
-    reflexivity.
-Qed.
-
-Lemma Rsum_plus : forall f g n, Rsum (fun x => (f x + g x)%R) n = (Rsum f n + Rsum g n)%R.
-Proof.
-  intros f g n.
-  induction n.
-  + simpl. lra.
-  + simpl. rewrite IHn. lra.
-Qed.
-
-Lemma Rsum_mult_l : forall c f n, (c * Rsum f n = Rsum (fun x => c * f x) n)%R.
-Proof.
-  intros c f n.
-  induction n.
-  + simpl; lra.
-  + simpl.
-    rewrite Rmult_plus_distr_l.
-    rewrite IHn.
-    reflexivity.
-Qed.
-
-Lemma Rsum_mult_r : forall c f n, (Rsum f n * c = Rsum (fun x => f x * c) n)%R.
-Proof.
-  intros c f n.
-  induction n.
-  + simpl; lra.
-  + simpl.
-    rewrite Rmult_plus_distr_r.
-    rewrite IHn.
-    reflexivity.
-Qed.
-
-Lemma Rsum_extend_r : forall n f, (Rsum f n + f n)%R = Rsum f (S n).
-Proof. reflexivity. Qed.
-
-Lemma Rsum_extend_l : forall n f, (f O + Rsum (fun x => f (S x)) n)%R = Rsum f (S n).
-Proof.
-  intros n f.
-  induction n.
-  + simpl; lra.
-  + simpl.
-    rewrite <- Rplus_assoc.
-    rewrite IHn.
-    simpl.
-    reflexivity.
-Qed.
-
-Lemma Rsum_sum : forall m n f, Rsum f (m + n) = 
-                          (Rsum f m + Rsum (fun x => f (m + x)%nat) n)%R. 
-Proof.    
-  intros m n f.
-  induction m.
-  + simpl. rewrite Rplus_0_l. reflexivity. 
-  + simpl.
-    rewrite IHm.
-    repeat rewrite <- Rplus_assoc.
-    remember (fun y => f (m + y)%nat) as g.
-    replace (f m) with (g O) by (subst; rewrite plus_0_r; reflexivity).
-    replace (f (m + n)%nat) with (g n) by (subst; reflexivity).
-    replace (Rsum (fun x : nat => f (S (m + x))) n) with
-            (Rsum (fun x : nat => g (S x)) n).
-    2:{ apply Rsum_eq; subst. apply functional_extensionality.
-    intros; rewrite <- plus_n_Sm. reflexivity. }
-    repeat rewrite Rplus_assoc.
-    rewrite Rsum_extend_l.
-    rewrite Rsum_extend_r.
-    reflexivity.
-Qed. 
-*)
-
-
-
 (*********************************************************************)
 (* defining poly_coef_norm and showing how it can be used as a bound *)
 (*********************************************************************)

Measurement.v

@@ -50,20 +50,6 @@ Proof.
   all: bdestruct_all; lca.
 Qed.
 
-(* 
-Lemma Rsum_Msum : forall n (f : nat -> Square 1),
-  big_sum (fun i : nat => fst (f i O O)) n = fst (big_sum f O O n).
-Proof.
-  intros.
-  rewrite Msum_Csum.
-  rewrite <- Rsum_Csum.
-  induction n; simpl.
-  reflexivity.
-  rewrite IHn.
-  reflexivity.
-Qed.
-*)
-
 Lemma prob_partial_meas_alt : 
   forall {m n} (ϕ : Vector (2^m)) (ψ : Vector (2^(m + n))),
   @prob_partial_meas m n ϕ ψ = ((norm ((ϕ ⊗ I (2 ^ n))† × ψ)) ^ 2)%R.
@@ -98,7 +84,6 @@ Proof.
   intros.
   destruct a; destruct b; easy. 
 Qed.
-
 
 Lemma partial_meas_tensor : 
   forall {m n} (ϕ : Vector (2^m)) (ψ1 : Vector (2^m)) (ψ2 : Vector (2^n)),

Prelim.v

@@ -419,53 +419,3 @@ Proof. induction n as [| n'].
 Qed.
 
 #[export] Hint Resolve firstn_subset skipn_subset : sub_db.
-
-(** Sums over natural numbers *)
-
-Fixpoint Nsum (n : nat) (f : nat -> nat) :=
-  match n with
-  | O => O
-  | S n' => (Nsum n' f + f n')%nat
-  end.
-
-Lemma Nsum_eq : forall n f g,
-  (forall x, (x < n)%nat -> f x = g x) ->
-  Nsum n f = Nsum n g.
-Proof.
-  intros. induction n. easy.
-  simpl. rewrite IHn. rewrite H. easy.
-  lia. intros. apply H. lia.
-Qed.
-
-Lemma Nsum_scale : forall n f d,
-  (Nsum n (fun i => d * f i) = d * Nsum n f)%nat.
-Proof.
-  intros. induction n. simpl. lia. 
-  simpl. rewrite IHn. lia.
-Qed.
-
-Lemma Nsum_le : forall n f g,
-  (forall x, x < n -> f x <= g x)%nat ->
-  (Nsum n f <= Nsum n g)%nat.
-Proof.
-  intros. induction n. simpl. easy.
-  simpl.
-  assert (f n <= g n)%nat.
-  { apply H. lia. }
-  assert (Nsum n f <= Nsum n g)%nat.
-  { apply IHn. intros. apply H. lia. }
-  lia.
-Qed.
-
-Lemma Nsum_add : forall n f g,
-  (Nsum n (fun i => f i + g i) = Nsum n f + Nsum n g)%nat.
-Proof.
-  intros. induction n. easy.
-  simpl. rewrite IHn. lia.
-Qed.
-
-Lemma Nsum_zero : forall n, Nsum n (fun _ => O) = O.
-Proof.
-  induction n. easy.
-  simpl. rewrite IHn. easy.
-Qed.

Quantum.v

@@ -1872,22 +1872,6 @@ Proof.
   reflexivity.
 Qed.
 
-
-(* This is compose_super_correct 
-Lemma WF_Superoperator_compose : forall m n p (s : Superoperator n p) (s' : Superoperator m n),
-    WF_Superoperator s ->
-    WF_Superoperator s' ->
-    WF_Superoperator (compose_super s s').
-Proof.
-  unfold WF_Superoperator.
-  intros m n p s s' H H0 ρ H1.
-  unfold compose_super.
-  apply H.
-  apply H0.
-  easy.
-Qed.
-*)
-
 (**************)
 (* Automation *)
 (**************)

RealAux.v

@@ -376,140 +376,3 @@ Proof. induction n as [| n'].
          apply IHn'; intros; apply H; lia. 
          apply H; lia. 
 Qed.
-
-
-
-
-(** * Sums *)
-
-
-(* TODO: merge with the above *)
-Definition Rsum (n : nat) (f : nat -> R) : R :=
-  match n with
-  | O => 0
-  | S n => sum_f_R0 f n
-  end.
-
-
-(*
-Lemma Rsum_geq :
-  forall n (f : nat -> R) A,
-    (forall (i : nat), (i < n)%nat -> f i >= A) ->
-    Rsum n f >= n * A.
-Proof.
-  intros. induction n. simpl. lra.
-  assert (Rsum n f >= n * A).
-  { apply IHn. intros. apply H. lia. }
-  rewrite Rsum_extend. replace (S n * A) with (A + n * A).
-  apply Rplus_ge_compat.
-  apply H; lia. assumption.
-  destruct n. simpl. lra. simpl. lra.
-Qed.
-
-Lemma Rsum_geq_0 :
-  forall n (f : nat -> R),
-    (forall (i : nat), (i < n)%nat -> f i >= 0) ->
-    Rsum n f >= 0.
-Proof. intros. specialize (Rsum_geq n f 0 H) as G. lra. Qed.
-
-Lemma Rsum_nonneg_Rsum_zero :
-  forall n (f : nat -> R),
-    (forall (i : nat), (i < n)%nat -> f i >= 0) ->
-    Rsum n f <= 0 ->
-    Rsum n f = 0.
-Proof. intros. specialize (Rsum_geq_0 n f H) as G. lra. Qed.
-
-Lemma Rsum_nonneg_f_zero :
-  forall n (f : nat -> R),
-    (forall (i : nat), (i < n)%nat -> f i >= 0) ->
-    Rsum n f = 0 ->
-    (forall (i : nat), (i < n)%nat -> f i = 0).
-Proof.
-  intros. induction n. lia.
-  rewrite Rsum_extend in H0.
-  assert (f n >= 0) by (apply H; lia).
-  assert (forall (i : nat), (i < n)%nat -> f i >= 0) by (intros; apply H; lia).
-  assert (Rsum n f <= 0) by lra.
-  specialize (Rsum_nonneg_Rsum_zero n f H3 H4) as G.
-  destruct (i =? n)%nat eqn:E.
-  apply beq_nat_true in E. rewrite G in H0. rewrite E. lra.
-  apply beq_nat_false in E. apply IHn; try assumption. lia.
-Qed.
-
-Lemma rsum_swap_order :
-  forall (m n : nat) (f : nat -> nat -> R),
-    sum_f_R0 (fun j => sum_f_R0 (fun i => f j i) m) n = sum_f_R0 (fun i => sum_f_R0 (fun j => f j i) n) m.
-Proof.
-  intros. induction n; try easy.
-  simpl. rewrite IHn. rewrite <- sum_plus. reflexivity.
-Qed.
-
-Lemma find_decidable :
-    forall (m t : nat) (g : nat -> nat),
-    (exists i, i <= m /\ g i = t)%nat \/ (forall i, i <= m -> g i <> t)%nat.
-Proof.
-  induction m; intros.
-  - destruct (dec_eq_nat (g O) t).
-    + left. exists O. split; easy.
-    + right. intros. replace i with O by lia. easy.
-  - destruct (IHm t g).
-    + left. destruct H. exists x. destruct H. split; lia.
-    + destruct (dec_eq_nat (g (S m)) t).
-      -- left. exists (S m). lia.
-      -- right. intros. inversion H1. lia. apply H. lia.
-Qed.
-
-Lemma rsum_unique :
-    forall (n : nat) (f : nat -> R) (r : R),
-    (exists (i : nat), i <= n /\ f i = r /\ (forall (j : nat), j <= n -> j <> i -> f j = 0)) ->
-    sum_f_R0 f n = r.
-Proof.
-  intros.
-  destruct H as (? & ? & ? & ?).
-  induction n. simpl. apply INR_le in H. inversion H. subst. easy.
-  simpl. destruct (S n =? x) eqn:E.
-  - apply beq_nat_true in E.
-    subst. replace (sum_f_R0 f n) with 0. lra.
-    symmetry. apply sum_eq_R0. intros. apply H1. apply le_INR. constructor. easy. lia.
-  - apply beq_nat_false in E.
-    apply INR_le in H. inversion H. lia. subst. replace (f (S n)) with 0.
-    rewrite IHn. lra. apply le_INR. easy. intros. apply H1; auto. apply Rle_trans with n; auto.
-    apply le_INR. lia. symmetry. apply H1; auto. apply Rle_refl.
-Qed.
-
-Theorem rsum_subset :
-  forall (m n : nat) (f : nat -> R)  (g : nat -> nat),
-    m < n -> (forall (i : nat), 0 <= f i) -> (forall i, i <= m -> g i <= n)%nat ->
-    (forall i j, i <= m -> j <= m -> g i = g j -> i = j)%nat ->
-    sum_f_R0 (fun i => f (g i)) m <= sum_f_R0 f n.
-Proof.
-  intros.
-  set (h := (fun (i : nat) => sum_f_R0 (fun (j : nat) => if i =? g j then f (g j) else 0) m)).
-  assert (forall (i : nat), i <= n -> h i <= f i).
-  { intros. unfold h. simpl.
-    destruct (find_decidable m i g).
-    - destruct H4 as (i0 & H4 & H5).
-      replace (sum_f_R0 (fun j : nat => if i =? g j then f (g j) else 0) m) with (f i). lra.
-      symmetry. apply rsum_unique. exists i0. split.
-      + apply le_INR. easy.
-      + split. subst.  rewrite Nat.eqb_refl. easy.
-        intros. assert (i <> g j). unfold not. intros. subst. apply H2 in H8. apply H7. easy.
-        easy. apply INR_le. easy.
-        replace (i  =? g j) with false. easy. symmetry. apply Nat.eqb_neq. easy.
-    - replace (sum_f_R0 (fun j : nat => if i =? g j then f (g j) else 0) m) with 0. easy.
-      symmetry. apply sum_eq_R0. intros. apply H4 in H5. apply Nat.eqb_neq in H5. rewrite Nat.eqb_sym. rewrite H5. easy. 
-  }
-  assert (sum_f_R0 h n <= sum_f_R0 f n).
-  { apply sum_Rle. intros. apply H3. apply le_INR. easy. }
-  apply Rle_trans with (sum_f_R0 h n); auto.
-  unfold h. rewrite rsum_swap_order.
-  replace (sum_f_R0 (fun i : nat => f (g i)) m) with 
-  (sum_f_R0 (fun i : nat => sum_f_R0 (fun j : nat => if j =? g i then f (g i) else 0) n) m).
-  apply Rle_refl. apply sum_eq. intros.
-  apply rsum_unique. exists (g i). split.
-  - apply le_INR. auto. 
-  - rewrite Nat.eqb_refl. split. easy.
-    intros. apply Nat.eqb_neq in H7. rewrite H7; easy.
-Qed.
-
-*)