feat: import LeanSAT LRAT

[hargoniX]

This PR imports LeanSAT's LRAT module as step 4/~6 (step 7 could go after I did some refactorings to import this) of the LeanSAT upstreaming. It is the last large component, after this only the LRAT parser and the reflection tactic that hooks everything up to the meta level remains. In particular it is the last component that contains notable proofs, yay!

Again a few remarks:

1. Why is this not in Std? I'm not quite sure whether it should be there. At the current level of code/proof quality we can certainly not import the checker itself into Std but maybe having the data type as well as the trimming algorithm there might be of interested? I'm hoping that as we refactor the checker in the future its quality will be high enough to be also put into Std. At this point we would have a full AIG -> CNF -> LRAT verification pipeline in Std for everyone to use. One additional blocker in this is that we cannot provide the parsers for the format in Std as of today because Parsec is still in Lean so that would also have to change.
2. There do exist two abstraction levels to make sure we can swap out the LRAT implementation at any time:
   • The public interface is just all files in the top level LRAT directory. It basically only contains the LRAT format itself, the checker + soundness proof and the trimming algorithm. As long as we don't need to change their API (which we shouldn't have to I think) we can always swap out the entire Internal directory without breaking anything else in LeanSAT.
   • The Internal module itself contains another layer of abstraction in the form of the Formula class. This allows us to swap out the most complex component in Internal as well, without having to touch any of the infrastructure that is built around it either.
3. I mostly performed stylistic cleanups on the Internal module. In my experience over upgrading to many nightlies during the course of LeanSAT development, I have gotten these proofs cleaned up to the point, where they only break if we change the List or Array proof API significantly. Given that we are currently in the process of stabilizing it I'm hoping that these proofs do not have to be touched anymore unless we do something crazy. All of the custom theory that the LRAT component developed around various basic data types has been upstreamed into Lean over the course of various other PRs.
4. If there are some simple tricks that we can pull off to increase the code / proof quality in Internal and in particular Internal.Formula (this module is not for the light-hearted Lean reviewer) I'm all for it. Otherwise the best course of action to provide LeanSAT to our users soon would probably be to merge it as is and do a cut + rewrite at one of the two interface points described above.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72f2e7aab1e041e361c0be39cc90751f91f8d6f0 --onto 0ecbcfdcc3785c155b8f394c655f48f4f7ed0e65. (2024-08-16 10:31:06)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72f2e7aab1e041e361c0be39cc90751f91f8d6f0 --onto 38288ae07a24f469a85fd10e93cbbb130f0e9f6c. (2024-08-19 07:49:44)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72f2e7aab1e041e361c0be39cc90751f91f8d6f0 --onto b486c6748b153bda628575635baa28aeeb38b8c5. (2024-08-19 10:12:29)

[kim-em]

!bench

[kim-em]

(I'm not going to complain whatever !bench says, just want to know how much extra build time we're in for!)

[leanprover-bot]

Here are the benchmark results for commit 66fa475.
There were significant changes against commit 72f2e7a:

  Benchmark                  Metric                 Change
  ===================================================================
- import Lean                branches                 1.1%   (21.4 σ)
- import Lean                instructions             1.1%   (24.1 σ)
- import Lean                maxrss                   1.5%   (59.4 σ)
- reduceMatch                maxrss                   1.4%  (189.0 σ)
- stdlib                     fix level params         4.4%   (19.8 σ)
- stdlib                     instantiate metavars    47.4%  (101.0 σ)
- stdlib                     instructions             2.7% (4089.0 σ)
- stdlib                     maxrss                   1.5% (1022.2 σ)
- stdlib                     share common exprs       3.8%   (46.1 σ)
- stdlib                     tactic execution        16.2%   (30.2 σ)
- stdlib                     task-clock               2.5%   (15.2 σ)
- stdlib size                bytes .olean             1.8%
- stdlib size                lines                    2.7%
- tests/bench/ interpreted   maxrss                   1.4%  (964.6 σ)
- workspaceSymbols           maxrss                   1.4%  (106.9 σ)

[TwoFX]

Probably makes sense to make one quick pass over the naming; I left some examples. Apart from that I guess there's not much point in spending too much time on the internal stuff as long as the performance of the LRAT.check function is good.