diff options
| -rw-r--r-- | proofs/signatures/th_lra.plf | 443 | ||||
| -rw-r--r-- | proofs/signatures/th_lra_test.plf | 167 |
2 files changed, 0 insertions, 610 deletions
diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf deleted file mode 100644 index 76e5127c2..000000000 --- a/proofs/signatures/th_lra.plf +++ /dev/null @@ -1,443 +0,0 @@ -; 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))))))) - diff --git a/proofs/signatures/th_lra_test.plf b/proofs/signatures/th_lra_test.plf deleted file mode 100644 index fb3ca828c..000000000 --- a/proofs/signatures/th_lra_test.plf +++ /dev/null @@ -1,167 +0,0 @@ -; Depends On: th_lra.plf -;; Proof (from predicates on linear polynomials) that the following imply bottom -; -; -x - 1/2 y + 2 >= 0 -; x + y - 8 >= 0 -; x - y + 0 >= 0 -; -(check - ; Variables - (% x var_real - (% y var_real - ; linear monomials (combinations) - (@ m1 (lmonc (~ 1/1) x (lmonc (~ 1/2) y lmonn)) - (@ m2 (lmonc 1/1 x (lmonc 1/1 y lmonn)) - (@ m3 (lmonc 1/1 x (lmonc (~ 1/1) y lmonn)) - ; linear polynomials (affine) - (@ p1 (polyc 2/1 m1) - (@ p2 (polyc (~ 8/1) m2) - (@ p3 (polyc 0/1 m3) - (% pf_nonneg_1 (th_holds (>=0_poly p1)) - (% pf_nonneg_2 (th_holds (>=0_poly p2)) - (% pf_nonneg_3 (th_holds (>=0_poly p3)) - (: - (holds cln) - (lra_contra_>= - _ - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 4/1 pf_nonneg_1) - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 3/1 pf_nonneg_2) - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 1/1 pf_nonneg_3) - (lra_axiom_>= 0/1)))))) - ))))) - )))) - )) -) - -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x - 1/2 y >= 2 -; x + y >= 8 -; x - y >= 0 -; -(check - ; Declarations - ; Variables - (% x var_real - (% y var_real - ; real predicates - (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (*_Real (a_real (~ 1/2)) (a_var_real y))) (a_real (~ 2/1))) - (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real 1/1) (a_var_real y))) (a_real 8/1)) - (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (a_var_real x)) (*_Real (a_real (~ 1/1)) (a_var_real y))) (a_real 0/1)) - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - - - ; Normalization - ; real term -> linear polynomial normalization witnesses - (@ n1 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_+ _ _ _ _ _ - (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x)) - (pn_mul_c_L _ _ _ (~ 1/2) (pn_var y))) - (pn_const (~ 2/1)))) - (@ n2 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_+ _ _ _ _ _ - (pn_mul_c_L _ _ _ 1/1 (pn_var x)) - (pn_mul_c_L _ _ _ 1/1 (pn_var y))) - (pn_const 8/1))) - (@ n3 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_+ _ _ _ _ _ - (pn_mul_c_L _ _ _ 1/1 (pn_var x)) - (pn_mul_c_L _ _ _ (~ 1/1) (pn_var y))) - (pn_const 0/1))) - ; proof of linear polynomial predicates - (@ pf_n1 (poly_form _ _ n1 pf_f1) - (@ pf_n2 (poly_form _ _ n2 pf_f2) - (@ pf_n3 (poly_form _ _ n3 pf_f3) - - ; derivation of a contradiction using farkas coefficients - (: - (holds cln) - (lra_contra_>= _ - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 4/1 pf_n1) - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 3/1 pf_n2) - (lra_add_>=_>= _ _ _ - (lra_mul_c_>= _ _ 1/1 pf_n3) - (lra_axiom_>= 0/1)))))) - ))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 (>=), one (not >=) -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x + y >= 2 -; x + y >= 2 -; not[ y >= -2] => [y < -2] => [-y > 2] -; -(check - ; Declarations - ; Variables - (% x var_real - (% y var_real - ; real predicates - (@ f1 (>=_Real - (+_Real (*_Real (a_real (~ 1/1)) (a_var_real x)) (a_var_real y)) - (a_real 2/1)) - (@ f2 (>=_Real - (+_Real (a_var_real x) (a_var_real y)) - (a_real 2/1)) - (@ f3 (not (>=_Real (a_var_real y) (a_real (~ 2/1)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_+ _ _ _ _ _ - (pn_mul_c_L _ _ _ (~ 1/1) (pn_var x)) - (pn_var y)) - (pn_const 2/1))) - (@ n2 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_+ _ _ _ _ _ - (pn_var x) - (pn_var y)) - (pn_const 2/1))) - (@ n3 (poly_formula_norm_>= _ _ _ - (pn_- _ _ _ _ _ - (pn_var y) - (pn_const (~ 2/1)))) - ; proof of linear polynomial predicates - (@ pf_n1 (poly_form _ _ n1 pf_f1) - (@ pf_n2 (poly_form _ _ n2 pf_f2) - (@ pf_n3 (poly_flip_not_>= _ _ (poly_form_not _ _ n3 pf_f3)) - - ; derivation of a contradiction using farkas coefficients - (: - (holds cln) - (lra_contra_> _ - (lra_add_>=_> _ _ _ - (lra_mul_c_>= _ _ 1/1 pf_n1) - (lra_add_>=_> _ _ _ - (lra_mul_c_>= _ _ 1/1 pf_n2) - (lra_add_>_>= _ _ _ - (lra_mul_c_> _ _ 2/1 pf_n3) - (lra_axiom_>= 0/1)))))) - ))) - ))) - ))) - ))) - )) -) |