MultiqubitEntanglement and Measurement
From VQC Require Import Qubit.
Require Import Bool.
Opaque C.
Require Import Bool.
Opaque C.
Notation QState n := (Vector (2^n)).
First, let's look at expressing the basis states:
Definition qubit (x : nat) : Qubit := if x =? 0 then ∣0⟩ else ∣1⟩.
Notation "'∣' x '⟩'" := (qubit x).
Notation "∣ x , y , .. , z ⟩" := (kron .. (kron ∣x⟩ ∣y⟩) .. ∣z⟩) (at level 0).
Check (∣0,0,1,0⟩).
Lemma test_qubits : ∣0,1⟩ = ∣0⟩ ⊗ ∣1⟩. Proof. reflexivity. Qed.
Notation "'∣' x '⟩'" := (qubit x).
Notation "∣ x , y , .. , z ⟩" := (kron .. (kron ∣x⟩ ∣y⟩) .. ∣z⟩) (at level 0).
Check (∣0,0,1,0⟩).
Lemma test_qubits : ∣0,1⟩ = ∣0⟩ ⊗ ∣1⟩. Proof. reflexivity. Qed.
Certain unitary matrices act on multiple qubits
CNOT: 1000
0100
0001
0010
0100
0001
0010
Definition CNOT : Unitary 4 :=
fun i j ⇒ if ((i =? j) && (i <? 2)) || (i + j =? 5) then 1 else 0.
Lemma CNOT00 : CNOT × ∣0,0⟩ == ∣0,0⟩. Proof. lma. Qed.
Lemma CNOT01 : CNOT × ∣0,1⟩ == ∣0,1⟩. Proof. lma. Qed.
Lemma CNOT10 : CNOT × ∣1,0⟩ == ∣1,1⟩. Proof. lma. Qed.
Lemma CNOT11 : CNOT × ∣1,1⟩ == ∣1,0⟩. Proof. lma. Qed.
Lemma CNOTp1 : CNOT × (∣+⟩ ⊗ ∣0⟩) == /√2 .* ∣0,0⟩ .+ /√2 .* ∣1,1⟩.
Proof. lma. Qed.
fun i j ⇒ if ((i =? j) && (i <? 2)) || (i + j =? 5) then 1 else 0.
Lemma CNOT00 : CNOT × ∣0,0⟩ == ∣0,0⟩. Proof. lma. Qed.
Lemma CNOT01 : CNOT × ∣0,1⟩ == ∣0,1⟩. Proof. lma. Qed.
Lemma CNOT10 : CNOT × ∣1,0⟩ == ∣1,1⟩. Proof. lma. Qed.
Lemma CNOT11 : CNOT × ∣1,1⟩ == ∣1,0⟩. Proof. lma. Qed.
Lemma CNOTp1 : CNOT × (∣+⟩ ⊗ ∣0⟩) == /√2 .* ∣0,0⟩ .+ /√2 .* ∣1,1⟩.
Proof. lma. Qed.
This particular qubit pair has a name: We call it a Bell state.
(Also known as an EPR pair.)
Definition bell : QState 2 := /√2 .* ∣0,0⟩ .+ /√2 .* ∣1,1⟩.
We can also apply single qubit gates to different qubits in a
single system, again by using the Kronecker product:
Lemma XH01 : (X ⊗ H) × ∣0,1⟩ == ∣1⟩⊗∣-⟩.
Proof. lma. Qed.
Lemma HH01 : (H ⊗ H) × ∣0,1⟩ == ∣+⟩⊗∣-⟩.
Proof. lma. Qed.
Proof. lma. Qed.
Lemma HH01 : (H ⊗ H) × ∣0,1⟩ == ∣+⟩⊗∣-⟩.
Proof. lma. Qed.
Let's generate a Bell pair from basis qubits and prove its
correctness
Definition bell' : QState 2 := CNOT × (H ⊗ I 2) × ∣0,0⟩.
Lemma bell_bell' : bell == bell'.
Proof.
(* WORK IN CLASS *) Admitted.
Lemma bell_bell' : bell == bell'.
Proof.
(* WORK IN CLASS *) Admitted.
Total and partial measurement
Inductive measure' : QState 1 → (R * QState 1) → Prop :=
| measure0' : ∀ϕ α β,
ϕ == α .* ∣0⟩ .+ β .* ∣1⟩ →
measure' ϕ (Cnorm2 α, ∣0⟩)
| measure1' : ∀ϕ α β,
ϕ == α .* ∣0⟩ .+ β .* ∣1⟩ →
measure' ϕ (Cnorm2 β, ∣1⟩).
| measure0' : ∀ϕ α β,
ϕ == α .* ∣0⟩ .+ β .* ∣1⟩ →
measure' ϕ (Cnorm2 α, ∣0⟩)
| measure1' : ∀ϕ α β,
ϕ == α .* ∣0⟩ .+ β .* ∣1⟩ →
measure' ϕ (Cnorm2 β, ∣1⟩).
Inductive measure_total : QState 2 → (R * QState 2) → Prop :=
| measure00 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 α, ∣0,0⟩)
| measure01 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 β, ∣0,1⟩)
| measure10 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 γ, ∣1,0⟩)
| measure11 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 δ, ∣1,1⟩).
Lemma measure_plus_minus : measure_total (∣+⟩⊗∣-⟩) ((/4)%R, ∣0,1⟩).
Proof.
(* WORK IN CLASS *) Admitted.
Lemma measure_bell : measure_total bell ((/2)%R, ∣1,1⟩).
Proof.
(* WORK IN CLASS *) Admitted.
| measure00 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 α, ∣0,0⟩)
| measure01 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 β, ∣0,1⟩)
| measure10 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 γ, ∣1,0⟩)
| measure11 : ∀(ϕ : QState 2) (α β γ δ : C),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
measure_total ϕ (Cnorm2 δ, ∣1,1⟩).
Lemma measure_plus_minus : measure_total (∣+⟩⊗∣-⟩) ((/4)%R, ∣0,1⟩).
Proof.
(* WORK IN CLASS *) Admitted.
Lemma measure_bell : measure_total bell ((/2)%R, ∣1,1⟩).
Proof.
(* WORK IN CLASS *) Admitted.
Inductive measure_partial : nat → QState 2 → (R * QState 2) → Prop :=
| measure_p_1_0 : ∀(ϕ ϕ' : QState 2) (α β γ δ : C) (p : R),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
p = (Cnorm2 α + Cnorm2 β)%R →
ϕ' == /√p .* (α .* ∣0,0⟩ .+ β .* ∣0,1⟩) →
measure_partial 1 ϕ (p, ϕ')
| measure_p_1_1 : ∀(ϕ ϕ' : QState 2) (α β γ δ : C) (p : R),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
p = (Cnorm2 γ + Cnorm2 δ)%R →
ϕ' == /√p .* (γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩) →
measure_partial 1 ϕ (p, ϕ')
| measure_p_2_0 : ∀(ϕ ϕ' : QState 2) (α β γ δ : C) (p : R),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
p = (Cnorm2 α + Cnorm2 γ)%R →
ϕ' == /√p .* (α .* ∣0,0⟩ .+ γ .* ∣1,0⟩) →
measure_partial 2 ϕ (p, ϕ')
| measure_p_2_1 : ∀(ϕ ϕ' : QState 2) (α β γ δ : C) (p : R),
ϕ == α .* ∣0,0⟩ .+ β .* ∣0,1⟩ .+ γ .* ∣1,0⟩ .+ δ .* ∣1,1⟩ →
p = (Cnorm2 β + Cnorm2 δ)%R →
ϕ' == /√p .* (β .* ∣0,1⟩ .+ δ .* ∣1,1⟩) →
measure_partial 2 ϕ (p, ϕ').
Lemma partial_measure_plus_minus : measure_partial 1 (∣+⟩⊗∣-⟩) ((/2)%R, ∣0⟩⊗∣-⟩).
Proof.
eapply measure_p_1_0 with (α := /2) (β := -/2) (γ := /2) (δ := -/2).
- unfold Cnorm2, q_plus, q_minus, Mplus, Mscale, kron; simpl.
unfold qubit, qubit0, qubit1; simpl.
by_cell; C_field.
- simpl; R_field.
- unfold Cnorm2, q_plus, q_minus, Mplus, Mscale, kron; simpl.
unfold qubit, qubit0, qubit1; simpl.
by_cell; C_field.
Qed.
Lemma partial_measure_bell : measure_partial 1 bell ((/2)%R, ∣1,1⟩).
Proof.
(* WORK IN CLASS *) Admitted.
(* *)