diff options
Diffstat (limited to 'proofs/lfsc')
| -rw-r--r-- | proofs/lfsc/signatures/arith_programs.plf | 80 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/arith_rules.plf | 76 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/boolean_programs.plf | 74 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/boolean_rules.plf | 52 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/cnf_rules.plf | 28 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/equality_rules.plf | 64 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/quantifiers_rules.plf | 51 | ||||
| -rw-r--r-- | proofs/lfsc/signatures/util_defs.plf | 5 |
8 files changed, 430 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)))))))) diff --git a/proofs/lfsc/signatures/boolean_programs.plf b/proofs/lfsc/signatures/boolean_programs.plf new file mode 100644 index 000000000..eecc71a98 --- /dev/null +++ b/proofs/lfsc/signatures/boolean_programs.plf @@ -0,0 +1,74 @@ +; depends: nary_programs.plf theory_def.plf + +; This side condition takes two terms c1 and c2. Via nary_intro, +; we consider theses terms to be either non-unit clauses if they are +; or-applications, or otherwise consider them to be unit clauses if they are +; not. For example, if c1 is (= x y), then (nary_intro f_or c1 false) returns +; (or (= x y) false) +; which we use to compute the concatenation described in following. After +; converting to n-ary form for both c1 and c2, we then concatenate the result +; of removing the first occurrence of l from c1, and the first occurrence of the negation of l from v2 +; when pol is tt, or vice versa when pol is ff. Since the resolution may result +; in a singleton list, we run nary_elim as a last step, which ensures that +; we conclude e.g. L and not (or L false), as done in PfRule::RESOLUTION. +; This side condition may fail if c1 or c2 does not contain l with the required +; polarity. +(program sc_resolution ((c1 term) (c2 term) (pol flag) (l term)) term + (nary_elim f_or + (nary_concat f_or + (nary_rm_first_or_self f_or (nary_intro f_or c1 false) (ifequal pol tt l (apply f_not l)) false) + (nary_rm_first_or_self f_or (nary_intro f_or c2 false) (ifequal pol tt (apply f_not l) l) false) + false) + false) +) + +; Helper for sc_not_and below, which pushes a not below an application of and. +; In terms of SMT-LIB, this side condition converts: +; (and F1 ... Fn) to (or (not F1) ... (not Fn)) +; This side condition may fail if t is not an and-application in n-ary form. +(program sc_not_and_rec ((t term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f_and t1) + (apply (apply f_or (apply f_not t12)) (sc_not_and_rec t2)))) ; otherwise not in n-ary form + (true false)) ; note we must flip true to false +) + +; Pushes a not below an application of and. In terms of SMT-LIB syntax, this +; side condition converts: +; (not (and F1 ... Fn)) to (or (not F1) ... (not Fn)) +(program sc_not_and ((t term)) term + (nary_elim f_or (sc_not_and_rec t) false) +) + +; Helper for sc_not_and_rev, which is the inverse of sc_not_and. +; (or (not F1) ... (not Fn)) to (and F1 ... Fn) +; This side condition may fail if t is not an or-application in n-ary form. +(program sc_not_and_rev_rec ((t term)) term + (match t + ((apply t1 t2) + (let t12 (getarg f_or t1) + (let t122 (getarg f_not t12) + (apply (apply f_and t122) (sc_not_and_rev_rec t2))))) ; otherwise not in n-ary form + (false true)) ; note we must flip true to false +) + +; Pulls not from a list of children of an or-application. In terms of SMT-LIB +; syntax, this side condition converts: +; (or (not F1) ... (not Fn)) to (and F1 ... Fn) +(program sc_not_and_rev ((t term)) term + (nary_elim f_and (sc_not_and_rev_rec t) true) +) + +; Process scope side condition. This side condition is used for constructing the +; proven formula for the two cases of PfRule::SCOPE. In particular, it takes: +; - a term t which is expected to be an or-application +; - a term c which is expected to be a suffix of t. +; It may conclude an implication, or the negation of t, based on whether c +; is false, according to the definition of PfRule::SCOPE. +; This side condition may fail if t and c do not have the above properties. +(program sc_process_scope ((t term) (c term)) term + (let premise (sc_not_and_rev (nary_truncate f_or t c false)) + (match c + (false (not premise)) + (default (=> premise c))))) diff --git a/proofs/lfsc/signatures/boolean_rules.plf b/proofs/lfsc/signatures/boolean_rules.plf new file mode 100644 index 000000000..af16af1f9 --- /dev/null +++ b/proofs/lfsc/signatures/boolean_rules.plf @@ -0,0 +1,52 @@ +; depends: boolean_programs.plf theory_def.plf + +(declare resolution (! c1 term (! c2 term (! c term (! p1 (holds c1) (! p2 (holds c2) (! pol flag (! l term (! r (^ (sc_resolution c1 c2 pol l) c) (holds c)))))))))) +(declare reordering (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (nary_is_subset f_or c1 c2) tt) (holds c2)))))) +(declare factoring (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (nary_drop_dups f_or c1 false) c2) (holds c2)))))) + +(declare split (! f term (holds (or f (or (not f) false))))) + +(declare eq_resolve (! f term (! g term (! p1 (holds f) (! p2 (holds (= f g)) (holds g)))))) + +(declare modus_ponens (! f term (! g term (! p1 (holds f) (! p2 (holds (=> f g)) (holds g)))))) + +(declare not_not_elim (! f term (! p (holds (not (not f))) (holds f)))) + +(declare contra (! f term (! p1 (holds f) (! p2 (holds (not f)) (holds false))))) + +(declare and_elim (! f1 term (! f2 term (! n mpz (! p (holds f1) (! r (^ (nary_extract f_and f1 n) f2) (holds f2))))))) + +; And introduction. Since PfRule::AND_INTRO is n-ary, we require n applications +; of the following two rules. The proof (AND_INTRO P1 ... Pn) is translated to +; the LFSC proof: (and_intro2* _ _ P{n-1} (and_intro1 _ Pn)). +(declare and_intro1 (! f term (! p (holds f) (holds (and f true))))) +(declare and_intro2 (! f1 term (! f2 term (! p1 (holds f1) (! p2 (holds f2) (holds (and f1 f2))))))) + +(declare not_or_elim (! f1 term (! f2 term (! n mpz (! p (holds (not f1)) (! r (^ (nary_extract f_or f1 n) f2) (holds (not f2)))))))) + +(declare implies_elim (! f1 term (! f2 term (! p1 (holds (=> f1 f2)) (holds (or (not f1) (or f2 false))))))) +(declare not_implies_elim1 (! f1 term (! f2 term (! p1 (holds (not (=> f1 f2))) (holds f1))))) +(declare not_implies_elim2 (! f1 term (! f2 term (! p1 (holds (not (=> f1 f2))) (holds (not f2)))))) + +(declare equiv_elim1 (! f1 term (! f2 term (! p1 (holds (= f1 f2)) (holds (or (not f1) (or f2 false))))))) +(declare equiv_elim2 (! f1 term (! f2 term (! p1 (holds (= f1 f2)) (holds (or f1 (or (not f2) false))))))) +(declare not_equiv_elim1 (! f1 term (! f2 term (! p1 (holds (not (= f1 f2))) (holds (or f1 (or f2 false))))))) +(declare not_equiv_elim2 (! f1 term (! f2 term (! p1 (holds (not (= f1 f2))) (holds (or (not f1) (or (not f2) false))))))) + +(declare xor_elim1 (! f1 term (! f2 term (! p1 (holds (xor f1 f2)) (holds (or f1 (or f2 false))))))) +(declare xor_elim2 (! f1 term (! f2 term (! p1 (holds (xor f1 f2)) (holds (or (not f1) (or (not f2) false))))))) +(declare not_xor_elim1 (! f1 term (! f2 term (! p1 (holds (not (xor f1 f2))) (holds (or f1 (or (not f2) false))))))) +(declare not_xor_elim2 (! f1 term (! f2 term (! p1 (holds (not (xor f1 f2))) (holds (or (not f1) (or f2 false))))))) + +(declare ite_elim1 (! c term (! f1 term (! f2 term (! p1 (holds (ite c f1 f2)) (holds (or (not c) (or f1 false)))))))) +(declare ite_elim2 (! c term (! f1 term (! f2 term (! p1 (holds (ite c f1 f2)) (holds (or c (or f2 false)))))))) +(declare not_ite_elim1 (! c term (! f1 term (! f2 term (! p1 (holds (not (ite c f1 f2))) (holds (or (not c) (or (not f1) false)))))))) +(declare not_ite_elim2 (! c term (! f1 term (! f2 term (! p1 (holds (not (ite c f1 f2))) (holds (or c (or (not f2) false)))))))) + +(declare not_and (! c1 term (! c2 term (! p1 (holds (not c1)) (! r (^ (sc_not_and c1) c2) (holds c2)))))) + +(declare not_and_rev (! c1 term (! c2 term (! p1 (holds c1) (! r (^ (sc_not_and_rev c1) c2) (holds (not c2))))))) + +; Process scope, which is used to translate PfRule::SCOPE. It runs the side +; condition sc_process_scope on f to generate an equivalent formula g. +(declare process_scope (! f term (! g term (! c term (! p1 (holds f) (! r (^ (sc_process_scope f c) g) (holds g)))))) diff --git a/proofs/lfsc/signatures/cnf_rules.plf b/proofs/lfsc/signatures/cnf_rules.plf new file mode 100644 index 000000000..c593a0a95 --- /dev/null +++ b/proofs/lfsc/signatures/cnf_rules.plf @@ -0,0 +1,28 @@ +; depends: boolean_programs.plf theory_def.plf + +(declare cnf_and_pos (! f1 term (! f2 term (! n mpz (! r (^ (nary_extract f_and f2 n) f1) (holds (or (not f2) (or f1 false)))))))) +; Note that we do not add a null terminator, since f1 is null terminated. +(declare cnf_and_neg (! f1 term (! f2 term (! r (^ (sc_not_and_rec f2) f1) (holds (or f2 f1)))))) +(declare cnf_or_pos (! f term (holds (or (not f) f)))) +(declare cnf_or_neg (! f1 term (! f2 term (! n mpz (! r (^ (nary_extract f_or f2 n) f1) (holds (or f2 (or (not f1) false)))))))) + +(declare cnf_implies_pos (! f1 term (! f2 term (holds (or (not (=> f1 f2)) (or (not f1) (or f2 false))))))) +(declare cnf_implies_neg1 (! f1 term (! f2 term (holds (or (=> f1 f2) (or f1 false)))))) +(declare cnf_implies_neg2 (! f1 term (! f2 term (holds (or (=> f1 f2) (or (not f2) false)))))) + +(declare cnf_equiv_pos1 (! f1 term (! f2 term (holds (or (not (= f1 f2)) (or (not f1) (or f2 false))))))) +(declare cnf_equiv_pos2 (! f1 term (! f2 term (holds (or (not (= f1 f2)) (or f1 (or (not f2) false))))))) +(declare cnf_equiv_neg1 (! f1 term (! f2 term (holds (or (= f1 f2) (or f1 (or f2 false))))))) +(declare cnf_equiv_neg2 (! f1 term (! f2 term (holds (or (= f1 f2) (or (not f1) (or (not f2) false))))))) + +(declare cnf_xor_pos1 (! f1 term (! f2 term (holds (or (not (xor f1 f2)) (or f1 (or f2 false))))))) +(declare cnf_xor_pos2 (! f1 term (! f2 term (holds (or (not (xor f1 f2)) (or (not f1) (or (not f2) false))))))) +(declare cnf_xor_neg1 (! f1 term (! f2 term (holds (or (xor f1 f2) (or (not f1) (or f2 false))))))) +(declare cnf_xor_neg2 (! f1 term (! f2 term (holds (or (xor f1 f2) (or f1 (or (not f2) false))))))) + +(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or (not c) (or f1 false))))))) +(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or c (or f2 false))))))) +(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not (ite c f1 f2)) (or f1 (or f2 false))))))) +(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not c) (or (not f1) false))))))) +(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or c (or (not f2) false))))))) +(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or (ite c f1 f2) (or (not f1) (or (not f2) false))))))) diff --git a/proofs/lfsc/signatures/equality_rules.plf b/proofs/lfsc/signatures/equality_rules.plf new file mode 100644 index 000000000..3144294d5 --- /dev/null +++ b/proofs/lfsc/signatures/equality_rules.plf @@ -0,0 +1,64 @@ +; depends: theory_def.plf + +; The following encodes the proof rules for the theory of equality in the +; internal proof calculus of cvc5 (see src/proof/proof_rule.h). Rules from +; that calculus are referenced by PfRule::NAME, where NAME is the name of the +; identifier in the PfRule enumeration (see src/proof/proof_rule.h). For this +; and other theory signature definitions, unless otherwise stated, we use a +; naming convention in which the corresponding LFSC rule is the same as the +; PfRule, but converted to lower case. For example, `refl` corresponds to the +; LFSC encoding of PfRule::REFL. We provide documentation when the proof rule +; differs from the original PfRule. + +(declare refl (! t term (holds (= t t)))) + +; symm is a special case of PfRule::SYMM that is applied only to equalties. +(declare symm (! s term + (! t term + (! u (holds (= s t)) + (holds (= t s)))))) + +; neg_symm is a special case of PfRule::SYMM that is applied only to disequalties, +; i.e. negated equalities. +(declare neg_symm (! s term + (! t term + (! u (holds (not (= s t))) + (holds (not (= t s))))))) + +(declare trans (! t1 term + (! t2 term + (! t3 term + (! u1 (holds (= t1 t2)) + (! u2 (holds (= t2 t3)) + (holds (= t1 t3)))))))) + +; In LFSC, congruence is applied to higher-order apply only. Thus, when +; applying congruence to n-ary symbols, we curry the applications of congruence +; e.g. consider (cong _ _ _ _ (cong _ _ _ _ P1 P2) P3) +; where P1 proves (= f g), P2 proves (= a b), P3 proves (= c d). The above +; proof proves (= (apply (apply f a) c) (apply (apply f b) d)), where assuming +; f is binary, is the LFSC encoding of the SMT-LIB equality (= (f a c) (f b d)). +(declare cong (! a1 term + (! b1 term + (! a2 term + (! b2 term + (! u1 (holds (= a1 b1)) + (! u2 (holds (= a2 b2)) + (holds (= (apply a1 a2) (apply b1 b2)))))))))) + +(declare true_intro (! f term + (! u (holds f) + (holds (= f true))))) + +(declare true_elim (! f term + (! u (holds (= f true)) + (holds f)))) + +(declare false_intro (! f term + (! u (holds (not f)) + (holds (= f false))))) + +(declare false_elim (! f term + (! u (holds (= f false)) + (holds (not f))))) + diff --git a/proofs/lfsc/signatures/quantifiers_rules.plf b/proofs/lfsc/signatures/quantifiers_rules.plf new file mode 100644 index 000000000..7bdd6539c --- /dev/null +++ b/proofs/lfsc/signatures/quantifiers_rules.plf @@ -0,0 +1,51 @@ +; depends: theory_def.plf util_defs.plf + +; Substitute, which returns the result of replacing all occurrences of the +; bound variable whose identifier is v with the term s. It is the responsibility +; of the caller to ensure that all occurrences of (bvar v u) in t are such that +; u is the sort of s. Otherwise, this will return a term that is not well +; sorted. +(program sc_substitute ((t term) (v mpz) (s term)) term + (match t + ((bvar v1 u1) (mpz_ifequal v v1 s t)) + ((apply t1 t2) (apply (sc_substitute t1 v s) (sc_substitute t2 v s))) + (default t) + )) + +; Concludes the instantiation for the term of the outermost quantifier in the +; rule PfRule::INSTANTIATE. We do not enforce type checking of term s +; currently, which should be of sort u. +(declare instantiate (! body term + (! v mpz + (! u sort + (! s term + (! bodyi term + (! p (holds (forall v u body)) + (! r (^ (sc_substitute body v s) bodyi) + (holds bodyi))))))))) + +; Concludes the skolemization for the term of the outermost quantifier in the +; rule PfRule::SKOLEMIZE. +(declare skolemize (! body term + (! v mpz + (! s sort + (! bodyi term + (! p (holds (exists v s body)) + (! r (^ (sc_substitute body v (skolem (witness v s body))) bodyi) + (holds bodyi)))))))) + +; We do not enforce type checking of s currently, which should be of +; sort u. +(declare exists_intro (! bodyi term + (! v mpz + (! u sort + (! s term + (! body term + (! p (holds bodyi) + (! r (^ (sc_substitute body v s) bodyi) + (holds (exists v u body))))))))) + +(declare skolem_intro (! u term + (! t term + (! r (^ (sc_mk_skolem t) u) + (holds (= u t)))))) diff --git a/proofs/lfsc/signatures/util_defs.plf b/proofs/lfsc/signatures/util_defs.plf index 5639cc54e..8d1793666 100644 --- a/proofs/lfsc/signatures/util_defs.plf +++ b/proofs/lfsc/signatures/util_defs.plf @@ -25,6 +25,11 @@ (declare bvn bitvec) (declare bvc (! b bit (! v bitvec bitvec))) +; Returns term t if v1 = v2, and term s otherwise. +(program mpz_ifequal ((v1 mpz) (v2 mpz) (t term) (s term)) term + (mp_ifzero (mp_add (mp_neg v1) v2) t s) +) + ;; ---- Side conditions ; Get the argument from an f-application t, fail if t is not an f-application. |