Merge pull request #8 from bernborgess/Documentation

Create Documentation main pages

book.toml

@@ -7,6 +7,9 @@ title = "Cutting Planes with Lean 4"
 
 [output.html]
 git-repository-url = "https://github.com/bernborgess/lean-cutting-planes"
+mathjax-support = true
 
 [output.html.playground.boring-prefixes]
 lean = "# "
+
+# mdbook serve -p 8000 -n 127.0.0.1

docs/SUMMARY.md

@@ -4,3 +4,5 @@
 [Cutting Planes with Lean 4](title_page.md)
 
 - [Introduction](./introduction.md)
+- [Pseudo Boolean Rules](./pseudo_boolean_rules.md)
+- [Worked Example](./worked_example.md)

docs/introduction.md

@@ -4,4 +4,20 @@ Introduction
 Cutting Planes and Lean 4
 -----------------------------
 
-*Cutting Planes* is a formal logic. 
+*Cutting Planes* is a formal logic used in the context of discrete combinatorial problems, that can be applied in _Software testing_, _Formal verification_ and _Proof logging_.
+
+Our proofs will consist of _Pseudo-Boolean Constraints_, that are 0-1 integer linear inequalities of the form:
+\\[ \sum_i{a_i l_i} \ge A \\]
+Where we have:
+- constant \\( A \in \mathbb{Z} \\)
+- coefficients \\( a_i \in \mathbb{Z} \\)
+- literals \\( l_i: x_i\ \text{or}\ \overline{x_i}\ (\text{where } x_i + \overline{x_i} = 1) \\)
+- variables \\( x_i \\) take values \\( 0 = false \\) or \\( 1 = true \\)
+
+Without loss of generality, we will use the [normalized form](Bar95), with all \\( a_i, A\\) non-negative.
+
+In this regard, _Pseudo-Boolean Reasoning_ works on two axioms and four rules, each of which are formally verified in this project using _Lean 4_
+
+Lean 4 is a theorem prover and programming language developed by Leonardo de Moura. In the last years it became proeminent in the mathematics community, after [The Xena Project](https://www.ma.imperial.ac.uk/~buzzard/xena/) of Imperial College London formalized Peter Scholze's proof in the area of condensed mathematics in 2021. In 2023 Terence Tao used Lean to formalize a proof of the _Polynomial Freiman-Ruzsa (PFR) conjecture_, published in the same year.
+
+Armed with a Lean 4 proof of the reasoning rules, complex proofs that involve these steps can be guaranteed to be correct.

docs/pseudo_boolean_rules.md

@@ -0,0 +1,49 @@
+Pseudo Boolean Rules
+============
+
+Input Axioms
+-----------------------------
+
+As a starting point for the pseudo boolean reasoning we will get constraints from the user, which are subject to a normalization process
+
+Literal Axioms
+-----------------------------
+
+For any literal \\( l_i\\) we can create a constraint:
+\\[ \frac{}
+    {l_i \ge 0}
+\\]
+
+Addition Rule
+-----------------------------
+Two constraints can be added together, adding the coefficients and the constants. Another behaviour is that \\(x_i\\) and \\(\overline{x_i}\\) that may appear together cancel each other:
+\\[ \frac
+    {{\sum_i{a_i l_i} \ge A}\qquad {\sum_i{b_i l_i} \ge B}}
+    {\sum_i{(a_i + b_i) l_i} \ge (A+B)}
+\\]
+
+Multiplication Rule
+-----------------------------
+A constraint can be multiplied by any \\( c \in \mathbb{N}^{+} \\):
+\\[ \frac
+    {\sum_i{a_i l_i} \ge A}
+    {\sum_i{c a_i l_i} \ge c A}
+\\]
+
+Division Rule
+-----------------------------
+A constraint can be divided by any \\( c \in \mathbb{N}^{+} \\), and the the ceiling of this division in applied:
+\\[ \frac
+    {\sum_i{a_i l_i} \ge A}
+    {\sum_i{ \lceil \frac{a_i}{c} \rceil l_i} \ge \lceil \frac{A}{c} \rceil}
+\\]
+
+Saturation Rule
+-----------------------------
+A constraint can be replace its coefficients by the minimum between them and the constant:
+\\[ \frac
+    {\sum_i{a_i l_i} \ge A}
+    {\sum_i{ \min(a_i,A)\cdot l_i} \ge A}
+\\]
+
+All these rules can be seen in practice in the Worked Example

docs/title_page.md

@@ -2,4 +2,6 @@
 
 *by Bernardo Borges*
 
-This book is the official documentation for the usage of the [lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) library. It is currently a work in progress, with the goal to provide full expressivity in Lean 4 for the cutting planes formal logic.
+This book is the official documentation for the usage of the [lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) library. It is currently a work in progress, with the goal to provide full expressivity in Lean 4 for the cutting planes formal logic.
+
+Future work in this project will aim to verify unsat demonstrations that were produced by solvers suchs as [RoundingSat](https://gitlab.com/MIAOresearch/software/roundingsat) and check that their reasoning was correct.

docs/worked_example.md

@@ -0,0 +1,97 @@
+Worked Example
+============
+
+Input
+-----------------------------
+
+For this example, in constraints over variables \\(w,x,y,z\\) we will have three input axioms:
+
+1. \\( w + 2x + y \ge 2 \\)
+1. \\( w + 2x + 4y + 2z \ge 5 \\)
+1. \\( \overline{z} \ge 0 \\)
+
+```lean
+example (xs : Fin 4 → Fin 2)
+  (c1 : PBIneq ![(1,0),(2,0),(1,0),(0,0)] xs 2)
+  (c2 : PBIneq ![(1,0),(2,0),(4,0),(2,0)] xs 5)
+  (c3 : PBIneq ![(0,0),(0,0),(0,0),(0,1)] xs 0)
+```
+
+Goal 
+-----------------------------
+The objective of this example is to prove:
+\\[ w + 2x + 2y \ge 3 \\]
+
+```lean
+  : PBIneq ![(1,0),(2,0),(2,0),(0,0)] xs 3 := by
+```
+
+Execution
+-----------------------------
+We start by using muliplication of the first constraint by 2:
+\\[ \frac
+    {w + 2x + y \ge 2}
+    {2w + 4x + 2y \ge 4}
+    (\text{Multiply by 2})
+\\]
+```lean
+  let t1 : PBIneq ![(2,0),(4,0),(2,0),(0,0)] xs 4  := by apply Multiplication c1 2
+```
+
+Now we add this result to constraint 2:
+\\[ \frac
+    {{2w + 4x + 2y \ge 4}\qquad {w + 2x + 4y + 2z \ge 5}}
+    {3w + 6x + 6y + 2z \ge 9}
+    (\text{Add})
+\\]
+```lean
+  let t2 : PBIneq ![(3,0),(6,0),(6,0),(2,0)] xs 9  := by apply Addition t1 c2
+```
+At this point we want to remove the variable \\(z\\), as it does not appear in our goal. Then we will introduce a \\(\overline{z} \ge 0\\) by the literal axiom and then multiply it by 2:
+\\[ \frac
+    {\overline{z} \ge 0}
+    {2\overline{z} \ge 0}
+    (\text{Multiply by 2})
+\\]
+```lean
+  let t3 : PBIneq ![(0,0),(0,0),(0,0),(0,2)] xs 0  := by apply Multiplication c3 2
+```
+Performing addition will cancel out the \\(z\\) variable:
+\\[ \frac
+    {{3w + 6x + 6y + 2z \ge 9}\qquad {2\overline{z} \ge 0}}
+    {3w + 6x + 6y \ge 7}
+    (\text{Add})
+\\]
+```lean
+  let t4 : PBIneq ![(3,0),(6,0),(6,0),(0,0)] xs 7  := by apply Addition t2 t3
+```
+And lastly a division by 3 is performed to arrive at the goal:
+\\[ \frac
+    {3w + 6x + 6y \ge 7}
+    {w + 2x + 2y \ge 3}
+    (\text{Divide by 3})
+\\]
+```lean
+  exact Division t4 3
+  done
+```
+
+Summarizing, this is the full proof:
+
+![toy_example](./assets/toy_example.png)
+
+```lean
+example
+  (xs : Fin 4 → Fin 2)
+  (c1 : PBIneq ![(1,0),(2,0),(1,0),(0,0)] xs 2)
+  (c2 : PBIneq ![(1,0),(2,0),(4,0),(2,0)] xs 5)
+  (c3 : PBIneq ![(0,0),(0,0),(0,0),(0,1)] xs 0)
+  : PBIneq ![(1,0),(2,0),(2,0),(0,0)] xs 3
+  := by
+  let t1 : PBIneq ![(2,0),(4,0),(2,0),(0,0)] xs 4  := by apply Multiplication c1 2
+  let t2 : PBIneq ![(3,0),(6,0),(6,0),(2,0)] xs 9  := by apply Addition t1 c2
+  let t3 : PBIneq ![(0,0),(0,0),(0,0),(0,2)] xs 0  := by apply Multiplication c3 2
+  let t4 : PBIneq ![(3,0),(6,0),(6,0),(0,0)] xs 7  := by apply Addition t2 t3
+  exact Division t4 3
+  done
+```