diff options
Diffstat (limited to 'proofs')
| -rwxr-xr-x | proofs/signatures/smt.plf | 124 | ||||
| -rwxr-xr-x | proofs/signatures/th_arrays.plf | 53 | ||||
| -rwxr-xr-x | proofs/signatures/th_base.plf | 100 |
3 files changed, 167 insertions, 110 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 67ce3988a..bbee2d49b 100755 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -3,15 +3,14 @@ ; SMT syntax and semantics (not theory-specific) ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on sat.plf (declare formula type) (declare th_holds (! f formula type)) -; constants +; standard logic definitions (declare true formula) (declare false formula) - -; logical connectives (declare not (! f formula formula)) (declare and (! f1 formula (! f2 formula formula))) (declare or (! f1 formula (! f2 formula formula))) @@ -21,24 +20,19 @@ (declare ifte (! b formula (! f1 formula (! f2 formula formula)))) ; terms -(declare sort type) ; sort in the theory -(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor - +(declare sort type) (declare term (! t sort type)) ; declared terms in formula -(declare apply (! s1 sort - (! s2 sort - (! t1 (term (arrow s1 s2)) - (! t2 (term s1) - (term s2)))))) - +; standard definitions for =, ite, let and flet +(declare = (! s sort + (! x (term s) + (! y (term s) + formula)))) (declare ite (! s sort (! f formula (! t1 (term s) (! t2 (term s) (term s)))))) - -; let/flet (declare let (! s sort (! t (term s) (! f (! v (term s) formula) @@ -47,38 +41,52 @@ (! f2 (! v formula formula) formula))) -; predicates -(declare = (! s sort - (! x (term s) - (! y (term s) - formula)))) - -; To avoid duplicating some of the rules (e.g., cong), we will view -; applications of predicates as terms of sort "Bool". +; We view applications of predicates as terms of sort "Bool". ; Such terms can be injected as atomic formulas using "p_app". - (declare Bool sort) ; the special sort for predicates (declare p_app (! x (term Bool) formula)) ; propositional application of term ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Examples +; +; CNF Clausification +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; an example of "(p1 or p2(0)) and t1=t2(1)" -;(! p1 (term Bool) -;(! p2 (term (arrow Int Bool)) -;(! t1 (term Int) -;(! t2 (term (arrow Int Int)) -;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) -; (= _ t1 (apply _ _ t2 1)))) -; ... +; binding between an LF var and an (atomic) formula +(declare atom (! v var (! p formula type))) -; another example of "p3(a,b)" -;(! a (term Int) -;(! b (term Int) -;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. -;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. -; ... +(declare decl_atom + (! f formula + (! u (! v var + (! a (atom v f) + (holds cln))) + (holds cln)))) + +; clausify a formula directly +(declare clausify_form + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds f) + (holds (clc (pos v) cln))))))) + +(declare clausify_form_not + (! f formula + (! v var + (! a (atom v f) + (! u (th_holds (not f)) + (holds (clc (neg v) cln))))))) + +(declare clausify_false + (! u (th_holds false) + (holds cln))) + +(declare th_let_pf + (! f formula + (! u (th_holds f) + (! u2 (! v (th_holds f) (holds cln)) + (holds cln))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -261,13 +269,41 @@ (! u2 (th_holds (not (ifte (not a) b c))) (th_holds (not c)))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; For theory lemmas +; - make a series of assumptions and then derive a contradiction (or false) +; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" +; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare ast + (! v var + (! f formula + (! C clause + (! r (atom v f) ;this is specified + (! u (! o (th_holds f) + (holds C)) + (holds (clc (neg v) C)))))))) + +(declare asf + (! v var + (! f formula + (! C clause + (! r (atom v f) + (! u (! o (th_holds (not f)) + (holds C)) + (holds (clc (pos v) C)))))))) + + -;; How to do CNF for disjunctions of theory literals. +;; Example: ;; -;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). +;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). ;; -;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn. +;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn). ;; Do this at the beginning of the proof: ;; ;; (decl_atom F1 (\ v1 (\ a1 @@ -275,7 +311,7 @@ ;; .... ;; (decl_atom Fn (\ vn (\ an ;; -;; Our input A is clausified by the following proof: +;; A is then clausified by the following proof: ;; ;;(satlem _ _ ;;(asf _ _ _ a1 (\ l1 @@ -294,7 +330,7 @@ ;; ;; We now have the free variable C, which should be the clause (v1 V ... V vn). ;; -;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). +;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). ;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip ;; the arguments of contra: ;; @@ -311,3 +347,5 @@ ;;))))))) (\ C ;; ;; C should be the clause (~v1 V v2 V ~v3 ) + + diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf new file mode 100755 index 000000000..6e0e6438d --- /dev/null +++ b/proofs/signatures/th_arrays.plf @@ -0,0 +1,53 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Theory of Arrays
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+; depdends on : th_base.plf
+
+; sorts
+
+(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element
+
+; functions
+(declare write (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (term (array s1 s2))))))))
+(declare read (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (term s2))))))
+
+; inference rules
+(declare row1 (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s2)
+ (th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))
+
+
+(declare row (! s1 sort
+ (! s2 sort
+ (! t1 (term (array s1 s2))
+ (! t2 (term s1)
+ (! t3 (term s1)
+ (! t4 (term s2)
+ (! u (th_holds (not (= _ t2 t3)))
+ (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))
+
+(declare ext (! s1 sort
+ (! s2 sort
+ (! f formula
+ (! t1 (term (array s1 s2))
+ (! t2 (term (array s1 s2))
+ (! u (th_holds (not (= _ t1 t2)))
+ (! u1 (! k (term s1)
+ (! u2 (th_holds (not (= _ (read t1 k) (read t2 k))))
+ (th_holds f)))
+ (th_holds f)))))))))
+
\ No newline at end of file diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 7b0b086dc..977409b6a 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -1,80 +1,28 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Atomization / Clausification -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -; binding between an LF var and an (atomic) formula -(declare atom (! v var (! p formula type))) - -(declare decl_atom - (! f formula - (! u (! v var - (! a (atom v f) - (holds cln))) - (holds cln)))) - -; direct clausify -(declare clausify_form - (! f formula - (! v var - (! a (atom v f) - (! u (th_holds f) - (holds (clc (pos v) cln))))))) - -(declare clausify_form_not - (! f formula - (! v var - (! a (atom v f) - (! u (th_holds (not f)) - (holds (clc (neg v) cln))))))) - -(declare clausify_false - (! u (th_holds false) - (holds cln))) -(declare th_let_pf - (! f formula - (! u (th_holds f) - (! u2 (! v (th_holds f) (holds cln)) - (holds cln))))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; -; Theory reasoning -; - make a series of assumptions and then derive a contradiction (or false) -; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" -; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" +; Theory of Equality and Congruence Closure ; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on : smt.plf -(declare ast - (! v var - (! f formula - (! C clause - (! r (atom v f) ;this is specified - (! u (! o (th_holds f) - (holds C)) - (holds (clc (neg v) C)))))))) +; sorts : -(declare asf - (! v var - (! f formula - (! C clause - (! r (atom v f) - (! u (! o (th_holds (not f)) - (holds C)) - (holds (clc (pos v) C)))))))) +(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Theory of Equality and Congruence Closure -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; functions : -; temporary : -(declare trust (th_holds false)) +(declare apply (! s1 sort + (! s2 sort + (! t1 (term (arrow s1 s2)) + (! t2 (term s1) + (term s2)))))) + + +; inference rules : + +(declare trust (th_holds false)) ; temporary (declare refl (! s sort @@ -105,3 +53,21 @@ (! u2 (th_holds (= _ a2 b2)) (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; Examples + +; an example of "(p1 or p2(0)) and t1=t2(1)" +;(! p1 (term Bool) +;(! p2 (term (arrow Int Bool)) +;(! t1 (term Int) +;(! t2 (term (arrow Int Int)) +;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) +; (= _ t1 (apply _ _ t2 1)))) +; ... + +; another example of "p3(a,b)" +;(! a (term Int) +;(! b (term Int) +;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. +;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. +; ... |