feat(Circuit): prove Shannon lower bound - #891
Conversation
|
|
||
| variable {n g s : ℕ} | ||
|
|
||
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ |
There was a problem hiding this comment.
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ | |
| /-- Boolean functions on `n` inputs computable with at most `s` De Morgan gates. -/ |
There was a problem hiding this comment.
Applied the suggested docstring.
| variable {n g s : ℕ} | ||
|
|
||
| /-- Boolean functions computable with at most `s` De Morgan gates. -/ | ||
| noncomputable def computableFunctions (n s : ℕ) : Finset (BooleanFunction n) := by |
There was a problem hiding this comment.
Would it be difficult to give an explicit definition (instead of using a tactic)?
I mean mem_computableFunctions gives a good definition so it's not too bad, but still a bit weird.
There was a problem hiding this comment.
Replaced both tactic blocks with direct Finset.univ.filter definitions using open scoped Classical in.
| classical | ||
| simp [computableFunctions] | ||
|
|
||
| private noncomputable def irredundantFunctions (n g : ℕ) : Finset (BooleanFunction n) := by |
There was a problem hiding this comment.
Can you give some intuition for this definition?
There was a problem hiding this comment.
Added a docstring explaining that the gates compute pairwise distinct functions, giving g! distinct relabelings for the counting bound.
| classical | ||
| simp [irredundantFunctions] | ||
|
|
||
| private instance opFintype : Fintype Op where |
There was a problem hiding this comment.
Maybe move to definition of Op, could be useful in general
There was a problem hiding this comment.
Moved the Fintype Op instance next to Op in Boolean/Basic.lean and made it public.
| intro gate | ||
| simp [Wire.Renaming.ofPermutation, Function.comp_def] | ||
|
|
||
| private noncomputable def representative (f : ↥(irredundantFunctions n g)) : |
There was a problem hiding this comment.
Is it possible to do this without the ↥?
There was a problem hiding this comment.
Removed the explicit ↥ here and in the related declarations; Lean infers the coercion.
| nlinarith | ||
|
|
||
| private theorem eventually_inputs_le_budget : | ||
| ∀ᶠ n : ℕ in atTop, n + 1 ≤ 2 ^ n / n := by |
There was a problem hiding this comment.
∀ᶠ n : ℕ in atTop, n ≤ 2 ^ n / n could also be a generic theorem
There was a problem hiding this comment.
Extracted public Nat.eventually_add_one_le_pow_div into Foundations/Data/Nat/Asymptotics.lean, retaining the stronger n + 1 bound and generalizing to natural bases greater than one.
Add semantic normalization and counting to prove the worst-case 2^n/n lower bound for De Morgan circuits.
2badbfa to
85805b8
Compare
| deriving DecidableEq | ||
|
|
||
| instance Op.instFintype : Fintype Op where | ||
| elems := {.const false, .const true, .not, .and, .or} | ||
| complete := by intro op; cases op <;> simp |
There was a problem hiding this comment.
We can save the instance by deriving also Fintype and proving that the cardinality is 5
| deriving DecidableEq | |
| instance Op.instFintype : Fintype Op where | |
| elems := {.const false, .const true, .not, .and, .or} | |
| complete := by intro op; cases op <;> simp | |
| deriving DecidableEq, Fintype | |
| @[simp] theorem Op.card : Fintype.card Op = 5 := rfl |
This needs the imports above swapped as well, and changing the proof in Cslib/Computability/Circuit/Boolean/Counting.lean:84 to just simp
There was a problem hiding this comment.
Fantastic! Thank you.
3 participants
Add semantic normalization and counting to prove the worst-case 2^n/n lower bound for De Morgan circuits.
Assisted by Codex, adapted from https://github.com/samuelSchlesinger/algebraic-circuits.