From 5c375aa95dce3be6a8b7abfa2f175de6c22b0627 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Oct 2021 09:53:49 -0500 Subject: [PATCH] LFSC signature for Booleans (#7443) --- proofs/lfsc/signatures/boolean_programs.plf | 74 +++++++++++++++++++++ proofs/lfsc/signatures/boolean_rules.plf | 52 +++++++++++++++ 2 files changed, 126 insertions(+) create mode 100644 proofs/lfsc/signatures/boolean_programs.plf create mode 100644 proofs/lfsc/signatures/boolean_rules.plf 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)))))) -- 2.30.2