diff options
Diffstat (limited to 'proofs/signatures/th_lra.plf')
| -rw-r--r-- | proofs/signatures/th_lra.plf | 451 |
1 files changed, 451 insertions, 0 deletions
diff --git a/proofs/signatures/th_lra.plf b/proofs/signatures/th_lra.plf new file mode 100644 index 000000000..88118e8d1 --- /dev/null +++ b/proofs/signatures/th_lra.plf @@ -0,0 +1,451 @@ +; 59 loc in side conditions
+
+(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 poly_term (! p poly (term Real)))
+
+;; create new equality out of inequality
+
+(declare lra_>=_>=_to_=
+ (! p1 poly
+ (! p2 poly
+ (! f1 (th_holds (>=0_Real (poly_term p1)))
+ (! f2 (th_holds (>=0_Real (poly_term p2)))
+ (! i2 (^ (mp_ifzero (is_poly_const (poly_add p1 p2)) tt ff) tt)
+ (th_holds (=0_Real (poly_term p2))))))))))
+
+;; axioms
+
+(declare lra_axiom_=
+ (th_holds (=0_Real (poly_term (polyc 0/1 lmonn)))))
+
+(declare lra_axiom_>
+ (! c mpq
+ (! i (^ (mpq_ifpos c) tt)
+ (th_holds (>0_Real (poly_term (polyc c lmonn)))))))
+
+(declare lra_axiom_>=
+ (! c mpq
+ (! i (^ (mp_ifneg c tt ff) ff)
+ (th_holds (>=0_Real (poly_term (polyc c lmonn)))))))
+
+(declare lra_axiom_distinct
+ (! c mpq
+ (! i (^ (mp_ifzero c tt ff) ff)
+ (th_holds (distinct0_Real (poly_term (polyc c lmonn)))))))
+
+;; contradiction rules
+
+(declare lra_contra_=
+ (! p poly
+ (! f (th_holds (=0_Real (poly_term p)))
+ (! i (^ (mp_ifzero (is_poly_const p) tt ff) ff)
+ (holds cln)))))
+
+(declare lra_contra_>
+ (! p poly
+ (! f (th_holds (>0_Real (poly_term p)))
+ (! i2 (^ (mpq_ifpos (is_poly_const p)) ff)
+ (holds cln)))))
+
+(declare lra_contra_>=
+ (! p poly
+ (! f (th_holds (>=0_Real (poly_term p)))
+ (! i2 (^ (mp_ifneg (is_poly_const p) tt ff) tt)
+ (holds cln)))))
+
+(declare lra_contra_distinct
+ (! p poly
+ (! f (th_holds (distinct0_Real (poly_term 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_Real (poly_term p)))
+ (! i (^ (poly_mul_c p c) p')
+ (th_holds (=0_Real (poly_term p')))))))))
+
+(declare lra_mul_c_>
+ (! p poly
+ (! p' poly
+ (! c mpq
+ (! f (th_holds (>0_Real (poly_term p)))
+ (! i (^ (mp_ifneg c (fail poly) (mp_ifzero c (fail poly) (poly_mul_c p c))) p')
+ (th_holds (>0_Real (poly_term p')))))))));)
+
+(declare lra_mul_c_>=
+ (! p poly
+ (! p' poly
+ (! c mpq
+ (! f (th_holds (>=0_Real (poly_term p)))
+ (! i (^ (mp_ifneg c (fail poly) (poly_mul_c p c)) p')
+ (th_holds (>=0_Real (poly_term p')))))))));)
+
+(declare lra_mul_c_distinct
+ (! p poly
+ (! p' poly
+ (! c mpq
+ (! f (th_holds (distinct0_Real (poly_term p)))
+ (! i (^ (mp_ifzero c (fail poly) (poly_mul_c p c)) p')
+ (th_holds (distinct0_Real (poly_term p')))))))));)
+
+;; adding equations
+
+(declare lra_add_=_=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (=0_Real (poly_term p1)))
+ (! f2 (th_holds (=0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (=0_Real (poly_term p3)))))))))))
+
+(declare lra_add_>_>
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (>0_Real (poly_term p1)))
+ (! f2 (th_holds (>0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (>0_Real (poly_term p3))))))))))
+
+(declare lra_add_>=_>=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (>=0_Real (poly_term p1)))
+ (! f2 (th_holds (>=0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (>=0_Real (poly_term p3))))))))))
+
+(declare lra_add_=_>
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (=0_Real (poly_term p1)))
+ (! f2 (th_holds (>0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (>0_Real (poly_term p3))))))))))
+
+(declare lra_add_=_>=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (=0_Real (poly_term p1)))
+ (! f2 (th_holds (>=0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (>=0_Real (poly_term p3))))))))))
+
+(declare lra_add_>_>=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (>0_Real (poly_term p1)))
+ (! f2 (th_holds (>=0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (>0_Real (poly_term p3))))))))))
+
+(declare lra_add_=_distinct
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (=0_Real (poly_term p1)))
+ (! f2 (th_holds (distinct0_Real (poly_term p2)))
+ (! i (^ (poly_add p1 p2) p3)
+ (th_holds (distinct0_Real (poly_term p3)))))))))))
+
+;; substracting equations
+
+(declare lra_sub_=_=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (=0_Real (poly_term p1)))
+ (! f2 (th_holds (=0_Real (poly_term p2)))
+ (! i (^ (poly_sub p1 p2) p3)
+ (th_holds (=0_Real (poly_term p3)))))))))))
+
+(declare lra_sub_>_=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (>0_Real (poly_term p1)))
+ (! f2 (th_holds (=0_Real (poly_term p2)))
+ (! i (^ (poly_sub p1 p2) p3)
+ (th_holds (>0_Real (poly_term p3))))))))))
+
+(declare lra_sub_>=_=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (>=0_Real (poly_term p1)))
+ (! f2 (th_holds (=0_Real (poly_term p2)))
+ (! i (^ (poly_sub p1 p2) p3)
+ (th_holds (>=0_Real (poly_term p3))))))))))
+
+(declare lra_sub_distinct_=
+ (! p1 poly
+ (! p2 poly
+ (! p3 poly
+ (! f1 (th_holds (distinct0_Real (poly_term p1)))
+ (! f2 (th_holds (=0_Real (poly_term p2)))
+ (! i (^ (poly_sub p1 p2) p3)
+ (th_holds (distinct0_Real (poly_term 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))))))))
+
+;; 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)))))))
+
+; form equivalence between term formula and polynomial formula
+
+(declare poly_norm_=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (= Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_>
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (>_Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (>0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_<
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (<_Real x y))
+ (! n (poly_norm (-_Real y x) p)
+ (! u (! pn (th_holds (>0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_>=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (>=_Real x y))
+ (! n (poly_norm (-_Real x y) p)
+ (! u (! pn (th_holds (>=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+(declare poly_norm_<=
+ (! x (term Real)
+ (! y (term Real)
+ (! p poly
+ (! h (th_holds (<=_Real x y))
+ (! n (poly_norm (-_Real y x) p)
+ (! u (! pn (th_holds (>=0_Real (poly_term p)))
+ (holds cln))
+ (holds cln))))))))
+
+
|