quantum-computing-lean/QuantumComputing/Gates/Basic.lean at main · duckki/quantum-computing-lean · GitHub

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
import QuantumComputing.States

/-!
# Basic Gates

Concrete one- and two-qubit gate matrices and basic controlled-gate
constructors.
-/

namespace QuantumComputing

def X : Square 2 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 1 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 0 then 1
    else 0

def Z : Square 2 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 0 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 1 then -1
    else 0

noncomputable def H : Square 2 :=
  fun i j =>
    if (i : ℕ) = 1 ∧ (j : ℕ) = 1 then -invSqrt2
    else invSqrt2

def CNOT : Square 4 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 0 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 1 then 1
    else if (i : ℕ) = 2 ∧ (j : ℕ) = 3 then 1
    else if (i : ℕ) = 3 ∧ (j : ℕ) = 2 then 1
    else 0

/-- Three-qubit Toffoli gate, flipping the last qubit when the first two are `1`. -/
def TOFFOLI : Square 8 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 0 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 1 then 1
    else if (i : ℕ) = 2 ∧ (j : ℕ) = 2 then 1
    else if (i : ℕ) = 3 ∧ (j : ℕ) = 3 then 1
    else if (i : ℕ) = 4 ∧ (j : ℕ) = 4 then 1
    else if (i : ℕ) = 5 ∧ (j : ℕ) = 5 then 1
    else if (i : ℕ) = 6 ∧ (j : ℕ) = 7 then 1
    else if (i : ℕ) = 7 ∧ (j : ℕ) = 6 then 1
    else 0

def CZ : Square 4 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 0 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 1 then 1
    else if (i : ℕ) = 2 ∧ (j : ℕ) = 2 then 1
    else if (i : ℕ) = 3 ∧ (j : ℕ) = 3 then -1
    else 0

def SWAP : Square 4 :=
  fun i j =>
    if (i : ℕ) = 0 ∧ (j : ℕ) = 0 then 1
    else if (i : ℕ) = 1 ∧ (j : ℕ) = 2 then 1
    else if (i : ℕ) = 2 ∧ (j : ℕ) = 1 then 1
    else if (i : ℕ) = 3 ∧ (j : ℕ) = 3 then 1
    else 0

noncomputable def controlledGate {n : ℕ} (U : Square n) : Square (2 * n) :=
  Matrix.proj ket0 ⊗ (I n) + Matrix.proj ket1 ⊗ U

noncomputable def gateControlled (U : Square 2) : Square 4 :=
  SWAP ⬝ controlledGate U ⬝ SWAP

end QuantumComputing