Gates.lean

1 import Std
2 
3 /-!
4 # Legal classical NOT/CNOT/Toffoli circuits
5 
6 Only classical Boolean gates are represented. Constructor proofs enforce distinct
7 control and target wires. A circuit may target or control any wire at any step.
8 No intermediate workspace-cleanness or output-passivity restriction is imposed.
9 -/
10 namespace CircuitObstructions
11 
12 abbrev State (W : Type) := W → Bool
13 
14 def write {W : Type} [DecidableEq W] (s : State W) (t : W) (b : Bool) : State W :=
15   fun i => if i = t then b else s i
16 
17 @[simp] theorem write_same {W : Type} [DecidableEq W] (s : State W) (t : W) (b : Bool) :
18     write s t b t = b := by simp [write]
19 
20 @[simp] theorem write_other {W : Type} [DecidableEq W] (s : State W) (t i : W)
21     (b : Bool) (h : i ≠ t) : write s t b i = s i := by simp [write, h]
22 
23 @[simp] theorem xor_cancel_right (a b : Bool) : Bool.xor (Bool.xor a b) b = a := by
24   cases a <;> cases b <;> rfl
25 
26 @[simp] theorem xor_cancel_left (a b : Bool) : Bool.xor a (Bool.xor a b) = b := by
27   cases a <;> cases b <;> rfl
28 
29 theorem xor_commute (a b : Bool) : Bool.xor a b = Bool.xor b a := by
30   cases a <;> cases b <;> rfl
31 
32 theorem xor_true_iff_ne (a b : Bool) : Bool.xor a b = true ↔ a ≠ b := by
33   cases a <;> cases b <;> decide
34 
35 inductive Gate (W : Type) where
36   | not (target : W)
37   | cnot (control target : W) (distinct : control ≠ target)
38   | toffoli (control₁ control₂ target : W)
39       (controls_distinct : control₁ ≠ control₂)
40       (first_distinct : control₁ ≠ target)
41       (second_distinct : control₂ ≠ target)
42 
43 def Gate.eval {W : Type} [DecidableEq W] : Gate W → State W → State W
44   | .not t, s => write s t (!s t)
45   | .cnot c t _, s => write s t (Bool.xor (s t) (s c))
46   | .toffoli a b t _ _ _, s => write s t (Bool.xor (s t) (s a && s b))
47 
48 theorem Gate.eval_involutive {W : Type} [DecidableEq W] (g : Gate W) (s : State W) :
49     g.eval (g.eval s) = s := by
50   cases g with
51   | not t =>
52       funext i
53       by_cases h : i = t
54       · subst i; simp [Gate.eval]
55       · simp [Gate.eval, write, h]
56   | cnot c t hct =>
57       funext i
58       by_cases h : i = t
59       · subst i; simp [Gate.eval, hct]
60       · simp [Gate.eval, write, h]
61   | toffoli a b t hab hat hbt =>
62       funext i
63       by_cases h : i = t
64       · subst i; simp [Gate.eval, hat, hbt]
65       · simp [Gate.eval, write, h]
66 
67 theorem Gate.eval_injective {W : Type} [DecidableEq W] (g : Gate W)
68     {s t : State W} (h : g.eval s = g.eval t) : s = t := by
69   have hh := congrArg g.eval h
70   simpa only [g.eval_involutive] using hh
71 
72 abbrev Circuit (W : Type) := List (Gate W)
73 
74 def run {W : Type} [DecidableEq W] : Circuit W → State W → State W
75   | [], s => s
76   | g :: gs, s => run gs (g.eval s)
77 
78 @[simp] theorem run_nil {W : Type} [DecidableEq W] (s : State W) :
79     run ([] : Circuit W) s = s := rfl
80 
81 @[simp] theorem run_cons {W : Type} [DecidableEq W] (g : Gate W) (gs : Circuit W)
82     (s : State W) : run (g :: gs) s = run gs (g.eval s) := rfl
83 
84 theorem run_append {W : Type} [DecidableEq W] (p q : Circuit W) (s : State W) :
85     run (p ++ q) s = run q (run p s) := by
86   induction p generalizing s with
87   | nil => rfl
88   | cons g gs ih => exact ih (g.eval s)
89 
90 @[simp] theorem run_reverse_run {W : Type} [DecidableEq W]
91     (c : Circuit W) (s : State W) : run c.reverse (run c s) = s := by
92   induction c generalizing s with
93   | nil => rfl
94   | cons g gs ih =>
95       simp only [List.reverse_cons, run_append, run_cons, run_nil]
96       rw [ih, Gate.eval_involutive]
97 
98 @[simp] theorem run_run_reverse {W : Type} [DecidableEq W]
99     (c : Circuit W) (s : State W) : run c (run c.reverse s) = s := by
100   simpa only [List.reverse_reverse] using run_reverse_run c.reverse s
101 
102 theorem run_injective {W : Type} [DecidableEq W] (c : Circuit W)
103     {s t : State W} (h : run c s = run c t) : s = t := by
104   have hh := congrArg (run c.reverse) h
105   simpa only [run_reverse_run] using hh
106 
107 def Gate.toffoliCost {W : Type} : Gate W → Nat
108   | .toffoli _ _ _ _ _ _ => 1
109   | _ => 0
110 
111 def toffoliCount {W : Type} (c : Circuit W) : Nat :=
112   (c.map Gate.toffoliCost).sum
113 
114 theorem toffoliCount_append {W : Type} (p q : Circuit W) :
115     toffoliCount (p ++ q) = toffoliCount p + toffoliCount q := by
116   simp [toffoliCount]
117 
118 theorem toffoliCount_reverse {W : Type} (c : Circuit W) :
119     toffoliCount c.reverse = toffoliCount c := by
120   simp [toffoliCount, List.map_reverse]
121 
122 end CircuitObstructions

Back to source controls