LFSC signature for Booleans (#7443)

2 files changed, 126 insertions, 0 deletions

diff --git a/proofs/lfsc/signatures/boolean_programs.plf b/proofs/lfsc/signatures/boolean_programs.plf
new file mode 100644
index 000000000..9bf87f69f
--- /dev/null
+++ b/proofs/lfsc/signatures/boolean_programs.plf
@@ -0,0 +1,74 @@
+; depends: nary_programs.plf theory_def.plf
+
+; This side condition takes two terms c1 and c2. Via nary_intro,
+; we consider theses terms to be either non-unit clauses if they are
+; or-applications, or otherwise consider them to be unit clauses if they are
+; not. For example, if c1 is (= x y), then (nary_intro f_or c1 false) returns
+;   (or (= x y) false)
+; which we use to compute the concatenation described in following. After
+; converting to n-ary form for both c1 and c2, we then concatenate the result
+; of removing the first occurrence of l from  c1, and the first occurrence of the  negation of l from v2
+; when pol is tt, or vice versa when pol is ff. Since the resolution may result
+; in a singleton list, we run nary_elim as a last step, which ensures that
+; we conclude e.g. L and not (or L false), as done in PfRule::RESOLUTION.
+; This side condition may fail if c1 or c2 does not contain l with the required
+; polarity.
+(program sc_resolution ((c1 term) (c2 term) (pol flag) (l term)) term
+  (nary_elim f_or
+    (nary_concat f_or
+      (nary_rm_first_or_self f_or (nary_intro f_or c1 false) (ifequal pol tt l (apply f_not l)) false) 
+      (nary_rm_first_or_self f_or (nary_intro f_or c2 false) (ifequal pol tt (apply f_not l) l) false)
+    false)
+  false)
+)
+
+; Helper for sc_not_and below, which pushes a not below an application of and.
+; In terms of SMT-LIB, this side condition converts:
+;   (and F1 ... Fn) to (or (not F1) ... (not Fn))
+; This side condition may fail if t is not an and-application in n-ary form.
+(program sc_not_and_rec ((t term)) term
+  (match t
+    ((apply t1 t2)
+      (let t12 (getarg f_and t1)
+        (apply (apply f_or (apply f_not t12)) (sc_not_and_rec t2))))   ; otherwise not in n-ary form
+    (true false))    ; note we must flip true to false
+)
+
+; Pushes a not below an application of and. In terms of SMT-LIB syntax, this
+; side condition converts:
+;   (not (and F1 ... Fn)) to (or (not F1) ... (not Fn))
+(program sc_not_and ((t term)) term
+  (nary_elim f_or (sc_not_and_rec t) false)
+)
+
+; Helper for sc_not_and_rev, which is the inverse of sc_not_and.
+;   (or (not F1) ... (not Fn)) to (and F1 ... Fn)
+; This side condition may fail if t is not an or-application in n-ary form.
+(program sc_not_and_rev_rec ((t term)) term
+  (match t
+    ((apply t1 t2)
+      (let t12 (getarg f_or t1)
+      (let t122 (getarg f_not t12) 
+        (apply (apply f_and t122) (sc_not_and_rev_rec t2)))))   ; otherwise not in n-ary form
+    (false true))    ; note we must flip true to false
+)
+
+; Pulls not from a list of children of an or-application. In terms of SMT-LIB
+; syntax, this side condition converts:
+;   (or (not F1) ... (not Fn)) to (not (and F1 ... Fn))
+(program sc_not_and_rev ((t term)) term
+  (not (nary_elim f_and (sc_not_and_rev_rec t) true))
+)
+
+; Process scope side condition. This side condition is used for constructing the
+; proven formula for the two cases of PfRule::SCOPE. In particular, it takes:
+; - a term t which is expected to be an or-application
+; - a term c which is expected to be a suffix of t.
+; It may conclude an implication, or the negation of t, based on whether c
+; is false, according to the definition of PfRule::SCOPE.
+; This side condition may fail if t and c do not have the above properties.
+(program sc_process_scope ((t term) (c term)) term
+  (let premise (sc_not_and_rev (nary_truncate f_or t c false))
+  (match c
+    (false (not premise))
+    (default (=> premise c)))))
diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf
new file mode 100644
index 000000000..b6df71177
--- /dev/null
+++ b/proofs/lfsc/signatures/boolean_rules.plf
@@ -0,0 +1,52 @@
+; depends: boolean_programs.plf theory_def.plf
+
+(declare resolution (! c1 term (! c2 term (! c term (! p1 (holds c1) (! p2 (holds c2) (! pol flag (! l term (! r (^ (sc_resolution c1 c2 pol l) c) (holds c))))))))))
+(declare reordering (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (nary_is_subset f_or c1 c2) tt) (holds c2))))))
+(declare factoring (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (nary_drop_dups f_or c1 false) c2) (holds c2))))))
+
+(declare split (! f term (holds (or f (or (not f) false)))))
+
+(declare eq_resolve (! f term (! g term (! p1 (holds f) (! p2 (holds (= f g)) (holds g))))))
+
+(declare modus_ponens (! f term (! g term (! p1 (holds f) (! p2 (holds (=> f g)) (holds g))))))
+
+(declare not_not_elim (! f term (! p (holds (not (not f))) (holds f))))
+
+(declare contra (! f term (! p1 (holds f) (! p2 (holds (not f)) (holds false)))))
+
+(declare and_elim (! f1 term (! f2 term (! n mpz (! p (holds f1) (! r (^ (nary_extract f_and f1 n) f2)  (holds f2)))))))
+
+; And introduction. Since PfRule::AND_INTRO is n-ary, we require n applications
+; of the following two rules. The proof (AND_INTRO P1 ... Pn) is translated to
+; the LFSC proof: (and_intro2* _ _ P{n-1} (and_intro1 _ Pn)).
+(declare and_intro1 (! f term (! p (holds f) (holds (and f true)))))
+(declare and_intro2 (! f1 term (! f2 term (! p1 (holds f1) (! p2 (holds f2) (holds (and f1 f2)))))))
+
+(declare not_or_elim (! f1 term (! f2 term (! n mpz (! p (holds (not f1)) (! r (^ (nary_extract f_or f1 n) f2) (holds (not f2))))))))
+
+(declare implies_elim (! f1 term (! f2 term (! p1 (holds (=> f1 f2)) (holds (or (not f1) (or f2 false)))))))
+(declare not_implies_elim1 (! f1 term (! f2 term (! p1 (holds (not (=> f1 f2))) (holds f1)))))
+(declare not_implies_elim2 (! f1 term (! f2 term (! p1 (holds (not (=> f1 f2))) (holds (not f2))))))
+
+(declare equiv_elim1 (! f1 term (! f2 term (! p1 (holds (= f1 f2)) (holds (or (not f1) (or f2 false)))))))
+(declare equiv_elim2 (! f1 term (! f2 term (! p1 (holds (= f1 f2)) (holds (or f1 (or (not f2) false)))))))
+(declare not_equiv_elim1 (! f1 term (! f2 term (! p1 (holds (not (= f1 f2))) (holds (or f1 (or f2 false)))))))
+(declare not_equiv_elim2 (! f1 term (! f2 term (! p1 (holds (not (= f1 f2))) (holds (or (not f1) (or (not f2) false)))))))
+
+(declare xor_elim1 (! f1 term (! f2 term (! p1 (holds (xor f1 f2)) (holds (or f1 (or f2 false)))))))
+(declare xor_elim2 (! f1 term (! f2 term (! p1 (holds (xor f1 f2)) (holds (or (not f1) (or (not f2) false)))))))
+(declare not_xor_elim1 (! f1 term (! f2 term (! p1 (holds (not (xor f1 f2))) (holds (or f1 (or (not f2) false)))))))
+(declare not_xor_elim2 (! f1 term (! f2 term (! p1 (holds (not (xor f1 f2))) (holds (or (not f1) (or f2 false)))))))
+
+(declare ite_elim1 (! c term (! f1 term (! f2 term (! p1 (holds (ite c f1 f2)) (holds (or (not c) (or f1 false))))))))
+(declare ite_elim2 (! c term (! f1 term (! f2 term (! p1 (holds (ite c f1 f2)) (holds (or c (or f2 false))))))))
+(declare not_ite_elim1 (! c term (! f1 term (! f2 term (! p1 (holds (not (ite c f1 f2))) (holds (or (not c) (or (not f1) false))))))))
+(declare not_ite_elim2 (! c term (! f1 term (! f2 term (! p1 (holds (not (ite c f1 f2))) (holds (or c (or (not f2) false))))))))
+
+(declare not_and (! c1 term (! c2 term (! p1 (holds (not c1)) (! r (^ (sc_not_and c1) c2) (holds c2))))))
+
+(declare not_and_rev (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (sc_not_and_rev c1) c2) (holds c2))))))
+
+; Process scope, which is used to translate PfRule::SCOPE. It runs the side
+; condition sc_process_scope on f to generate an equivalent formula g.
+(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g))))))