MultiplicativeDegree.lean

1 import CircuitObstructions.Degree
2 import CircuitObstructions.CutComparison
3 
4 /-!
5 # Degree growth with sharing
6 
7 The invariant covers products of arbitrary lists of register coordinates.
8 Boolean idempotence removes repeated occurrences of an updated target before
9 expansion. One Toffoli can therefore add at most one to the degree budget,
10 independently of fan-out, workspace, and output feedback.
11 -/
12 namespace CircuitObstructions
13 
14 def withoutWire {W : Type} [DecidableEq W] (l : List W) (t : W) : List W :=
15   l.filter (fun i => decide (i ≠ t))
16 
17 theorem withoutWire_length_le {W : Type} [DecidableEq W] (l : List W) (t : W) :
18     (withoutWire l t).length ≤ l.length := by
19   exact List.length_filter_le _ _
20 
21 theorem withoutWire_length_lt {W : Type} [DecidableEq W]
22     (l : List W) (t : W) (ht : t ∈ l) :
23     (withoutWire l t).length + 1 ≤ l.length := by
24   induction l with
25   | nil => simp at ht
26   | cons i is ih =>
27       by_cases hit : i = t
28       · subst i
29         simpa [withoutWire] using Nat.add_le_add_right (withoutWire_length_le is t) 1
30       · have htail : t ∈ is := by simpa [hit, Ne.symm hit] using ht
31         simpa [withoutWire, hit] using Nat.add_le_add_right (ih htail) 1
32 
33 theorem bprod_write {W : Type} [DecidableEq W]
34     (l : List W) (s : State W) (t : W) (b : Bool) :
35     bprod l (write s t b) =
36       ((if t ∈ l then b else true) && bprod (withoutWire l t) s) := by
37   induction l with
38   | nil => simp [bprod, withoutWire]
39   | cons i is ih =>
40       by_cases hit : i = t
41       · subst i
42         by_cases hm : t ∈ is <;>
43           simp [bprod, withoutWire, write, ih, hm]
44       · by_cases hm : t ∈ is <;>
45           simp [bprod, withoutWire, write, ih, hit, Ne.symm hit, hm,
46                 Bool.and_left_comm]
47 
48 theorem bprod_write_absent {W : Type} [DecidableEq W]
49     (l : List W) (s : State W) (t : W) (b : Bool) (ht : t ∉ l) :
50     bprod l (write s t b) = bprod l s := by
51   induction l with
52   | nil => rfl
53   | cons i is ih =>
54       have hi : i ≠ t := by intro h; subst i; exact ht (by simp)
55       have his : t ∉ is := by intro h; exact ht (by simp [h])
56       simp only [bprod_cons, write_other s t i b hi, ih his]
57 
58 def WorkspaceDegree {n : Nat} {W : Type}
59     (s : (Fin n → Bool) → State W) (t : Nat) : Prop :=
60   ∀ l : List W, DegreeLE (t + l.length) (fun x => bprod l (s x))
61 
62 theorem workspaceDegree_initial {n : Nat} {W : Type}
63     (s : (Fin n → Bool) → State W)
64     (h : ∀ i, DegreeLE 1 (fun x => s x i)) : WorkspaceDegree s 0 := by
65   intro l
66   simpa using DegreeLE.product l s h
67 
68 def toggleProduct {n : Nat} {W : Type} [DecidableEq W]
69     (s : (Fin n → Bool) → State W) (t : W) (controls : List W) :
70     (Fin n → Bool) → State W :=
71   fun x => write (s x) t (Bool.xor (s x t) (bprod controls (s x)))
72 
73 theorem workspaceDegree_toggle {n : Nat} {W : Type} [DecidableEq W]
74     (s : (Fin n → Bool) → State W) (t : W) (controls : List W)
75     (k : Nat) (h : WorkspaceDegree s k) :
76     WorkspaceDegree (toggleProduct s t controls) (k + (controls.length - 1)) := by
77   intro l
78   by_cases ht : t ∈ l
79   · let rest := withoutWire l t
80     have hlen : rest.length + 1 ≤ l.length := withoutWire_length_lt l t ht
81     have hfirst := h (t :: rest)
82     have hsecond := h (controls ++ rest)
83     have hb1 : k + (t :: rest).length ≤ k + (controls.length - 1) + l.length := by
84       simp only [List.length_cons]; omega
85     have hb2 : k + (controls ++ rest).length ≤ k + (controls.length - 1) + l.length := by
86       simp only [List.length_append]; omega
87     have hb := DegreeLE.add (hfirst.mono hb1) (hsecond.mono hb2)
88     have heq : (fun x => bprod l (toggleProduct s t controls x)) =
89         (fun x => Bool.xor (bprod (t :: rest) (s x))
90           (bprod (controls ++ rest) (s x))) := by
91       funext x
92       simp only [toggleProduct, bprod_write, ite_eq_left ht, xor_and_right,
93                  bprod_cons, bprod_append]
94       rfl
95     rw [heq]
96     exact hb
97   · have heq : (fun x => bprod l (toggleProduct s t controls x)) =
98         (fun x => bprod l (s x)) := by
99       funext x
100       exact bprod_write_absent l (s x) t _ ht
101     rw [heq]
102     exact (h l).mono (by omega)
103 
104 theorem workspaceDegree_gate {n : Nat} {W : Type} [DecidableEq W]
105     (s : (Fin n → Bool) → State W) (g : Gate W) (k : Nat)
106     (h : WorkspaceDegree s k) :
107     WorkspaceDegree (fun x => g.eval (s x)) (k + g.toffoliCost) := by
108   cases g with
109   | not t =>
110       have hh := workspaceDegree_toggle s t [] k h
111       change WorkspaceDegree (fun x => write (s x) t
112         (Bool.xor (s x t) (bprod [] (s x)))) (k + ([].length - 1)) at hh
113       simpa only [Gate.eval, Gate.toffoliCost, bprod_nil, List.length_nil,
114         Nat.zero_sub, Nat.add_zero, not_as_xor_one] using hh
115   | cnot c t hct =>
116       have hh := workspaceDegree_toggle s t [c] k h
117       change WorkspaceDegree (fun x => write (s x) t
118         (Bool.xor (s x t) (bprod [c] (s x)))) (k + ([c].length - 1)) at hh
119       simpa only [Gate.eval, Gate.toffoliCost, bprod_cons, bprod_nil,
120         Bool.and_true, List.length_cons, List.length_nil, Nat.add_zero, Nat.add_sub_cancel] using hh
121   | toffoli a b t hab hat hbt =>
122       have hh := workspaceDegree_toggle s t [a,b] k h
123       change WorkspaceDegree (fun x => write (s x) t
124         (Bool.xor (s x t) (bprod [a,b] (s x)))) (k + ([a,b].length - 1)) at hh
125       simpa only [Gate.eval, Gate.toffoliCost, bprod_cons, bprod_nil,
126         Bool.and_true, List.length_cons, List.length_nil] using hh
127 
128 theorem workspaceDegree_run {n : Nat} {W : Type} [DecidableEq W]
129     (c : Circuit W) (s : (Fin n → Bool) → State W) (k : Nat)
130     (h : WorkspaceDegree s k) :
131     WorkspaceDegree (fun x => run c (s x)) (k + toffoliCount c) := by
132   induction c generalizing s k with
133   | nil => simpa [toffoliCount] using h
134   | cons g gs ih =>
135       have hg := workspaceDegree_gate s g k h
136       have hh := ih (fun x => g.eval (s x)) (k + g.toffoliCost) hg
137       simpa [toffoliCount, Nat.add_assoc] using hh
138 
139 theorem run_coordinate_degree {n : Nat} {W : Type} [DecidableEq W]
140     (c : Circuit W) (s : (Fin n → Bool) → State W)
141     (hs : ∀ i, DegreeLE 1 (fun x => s x i)) (i : W) :
142     DegreeLE (toffoliCount c + 1) (fun x => run c (s x) i) := by
143   have h := workspaceDegree_run c s 0 (workspaceDegree_initial s hs) [i]
144   simpa [bprod] using h
145 
146 theorem canonical_boundary_degree (n a : Nat) (b : Bool) (i : CanonicalWire n a) :
147     DegreeLE 1 (fun x => (canonicalBoundary n a).encode x b i) := by
148   cases i with
149   | inl j => exact DegreeLE.variable j
150   | inr j =>
151       cases j with
152       | inl j => exact DegreeLE.constant n 1 false
153       | inr j => exact DegreeLE.constant n 1 b
154 
155 theorem canonical_run_coordinate_degree (n a : Nat) (c : Circuit (CanonicalWire n a))
156     (b : Bool) (i : CanonicalWire n a) :
157     DegreeLE (toffoliCount c + 1)
158       (fun x => run c ((canonicalBoundary n a).encode x b) i) := by
159   exact run_coordinate_degree c _ (canonical_boundary_degree n a b) i
160 
161 theorem canonical_cut_packet_degree (n a : Nat)
162     (p q : Circuit (CanonicalWire n a)) (i : CanonicalWire n a) :
163     DegreeLE (max (toffoliCount p) (toffoliCount q) + 1)
164       (fun x => packet (canonicalBoundary n a) p q x i) := by
165   have h := (canonical_run_coordinate_degree n a p false i).xor
166     (canonical_run_coordinate_degree n a q.reverse false i)
167   have hm : max (toffoliCount p + 1) (toffoliCount q + 1) =
168       max (toffoliCount p) (toffoliCount q) + 1 := by omega
169   simpa only [toffoliCount_reverse, hm, packet] using h
170 
171 end CircuitObstructions

Back to source controls