LRA proof signature fixes and a first proof for linear polynomials (#2713)

* LRA proof signature fixes and a first proof

The existing LRA signature had a few problems (e.g. referencing symbols
that didn't exist, extra parentheses, etc). I patched it up and wrote an
first example LRA proof. load `th_lra_test.plf` last to run that test.

* Add dependency info to signatures

I chose to indicate shallow dependencies only.

diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf
index d67fdc84fd5d860174528625d4a322f55be171f6..67b17c9affd89cc4944b00b442d076680d67a1a5 100644 (file)
--- a/proofs/signatures/th_lra.plf
+++ b/proofs/signatures/th_lra.plf
@@ -1,5 +1,4 @@
-; 59 loc in side conditions
-
+; Depends on th_real.plf, th_smt.plf
 (program mpq_ifpos ((x mpq)) bool
   (mp_ifneg x ff (mp_ifzero x ff tt)))
 
@@ -111,7 +110,7 @@
   (! f1 (th_holds (>=0_Real (poly_term p1)))
   (! f2 (th_holds (>=0_Real (poly_term p2)))
   (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
-    (th_holds (=0_Real (poly_term p2))))))))))
+    (th_holds (=0_Real (poly_term p2)))))))))
 
 ;; axioms
 
@@ -202,7 +201,7 @@
   (! f1 (th_holds (=0_Real (poly_term p1)))
   (! f2 (th_holds (=0_Real (poly_term p2)))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (=0_Real (poly_term p3)))))))))))
+    (th_holds (=0_Real (poly_term p3))))))))))
 
 (declare lra_add_>_>
   (! p1 poly
@@ -256,7 +255,7 @@
   (! f1 (th_holds (=0_Real (poly_term p1)))
   (! f2 (th_holds (distinct0_Real (poly_term p2)))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (distinct0_Real (poly_term p3)))))))))))
+    (th_holds (distinct0_Real (poly_term p3))))))))))
 
 ;; substracting equations
 

diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf
new file mode 100644 (file)
index 0000000..687ff98
--- /dev/null
+++ b/proofs/signatures/th_lra_test.plf
@@ -0,0 +1,32 @@
+; Depends On: th_lra.plf
+(check
+  ; Variables
+  (% x var_real
+  (% y var_real
+  ; linear monomials (combinations)
+  (@ m1 (lmonc (~ 1/1) x (lmonc (~ 1/2) y lmonn))
+  (@ m2 (lmonc 1/1 x (lmonc 1/1 y lmonn))
+  (@ m3 (lmonc 1/1 x (lmonc (~ 1/1) y lmonn))
+  ; linear polynomials (affine)
+  (@ p1 (polyc 2/1 m1)
+  (@ p2 (polyc (~ 8/1) m2)
+  (@ p3 (polyc 0/1 m3)
+  (% pf_nonneg_1 (th_holds (>=0_Real (poly_term p1)))
+  (% pf_nonneg_2 (th_holds (>=0_Real (poly_term p2)))
+  (% pf_nonneg_3 (th_holds (>=0_Real (poly_term p3)))
+     (lra_contra_>=
+       _
+       (lra_add_>=_>= _ _ _
+         (lra_mul_c_>= _ _ 4/1 pf_nonneg_1)
+         (lra_add_>=_>= _ _ _
+           (lra_mul_c_>= _ _ 3/1 pf_nonneg_2)
+           (lra_add_>=_>= _ _ _
+             (lra_mul_c_>= _ _ 1/1 pf_nonneg_3)
+             (lra_axiom_>= 0/1)))))
+  )))))
+  ))))
+  ))
+)
+
+
+

diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf
index 3478e23ef6fdac724156eab66736a59777757821..3529779f3c7ce5153bb637519c565d3dadf9c4e3 100644 (file)
--- a/proofs/signatures/th_real.plf
+++ b/proofs/signatures/th_real.plf
@@ -1,3 +1,4 @@
+; Depends On: th_smt.plf
 (declare Real sort)
 
 (define arithpred_Real (! x (term Real)
@@ -21,5 +22,10 @@
 ; a constant term
 (declare a_real (! x mpq (term Real)))
 
+(declare >=0_Real (! x (term Real) formula))
+(declare =0_Real (! x (term Real) formula))
+(declare >0_Real (! x (term Real) formula))
+(declare distinct0_Real (! x (term Real) formula))
+
 ; unary negation
 (declare u-_Real (! t (term Real) (term Real)))