Add working example of LFSC proof with quantifiers. Update quantifiers signature to avoid dependent types in side condition.

2 files changed, 153 insertions, 28 deletions

diff --git a/proofs/signatures/example-quant.plf b/proofs/signatures/example-quant.plf
new file mode 100755
index 000000000..086633be9
--- /dev/null
+++ b/proofs/signatures/example-quant.plf
@@ -0,0 +1,95 @@
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf
+
+; --------------------------------------------------------------------------------
+; literals :
+; L1 : forall x. x != x
+; L2 : t = t
+
+; input :
+; L1
+
+; (instantiation) lemma : 
+; L1 => L2
+
+; theory conflicts :
+; ~L2
+
+
+;  With the theory lemma, the input is unsatisfiable.
+; --------------------------------------------------------------------------------
+
+
+; (0) -------------------- term declarations -----------------------------------
+
+(check
+(% s sort
+(% t (term s)
+
+
+; (1) -------------------- input formula -----------------------------------
+
+(% x (term s)
+(% A1 (th_holds (forall _ x (not (= _ x x))))
+
+
+
+; (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 ...)
+
+
+; instantiation lemma
+(inst _ _ _ t (not (= _ t t)) A1 (\ A2
+
+
+
+
+; (4) -------------------- map theory literals to boolean variables
+;     --- maps all theory literals involved in proof to boolean literals
+
+(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1
+(decl_atom (= _ t t) (\ v2 (\ a2
+
+
+
+
+; (5) -------------------- theory conflicts ---------------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(asf _ _ _ a2 (\ l2
+(clausify_false
+
+   (contra _ (refl _ t) l2)
+   
+))) (\ CT1
+; CT1 is the clause ( v2 )
+
+
+; (6) -------------------- clausification -----------------------------------------
+;     ---  these should introduce (holds ...)
+
+(satlem _ _
+(ast _ _ _ a2 (\ l2
+(clausify_false
+
+  (contra _ l2 A2)
+
+))) (\ C1
+; C1 is the clause ( ~v2 )
+
+
+; (7) -------------------- resolution proof ------------------------------------------------------------
+
+(satlem_simplify _ _ _
+
+(R _ _ CT1 C1 v2)
+
+(\ x x))
+
+))))))))))))))))))
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf
index d18812380..98b53e43d 100755
--- a/proofs/signatures/th_quant.plf
+++ b/proofs/signatures/th_quant.plf
@@ -3,39 +3,69 @@
                 (! 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 eqterm ((n1 term) (n2 term)) bool

+    (do (markvar n1)

+        (let s (ifmarked n2 tt ff)

+           (do (markvar n1) s))))

 

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

+(program is_inst_t ((ti term) (t term) (k term)) bool

   (match t

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

-    (default (ifmarked t k t))))

+    ((apply s1 s2 t1 t2) 

+      (match ti

+        ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))

+        (default ff)))

+    (default 

+      (match ti

+        ((apply si1 si2 ti1 ti2) ff)

+        (default (eqterm ti (ifmarked t k t)))))))

+

+(program is_inst_f ((fi formula) (f formula) (k term)) bool

+  (match f 

+    ((and f1 f2) (match fi

+    		   ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))

+    		   (default ff)))

+    ((or f1 f2) (match fi

+    		   ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))

+    		   (default ff)))

+    ((impl f1 f2) (match fi

+    		   ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))

+    		   (default ff)))

+    ((not f1) (match fi

+    		   ((not fi1) (is_inst_f fi1 f1 k))

+    		   (default ff)))

+    ((iff f1 f2) (match fi

+    		   ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))

+    		   (default ff)))

+    ((xor f1 f2) (match fi

+    		   ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))

+    		   (default ff)))

+    ((ifte f1 f2 f3) (match fi

+    		       ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k) 

+    		       			     (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff))) 

+    		       			     (ff ff)))

+    		       (default ff)))

+    ((= s t1 t2) (match fi

+    		   ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))

+    		   (default ff)))

+    ((forall s t1 f1) (match fi

+    		      ((forall s ti1 fi1) (is_inst_f fi1 f1 k))

+    		      (default ff)))

+    (default ff)))

 

+(program is_inst ((fi formula) (f formula) (t term) (k term)) bool

+  (do (markvar t) 

+     (let f1 (is_inst_f fi f k)

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

 

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

+  (! u (! k (term s)

+       (! fi formula

+       (! p1 (th_holds (not fi))

+       (! r (^ (is_inst fi f t k) tt)

          (holds cln)))))

     (holds cln)))))))

     

@@ -43,10 +73,10 @@
   (! 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)

+  (! fi formula

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

+  (! r (^ (is_inst fi f t k) tt)

+  (! u (! p1 (th_holds fi)

             (holds cln))

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