Types and side conditions for affine bounds (#3631)

* Types and side conditions for affine bounds

Bounds (being positive, non-negative) actually have an arithmetic.
This PR defines that.

Useful b/c Farkas proofs are basically just sums of bounded affine
functions.

* Address Yoni's comments. Thanks!

* Moved a positivity-test to th_real
* Describe what an affine bound is in better detail

diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf
index 4be9c6015bc25b67bcb3a0523e8d29ac9b6dc821..ab0da87351ae4ba8008553f6521ade70a116213c 100644 (file)
--- a/proofs/signatures/th_lira.plf
+++ b/proofs/signatures/th_lira.plf
@@ -353,3 +353,46 @@
     (! is_affy (is_aff y aff_y)
       (! a (^ (aff_mul_c aff_y x) aff_z)
         (is_aff (*_Real y (a_real x)) aff_z))))))))
+
+;; ========================== ;;
+;; Bounds on Affine Functions ;;
+;; ========================== ;;
+
+; Bounds that an affine function might satisfy
+(declare bound type)
+(declare bound_pos bound)           ; > 0
+(declare bound_non_neg bound)       ; >= 0
+
+; formulas over affine functions
+; the statement that `a` satisfies `b` for all inputs
+(declare bounded_aff (! a aff (! b bound formula)))
+
+; Sum of two bounds (the bound satisfied by the sum of two functions satifying
+; the input bounds)
+(program bound_add ((b bound) (b2 bound)) bound
+  (match b
+    (bound_pos bound_pos)
+    (bound_non_neg b2)))
+
+; The implication of `a1` satisfying `b` and `a2` satisfying `b2`, obtained by
+; summing the inequalities.
+(program bounded_aff_add ((a1 aff) (b bound) (a2 aff) (b2 bound)) formula
+  (bounded_aff (aff_add a1 a2) (bound_add b b2)))
+
+
+; The implication of scaling the inequality of `a1` satisfying `b`.
+(program bounded_aff_mul_c ((a1 aff) (b bound) (c mpq)) formula
+  (match (mpq_ispos c)
+    (tt (bounded_aff (aff_mul_c a1 c) b))
+    (ff (fail formula))))
+
+; Does an affine function actuall satisfy a bound, for all inputs?
+(program bound_respected ((b bound) (a aff)) bool
+  (match a
+    ((aff_cons c combo)
+      (match combo
+        (lc_null
+          (match b
+            (bound_pos (mpq_ispos c))
+            (bound_non_neg (mp_ifneg c ff tt))))
+        (default tt)))))

diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf
index 3529779f3c7ce5153bb637519c565d3dadf9c4e3..112328b63e73fbd97fdfdc839cb84fd48fec0fcf 100644 (file)
--- a/proofs/signatures/th_real.plf
+++ b/proofs/signatures/th_real.plf
@@ -4,7 +4,6 @@
 (define arithpred_Real (! x (term Real)
                        (! y (term Real)
                          formula)))
-
 (declare >_Real arithpred_Real)
 (declare >=_Real arithpred_Real)
 (declare <_Real  arithpred_Real)
@@ -29,3 +28,7 @@
 
 ; unary negation
 (declare u-_Real (! t (term Real) (term Real)))
+
+; Is this rational positive?
+(program mpq_ispos ((x mpq)) bool
+  (mp_ifneg x ff (mp_ifzero x ff tt)))