-
Notifications
You must be signed in to change notification settings - Fork 2
/
QFT.idr
67 lines (45 loc) · 1.2 KB
/
QFT.idr
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
module QFT
import Data.Nat
import Data.Vect
import Decidable.Equality
import Unitary
import Injection
import Lemmas
%default total
|||Quantum circuit for the Quantum Fourier Transform
--CONTROLLED PHASE GATES FOR THE QFT
||| Phase gate with phase 2 pi / (2^m)
Rm : Nat -> Unitary 1
Rm m = PGate (2 * pi / (pow 2 (cast m)))
||| Controlled phase gate with phase 2 pi / (2^m)
cRm : Nat -> Unitary 2
cRm m = controlled (Rm m)
--A FEW LEMMAS FOR THE QFT
kLTSucc1 : (k : Nat) -> k < (k + 1) = True
kLTSucc1 0 = Refl
kLTSucc1 (S k) = kLTSucc1 k
lemmaInj1 : (k : Nat) -> isInjective (S (k + 1)) [S k, 0] = True
lemmaInj1 k =
let p1 = kLTSucc1 k
in lemmaAnd (lemmaAnd p1 Refl) Refl
--QFT
||| Auxiliary function for QFT : builds the recursive pattern
|||
||| n -- number of qubits
export
qftRec : (n : Nat) -> Unitary n
qftRec 0 = IdGate
qftRec 1 = HGate
qftRec (S (S k)) =
let t1 = (qftRec (S k)) # IdGate
in rewrite sym $ lemmaplusOneRight k in apply (cRm (S (S k))) t1 [S k, 0] {prf = lemmaInj1 k}
||| QFT unitary circuit for n qubits
|||
||| n -- number of qubits
export
qft : (n : Nat) -> Unitary n
qft 0 = IdGate
qft (S k) =
let g = qftRec (S k)
h = (IdGate {n = 1}) # (qft k)
in h . g