-
Notifications
You must be signed in to change notification settings - Fork 0
/
qexamples_qutrit.v
110 lines (92 loc) · 3.33 KB
/
qexamples_qutrit.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
From mathcomp Require Import all_ssreflect all_algebra complex ring.
Require Export lens lens_tactics dpower unitary density endo_monoid.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Export GRing.Theory Num.Theory.
Open Scope ring_scope.
Open Scope complex_scope.
Axiom R : rcfType.
Definition C : comRingType := R[i].
Definition Co : lmodType C := C^o.
Definition I : finType := 'I_3.
Definition dI : I := 0.
Notation "¦ x1 , .. , xn ⟩" :=
(dpbasis _ [tuple of x1 :: .. [:: xn] ..]) (at level 0).
Notation focus := (focus dI).
Notation dpmerge_dpbasis := (dpmerge_dpbasis dI).
Notation dpsquare n := (dpmatrix I C n n).
Notation endo n := (mor I C n n).
Notation "T '^^' n" := (dpower I n T).
Definition ω : C := (3.-root (-1))^2.
Definition hadamard_dpmatrix : dpsquare 1 :=
(1 / Num.sqrt 3)%:C *:
(ket_bra ¦0⟩ ¦0⟩ + ket_bra ¦0⟩ ¦1⟩ + ket_bra ¦0⟩ ¦2⟩ +
ket_bra ¦1⟩ ¦0⟩ + ket_bra ¦2⟩ ¦0⟩ +
ω *: (ket_bra ¦1⟩ ¦1⟩ + ket_bra ¦2⟩ ¦2⟩) +
ω^2 *: (ket_bra ¦1⟩ ¦2⟩ + ket_bra ¦2⟩ ¦1⟩)).
Definition hadamard : endo 1 := dpmor hadamard_dpmatrix.
Definition qnot12 : endo 1 :=
dpmor [ffun vi => let i := tnth vi 0 in ¦-i⟩].
Definition cnot : endo 2 :=
dpmor [ffun vi => let i := tnth vi 0 in
let j := tnth vi 1 in
¦i, i + j ⟩].
Definition swap : endo 2 :=
dpmor [ffun vi => let i := tnth vi 0 in
let j := tnth vi 1 in
¦j, i ⟩].
Section enum3.
Definition enum3 : seq I := [:: 0; 1; 2].
Lemma uniq_enum3 : uniq enum3. Proof. by []. Qed.
Lemma mem_enum3 i : i \in enum3.
Proof. by rewrite !inE; case: i => -[|[|[]]]. Qed.
End enum3.
(* Enumeration lemmas *)
Notation enum_indices := (enum_indices enum3).
Definition mem_enum_indices := mem_enum_indices mem_enum3.
Definition eq_from_indicesP := eq_from_indicesP mem_enum3.
Definition uniq_enum_indices := uniq_enum_indices uniq_enum3 mem_enum3.
Definition sum_enum_indices := sum_enum_indices uniq_enum3 mem_enum3.
Lemma cnotE (i j : I) : cnot Co ¦i, j⟩ = ¦i, i + j⟩.
Proof.
by apply/ffunP => vi; rewrite !ffunE !dpmorE /= sum_dpbasisKo !ffunE !(tnth_nth 0).
Qed.
Lemma swapE (i j : I) : swap Co ¦i, j⟩ = ¦j, i⟩.
Proof.
by apply/ffunP => vi; rewrite !ffunE !dpmorE /= sum_dpbasisKo !ffunE !(tnth_nth 0).
Qed.
Lemma qnot12E (i : I) : qnot12 Co ¦i⟩ = ¦-i⟩.
Proof.
by apply/ffunP => vi; rewrite !ffunE !dpmorE /= sum_dpbasisKo !ffunE !(tnth_nth 0).
Qed.
Lemma hadamard2 : hadamard \v hadamard =e qnot12.
Proof.
apply/lift_mor_eq => vi.
rewrite -dpmor_comp.
congr (dpmor _ C^o vi).
apply/eq_from_indicesP => {vi} /=.
do! (apply/andP; split => //); rewrite ffunE; apply/eqP/ffunP=>/=vi; rewrite ffunE.
Admitted.
Lemma swap_def :
cnot \v cnot \v focus [lens 1; 0] cnot \v focus [lens 0] qnot12 \v cnot =e swap.
Proof.
apply/lift_mor_eq => v.
rewrite (decompose_dpower v) !linear_sum.
apply eq_bigr => -[[|i [|j []]] Ht] _ //.
simpl_tuple (Tuple Ht).
rewrite dpmap_scale !linearZ_LR.
congr (_ *: _).
rewrite /= cnotE focus_dpbasis.
simpl_extract.
rewrite qnot12E dpmerge_dpbasis.
simpl_merge.
rewrite focus_dpbasis.
simpl_extract.
rewrite cnotE addrAC subrr add0r dpmerge_dpbasis.
simpl_merge.
rewrite 2!cnotE.
have -> : j + (j + (i + j)) = 3 * j + i by ring.
rewrite (@char_Zp 3) // !linE.
by rewrite swapE.
Qed.