diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /proofs | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/signatures/Makefile.am | 2 | ||||
-rwxr-xr-x | proofs/signatures/example-arrays.plf | 18 | ||||
-rwxr-xr-x | proofs/signatures/th_arrays.plf | 34 | ||||
-rwxr-xr-x | proofs/signatures/th_base.plf | 26 | ||||
-rw-r--r-- | proofs/signatures/th_int.plf | 25 | ||||
-rw-r--r-- | proofs/signatures/th_lra.plf | 451 | ||||
-rw-r--r-- | proofs/signatures/th_real.plf | 25 |
7 files changed, 558 insertions, 23 deletions
diff --git a/proofs/signatures/Makefile.am b/proofs/signatures/Makefile.am index 82d8c2caa..2b6d16cfd 100644 --- a/proofs/signatures/Makefile.am +++ b/proofs/signatures/Makefile.am @@ -3,7 +3,7 @@ # add support for more theories, just list them here in the same order # you would to the LFSC proof-checker binary. # -CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf +CORE_PLFS = sat.plf smt.plf th_base.plf th_arrays.plf th_bv.plf th_bv_bitblast.plf th_real.plf th_int.plf noinst_LTLIBRARIES = libsignatures.la diff --git a/proofs/signatures/example-arrays.plf b/proofs/signatures/example-arrays.plf index 600fc11c9..c454a6dfe 100755 --- a/proofs/signatures/example-arrays.plf +++ b/proofs/signatures/example-arrays.plf @@ -9,7 +9,7 @@ ; input : ; ~L1 -; (extenstionality) lemma : +; (extenstionality) lemma : ; L1 or ~L2 ; theory conflicts : @@ -26,13 +26,13 @@ (check (% I sort (% E sort -(% a (term (array I E)) +(% a (term (Array I E)) (% i (term I) ; (1) -------------------- input formula ----------------------------------- -(% A1 (th_holds (not (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) +(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) @@ -57,7 +57,7 @@ ; (4) -------------------- map theory literals to boolean variables ; --- maps all theory literals involved in proof to boolean literals -(decl_atom (= (array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 +(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 (decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 (decl_atom (= I i k) (\ v3 (\ a3 @@ -73,7 +73,7 @@ ; use read over write rule "row" (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) - + ))))) (\ CT1 ; CT1 is the clause ( v2 V v3 ) @@ -83,9 +83,9 @@ (clausify_false ; use read over write rule "row1" - (contra _ (symm _ _ _ - (trans _ _ _ _ - (symm _ _ _ (cong _ _ _ _ _ _ + (contra _ (symm _ _ _ + (trans _ _ _ _ + (symm _ _ _ (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) l3)) (trans _ _ _ _ @@ -93,7 +93,7 @@ (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) ))) l2) - + ))))) (\ CT2 ; CT2 is the clause ( v2 V ~v3 ) diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf index 8334f51de..5ed3d2f6f 100755 --- a/proofs/signatures/th_arrays.plf +++ b/proofs/signatures/th_arrays.plf @@ -7,44 +7,56 @@ ; sorts -(declare array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element +(declare Array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element ; functions (declare write (! s1 sort (! s2 sort - (term (arrow (array s1 s2) + (term (arrow (Array s1 s2) (arrow s1 - (arrow s2 (array s1 s2)))))))) + (arrow s2 (Array s1 s2)))))))) (declare read (! s1 sort (! s2 sort - (term (arrow (array s1 s2) + (term (arrow (Array s1 s2) (arrow s1 s2)))))) ; inference rules + +; read( a[i] = b, i ) == b (declare row1 (! s1 sort (! s2 sort - (! t1 (term (array s1 s2)) + (! t1 (term (Array s1 s2)) (! t2 (term s1) (! t3 (term s2) - (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) - t3)))))))) - + (th_holds (= _ + (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3)))))))) (declare row (! s1 sort (! s2 sort (! t2 (term s1) (! t3 (term s1) - (! t1 (term (array s1 s2)) + (! t1 (term (Array s1 s2)) (! t4 (term s2) (! u (th_holds (not (= _ t2 t3))) (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) (apply _ _ (apply _ _ (read s1 s2) t1) t3))))))))))) +(declare negativerow (! s1 sort + (! s2 sort + (! t2 (term s1) + (! t3 (term s1) + (! t1 (term (Array s1 s2)) + (! t4 (term s2) + (! u (th_holds (not (= _ + (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) + (apply _ _ (apply _ _ (read s1 s2) t1) t3)))) + (th_holds (= _ t2 t3)))))))))) + (declare ext (! s1 sort (! s2 sort - (! t1 (term (array s1 s2)) - (! t2 (term (array s1 s2)) + (! t1 (term (Array s1 s2)) + (! t2 (term (Array s1 s2)) (! u1 (! k (term s1) (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) (holds cln))) diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf index 9dd950b5b..d6b283752 100755 --- a/proofs/signatures/th_base.plf +++ b/proofs/signatures/th_base.plf @@ -18,8 +18,8 @@ (! t1 (term (arrow s1 s2)) (! t2 (term s1) (term s2)))))) - - + + ; inference rules : (declare trust (th_holds false)) ; temporary @@ -44,6 +44,28 @@ (! u (th_holds (= _ y z)) (th_holds (= _ x z))))))))) +(declare negsymm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (not (= _ x y))) + (th_holds (not (= _ y x)))))))) + +(declare negtrans1 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (not (= _ x y))) + (! u (th_holds (= _ y z)) + (th_holds (not (= _ x z)))))))))) + +(declare negtrans2 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (not (= _ y z))) + (th_holds (not (= _ x z)))))))))) + (declare cong (! s1 sort (! s2 sort (! a1 (term (arrow s1 s2)) diff --git a/proofs/signatures/th_int.plf b/proofs/signatures/th_int.plf new file mode 100644 index 000000000..9a0a2d63c --- /dev/null +++ b/proofs/signatures/th_int.plf @@ -0,0 +1,25 @@ +(declare Int sort) + +(define arithpred_Int (! x (term Int) + (! y (term Int) + formula))) + +(declare >_Int arithpred_Int) +(declare >=_Int arithpred_Int) +(declare <_Int arithpred_Int) +(declare <=_Int arithpred_Int) + +(define arithterm_Int (! x (term Int) + (! y (term Int) + (term Int)))) + +(declare +_Int arithterm_Int) +(declare -_Int arithterm_Int) +(declare *_Int arithterm_Int) ; is * ok to use? +(declare /_Int arithterm_Int) ; is / ok to use? + +; a constant term +(declare a_int (! x mpz (term Int))) + +; unary negation +(declare u-_Int (! t (term Int) (term Int))) 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))))))))
+
+
diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf new file mode 100644 index 000000000..3478e23ef --- /dev/null +++ b/proofs/signatures/th_real.plf @@ -0,0 +1,25 @@ +(declare Real sort) + +(define arithpred_Real (! x (term Real) + (! y (term Real) + formula))) + +(declare >_Real arithpred_Real) +(declare >=_Real arithpred_Real) +(declare <_Real arithpred_Real) +(declare <=_Real arithpred_Real) + +(define arithterm_Real (! x (term Real) + (! y (term Real) + (term Real)))) + +(declare +_Real arithterm_Real) +(declare -_Real arithterm_Real) +(declare *_Real arithterm_Real) ; is * ok to use? +(declare /_Real arithterm_Real) ; is / ok to use? + +; a constant term +(declare a_real (! x mpq (term Real))) + +; unary negation +(declare u-_Real (! t (term Real) (term Real))) |