Formalisation of Barrington's Theorem

Stream: CSLib

[Anvit Aggarwal]

Hi everyone,
I'm Anvit, a second-year Computer Science student at IIT Gandhinagar. I have been working on formalising a group-theoretic version of Barrington's theorem in Lean. Below is the repository link:

https://github.com/AnvitAggarwal/barrington-theorem-lean

I’d love to eventually get it merged into CSLib. I’d really appreciate any feedback on aligning it with CSLib and Lean conventions, and on improving the proof itself.

Thanks!

[Chris Henson]

Hi! Could you share what references you've been following? I'd like to think a bit about the definitions you've chosen.

A few pieces of feedback:

• when simp is in the middle of a proof branch, you should use simp only
• in general, you have a lot of simp that can be combined or removed entirely if you make use of simp_all or grind
• some of the arithmetic lemmas can be simplified/removed with grind, omega, etc.
• some of the proofs are a bit long, and I suspect could be split up nicely

[Anvit Aggarwal]

Hi! Thanks for the feedback.

I’ve tried to formalise Theorem 3 from these lecture notes:
https://www.ccs.neu.edu/home/viola/classes/gems-08/lectures/le11.pdf

I also referred to:

• https://www.dainiak.com/teaching/courses/algalg/texts/barrington-huq.pdf
• https://www.math.toronto.edu/swastik/courses/rutgers/topics-S20/lec1.1.pdf (for my definition of formula)

Thanks!

[Thomas Waring]

I think some of your results could be generalised, as well. EG for a different input alphabet (than Bool) and group (than Perm (Fin n)) you would replace g0 and g1 with a map Sym -> G

[Thomas Waring]

This should also fit nicely into the LTS framework: a branching program is (experts please correct me if i’m wrong) a certain kind of labelled transition system

[Chris Henson]

Yeah, the definition of Formula versus branching programs generally is what stood out to me most, but I wasn't 100% what definition would be best.

[Anvit Aggarwal]

Chris Henson said:

Yeah, the definition of Formula versus branching programs generally is what stood out to me most, but I wasn't 100% what definition would be best.

Could you explain what you mean by the 'best definition'? Do you mean that the current definition doesn't highlight the difference between Formula and branching programs sufficiently?

[Chris Henson]

By "best" definition, I mean one that is somewhat general and practical to work with. For example, your Formula has fixed a particular basis. This is not required for the proof, right?

[Anvit Aggarwal]

Ok, got it. Yes, the Formula need not have a fixed basis. The idea was that every Formula can be represented using just AND and NOT gates.

[Chris Henson]

The other definition that could use some refinement is branching programs. You do not define these yet, only "group programs"? I understand you were just starting with theorem 3 from the first reference, but since it is to be used within Barrington’s Theorem, I think it is important to think about how those definitions will fit together.

[Chris Henson]

(to be clear I am not meaning to discourage you, I think this could be a good first contribution if we nail down the definitions!)

[Anvit Aggarwal]

Sure. Thanks for your feedback. I'll work on the definitions, fix the usage of simp, and split the longer proofs.

[Anvit Aggarwal]

Thanks for your suggestions, Thomas! I'll try to replace Bool and Perm (Fin n) with Sym -> G. I am not familiar with LTS, but will read up on it to see how I could incorporate it.

[Thomas Waring]

no problem! looking closer you will need Perm (Fin n) once you integrate with branching programs, but the lemmas could be proven for any G

[Chris Henson]

I didn't go through the whole repo, but here is a fork where I started just a little bit of cleaning up proofs: https://github.com/chenson2018/barrington-theorem-lean

We can always do more during the review process, but I just wanted to give you a few concrete examples of my above feedback to help you get started.

[Thomas Waring]

Im also more than happy to help straighten out those generalisations! i’m away for my computer for the next week about after that feel free to reach out :))