Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Finshed Lemma A24 #29

Merged
merged 13 commits into from
Feb 25, 2024
Merged
30 changes: 30 additions & 0 deletions AlgebraHelpers.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
Require Import QuantumLib.Complex.
(* @Kyle: this Matrix dependency is for just 1 thing. Maybe better to rewrite the sub_mul_mod
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Which Lemma(s) are needed from Matrix? It seems like you've already moved over nat_tight_bound and sub_mod_equiv

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh wait this is from QuantumLib.Matrix; what's the import for?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

its sub_mul_mod

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh I see; I feel like it's fine because we aren't introducing any potential cyclic dependency issues as we are pulling from QuantumLib, not reorganizing code in our own codebase.

proof in here *)
Require Import QuantumLib.Matrix.
Lemma conj_mult_re_is_nonneg: forall (a: C),
Re (a^* * a) >= 0.
Proof.
Expand Down Expand Up @@ -772,4 +775,31 @@ lca.
8,9: assumption.
all: apply RtoC_neq.
all: lra.
Qed.

Lemma nat_tight_bound: forall (i j: nat),
(i <= j -> j < S i -> i = j)%nat.
Proof.
intros i j lb up.
apply Nat.le_antisymm.
assumption.
apply le_S_n. apply up.
Qed.

Lemma sub_mod_equiv: forall (i j: nat),
(i < j * 2 -> j <= i -> (i mod j) = i - j)%nat.
Proof.
intros.
assert ((i - j) = ((i - j) mod j))%nat.
{
symmetry.
apply Nat.mod_small.
lia.
}
rewrite H1.
symmetry.
rewrite <- Nat.mul_1_l with (n := j) at 1.
apply sub_mul_mod.
rewrite Nat.mul_1_l.
assumption.
Qed.
3 changes: 2 additions & 1 deletion ControlledUnitaries.v
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,8 @@ assert (prod_decomp_1 : forall (w : Vector 2), WF_Matrix w -> U × (I 2 ⊗ Q)
rewrite U_beta at 1. rewrite U_beta_p at 1.
lma'.
}
destruct (block_decomp_4 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]]. apply U_unitary.
destruct (@block_decomp_general 2 U) as [P00 [P01 [P10 [P11 [WF_P00 [WF_P01 [WF_P10 [WF_P11 U_block_decomp]]]]]]]]. lia.
apply U_unitary.
assert (prod_decomp_2: forall (w : Vector 2), WF_Matrix w -> U × (I 2 ⊗ Q) × (∣0⟩ ⊗ w) = ∣0⟩ ⊗ (P00 × Q × w) .+ ∣1⟩ ⊗ (P10 × Q × w)).
{
intros w WF_w.
Expand Down
40 changes: 0 additions & 40 deletions ExplicitDecompositions.v
Original file line number Diff line number Diff line change
Expand Up @@ -250,46 +250,6 @@ intros.
lca.
Qed.

Lemma vector2_inner_prod_decomp: forall (a b : Vector 2),
(⟨ a, b ⟩ = (a 0%nat 0%nat)^* * (b 0%nat 0%nat) + (a 1%nat 0%nat)^* * (b 1%nat 0%nat)).
Proof.
intros.
lca.
Qed.

Lemma Mmult_square2_explicit: forall (A B: Square 2),
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).
Proof.
intros. lma'.
unfold WF_Matrix.
intros.
destruct H1.
repeat rewrite H. lca. 1,2: lia.
repeat rewrite H0. lca. 1,2: lia.
Qed.

Lemma Mv_prod_21_explicit: forall (A: Square 2) (v : Vector 2),
WF_Matrix A -> WF_Matrix v ->
(A × v) = ((fun x y =>
match (x,y) with
| (0,0) => (A 0 0)%nat * (v 0 0)%nat + (A 0 1)%nat * (v 1 0)%nat
| (1,0) => (A 1 0)%nat * (v 0 0)%nat + (A 1 1)%nat * (v 1 0)%nat
| _ => C0
end): Square 2).
Proof.
intros.
lma'.
unfold WF_Matrix.
intros.
destruct H1.
destruct x as [|a]. contradict H. lia.
destruct a as [|x]. contradict H. lia. reflexivity.
destruct x as [|a]. destruct y as [|b]. contradict H. lia.
reflexivity.
destruct a as [|x]. destruct y as [|b]. contradict H. lia. reflexivity. reflexivity.
Qed.

Lemma trace_outer_zero_vec2: forall (a : Vector 2),
WF_Matrix a ->
trace (a × (a) †) = 0 -> a = Zero.
Expand Down
Loading