From 72f1d72852213f46d77c85216c9250bb0f0e3eae Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Tue, 27 Nov 2018 00:59:22 -0800
Subject: [PATCH] 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.
---
 proofs/signatures/th_lra.plf      |  9 ++++-----
 proofs/signatures/th_lra_test.plf | 32 +++++++++++++++++++++++++++++++
 proofs/signatures/th_real.plf     |  6 ++++++
 3 files changed, 42 insertions(+), 5 deletions(-)
 create mode 100644 proofs/signatures/th_lra_test.plf

diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf
index d67fdc84f..67b17c9af 100644
--- 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
index 000000000..687ff988b
--- /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 3478e23ef..3529779f3 100644
--- 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)))
-- 
2.30.2