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))))))))))