Add LFSC signature for quantifiers (#7540)

Also includes a fix for the Boolean signature. After the strings PR and this one, the initial LFSC signature is complete.

diff --git a/proofs/lfsc/signatures/boolean_programs.plf b/proofs/lfsc/signatures/boolean_programs.plf
index 9bf87f69f6d5715dd7774045e0a84150b15aa954..eecc71a98f949ddc28f906696a44aaefaf71efac 100644 (file)
--- a/proofs/lfsc/signatures/boolean_programs.plf
+++ b/proofs/lfsc/signatures/boolean_programs.plf
@@ -55,9 +55,9 @@
 
 ; 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))
+;   (or (not F1) ... (not Fn)) to (and F1 ... Fn)
 (program sc_not_and_rev ((t term)) term
-  (not (nary_elim f_and (sc_not_and_rev_rec t) true))
+  (nary_elim f_and (sc_not_and_rev_rec t) true)
 )
 
 ; Process scope side condition. This side condition is used for constructing the

diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf
index b6df71177d0fdf4b25d7100d68af0da30d58aae4..af16af1f9e431a5a477bfc4ef5313d8d1b3cb5cb 100644 (file)
--- a/proofs/lfsc/signatures/boolean_rules.plf
+++ b/proofs/lfsc/signatures/boolean_rules.plf
@@ -45,7 +45,7 @@
 
 (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))))))
+(declare not_and_rev (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (sc_not_and_rev c1) c2) (holds (not 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.

diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf
new file mode 100644 (file)
index 0000000..7bdd653
--- /dev/null
+++ b/proofs/lfsc/signatures/quantifiers_rules.plf
@@ -0,0 +1,51 @@
+; depends: theory_def.plf util_defs.plf
+
+; Substitute, which returns the result of replacing all occurrences of the
+; bound variable whose identifier is v with the term s. It is the responsibility
+; of the caller to ensure that all occurrences of (bvar v u) in t are such that
+; u is the sort of s. Otherwise, this will return a term that is not well
+; sorted.
+(program sc_substitute ((t term) (v mpz) (s term)) term
+  (match t
+    ((bvar v1 u1) (mpz_ifequal v v1 s t))
+    ((apply t1 t2) (apply (sc_substitute t1 v s) (sc_substitute t2 v s)))
+    (default t)
+  ))
+
+; Concludes the instantiation for the term of the outermost quantifier in the
+; rule PfRule::INSTANTIATE. We do not enforce type checking of term s
+; currently, which should be of sort u.
+(declare instantiate (! body term
+                     (! v mpz
+                     (! u sort
+                     (! s term
+                     (! bodyi term
+                     (! p (holds (forall v u body))
+                     (! r (^ (sc_substitute body v s) bodyi)
+                       (holds bodyi)))))))))
+
+; Concludes the skolemization for the term of the outermost quantifier in the
+; rule PfRule::SKOLEMIZE.
+(declare skolemize (! body term
+                     (! v mpz
+                     (! s sort
+                     (! bodyi term
+                     (! p (holds (exists v s body))
+                     (! r (^ (sc_substitute body v (skolem (witness v s body))) bodyi)
+                       (holds bodyi))))))))
+
+; We do not enforce type checking of s currently, which should be of
+; sort u.
+(declare exists_intro (! bodyi term
+                      (! v mpz
+                      (! u sort
+                      (! s term
+                      (! body term
+                      (! p (holds bodyi)
+                      (! r (^ (sc_substitute body v s) bodyi)
+                        (holds (exists v u body)))))))))
+
+(declare skolem_intro (! u term
+                      (! t term
+                      (! r (^ (sc_mk_skolem t) u)
+                        (holds (= u t))))))

diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf
index 5639cc54e8d164ce28903a6856c81a88cc127b80..8d1793666870755f9cdeec4a624a84dbbaecda7f 100644 (file)
--- a/proofs/lfsc/signatures/util_defs.plf
+++ b/proofs/lfsc/signatures/util_defs.plf
@@ -25,6 +25,11 @@
 (declare bvn bitvec)
 (declare bvc (! b bit (! v bitvec bitvec)))
 
+; Returns term t if v1 = v2, and term s otherwise.
+(program mpz_ifequal ((v1 mpz) (v2 mpz) (t term) (s term)) term
+  (mp_ifzero (mp_add (mp_neg v1) v2) t s)
+)
+
 ;; ---- Side conditions
 
 ; Get the argument from an f-application t, fail if t is not an f-application.