Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.

3 files changed, 205 insertions, 15 deletions

diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf
new file mode 100755
index 000000000..600fc11c9
--- /dev/null
+++ b/proofs/signatures/example-arrays.plf
@@ -0,0 +1,139 @@
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+
+; --------------------------------------------------------------------------------
+; literals :
+; L1 : a = write( a, i, read( a, i )
+; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k )
+; L3 : i = k
+
+; input :
+; ~L1
+
+; (extenstionality) lemma : 
+; L1 or ~L2
+
+; theory conflicts :
+; L2 or ~L3
+; L2 or L3
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+; (0) -------------------- term declarations -----------------------------------
+
+(check
+(% I sort
+(% E sort
+(% a (term (array I E))
+(% i (term I)
+
+
+; (1) -------------------- input formula -----------------------------------
+
+(% A1 (th_holds (not (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))))
+
+
+
+
+; (2) ------------------- specify that the following is a proof of the empty clause -----------------
+
+(: (holds cln)
+
+
+
+
+; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF -----------------
+;     ---  these should introduce (th_holds ...)
+
+
+; extensionality lemma : notice this also introduces skolem k
+(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2
+
+
+
+
+; (4) -------------------- map theory literals to boolean variables
+;     --- maps all theory literals involved in proof to boolean literals
+
+(decl_atom (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1
+(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2
+(decl_atom (= I i k) (\ v3 (\ a3
+
+
+
+; (5) -------------------- theory conflicts ---------------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(asf _ _ _ a3 (\ l3
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   ; use read over write rule "row"
+   (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2)
+   
+))))) (\ CT1
+; CT1 is the clause ( v2 V v3 )
+
+(satlem _ _
+(ast _ _ _ a3 (\ l3
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   ; use read over write rule "row1"
+   (contra _ (symm _ _ _ 
+   	     (trans _ _ _ _ 
+               (symm _ _ _ (cong _ _ _ _ _ _ 
+               	 (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))
+               	 l3))
+               (trans _ _ _ _
+                 (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i))
+                 (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3)
+                 )))
+            l2)
+   
+))))) (\ CT2
+; CT2 is the clause ( v2 V ~v3 )
+
+
+; (6) -------------------- clausification -----------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(ast _ _ _ a1 (\ l1
+(clausify_false
+
+; input formula A1 is ( ~a1 )
+; the following is a proof of a1 ^ ( ~a1 ) => false
+
+  (contra _ l1 A1)
+
+))) (\ C1
+; C1 is the clause ( ~v1 )
+
+
+(satlem _ _
+(asf _ _ _ a1 (\ l1
+(ast _ _ _ a2 (\ l2
+(clausify_false
+
+; lemma A2 is ( a1 V ~a2 )
+; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false
+
+  (contra _ l2 (or_elim_1 _ _ l1 A2))
+
+))))) (\ C2
+; C2 is the clause ( v1 V ~v2 )
+
+
+; (7) -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2)
+
+(\ x x))
+
+)))))))))))))))))))))))))))
diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index 6e0e6438d..edb6dc96e 100755
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -12,15 +12,14 @@
 ; functions

 (declare write (! s1 sort

                (! s2 sort

-               (! t1 (term (array s1 s2))

-               (! t2 (term s1)

-               (! t3 (term s2)

-                (term (array s1 s2))))))))

+                 (term (arrow (array s1 s2) 

+                       (arrow s1 

+                       (arrow s2 (array s1 s2))))))))

+                 

 (declare read (! s1 sort

               (! s2 sort

-              (! t1 (term (array s1 s2))

-              (! t2 (term s1)

-                (term s2))))))

+              	(term (arrow (array s1 s2)

+               	      (arrow s1 s2))))))

                 

 ; inference rules

 (declare row1 (! s1 sort

@@ -28,26 +27,26 @@
               (! t1 (term (array s1 s2))

               (! t2 (term s1)

               (! t3 (term s2)

-              	(th_holds (= _ (read (write t1 t2 t3) t2) t3))))))))

+              	(th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) 

+              		       t3))))))))

               	

 

 (declare row (! s1 sort

              (! s2 sort

-             (! t1 (term (array s1 s2))

              (! t2 (term s1)

              (! t3 (term s1)

+             (! t1 (term (array s1 s2))

              (! t4 (term s2)

              (! u (th_holds (not (= _ t2 t3)))

-               (th_holds (= _ (read (write t1 t2 t4) t3) (read t1 t3))))))))))

+               (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) 

+               		      (apply _ _ (apply _ _ (read s1 s2) 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)))))))))

+                   (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))

+                     (holds cln)))

+               (holds cln)))))))

                
\ No newline at end of file
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
new file mode 100755
index 000000000..d18812380
--- /dev/null
+++ b/proofs/signatures/th_quant.plf
@@ -0,0 +1,52 @@
+(declare forall (! s sort

+                (! t (term s)

+                (! f formula

+                  formula))))

+

+(program instantiate ((f formula) (t term) (k term))

+  (do (markvar t) 

+     (let f1 (inst_f f t)

+        (do (markvar t) f1))))

+

+(program instantiate_f ((f formula) (k term)) formula

+  (match f 

+    ((and f1 f2) (and (instantiate_f f1 t) (instantiate_f f2 t)))

+    ((or f1 f2) (or (instantiate_f f1 t) (instantiate_f f2 t)))

+    ((impl f1 f2) (impl (instantiate_f f1 t) (instantiate_f f2 t)))

+    ((not f1) (not (instantiate_f f1 t)))

+    ((iff f1 f2) (iff (instantiate_f f1 t) (instantiate_f f2 t)))

+    ((xor f1 f2) (xor (instantiate_f f1 t) (instantiate_f f2 t)))

+    ((ifte f1 f2 f3) (ifte (instantiate_f f1 t) (instantiate_f f2 t) (instantiate_f f3 t)))

+    ((= s t1 t2) (= s (inst_t t1 t) (inst_t t2 t)))

+    ((forall t1 f1) (forall t1 (instantiate_f f1 t)))

+    (default f)))

+

+(program instantiate_t ((t term) (k term)) formula

+  (match t

+    ((apply s1 s2 t1 t2) (apply s1 s2 t1 (instantiate_t t2 t)))

+    (default (ifmarked t k t))))

+

+

+(declare skolem

+  (! s sort

+  (! t (term s)

+  (! f formula

+  (! p (th_holds (not (forall s t f)))

+  (! u (! f1 formula

+       (! k (term s)

+       (! r (^ (instantiate f t k) f1)

+       (! p1 (th_holds (not f1))

+         (holds cln)))))

+    (holds cln)))))))

+    

+(declare inst

+  (! s sort

+  (! t (term s)

+  (! f formula

+  (! f1 formula

+  (! p (th_holds (forall s t f))

+  (! k (term s)

+  (! r (^ (instantiate f t k) f1)

+  (! u (! p1 (th_holds f1)

+            (holds cln))

+    (holds cln))))))))))
\ No newline at end of file