Extended Resolution Signature (#2788)

* Extended Resolution Signature

While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form

    new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)

This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:

   1. Introducing a **fresh** variable, defined in the form above
   2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
      clauses in the form of two clauses, and a cnf with $$ n $$ clauses
   3. An axiom for unrolling the proof of the cnf into proofs of the
      original clauses.

* Addressing Yoni's comments

1. Added a new (trivial) test
2. Improved a bunch of documentation

* Update proofs/signatures/er.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Removed references to RATs from the signature

There are still a few references in the header comment.

* Aside on continuations

* Scrap the elision annotations

5 files changed, 287 insertions, 45 deletions

diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf
index d52586bc9..b529ff893 100644
--- a/proofs/signatures/drat.plf
+++ b/proofs/signatures/drat.plf
@@ -13,17 +13,6 @@
 ;
 ; This signature checks **Specified DRAT**.
 
-(declare cnf_holds (! c cnf type))
-(declare cnfn_proof (cnf_holds cnfn))
-(declare cnfc_proof
-         (! c clause
-         (! deduped_c clause
-            (! rest cnf
-               (! proof_c (holds c)
-                  (! proof_rest (cnf_holds rest)
-                     (! sc (^ (clause_dedup c) deduped_c)
-                        (cnf_holds (cnfc c rest)))))))))
-
 ; A DRAT proof itself: a list of addition or deletion instructions.
 (declare DRATProof type)
 (declare DRATProofn DRATProof)
diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf
new file mode 100644
index 000000000..8b559671e
--- /dev/null
+++ b/proofs/signatures/er.plf
@@ -0,0 +1,125 @@
+; Depends on sat.plf
+
+; This file exists to support the **definition introduction** (or **extension**)
+; rule in the paper:
+;  "Extended Resolution Simulates DRAT"
+; which can be found at http://www.cs.utexas.edu/~marijn/publications/ijcar18.pdf
+;
+; The core idea of extended resolution is that given **any** formula f
+; involving the variables from some SAT problem, one can introduce the
+; constraint
+;
+;    new <=> f
+;
+; without changing satisfiability, where "new" is a fresh variable.
+;
+; This signature does not provide axioms for facilitating full use of this
+; idea. Instead, this signature facilitates use of one specific kind of
+; extension, that of the form:
+;
+;     new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
+;
+; which translates into the clauses:
+;
+;                      new v l_1 v l_2 v ... v l_n
+;                      new v ~old
+;     for each i <= n: l_i v ~new v old
+;
+; This kind of extension is (a) sufficient to simulate DRAT proofs and (b) easy
+; to convert to clauses, which is why we use it.
+
+; A definition witness value for:
+;              new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
+; It witnesses the fact that new was fresh when it was defined by the above.
+;
+; Thus it witnesses that the above, when added to the formula consisting of the
+; conjunction all the already-proven clauses, produces an equisatisfiable
+; formula.
+(declare definition (! new var (! old lit (! others clause type))))
+
+; Given `old` and `others`, this takes a continuation which expects
+;      1. a fresh variable `new`
+;      2. a definition witness value for:
+;              new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n)
+;
+; Aside:
+;    In programming a **continuation** of some computation is a function that
+;    takes the results of that computation as arguments to produce a final
+;    result.
+;
+;    In proof-construction a **continuation** of some reasoning is a function
+;    that takes the results of that reasoning as arguments to proof a final
+;    result.
+;
+; That definition witness value can be clausified using the rule below.
+;
+; There need to be two different rules because the side-condition for
+; clausification needs access to the new variable, which doesn't exist except
+; inside the continuation, which is out-of-scope for any side-condition
+; associated with this rule.
+(declare decl_definition
+         (! old lit
+            (! others clause ; List of vars
+               (! pf_continuation (! new var (! def (definition new old others)
+                                           (holds cln)))
+                  (holds cln)))))
+
+; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each
+; literal and returns a list of clauses as a `cnf`.
+(program clause_add_suffix_all ((list clause) (suffix clause)) cnf
+         (match list
+                (cln cnfn)
+                ((clc l rest) (cnfc (clc l suffix)
+                                    (clause_add_suffix_all rest suffix)))))
+
+; This translates a definition witness value for the def:
+;
+;    new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
+;
+; into the clauses:
+;
+;                      new v l_1 v l_2 v ... v l_n
+;                      new v ~old
+;     for each i <= n: l_i v ~new v old              (encoded as (cnf_holds ...))
+(declare clausify_definition
+         (! new var
+         (! old lit
+         (! others clause
+         ; Given a definition { new <-> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) }
+         (! def (definition new old others)
+         (! negOld lit
+         (! mkNegOld (^ (lit_flip old) negOld)
+         (! provenCnf cnf
+         (! mkProvenCnf (^ (clause_add_suffix_all
+                             others
+                             (clc (neg new) (clc old cln))) provenCnf)
+         ; If you can prove bottom from its clausal representation
+         (! pf_continuation
+            ; new v l_1 v l_2 v ... v l_n
+            (! pf_c1 (holds (clc (pos new) others))
+               ; new v ~old
+               (! pf_c2 (holds (clc (pos new) (clc negOld cln)))
+                  ; for each i <= n: l_i v ~new v old
+                  (! pf_cs (cnf_holds provenCnf)
+                     (holds cln))))
+         ; Then you've proven bottom
+         (holds cln)))))))))))
+
+; This axiom is useful for converting a proof of some CNF formula (a value of
+; type (cnf_holds ...)) into proofs of the constituent clauses (many values of
+; type (holds ...)).
+; Given
+;    1. a proof of some cnf, first ^ rest, and
+;    2. a proof continuation that
+;       a. takes in proofs of
+;          i. first and
+;          ii. rest and
+;       b. proceeds to prove bottom,
+; proves bottom.
+(declare cnfc_unroll_towards_bottom
+         (! first clause
+            (! rest cnf
+               (! pf (cnf_holds (cnfc first rest))
+                  (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln)))
+                    (holds cln))))))
+
diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf
new file mode 100644
index 000000000..27c61de1f
--- /dev/null
+++ b/proofs/signatures/er_test.plf
@@ -0,0 +1,116 @@
+; Depends on er.plf
+
+; Type for representing success when testing a side-condition
+(declare TestSuccess type)
+
+; Test for clause_add_suffix_all
+(declare test_clause_add_suffix_all
+         (! list clause
+            (! suffix clause
+               (! result cnf
+                  (! (^ (clause_add_suffix_all list suffix) result)
+                     TestSuccess)))))
+
+(check
+  (% a lit
+  (% b lit
+  (% c lit
+     (test_clause_add_suffix_all
+       (clc a (clc b cln))
+       (clc c cln)
+       (cnfc (clc a (clc c cln))
+        (cnfc (clc b (clc c cln))
+        cnfn))
+     )
+  )))
+)
+
+; This is a circuitous proof that uses the definition introduction and
+; unrolling rules
+(check
+  (% v1 var
+  (% v2 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln)))
+    (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln)))
+    (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln)))
+    (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln)))
+       (: (holds cln)
+          (decl_definition
+            (neg v1)
+            (clc (neg v2) cln)
+            (\ v3
+            (\ def3
+              (clausify_definition _ _ _ def3 _ _
+                (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
+                (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
+                (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
+                  (cnfc_unroll_towards_bottom _ _ pf_cnf3
+                    (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
+                    (\ pf_cnfn
+                                                                          ; Clauses
+                  (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1)  (\ pf_c8 ; v2
+                  (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2)  (\ pf_c9 ; v3
+                  (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3)  (\ pf_c10 ; ~v2  ~v1
+                  (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2)  (\ pf_c11 ; ~v1
+                  (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1)  (\ pf_c12 ; ~v2
+                  (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2)  (\ pf_c13 ; empty
+                        pf_c13
+                  ))
+                  ))
+                  ))
+                  ))
+                  ))
+                  ))
+                  )))
+                )))
+              )
+            ))
+          )
+        )
+    ))))
+  ))
+)
+
+; This is a test of ER proof produced by drat2er on Example 1 from:
+; https://www.cs.utexas.edu/~marijn/drat-trim/
+(check
+  (% v1 var
+  (% v2 var
+  (% v3 var
+  (% v4 var
+    (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))
+    (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))))
+    (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))))
+    (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))))
+    (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))))
+    (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))))
+    (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))))
+    (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))))
+       (: (holds cln)
+          (decl_definition
+            (neg v1)
+            cln
+            (\ v5
+            (\ def1
+              (clausify_definition _ _ _ def1 _ _
+                (\ pf_c9 ; type: (holds (clc (pos def1v) cln))
+                (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
+                (\ idc0 ; type: (cnf_holds cnfn)
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
+                  (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16
+                  (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17
+                  (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18
+                    pf_c18
+                  ))))))))))))))))
+                )))
+              )
+            ))
+          )
+       )
+    ))))))))
+  ))))
+)
diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf
index 5224cf3ce..ae6cbd101 100644
--- a/proofs/signatures/lrat.plf
+++ b/proofs/signatures/lrat.plf
@@ -9,12 +9,6 @@
 ;  Some side-conditions make use of a _global assignment_ encoded in
 ;  0 (true) / 1 (false) marks on variables.
 
-; A list of clauses, CNF if interpretted as a formula,
-; but also sometimes just a list
-(declare cnf type)
-(declare cnfn cnf)
-(declare cnfc (! h clause (! t cnf cnf)))
-
 ; Unit (https://en.wikipedia.org/wiki/Unit_type)
 ; For functions that don't return anything
 (declare Unit type) ; The type with only one value (like `void` in C)
@@ -89,12 +83,6 @@
 ; Functional programs for manipulating types ;
 ; ========================================== ;
 
-; Flip the polarity of the literal
-(program lit_flip ((l lit)) lit
-         (match l
-                ((pos v) (neg v))
-                ((neg v) (pos v))))
-
 ; Are two literal equal?
 (program lit_eq ((l1 lit) (l2 lit)) bool
          (match l1
@@ -130,28 +118,6 @@
                                     (ff (clause_contains_lit c' l))))
                 (cln ff)))
 
-; Returns a copy of `c` with any duplicate literals removed.
-; Never fails.
-; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
-; afterwards.
-(program clause_dedup ((c clause)) clause
-         (match c
-                (cln cln)
-                ((clc l rest)
-                 (match l
-                        ((pos v) (ifmarked3
-                                   v
-                                   (clause_dedup rest)
-                                   (do (markvar3 v)
-                                     (let result (clc (pos v) (clause_dedup rest))
-                                       (do (markvar3 v) result)))))
-                        ((neg v) (ifmarked4
-                                   v
-                                   (clause_dedup rest)
-                                   (do (markvar4 v)
-                                     (let result (clc (neg v) (clause_dedup rest))
-                                       (do (markvar4 v) result)))))))))
-
 ; Append two traces
 (program Trace_concat ((t1 Trace) (t2 Trace)) Trace
          (match t1
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf
index 8f40aa8bf..574191493 100644
--- a/proofs/signatures/sat.plf
+++ b/proofs/signatures/sat.plf
@@ -8,10 +8,22 @@
 (declare pos (! x var lit))
 (declare neg (! x var lit))
 
+; Flip the polarity of the literal
+(program lit_flip ((l lit)) lit
+         (match l
+                ((pos v) (neg v))
+                ((neg v) (pos v))))
+
 (declare clause type)
 (declare cln clause)
 (declare clc (! x lit (! c clause clause)))
 
+; A list of clauses, CNF if interpretted as a formula,
+; but also sometimes just a list
+(declare cnf type)
+(declare cnfn cnf)
+(declare cnfc (! h clause (! t cnf cnf)))
+
 ; constructs for general clauses for R, Q, satlem
 
 (declare concat_cl (! c1 clause (! c2 clause clause)))
@@ -107,6 +119,40 @@
   (! u2 (! v (holds c) (holds c2))
     (holds c2))))))
 
+
+; Returns a copy of `c` with any duplicate literals removed.
+; Never fails.
+; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
+; afterwards.
+(program clause_dedup ((c clause)) clause
+         (match c
+                (cln cln)
+                ((clc l rest)
+                 (match l
+                        ((pos v) (ifmarked3
+                                   v
+                                   (clause_dedup rest)
+                                   (do (markvar3 v)
+                                     (let result (clc (pos v) (clause_dedup rest))
+                                       (do (markvar3 v) result)))))
+                        ((neg v) (ifmarked4
+                                   v
+                                   (clause_dedup rest)
+                                   (do (markvar4 v)
+                                     (let result (clc (neg v) (clause_dedup rest))
+                                       (do (markvar4 v) result)))))))))
+
+(declare cnf_holds (! c cnf type))
+(declare cnfn_proof (cnf_holds cnfn))
+(declare cnfc_proof
+         (! c clause
+         (! deduped_c clause
+            (! rest cnf
+               (! proof_c (holds c)
+                  (! proof_rest (cnf_holds rest)
+                     (! sc (^ (clause_dedup c) deduped_c)
+                        (cnf_holds (cnfc c rest)))))))))
+
 ; A little example to demonstrate simplify_clause.
 ; It can handle nested clr's of both polarities,
 ; and correctly cleans up marks when it leaves a