path: root/proofs/signatures/th_lra.plf

; Depends on th_real.plf, smt.plf, sat.plf

; LRA proofs have the following interface:
;    * Given predicates between real terms
;    * Prove bottom
;
; However, even though the type of the interface does not express this,
; the predicates are **linear bounds**, not arbitrary real bounds. Thus
; LRA proofs have the following structure:
;
;    1. Prove that the input predicates are equivalent to a set of linear
;       bounds.
;    2. Use the linear bounds to prove bottom using farkas coefficients.
;
; Notice that the distinction between linear bounds (associated in the signature
; with the string "poly") and real predicates (which relate "term Real"s to one
; another) matters quite a bit. We have certain kinds of axioms for one, and
; other axioms for the other.

(program mpq_ifpos ((x mpq)) bool
  (mp_ifneg x ff (mp_ifzero x ff tt)))

; a real variable
(declare var_real type)
; a real variable term
(declare a_var_real (! v var_real (term Real)))

;; linear polynomials in the form a_1*x_1 + a_2*x_2 .... + a_n*x_n

(declare lmon type)
(declare lmonn lmon)
(declare lmonc (! c mpq (! v var_real (! l lmon lmon))))

(program lmon_neg ((l lmon)) lmon
  (match l
    (lmonn l)
    ((lmonc c' v' l') (lmonc (mp_neg c') v' (lmon_neg l')))))

(program lmon_add ((l1 lmon) (l2 lmon)) lmon
  (match l1
    (lmonn l2)
    ((lmonc c' v' l')
      (match l2
        (lmonn l1)
        ((lmonc c'' v'' l'')
          (compare v' v''
            (lmonc c' v' (lmon_add l' l2))
            (lmonc c'' v'' (lmon_add l1 l''))))))))

(program lmon_mul_c ((l lmon) (c mpq)) lmon
  (match l
    (lmonn l)
    ((lmonc c' v' l') (lmonc (mp_mul c c') v' (lmon_mul_c l' c)))))

;; linear polynomials in the form (a_1*x_1 + a_2*x_2 .... + a_n*x_n) + c

(declare poly type)
(declare polyc (! c mpq (! l lmon poly)))

(program poly_neg ((p poly)) poly
  (match p
    ((polyc m' p') (polyc (mp_neg m') (lmon_neg p')))))

(program poly_add ((p1 poly) (p2 poly)) poly
  (match p1
    ((polyc c1 l1)
      (match p2
        ((polyc c2 l2) (polyc (mp_add c1 c2) (lmon_add l1 l2)))))))

(program poly_sub ((p1 poly) (p2 poly)) poly
  (poly_add p1 (poly_neg p2)))

(program poly_mul_c ((p poly) (c mpq)) poly
  (match p
    ((polyc c' l') (polyc (mp_mul c' c) (lmon_mul_c l' c)))))

;; code to isolate a variable from a term
;; if (isolate v l) returns (c,l'), this means l = c*v + l', where v is not in FV(t').

(declare isol type)
(declare isolc (! r mpq (! l lmon isol)))

(program isolate_h ((v var_real) (l lmon) (e bool)) isol
  (match l
    (lmonn (isolc 0/1 l))
    ((lmonc c' v' l')
      (ifmarked v'
        (match (isolate_h v l' tt)
          ((isolc ci li) (isolc (mp_add c' ci) li)))
        (match e
          (tt (isolc 0/1 l))
          (ff (match (isolate_h v l' ff)
                ((isolc ci li) (isolc ci (lmonc c' v' li))))))))))

(program isolate ((v var_real) (l lmon)) isol
  (do (markvar v)
  (let i (isolate_h v l ff)
  (do (markvar v) i))))

;; determine if a monomial list is constant

(program is_lmon_zero ((l lmon)) bool
  (match l
    (lmonn tt)
    ((lmonc c v l')
      (match (isolate v l)
        ((isolc ci li)
          (mp_ifzero ci (is_lmon_zero li) ff))))))

;; return the constant that p is equal to.  If p is not constant, fail.

(program is_poly_const ((p poly)) mpq
  (match p
    ((polyc c' l')
      (match (is_lmon_zero l')
        (tt c')
        (ff (fail mpq))))))

;; conversion to use polynomials in term formulas


(declare >=0_poly (! x poly formula))
(declare =0_poly (! x poly formula))
(declare >0_poly (! x poly formula))
(declare distinct0_poly (! x poly formula))

;; create new equality out of inequality

(declare lra_>=_>=_to_=
  (! p1 poly
  (! p2 poly
  (! f1 (th_holds (>=0_poly p1))
  (! f2 (th_holds (>=0_poly p2))
  (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
    (th_holds (=0_poly p2))))))))

;; axioms

(declare lra_axiom_=
   (th_holds (=0_poly (polyc 0/1 lmonn))))

(declare lra_axiom_>
  (! c mpq
  (! i (^ (mpq_ifpos c) tt)
    (th_holds (>0_poly (polyc c lmonn))))))

(declare lra_axiom_>=
  (! c mpq
  (! i (^ (mp_ifneg c tt ff) ff)
    (th_holds (>=0_poly (polyc c lmonn))))))

(declare lra_axiom_distinct
  (! c mpq
  (! i (^ (mp_ifzero c tt ff) ff)
    (th_holds (distinct0_poly (polyc c lmonn))))))

;; contradiction rules

(declare lra_contra_=
  (! p poly
  (! f (th_holds (=0_poly p))
  (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
    (holds cln)))))

(declare lra_contra_>
  (! p poly
  (! f (th_holds (>0_poly p))
  (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
    (holds cln)))))

(declare lra_contra_>=
  (! p poly
  (! f (th_holds (>=0_poly p))
  (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
    (holds cln)))))

(declare lra_contra_distinct
  (! p poly
  (! f (th_holds (distinct0_poly p))
  (! i2 (^ (mp_ifzero (is_poly_const p) tt ff) tt)
    (holds cln)))))

;; muliplication by a constant

(declare lra_mul_c_=
  (! p poly
  (! p' poly
  (! c mpq
  (! f (th_holds (=0_poly p))
  (! i (^ (poly_mul_c p c) p')
    (th_holds (=0_poly p'))))))))

(declare lra_mul_c_>
  (! p poly
  (! p' poly
  (! c mpq
  (! f (th_holds (>0_poly p))
  (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
    (th_holds (>0_poly p'))))))));

(declare lra_mul_c_>=
  (! p poly
  (! p' poly
  (! c mpq
  (! f (th_holds (>=0_poly p))
  (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
    (th_holds (>=0_poly p'))))))))

(declare lra_mul_c_distinct
  (! p poly
  (! p' poly
  (! c mpq
  (! f (th_holds (distinct0_poly p))
  (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
    (th_holds (distinct0_poly p'))))))))

;; adding equations

(declare lra_add_=_=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (=0_poly p1))
  (! f2 (th_holds (=0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (=0_poly p3)))))))))

(declare lra_add_>_>
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>0_poly p1))
  (! f2 (th_holds (>0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>0_poly p3)))))))))

(declare lra_add_>=_>=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>=0_poly p1))
  (! f2 (th_holds (>=0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>=0_poly p3)))))))))

(declare lra_add_=_>
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (=0_poly p1))
  (! f2 (th_holds (>0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>0_poly p3)))))))))

(declare lra_add_=_>=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (=0_poly p1))
  (! f2 (th_holds (>=0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>=0_poly p3)))))))))

(declare lra_add_>_>=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>0_poly p1))
  (! f2 (th_holds (>=0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>0_poly p3)))))))))

(declare lra_add_>=_>
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>=0_poly p1))
  (! f2 (th_holds (>0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (>0_poly p3)))))))))

(declare lra_add_=_distinct
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (=0_poly p1))
  (! f2 (th_holds (distinct0_poly p2))
  (! i (^ (poly_add p1 p2) p3)
    (th_holds (distinct0_poly p3)))))))))

;; substracting equations

(declare lra_sub_=_=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (=0_poly p1))
  (! f2 (th_holds (=0_poly p2))
  (! i (^ (poly_sub p1 p2) p3)
    (th_holds (=0_poly p3)))))))))

(declare lra_sub_>_=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>0_poly p1))
  (! f2 (th_holds (=0_poly p2))
  (! i (^ (poly_sub p1 p2) p3)
    (th_holds (>0_poly p3)))))))))

(declare lra_sub_>=_=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (>=0_poly p1))
  (! f2 (th_holds (=0_poly p2))
  (! i (^ (poly_sub p1 p2) p3)
    (th_holds (>=0_poly p3)))))))))

(declare lra_sub_distinct_=
  (! p1 poly
  (! p2 poly
  (! p3 poly
  (! f1 (th_holds (distinct0_poly p1))
  (! f2 (th_holds (=0_poly p2))
  (! i (^ (poly_sub p1 p2) p3)
    (th_holds (distinct0_poly p3)))))))))

 ;; converting between terms and polynomials

(declare poly_norm (! t (term Real) (! p poly type)))

(declare pn_let
  (! t (term Real)
  (! p poly
  (! pn (poly_norm t p)

  (! u (! pnt (poly_norm t p)
         (holds cln))
    (holds cln))))))

(declare pn_const
  (! x mpq
    (poly_norm (a_real x) (polyc x lmonn))))

(declare pn_var
  (! v var_real
    (poly_norm (a_var_real v) (polyc 0/1 (lmonc 1/1 v lmonn)))))


(declare pn_+
  (! x (term Real)
  (! px poly
  (! y (term Real)
  (! py poly
  (! pz poly
  (! pnx (poly_norm x px)
  (! pny (poly_norm y py)
  (! a (^ (poly_add px py) pz)
    (poly_norm (+_Real x y) pz))))))))))

(declare pn_-
  (! x (term Real)
  (! px poly
  (! y (term Real)
  (! py poly
  (! pz poly
  (! pnx (poly_norm x px)
  (! pny (poly_norm y py)
  (! a (^ (poly_sub px py) pz)
    (poly_norm (-_Real x y) pz))))))))))

(declare pn_mul_c_L
  (! y (term Real)
  (! py poly
  (! pz poly
  (! x mpq
  (! pny (poly_norm y py)
  (! a (^ (poly_mul_c py x) pz)
    (poly_norm (*_Real (a_real x) y) pz))))))))

(declare pn_mul_c_R
  (! y (term Real)
  (! py poly
  (! pz poly
  (! x mpq
  (! pny (poly_norm y py)
  (! a (^ (poly_mul_c py x) pz)
    (poly_norm (*_Real y (a_real x)) pz))))))))

(declare poly_flip_not_>=
  (! p poly
  (! p_negged poly
  (! pf_formula (th_holds (not (>=0_poly p)))
  (! sc (^ (poly_neg p) p_negged)
     (th_holds (>0_poly p_negged)))))))


;; for polynomializing other terms, in particular ite's

(declare term_atom (! v var_real (! t (term Real) type)))

(declare decl_term_atom
  (! t (term Real)
  (! u (! v var_real
       (! a (term_atom v t)
         (holds cln)))
    (holds cln))))

(declare pn_var_atom
  (! v var_real
  (! t (term Real)
  (! a (term_atom v t)
    (poly_norm t (polyc 0/1 (lmonc 1/1 v lmonn)))))))


;; conversion between term formulas and polynomial formulas

(declare poly_formula_norm (! ft formula (! fp formula type)))

; convert between term formulas and polynomial formulas

(declare poly_form
  (! ft formula
  (! fp formula
  (! p (poly_formula_norm ft fp)
  (! u (th_holds ft)
    (th_holds fp))))))

(declare poly_form_not
  (! ft formula
  (! fp formula
  (! p (poly_formula_norm ft fp)
  (! u (th_holds (not ft))
    (th_holds (not fp)))))))

(declare poly_formula_norm_>=
  (! x (term Real)
  (! y (term Real)
  (! p poly
  (! n (poly_norm (-_Real y x) p)
     (poly_formula_norm (>=_Real y x) (>=0_poly p)))))))