diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-01-21 15:05:52 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-21 15:05:52 -0800 |
commit | 3de5e8df6a6adcd0efe51db9d9eadad284ad3a64 (patch) | |
tree | 0405a366343689b610e988841a924c29b9fd6841 /proofs/signatures/th_lira.plf | |
parent | d99fc9153d8260cfc6dd2aa7d2a2ea96ab5c4925 (diff) |
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
Diffstat (limited to 'proofs/signatures/th_lira.plf')
-rw-r--r-- | proofs/signatures/th_lira.plf | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index 4be9c6015..ab0da8735 100644 --- 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))))) |