diff options
Diffstat (limited to 'proofs/signatures/th_lira.plf')
-rw-r--r-- | proofs/signatures/th_lira.plf | 61 |
1 files changed, 60 insertions, 1 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index ab0da8735..145980b24 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -386,7 +386,7 @@ (tt (bounded_aff (aff_mul_c a1 c) b)) (ff (fail formula)))) -; Does an affine function actuall satisfy a bound, for all inputs? +; Does an affine function actuall satisfy a bound, for some input? (program bound_respected ((b bound) (a aff)) bool (match a ((aff_cons c combo) @@ -396,3 +396,62 @@ (bound_pos (mpq_ispos c)) (bound_non_neg (mp_ifneg c ff tt)))) (default tt))))) + +;; =================================== ;; +;; Axioms for bounded affine functions ;; +;; =================================== ;; + +; Always true (used as a initial value when summing many bounds together) +(declare bounded_aff_ax_0_>=_0 + (th_holds (bounded_aff (aff_cons 0/1 lc_null) bound_non_neg))) + +; Contradiction axiom: an affine function that does not respect its bounds +(declare bounded_aff_contra + (! a aff ; Omit + (! b bound ; Omit + (! pf (th_holds (bounded_aff a b)) + (! sc (^ (bound_respected b a) ff) + (th_holds false)))))) + +; Rule for summing two affine bounds to get a third +(declare bounded_aff_add + (! a1 aff ; Omit + (! a2 aff ; Omit + (! b bound ; Omit + (! b2 bound ; Omit + (! ba_sum formula ; Omit + (! pf_a1 (th_holds (bounded_aff a1 b)) + (! pf_a2 (th_holds (bounded_aff a2 b2)) + (! sc (^ (bounded_aff_add a1 b a2 b2) ba_sum) + (th_holds ba_sum)))))))))) + +; Rule for scaling an affine bound +(declare bounded_aff_mul_c + (! a aff ; Omit + (! b bound ; Omit + (! ba formula ; Omit + (! c mpq + (! pf_a (th_holds (bounded_aff a b)) + (! sc (^ (bounded_aff_mul_c a b c) ba) + (th_holds ba)))))))) + + +; [y >= x] implies that the aff. function y - x is >= 0 +(declare aff_>=_from_term + (! y (term Real) ; Omit + (! x (term Real) ; Omit + (! p aff ; Omit + (! pf_affine (is_aff (-_Real y x) p) + (! pf_term_bound (th_holds (>=_Real y x)) + (th_holds (bounded_aff p bound_non_neg)))))))) + +; not [y >= x] implies that the aff. function -(y - x) is > 0 +(declare aff_>_from_term + (! y (term Real) ; Omit + (! x (term Real) ; Omit + (! p aff ; Omit + (! p_n aff ; Omit + (! pf_affine (is_aff (-_Real y x) p) + (! pf_term_bound (th_holds (not (>=_Real y x))) + (! sc_neg (^ (aff_neg p) p_n) + (th_holds (bounded_aff p_n bound_pos)))))))))) |