LFSC signature for linear arithmetic (#7445)

2 files changed, 156 insertions, 0 deletions

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))))))))