1 files changed, 145 insertions, 10 deletions
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))))))
+  )))
+  )))
+  )))
+  )))
+  ))
+)