From e2b5b08d732b007caae6059616bb341a58d143e3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Oct 2021 10:31:29 -0500 Subject: [PATCH] LFSC signature for linear arithmetic (#7445) --- proofs/lfsc/signatures/arith_programs.plf | 80 +++++++++++++++++++++++ proofs/lfsc/signatures/arith_rules.plf | 76 +++++++++++++++++++++ 2 files changed, 156 insertions(+) create mode 100644 proofs/lfsc/signatures/arith_programs.plf create mode 100644 proofs/lfsc/signatures/arith_rules.plf diff --git a/proofs/lfsc/signatures/arith_programs.plf b/proofs/lfsc/signatures/arith_programs.plf new file mode 100644 index 000000000..219bbe326 --- /dev/null +++ b/proofs/lfsc/signatures/arith_programs.plf @@ -0,0 +1,80 @@ +; depends: theory_def.plf + +; get the relation symbol from f, for example for (a.>= t1 t2), return a.>= +(program sc_arith_get_rel ((f term)) term + (match f ((apply f1 f2) (match f1 ((apply f11 f12) f11))))) + +; get the left hand side of a relation, for example for (a.>= t1 t2), return t1 +(program sc_arith_get_lhs ((f term)) term + (match f ((apply f1 f2) (match f1 ((apply f11 f12) f12))))) + +; get the right hand side of a relation, for example for (a.>= t1 t2), return t2 +(program sc_arith_get_rhs ((f term)) term + (match f ((apply f1 f2) (match f1 ((apply f11 f12) f2))))) + +; Get the relation entailed by summing two arithmetic relations. +; This side condition handles lower bounds only. +; Note that = summed with = is <= to match internal calculus, although it could +; be =. +(program sc_arith_sum_rels ((r1 term) (r2 term)) term + (match r1 + (f_a.< f_a.<) + (default + (match r2 + (f_a.< f_a.<) + (f_a.<= f_a.<=) + (f_= f_a.<=))))) + +; Get the inverse relation for r, i.e. flips left and right hand side. +(program sc_arith_rel_inv ((r term)) term + (match r + (f_= f_=) + (f_a.< f_a.>) + (f_a.> f_a.<) + (f_a.<= f_a.>=) + (f_a.>= f_a.<=))) + +; Get the negated relation for r, i.e. is equivalent to negating the relation. +(program sc_arith_rel_neg ((r term)) term + (match r + (f_a.< f_a.>=) + (f_a.> f_a.<=) + (f_a.<= f_a.>) + (f_a.>= f_a.<))) + +; A helper for computing the conclusion relation used in the rule +; PfRule::ARITH_TRICHOTOMY. For relations r1 and r2, this returns the +; third possibility for the relationship between two arithmetic terms. +(program sc_arith_rel_trichotomy ((r1 term) (r2 term)) term + (match r1 + (f_= (match r2 (f_a.> f_a.<) (f_a.< f_a.>))) + (f_a.> (match r2 (f_= f_a.<) (f_a.< f_=))) + (f_a.< (match r2 (f_= f_a.>) (f_a.> f_=))))) + +; Add term for t1 and t2. Assumes t2 in n-ary form. +(program sc_arith_add_nary ((t1 term) (t2 term)) term + (a.+ t1 t2)) + +; Multiply term for t1 and t2, where t2 is not in n-ary form. +(program sc_arith_mult ((t1 term) (t2 term)) term + (a.* t1 (a.* t2 (int 1)))) + +; Returns (> t 0). +(program sc_arith_>_zero ((t term)) term + (a.> t (int 0))) + +; Returns (< t 0). +(program sc_arith_<_zero ((t term)) term + (a.< t (int 0))) + +; Get relation for the negation of arithmetic literal f. +(program sc_arith_get_rel_neg ((f term)) term + (match f + ((apply f1 f2) + (ifequal f1 f_not + (sc_arith_get_rel f2) + (sc_arith_rel_neg (sc_arith_get_rel f)))))) + +; Get the atom for possibly negated arithmetic literal f. +(program sc_arith_get_atom ((f term)) term + (match f ((apply f1 f2) (ifequal f1 f_not f2 f)))) diff --git a/proofs/lfsc/signatures/arith_rules.plf b/proofs/lfsc/signatures/arith_rules.plf new file mode 100644 index 000000000..850c2b5e6 --- /dev/null +++ b/proofs/lfsc/signatures/arith_rules.plf @@ -0,0 +1,76 @@ +; depends: arith_programs.plf + +; Computes the conclusion of the PfRule::ARITH_SUM_UB rule. +; Note that f2 is a a.+ application in n-ary form. +(program sc_arith_sum_ub ((f1 term) (f2 term)) term + (let r1 (sc_arith_get_rel f1) + (let lhs1 (sc_arith_get_lhs f1) + (let rhs1 (sc_arith_get_rhs f1) + (let r2 (sc_arith_get_rel f2) + (let lhs2 (sc_arith_get_lhs f2) + (let rhs2 (sc_arith_get_rhs f2) + (apply (apply (sc_arith_sum_rels r1 r2) (sc_arith_add_nary lhs1 lhs2)) (sc_arith_add_nary rhs1 rhs2))))))))) + +(declare arith_sum_ub + (! f1 term + (! f2 term + (! res term + (! p (holds f1) + (! p (holds f2) + (! r (^ (sc_arith_sum_ub f1 f2) res) + (holds res)))))))) + +; Computes the conclusion of the PfRule::ARITH_MULT_POS rule. +(program sc_arith_mult_pos ((m term) (f term)) term + (let r (sc_arith_get_rel f) + (let lhs (sc_arith_get_lhs f) + (let rhs (sc_arith_get_rhs f) + (=> (and (sc_arith_>_zero m) (and f true)) + (apply (apply r (sc_arith_mult m lhs)) (sc_arith_mult m rhs))))))) + +(declare arith_mult_pos + (! res term + (! m term + (! f term + (! r (^ (sc_arith_mult_pos m f) res) + (holds res)))))) + +; Computes the conclusion of the PfRule::ARITH_MULT_NEG rule. +(program sc_arith_mult_neg ((m term) (f term)) term + (let r (sc_arith_get_rel f) + (let lhs (sc_arith_get_lhs f) + (let rhs (sc_arith_get_rhs f) + (=> (and (sc_arith_<_zero m) (and f true)) + (apply (apply (sc_arith_rel_inv r) (sc_arith_mult m lhs)) (sc_arith_mult m rhs))))))) + +(declare arith_mult_neg + (! res term + (! m term + (! f term + (! r (^ (sc_arith_mult_neg m f) res) + (holds res)))))) + +; Computes the conclusion of the PfRule::ARITH_TRICHOTOMY rule. +(program sc_arith_trichotomy ((f1 term) (f2 term)) term + (let r1 (sc_arith_get_rel_neg f1) + (let a1 (sc_arith_get_atom f1) + (let lhs1 (sc_arith_get_lhs a1) + (let rhs1 (sc_arith_get_rhs a1) + (let r2 (sc_arith_get_rel_neg f2) + (let a2 (sc_arith_get_atom f1) + (let lhs2 (sc_arith_get_lhs a2) + (let rhs2 (sc_arith_get_rhs a2) + (ifequal lhs1 lhs2 + (ifequal rhs1 rhs2 + (apply (apply (sc_arith_rel_trichotomy r1 r2) lhs1) rhs1) + (fail term)) + (fail term))))))))))) + +(declare arith_trichotomy + (! res term + (! f1 term + (! f2 term + (! p (holds f1) + (! p (holds f2) + (! r (^ (sc_arith_trichotomy f1 f2) res) + (holds res)))))))) -- 2.30.2