[LRA proof] More complete LRA example proofs. (#2722)

* [LRA proof] Refine "poly" and "term Real" distinction

Short Version:

Refined the LRA signature and used the refined version to write two new
test proofs which are close to interface compatible with the LRA proofs
that CVC4 will produce.

Love Version:

LRA proofs have the following interface:
   * Given predicates between real terms
   * Prove bottom

However, even though the type of the interface does not express this,
the predicates are **linear bounds**, not arbitrary real bounds. Thus
LRA proofs have the following structure:

   1. Prove that the input predicates are equivalent to a set of linear
      bounds.
   2. Use the linear bounds to prove bottom using farkas coefficients.

Notice that the distinction between linear bounds (associated in the
signature with the string "poly") and real predicates (which relate
"term Real"s to one another) matters quite a bit. We have certain inds
of axioms for one, and other axioms for the other.

The signature used to muddy this distinction using a constructor called
"term_poly" which converted between them. I decided it was better to buy
into the distinction fully.

Now all of the axioms for step (2) use the linear bounds and axioms for
step (1) use both kinds of bounds, which makes sense because step (1) is
basically a conversion.

Also had to add an axiom or two, because some were missing.

* Update proofs/signatures/th_lra.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Improved test readability, removed unused axioms

The LRA proof tests did not have appropriate documentation, and did not
specify **what** they proved. Now they each have a header comment
stating their premises and conclusion, and that conclusion is enforced
by a type annotation in the test.

The LRA signature included some unused axioms concerning `poly_term`.
Now they've been removed.

Credits to Yoni for noticing both problems.

2 files changed, 240 insertions, 110 deletions

diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf
index 67b17c9af..76e5127c2 100644
--- a/proofs/signatures/th_lra.plf
+++ b/proofs/signatures/th_lra.plf
@@ -1,4 +1,22 @@
-; Depends on th_real.plf, th_smt.plf
+; Depends on th_real.plf, smt.plf, sat.plf
+
+; LRA proofs have the following interface:
+;    * Given predicates between real terms
+;    * Prove bottom
+;
+; However, even though the type of the interface does not express this,
+; the predicates are **linear bounds**, not arbitrary real bounds. Thus
+; LRA proofs have the following structure:
+;
+;    1. Prove that the input predicates are equivalent to a set of linear
+;       bounds.
+;    2. Use the linear bounds to prove bottom using farkas coefficients.
+;
+; Notice that the distinction between linear bounds (associated in the signature
+; with the string "poly") and real predicates (which relate "term Real"s to one
+; another) matters quite a bit. We have certain kinds of axioms for one, and
+; other axioms for the other.
+
 (program mpq_ifpos ((x mpq)) bool
   (mp_ifneg x ff (mp_ifzero x ff tt)))
 
@@ -100,61 +118,65 @@
 
 ;; conversion to use polynomials in term formulas
 
-(declare poly_term (! p poly (term Real)))
+
+(declare >=0_poly (! x poly formula))
+(declare =0_poly (! x poly formula))
+(declare >0_poly (! x poly formula))
+(declare distinct0_poly (! x poly formula))
 
 ;; create new equality out of inequality
 
 (declare lra_>=_>=_to_=
   (! p1 poly
   (! p2 poly
-  (! f1 (th_holds (>=0_Real (poly_term p1)))
-  (! f2 (th_holds (>=0_Real (poly_term p2)))
+  (! f1 (th_holds (>=0_poly p1))
+  (! f2 (th_holds (>=0_poly p2))
   (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
-    (th_holds (=0_Real (poly_term p2)))))))))
+    (th_holds (=0_poly p2))))))))
 
 ;; axioms
 
 (declare lra_axiom_=
-   (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))
+   (th_holds (=0_poly (polyc 0/1 lmonn))))
 
 (declare lra_axiom_>
   (! c mpq
   (! i (^ (mpq_ifpos c) tt)
-    (th_holds (>0_Real (poly_term (polyc c lmonn)))))))
+    (th_holds (>0_poly (polyc c lmonn))))))
 
 (declare lra_axiom_>=
   (! c mpq
   (! i (^ (mp_ifneg c tt ff) ff)
-    (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))
+    (th_holds (>=0_poly (polyc c lmonn))))))
 
 (declare lra_axiom_distinct
   (! c mpq
   (! i (^ (mp_ifzero c tt ff) ff)
-    (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))
+    (th_holds (distinct0_poly (polyc c lmonn))))))
 
 ;; contradiction rules
 
 (declare lra_contra_=
   (! p poly
-  (! f (th_holds (=0_Real (poly_term p)))
+  (! f (th_holds (=0_poly p))
   (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
     (holds cln)))))
 
 (declare lra_contra_>
   (! p poly
-  (! f (th_holds (>0_Real (poly_term p)))
+  (! f (th_holds (>0_poly p))
   (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
     (holds cln)))))
 
 (declare lra_contra_>=
   (! p poly
-  (! f (th_holds (>=0_Real (poly_term p)))
+  (! f (th_holds (>=0_poly p))
   (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
     (holds cln)))))
 
 (declare lra_contra_distinct
   (! p poly
-  (! f (th_holds (distinct0_Real (poly_term p)))
+  (! f (th_holds (distinct0_poly p))
   (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
     (holds cln)))))
 
@@ -164,33 +186,33 @@
   (! p poly
   (! p' poly
   (! c mpq
-  (! f (th_holds (=0_Real (poly_term p)))
+  (! f (th_holds (=0_poly p))
   (! i (^ (poly_mul_c p c) p')
-    (th_holds (=0_Real (poly_term p')))))))))
+    (th_holds (=0_poly p'))))))))
 
 (declare lra_mul_c_>
   (! p poly
   (! p' poly
   (! c mpq
-  (! f (th_holds (>0_Real (poly_term p)))
+  (! f (th_holds (>0_poly p))
   (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
-    (th_holds (>0_Real (poly_term p')))))))));)
+    (th_holds (>0_poly p'))))))));
 
 (declare lra_mul_c_>=
   (! p poly
   (! p' poly
   (! c mpq
-  (! f (th_holds (>=0_Real (poly_term p)))
+  (! f (th_holds (>=0_poly p))
   (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
-    (th_holds (>=0_Real (poly_term p')))))))));)
+    (th_holds (>=0_poly p'))))))))
 
 (declare lra_mul_c_distinct
   (! p poly
   (! p' poly
   (! c mpq
-  (! f (th_holds (distinct0_Real (poly_term p)))
+  (! f (th_holds (distinct0_poly p))
   (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
-    (th_holds (distinct0_Real (poly_term p')))))))));)
+    (th_holds (distinct0_poly p'))))))))
 
 ;; adding equations
 
@@ -198,64 +220,73 @@
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (=0_Real (poly_term p1)))
-  (! f2 (th_holds (=0_Real (poly_term p2)))
+  (! f1 (th_holds (=0_poly p1))
+  (! f2 (th_holds (=0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (=0_Real (poly_term p3))))))))))
+    (th_holds (=0_poly p3)))))))))
 
 (declare lra_add_>_>
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (>0_Real (poly_term p1)))
-  (! f2 (th_holds (>0_Real (poly_term p2)))
+  (! f1 (th_holds (>0_poly p1))
+  (! f2 (th_holds (>0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (>0_Real (poly_term p3))))))))))
+    (th_holds (>0_poly p3)))))))))
 
 (declare lra_add_>=_>=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (>=0_Real (poly_term p1)))
-  (! f2 (th_holds (>=0_Real (poly_term p2)))
+  (! f1 (th_holds (>=0_poly p1))
+  (! f2 (th_holds (>=0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (>=0_Real (poly_term p3))))))))))
+    (th_holds (>=0_poly p3)))))))))
 
 (declare lra_add_=_>
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (=0_Real (poly_term p1)))
-  (! f2 (th_holds (>0_Real (poly_term p2)))
+  (! f1 (th_holds (=0_poly p1))
+  (! f2 (th_holds (>0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (>0_Real (poly_term p3))))))))))
+    (th_holds (>0_poly p3)))))))))
 
 (declare lra_add_=_>=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (=0_Real (poly_term p1)))
-  (! f2 (th_holds (>=0_Real (poly_term p2)))
+  (! f1 (th_holds (=0_poly p1))
+  (! f2 (th_holds (>=0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (>=0_Real (poly_term p3))))))))))
+    (th_holds (>=0_poly p3)))))))))
 
 (declare lra_add_>_>=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (>0_Real (poly_term p1)))
-  (! f2 (th_holds (>=0_Real (poly_term p2)))
+  (! f1 (th_holds (>0_poly p1))
+  (! f2 (th_holds (>=0_poly p2))
+  (! i (^ (poly_add p1 p2) p3)
+    (th_holds (>0_poly p3)))))))))
+
+(declare lra_add_>=_>
+  (! p1 poly
+  (! p2 poly
+  (! p3 poly
+  (! f1 (th_holds (>=0_poly p1))
+  (! f2 (th_holds (>0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (>0_Real (poly_term p3))))))))))
+    (th_holds (>0_poly p3)))))))))
 
 (declare lra_add_=_distinct
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (=0_Real (poly_term p1)))
-  (! f2 (th_holds (distinct0_Real (poly_term p2)))
+  (! f1 (th_holds (=0_poly p1))
+  (! f2 (th_holds (distinct0_poly p2))
   (! i (^ (poly_add p1 p2) p3)
-    (th_holds (distinct0_Real (poly_term p3))))))))))
+    (th_holds (distinct0_poly p3)))))))))
 
 ;; substracting equations
 
@@ -263,37 +294,37 @@
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (=0_Real (poly_term p1)))
-  (! f2 (th_holds (=0_Real (poly_term p2)))
+  (! f1 (th_holds (=0_poly p1))
+  (! f2 (th_holds (=0_poly p2))
   (! i (^ (poly_sub p1 p2) p3)
-    (th_holds (=0_Real (poly_term p3)))))))))))
+    (th_holds (=0_poly p3)))))))))
 
 (declare lra_sub_>_=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (>0_Real (poly_term p1)))
-  (! f2 (th_holds (=0_Real (poly_term p2)))
+  (! f1 (th_holds (>0_poly p1))
+  (! f2 (th_holds (=0_poly p2))
   (! i (^ (poly_sub p1 p2) p3)
-    (th_holds (>0_Real (poly_term p3))))))))))
+    (th_holds (>0_poly p3)))))))))
 
 (declare lra_sub_>=_=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (>=0_Real (poly_term p1)))
-  (! f2 (th_holds (=0_Real (poly_term p2)))
+  (! f1 (th_holds (>=0_poly p1))
+  (! f2 (th_holds (=0_poly p2))
   (! i (^ (poly_sub p1 p2) p3)
-    (th_holds (>=0_Real (poly_term p3))))))))))
+    (th_holds (>=0_poly p3)))))))))
 
 (declare lra_sub_distinct_=
   (! p1 poly
   (! p2 poly
   (! p3 poly
-  (! f1 (th_holds (distinct0_Real (poly_term p1)))
-  (! f2 (th_holds (=0_Real (poly_term p2)))
+  (! f1 (th_holds (distinct0_poly p1))
+  (! f2 (th_holds (=0_poly p2))
   (! i (^ (poly_sub p1 p2) p3)
-    (th_holds (distinct0_Real (poly_term p3)))))))))))
+    (th_holds (distinct0_poly p3)))))))))
 
  ;; converting between terms and polynomials
 
@@ -357,6 +388,14 @@
   (! a (^ (poly_mul_c py x) pz)
     (poly_norm (*_Real y (a_real x)) pz))))))))
 
+(declare poly_flip_not_>=
+  (! p poly
+  (! p_negged poly
+  (! pf_formula (th_holds (not (>=0_poly p)))
+  (! sc (^ (poly_neg p) p_negged)
+     (th_holds (>0_poly p_negged)))))))
+
+
 ;; for polynomializing other terms, in particular ite's
 
 (declare term_atom (! v var_real (! t (term Real) type)))
@@ -395,54 +434,10 @@
   (! u (th_holds (not ft))
     (th_holds (not fp)))))))
 
-; form equivalence between term formula and polynomial formula
-
-(declare poly_norm_=
-  (! x (term Real)
-  (! y (term Real)
-  (! p poly
-  (! h (th_holds (= Real x y))
-  (! n (poly_norm (-_Real x y) p)
-  (! u (! pn (th_holds (=0_Real (poly_term p)))
-         (holds cln))
-    (holds cln))))))))
-
-(declare poly_norm_>
+(declare poly_formula_norm_>=
   (! x (term Real)
   (! y (term Real)
   (! p poly
-  (! h (th_holds (>_Real x y))
-  (! n (poly_norm (-_Real x y) p)
-  (! u (! pn (th_holds (>0_Real (poly_term p)))
-         (holds cln))
-    (holds cln))))))))
-
-(declare poly_norm_<
-  (! x (term Real)
-  (! y (term Real)
-  (! p poly
-  (! h (th_holds (<_Real x y))
   (! n (poly_norm (-_Real y x) p)
-  (! u (! pn (th_holds (>0_Real (poly_term p)))
-         (holds cln))
-    (holds cln))))))))
-
-(declare poly_norm_>=
-  (! x (term Real)
-  (! y (term Real)
-  (! p poly
-  (! h (th_holds (>=_Real x y))
-  (! n (poly_norm (-_Real x y) p)
-  (! u (! pn (th_holds (>=0_Real (poly_term p)))
-         (holds cln))
-    (holds cln))))))))
+     (poly_formula_norm (>=_Real y x) (>=0_poly p)))))))
 
-(declare poly_norm_<=
-  (! x (term Real)
-  (! y (term Real)
-  (! p poly
-  (! h (th_holds (<=_Real x y))
-  (! n (poly_norm (-_Real y x) p)
-  (! u (! pn (th_holds (>=0_Real (poly_term p)))
-         (holds cln))
-    (holds cln))))))))
diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf
index 687ff988b..fb3ca828c 100644
--- a/proofs/signatures/th_lra_test.plf
+++ b/proofs/signatures/th_lra_test.plf
@@ -1,4 +1,10 @@
 ; Depends On: th_lra.plf
+;; Proof (from predicates on linear polynomials) that the following imply bottom
+;
+; -x - 1/2 y + 2 >= 0
+;  x +     y - 8 >= 0
+;  x -     y + 0 >= 0
+;
 (check
   ; Variables
   (% x var_real
@@ -11,22 +17,151 @@
   (@ 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)
+  (% pf_nonneg_1 (th_holds (>=0_poly p1))
+  (% pf_nonneg_2 (th_holds (>=0_poly p2))
+  (% pf_nonneg_3 (th_holds (>=0_poly p3))
+     (:
+       (holds cln)
+       (lra_contra_>=
+         _
          (lra_add_>=_>= _ _ _
-           (lra_mul_c_>= _ _ 3/1 pf_nonneg_2)
+           (lra_mul_c_>= _ _ 4/1 pf_nonneg_1)
            (lra_add_>=_>= _ _ _
-             (lra_mul_c_>= _ _ 1/1 pf_nonneg_3)
-             (lra_axiom_>= 0/1)))))
+             (lra_mul_c_>= _ _ 3/1 pf_nonneg_2)
+             (lra_add_>=_>= _ _ _
+               (lra_mul_c_>= _ _ 1/1 pf_nonneg_3)
+               (lra_axiom_>= 0/1))))))
   )))))
   ))))
   ))
 )
 
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+; -x - 1/2 y >= 2
+;  x +     y >= 8
+;  x -     y >= 0
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x var_real
+  (% y var_real
+  ; real predicates
+  (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (*_Real (a_real (~ 1/2)) (a_var_real y))) (a_real (~ 2/1)))
+  (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real 1/1) (a_var_real y))) (a_real 8/1))
+  (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real (~ 1/1)) (a_var_real y))) (a_real 0/1))
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+
+
+  ; Normalization
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_+ _ _ _ _ _
+            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
+            (pn_mul_c_L _ _ _ (~ 1/2) (pn_var y)))
+          (pn_const (~ 2/1))))
+  (@ n2 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_+ _ _ _ _ _
+            (pn_mul_c_L _ _ _ 1/1 (pn_var x))
+            (pn_mul_c_L _ _ _ 1/1 (pn_var y)))
+          (pn_const 8/1)))
+  (@ n3 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_+ _ _ _ _ _
+            (pn_mul_c_L _ _ _ 1/1 (pn_var x))
+            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var y)))
+          (pn_const 0/1)))
+  ; proof of linear polynomial predicates
+  (@ pf_n1 (poly_form _ _ n1 pf_f1)
+  (@ pf_n2 (poly_form _ _ n2 pf_f2)
+  (@ pf_n3 (poly_form _ _ n3 pf_f3)
+
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (holds cln)
+      (lra_contra_>= _
+       (lra_add_>=_>= _ _ _
+         (lra_mul_c_>= _ _ 4/1 pf_n1)
+         (lra_add_>=_>= _ _ _
+           (lra_mul_c_>= _ _ 3/1 pf_n2)
+           (lra_add_>=_>= _ _ _
+             (lra_mul_c_>= _ _ 1/1 pf_n3)
+             (lra_axiom_>= 0/1))))))
+  )))
+  )))
+  )))
+  )))
+  ))
+)
+
+;; Term proof, 2 (>=), one (not >=)
+;; Proof (from predicates on real terms) that the following imply bottom
+;
+;        -x +     y >=  2
+;         x +     y >=  2
+;     not[        y >= -2] => [y < -2] => [-y > 2]
+;
+(check
+  ; Declarations
+  ; Variables
+  (% x var_real
+  (% y var_real
+  ; real predicates
+  (@ f1 (>=_Real
+          (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (a_var_real y))
+          (a_real 2/1))
+  (@ f2 (>=_Real
+          (+_Real (a_var_real x) (a_var_real y))
+          (a_real 2/1))
+  (@ f3 (not (>=_Real (a_var_real y) (a_real (~ 2/1))))
 
+  ; Normalization
+  ; proof of real predicates
+  (% pf_f1 (th_holds f1)
+  (% pf_f2 (th_holds f2)
+  (% pf_f3 (th_holds f3)
+  ; real term -> linear polynomial normalization witnesses
+  (@ n1 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_+ _ _ _ _ _
+            (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x))
+            (pn_var y))
+          (pn_const 2/1)))
+  (@ n2 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_+ _ _ _ _ _
+            (pn_var x)
+            (pn_var y))
+          (pn_const 2/1)))
+  (@ n3 (poly_formula_norm_>=  _ _ _
+        (pn_- _ _ _ _ _
+          (pn_var y)
+          (pn_const (~ 2/1))))
+  ; proof of linear polynomial predicates
+  (@ pf_n1 (poly_form _ _ n1 pf_f1)
+  (@ pf_n2 (poly_form _ _ n2 pf_f2)
+  (@ pf_n3 (poly_flip_not_>= _ _ (poly_form_not _ _ n3 pf_f3))
 
+  ; derivation of a contradiction using farkas coefficients
+    (:
+      (holds cln)
+      (lra_contra_> _
+       (lra_add_>=_> _ _ _
+         (lra_mul_c_>= _ _ 1/1 pf_n1)
+         (lra_add_>=_> _ _ _
+           (lra_mul_c_>= _ _ 1/1 pf_n2)
+           (lra_add_>_>= _ _ _
+             (lra_mul_c_> _ _ 2/1 pf_n3)
+             (lra_axiom_>= 0/1))))))
+  )))
+  )))
+  )))
+  )))
+  ))
+)