Adding example proof signatures for LFSC.

4 files changed, 663 insertions, 0 deletions

diff --git a/proofs/signatures/example.plf b/proofs/signatures/example.plf
new file mode 100755
index 000000000..5df1f31c3
--- /dev/null
+++ b/proofs/signatures/example.plf
@@ -0,0 +1,116 @@
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf

+

+; -------------------------------------------------------------------------------- 

+; input :

+; ( a = b )

+; ( b = f(c) )

+; ( a != f(c) V a != b )

+

+; theory lemma (by transitivity) :

+; ( a != b V b != f(c) V a = f(c) )

+

+

+;  With the theory lemma, the input is unsatisfiable.

+; -------------------------------------------------------------------------------- 

+

+

+

+(check 

+(% s sort

+(% a (term s)

+(% b (term s)

+(% c (term s)

+(% f (term (arrow s s))

+

+; -------------------- declaration of input formula -----------------------------------

+

+(% A1 (th_holds (= s a b))

+(% A2 (th_holds (= s b (apply _ _ f c)))

+(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))

+

+

+; ------------------- specify that the following is a proof of the empty clause -----------------

+

+(: (holds cln)

+

+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------

+

+(decl_atom (= s a b) (\ v1 (\ a1

+(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2

+(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3

+

+

+; --------------------------- proof of theory lemma ---------------------------------------------

+

+(satlem _ _

+(ast _ _ _ a1 (\ l1

+(ast _ _ _ a2 (\ l2

+(asf _ _ _ a3 (\ l3

+(clausify_false

+

+; this should be a proof of l1 ^ l2 ^ ~l3 => false

+; this is done by theory proof rules (currently just use "trust")

+

+  trust

+

+))))))) (\ CT

+; CT is the clause ( ~v1 V ~v2 V v3 )

+

+; -------------------- clausification of input formulas -----------------------------------------

+

+(satlem _ _

+(asf _ _ _ a1 (\ l1

+(clausify_false

+

+; input formula A1 is ( ~l1 )

+; the following should be a proof of l1 ^ ( ~l1 ) => false

+; this is done by natural deduction rules

+

+  (contra _ A1 l1)

+

+))) (\ C1

+; C1 is the clause ( v1 )

+

+

+(satlem _ _

+(asf _ _ _ a2 (\ l2

+(clausify_false

+

+; input formula A2 is ( ~l2 )

+; the following should be a proof of l2 ^ ( ~l2 ) => false

+; this is done by natural deduction rules

+

+   (contra _ A2 l2)

+   

+))) (\ C2 

+; C2 is the clause ( v2 )

+

+

+(satlem _ _

+(ast _ _ _ a3 (\ l3

+(ast _ _ _ a1 (\ l1

+(clausify_false

+

+; input formula A3 is ( ~a3 V ~a1 ) 

+; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false

+; this is done by natural deduction rules

+

+  (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))

+

+))))) (\ C3  

+; C3 is the clause ( ~v3 V ~v1 )

+

+

+

+; -------------------- resolution proof ------------------------------------------------------------

+

+(satlem_simplify _ _ _ 

+

+(R _ _ C1

+(R _ _ C2

+(R _ _ CT C3 v3) v2) v1)

+

+(\ x x))

+

+))))))))))))))))))))))))))

+)
\ No newline at end of file
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf
new file mode 100755
index 000000000..09255f612
--- /dev/null
+++ b/proofs/signatures/sat.plf
@@ -0,0 +1,127 @@
+(declare bool type)

+(declare tt bool)

+(declare ff bool)

+

+(declare var type) 

+

+(declare lit type)

+(declare pos (! x var lit))

+(declare neg (! x var lit))

+

+(declare clause type)

+(declare cln clause)

+(declare clc (! x lit (! c clause clause)))

+

+; constructs for general clauses for R, Q, satlem

+

+(declare concat (! c1 clause (! c2 clause clause)))

+(declare clr (! l lit (! c clause clause))) 

+

+; code to check resolutions

+

+(program append ((c1 clause) (c2 clause)) clause

+  (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))

+

+; we use marks as follows:

+; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.

+; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.

+; -- mark 3 if we did indeed remove the variable positively

+; -- mark 4 if we did indeed remove the variable negatively

+(program simplify_clause ((c clause)) clause

+  (match c

+    (cln cln)

+    ((clc l c1)

+      (match l

+        ; Set mark 1 on v if it is not set, to indicate we should remove it.

+        ; After processing the rest of the clause, set mark 3 if we were already 

+        ; supposed to remove v (so if mark 1 was set when we began).  Clear mark3

+        ; if we were not supposed to be removing v when we began this call.

+        ((pos v)

+          (let m (ifmarked v tt (do (markvar v) ff))

+          (let c' (simplify_clause c1)

+            (match m

+              (tt (do (ifmarked3 v v (markvar3 v)) c'))                            

+              (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))

+        ; the same as the code for tt, but using different marks.

+        ((neg v)

+          (let m (ifmarked2 v tt (do (markvar2 v) ff))

+          (let c' (simplify_clause c1)

+            (match m

+              (tt (do (ifmarked4 v v (markvar4 v)) c'))                            

+              (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))

+    ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))

+    ((clr l c1)

+      (match l

+        ; set mark 1 to indicate we should remove v, and fail if

+        ; mark 3 is not set after processing the rest of the clause

+        ; (we will set mark 3 if we remove a positive occurrence of v).

+        ((pos v)

+            (let m (ifmarked v tt (do (markvar v) ff))

+            (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)

+            (let c' (simplify_clause c1)

+              (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))

+                                (match m (tt v) (ff (markvar v))) c')

+                          (fail clause))))))

+        ; same as the tt case, but with different marks.

+        ((neg v)

+            (let m2 (ifmarked2 v tt (do (markvar2 v) ff))

+            (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)

+            (let c' (simplify_clause c1)

+              (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))

+                                (match m2 (tt v) (ff (markvar2 v))) c')

+                          (fail clause))))))

+   ))))

+

+

+; resolution proofs

+          

+(declare holds (! c clause type))

+

+(declare R (! c1 clause (! c2 clause 

+           (! u1 (holds c1)

+           (! u2 (holds c2)

+           (! n var

+            (holds (concat (clr (pos n) c1)

+                     (clr (neg n) c2)))))))))   

+

+(declare Q (! c1 clause (! c2 clause 

+           (! u1 (holds c1)

+           (! u2 (holds c2)

+           (! n var

+            (holds (concat (clr (neg n) c1)

+                     (clr (pos n) c2)))))))))

+                     

+(declare satlem_simplify

+                (! c1 clause

+                (! c2 clause

+                (! c3 clause

+                (! u1 (holds c1)

+                (! r (^ (simplify_clause c1) c2)

+                (! u2 (! x (holds c2) (holds c3))

+                   (holds c3))))))))

+                   

+(declare satlem

+  (! c clause

+  (! c2 clause

+  (! u (holds c)

+  (! u2 (! v (holds c) (holds c2))

+    (holds c2))))))

+

+; 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

+; clr or clc scope.  Uncomment and run with 

+; --show-runs to see it in action.

+; 

+; (check 

+;   (% v1 var

+;   (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))

+;                    (clc (pos v1) (clc (pos v1) cln))))

+;    (satlem _ _ _ u1 (\ x x))))))

+

+

+;(check 

+;   (% v1 var

+;   (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)

+;                                      (clr (neg v1) (clc (neg v1) cln)))))

+;    (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
new file mode 100755
index 000000000..75bfc442f
--- /dev/null
+++ b/proofs/signatures/smt.plf
@@ -0,0 +1,313 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; SMT syntax and semantics (not theory-specific)
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(declare formula type)
+(declare th_holds (! f formula type))
+
+; constants
+(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)))
+(declare impl (! f1 formula (! f2 formula formula)))
+(declare iff (! f1 formula (! f2 formula formula)))
+(declare xor (! f1 formula (! f2 formula formula)))
+(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 term (! t sort type))	; declared terms in formula
+
+(declare apply (! s1 sort
+               (! s2 sort
+               (! t1 (term (arrow s1 s2))
+               (! t2 (term s1)
+                (term s2))))))
+                
+(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)
+               formula))))
+(declare flet (! f1 formula
+              (! 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".
+; 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
+
+; 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.
+;  ...
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; Natural deduction rules : used for CNF
+;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+;; contradiction
+
+(declare contra
+  (! f formula
+  (! r1 (th_holds f)
+  (! r2 (th_holds (not f))
+    (th_holds false)))))
+
+;; not not
+
+(declare not_not_intro
+  (! f formula
+  (! u (th_holds f)
+    (th_holds (not (not f))))))
+    
+(declare not_not_elim
+  (! f formula
+  (! u (th_holds (not (not f)))
+    (th_holds f))))
+
+;; or elimination
+
+(declare or_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f1))
+  (! u2 (th_holds (or f1 f2))
+    (th_holds f2))))))
+    
+(declare or_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f2))
+  (! u2 (th_holds (or f1 f2))
+    (th_holds f1))))))
+    
+;; and elimination
+
+(declare and_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (and f1 f2))
+    (th_holds f1)))))
+    
+(declare and_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (and f1 f2))
+    (th_holds f2)))))
+    
+;; not impl elimination
+
+(declare not_impl_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (not (impl f1 f2)))
+    (th_holds f1)))))
+    
+(declare not_impl_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (not (impl f1 f2)))
+    (th_holds (not f2))))))
+    
+;; impl elimination
+
+(declare impl_intro (! f1 formula
+                    (! f2 formula
+                    (! i1 (! u (th_holds f1) 
+                              (th_holds f2))
+                      (th_holds (impl f1 f2))))))
+
+(declare impl_elim
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds f1)
+  (! u2 (th_holds (impl f1 f2))  
+    (th_holds f2))))))
+    
+;; iff elimination
+
+(declare iff_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (iff f1 f2))
+    (th_holds (impl f1 f2))))))
+    
+(declare iff_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (iff f1 f2))
+    (th_holds (impl f2 f1))))))
+
+(declare not_iff_elim_1
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (not f1))
+  (! u2 (th_holds (not (iff f1 f2)))
+    (th_holds f2))))))
+
+(declare not_iff_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds f1)
+  (! u2 (th_holds (not (iff f1 f2)))
+    (th_holds (not f2)))))))
+
+;; ite elimination
+
+(declare ite_elim_1
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (ifte a b c))
+    (th_holds b)))))))
+    
+(declare ite_elim_2
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not a))
+  (! u2 (th_holds (ifte a b c))
+    (th_holds c)))))))
+    
+(declare ite_elim_3
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not b))
+  (! u2 (th_holds (ifte a b c))
+    (th_holds c)))))))
+    
+(declare ite_elim_2n
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (ifte (not a) b c))
+    (th_holds c)))))))
+
+(declare not_ite_elim_1
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not b))))))))
+    
+(declare not_ite_elim_2
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds (not a))
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not c))))))))
+    
+(declare not_ite_elim_3
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds b)
+  (! u2 (th_holds (not (ifte a b c)))
+    (th_holds (not c))))))))
+    
+(declare not_ite_elim_2n
+  (! a formula
+  (! b formula
+  (! c formula
+  (! u1 (th_holds a)
+  (! u2 (th_holds (not (ifte (not a) b c)))
+    (th_holds (not c))))))))
+    
+    
+    
+;; How to do CNF for disjunctions of theory literals.
+;;
+;; 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.
+;; Do this at the beginning of the proof:
+;;
+;; (decl_atom F1 (\ v1 (\ a1
+;; (decl_atom F2 (\ v2 (\ a2
+;; ....
+;; (decl_atom Fn (\ vn (\ an
+;;
+;; Our input A is clausified by the following proof:
+;;
+;;(satlem _ _
+;;(asf _ _ _ a1 (\ l1
+;;(asf _ _ _ a2 (\ l2
+;;...
+;;(asf _ _ _ an (\ ln
+;;(clausify_false
+;;
+;;   (contra _
+;;      (or_elim_1 _ _ l{n-1}
+;;	...
+;;      (or_elim_1 _ _ l2 
+;; 	(or_elim_1 _ _ l1 A))))) ln)
+;;	
+;;))))))) (\ C
+;;
+;; 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)))).
+;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
+;; the arguments of contra:
+;;
+;;(satlem _ _
+;;(ast _ _ _ a1 (\ l1
+;;(asf _ _ _ a2 (\ l2
+;;(ast _ _ _ a3 (\ l3
+;;(clausify_false
+;;
+;;   (contra _ l3
+;;      (or_elim_1 _ _ l2 
+;; 	(or_elim_1 _ _ (not_not_intro l1) A))))
+;;	
+;;))))))) (\ C
+;;
+;; C should be the clause (~v1 V v2 V ~v3 )
\ No newline at end of file
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
new file mode 100755
index 000000000..e66990de4
--- /dev/null
+++ b/proofs/signatures/th_base.plf
@@ -0,0 +1,107 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+;

+; 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"

+;

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+

+(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))))))))

+

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+;

+; Theory of Equality and Congruence Closure

+;

+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

+

+; temporary : 

+(declare trust (th_holds false))

+

+(declare refl

+  (! s sort

+  (! t (term s)

+    (th_holds (= s t t)))))

+

+(declare symm (! s sort

+              (! x (term s)

+              (! y (term s)

+              (! u (th_holds (= _ x y))

+                (th_holds (= _ y x)))))))

+

+(declare trans (! s sort

+               (! x (term s)

+               (! y (term s)

+               (! z (term s)

+               (! u (th_holds (= _ x y))

+               (! u (th_holds (= _ y z))

+                 (th_holds (= _ x z)))))))))

+

+(declare cong (! s1 sort

+              (! s2 sort

+              (! a1 (term (arrow s1 s2))

+              (! b1 (term (arrow s1 s2))

+              (! a2 (term s1)

+              (! b2 (term s1)

+              (! u1 (th_holds (= _ a1 b1))

+              (! u2 (th_holds (= _ a2 b2))

+                (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))

+