Add proof reconstruction for ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ (

cvc5#11323) Handles nearly all cases of this rule, although 4/126 are instances of a more complex rewrite ("datatype tester expansion") which need separate treatment. --------- Co-authored-by: Abdalrhman Mohamed <[email protected]>
ajreynol · Nov 9, 2024 · a7021cd · a7021cd
1 parent 44b2405
commit a7021cd
Show file tree

Hide file tree

Showing 9 changed files with 285 additions and 13 deletions.
diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
@@ -2571,6 +2571,21 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(MACRO_QUANT_VAR_ELIM_EQ),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Quantifiers -- Macro variable elimination equality**
+   *
+   * .. math::
+   *  (\forall x.\> x \neq t \vee F) = F \{ x \mapsto t \}
+   *
+   * or alternatively
+   *
+   * .. math::
+   *  (\forall x.\> x \neq t) = \bot
+   *
+   * \endverbatim
+   */
+  EVALUE(QUANT_VAR_ELIM_EQ),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Quantifiers -- Macro variable elimination inequality**

diff --git a/proofs/eo/cpc/rules/Quantifiers.eo b/proofs/eo/cpc/rules/Quantifiers.eo
@@ -209,3 +209,44 @@
   :requires ((($is_quant_miniscope_fv x F G) true))
   :conclusion (= (forall x F) G)
 )
+
+;;;;; ProofRewriteRule::QUANT_VAR_ELIM_EQ
+
+; define: $mk_quant_var_elim_eq_subs
+; - x T: The variable we are eliminating
+; - t T: The term x was equated to
+; - F Bool: The (remaining) body of the quantified formula from which we are eliminating x.
+; return: >
+;    The result of eliminating x from F. This method does not evaluate if t contains x.
+(define $mk_quant_var_elim_eq_subs ((T Type :implicit) (x T) (t T) (F Bool))
+  (eo::requires ($contains_subterm t x) false ($substitute x t F)))
+
+; program: $mk_quant_var_elim_eq
+; args:
+; - x T: The variable we are eliminating
+; - F Bool: The body of the quantified formula in question.
+; return: >
+;    The result of eliminating x from F. This method does not evaluate if this
+;    is not a variable elimination, i.e. if F does not begin with a disequality
+;    between x and a term not containing x.
+(program $mk_quant_var_elim_eq ((T Type) (x T) (t Type) (F Bool :list))
+  (T Bool) Bool
+  (
+  (($mk_quant_var_elim_eq x (not (= x t)))        ($mk_quant_var_elim_eq_subs x t false))
+  (($mk_quant_var_elim_eq x (or (not (= x t)) F)) ($mk_quant_var_elim_eq_subs x t ($singleton_elim F)))
+  )
+)
+
+; rule: quant-var-elim-eq
+; implements: QUANT_VAR_ELIM_EQ
+; args:
+; - eq Bool: The equality whose left hand side is a quantified formula.
+; requires: >
+;   The right hand side of the equality is the result of a legal variable
+;   elimination.
+; conclusion: The given equality.
+(declare-rule quant-var-elim-eq ((T Type) (x T) (F Bool) (G Bool))
+  :args ((= (forall (@list x) F) G))
+  :requires ((($mk_quant_var_elim_eq x F) G))
+  :conclusion (= (forall (@list x) F) G)
+)
diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp
@@ -250,6 +250,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
       return "macro-quant-var-elim-eq";
     case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ:
       return "macro-quant-var-elim-ineq";
+    case ProofRewriteRule::QUANT_VAR_ELIM_EQ: return "quant-var-elim-eq";
     case ProofRewriteRule::DT_INST: return "dt-inst";
     case ProofRewriteRule::DT_COLLAPSE_SELECTOR: return "dt-collapse-selector";
     case ProofRewriteRule::DT_COLLAPSE_TESTER: return "dt-collapse-tester";

diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp
@@ -260,6 +260,7 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n)
     case ProofRewriteRule::QUANT_UNUSED_VARS:
     case ProofRewriteRule::ARRAYS_SELECT_CONST:
     case ProofRewriteRule::QUANT_MINISCOPE_FV:
+    case ProofRewriteRule::QUANT_VAR_ELIM_EQ:
     case ProofRewriteRule::RE_LOOP_ELIM:
     case ProofRewriteRule::SETS_IS_EMPTY_EVAL:
     case ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR:

diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp
@@ -28,6 +28,7 @@
 #include "theory/arith/arith_proof_utilities.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 #include "theory/strings/strings_entail.h"
@@ -199,6 +200,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(
         handledMacro = true;
       }
       break;
+    case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ:
+      if (ensureProofMacroQuantVarElimEq(cdp, eq))
+      {
+        handledMacro = true;
+      }
+      break;
     default: break;
   }
   if (handledMacro)
@@ -626,6 +633,151 @@ bool BasicRewriteRCons::ensureProofMacroQuantPartitionConnectedFv(
   return true;
 }
 
+bool BasicRewriteRCons::ensureProofMacroQuantVarElimEq(CDProof* cdp,
+                                                       const Node& eq)
+{
+  Node q = eq[0];
+  Assert(q.getKind() == Kind::FORALL);
+  std::vector<Node> args(q[0].begin(), q[0].end());
+  std::vector<Node> vars;
+  std::vector<Node> subs;
+  std::vector<Node> lits;
+  theory::quantifiers::QuantifiersRewriter qrew(
+      nodeManager(), d_env.getRewriter(), options());
+  if (!qrew.getVarElim(q[1], args, vars, subs, lits))
+  {
+    return false;
+  }
+  if (args.size() != q[0].getNumChildren() - 1)
+  {
+    // a rare case of MACRO_QUANT_VAR_ELIM_EQ does "datatype tester expansion"
+    // e.g. forall x. is-cons(x) => P(x) ----> forall yz. P(cons(y,z))
+    // This is not handled currently.
+    return false;
+  }
+  Assert(vars.size() == 1);
+  Trace("brc-macro") << "Ensure quant var elim eq: " << eq << std::endl;
+  Trace("brc-macro") << "Eliminate " << vars << " -> " << subs << " from "
+                     << lits << std::endl;
+  // merge prenex in reverse to handle the other irrelevant variables first
+  NodeManager* nm = nodeManager();
+  Node body1;
+  Node body2;
+  if (eq[1].getKind() == Kind::FORALL)
+  {
+    body1 = nm->mkNode(
+        Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, vars[0]), q[1]);
+    std::vector<Node> transEq;
+    Node unmergeQ = nm->mkNode(Kind::FORALL, eq[1][0], body1);
+    Node mergeQ;
+    Node q0v = q[0];
+    if (vars[0] != q0v[q0v.getNumChildren() - 1])
+    {
+      // use reordering if the eliminated variable is not the last one
+      std::vector<Node> mvars(eq[1][0].begin(), eq[1][0].end());
+      mvars.push_back(vars[0]);
+      mergeQ = nm->mkNode(
+          Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, mvars), q[1]);
+      Node eqq = q.eqNode(mergeQ);
+      cdp->addStep(eqq, ProofRule::QUANT_VAR_REORDERING, {}, {eqq});
+      transEq.push_back(eqq);
+    }
+    else
+    {
+      mergeQ = q;
+    }
+    Node eqq2s = unmergeQ.eqNode(mergeQ);
+    cdp->addTheoryRewriteStep(eqq2s, ProofRewriteRule::QUANT_MERGE_PRENEX);
+    Node eqq2 = mergeQ.eqNode(unmergeQ);
+    cdp->addStep(eqq2, ProofRule::SYMM, {eqq2s}, {});
+    transEq.push_back(eqq2);
+    body2 = eq[1][1];
+    std::vector<Node> cargs;
+    ProofRule cr = expr::getCongRule(unmergeQ, cargs);
+    Node beq = body1.eqNode(body2);
+    Node eqq3 = unmergeQ.eqNode(eq[1]);
+    cdp->addStep(eqq3, cr, {beq}, cargs);
+    transEq.push_back(eqq3);
+    cdp->addStep(eq, ProofRule::TRANS, transEq, {});
+  }
+  else
+  {
+    body1 = eq[0];
+    body2 = eq[1];
+  }
+  // we now have proven forall Y1 x Y2. F = forall Y1 Y2. F *sigma is a
+  // consequence of forall x. F = F * sigma, now prove the latter equality.
+  Trace("brc-macro") << "Remains to prove: " << body1 << " == " << body2
+                     << std::endl;
+  Assert(body1.getKind() == Kind::FORALL);
+  Node eqLit = vars[0].eqNode(subs[0]).notNode();
+  Node lit = lits[0].negate();
+  // add a copy of the equality literal and prove it is redundant with ACI_NORM
+  std::vector<Node> disj;
+  disj.push_back(lit);
+  if (body1[1].getKind() == Kind::OR)
+  {
+    disj.insert(disj.end(), body1[1].begin(), body1[1].end());
+  }
+  else
+  {
+    disj.push_back(body1[1]);
+  }
+  Node body1r = nm->mkOr(disj);
+  disj[0] = eqLit;
+  Node body1re = nm->mkOr(disj);
+  std::vector<Node> transEqBody;
+  Node eqBody = body1[1].eqNode(body1r);
+  cdp->addStep(eqBody, ProofRule::ACI_NORM, {}, {eqBody});
+  transEqBody.push_back(eqBody);
+  if (eqLit != lit)
+  {
+    std::vector<Node> cprems;
+    for (size_t i = 0, nchild = body1r.getNumChildren(); i < nchild; i++)
+    {
+      Node eql = body1r[i].eqNode(body1re[i]);
+      if (body1r[i] == body1re[i])
+      {
+        cdp->addStep(eql, ProofRule::REFL, {}, {eql[0]});
+      }
+      else
+      {
+        cdp->addTrustedStep(
+            eql, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
+      }
+      cprems.emplace_back(eql);
+    }
+    std::vector<Node> cargs;
+    ProofRule cr = expr::getCongRule(body1r, cargs);
+    Node eqbr = body1r.eqNode(body1re);
+    cdp->addStep(eqbr, cr, cprems, cargs);
+    transEqBody.emplace_back(eqbr);
+    eqBody = body1[1].eqNode(body1re);
+  }
+  if (transEqBody.size() > 1)
+  {
+    cdp->addStep(eqBody, ProofRule::TRANS, transEqBody, {});
+  }
+  // We've now proven that (or (not (= x t)) F) is equivalent to F, we can
+  // forall x. F =
+  // forall x. (or (not (= x t)) F) =
+  // F * { x -> t }
+  // where the latter equality is proven by QUANT_VAR_ELIM_EQ.
+  std::vector<Node> finalTransEq;
+  std::vector<Node> cargs;
+  ProofRule cr = expr::getCongRule(body1, cargs);
+  Node body1p = nm->mkNode(Kind::FORALL, body1[0], body1re);
+  Node eqq = body1.eqNode(body1p);
+  cdp->addStep(eqq, cr, {eqBody}, cargs);
+  finalTransEq.push_back(eqq);
+  eqq = body1p.eqNode(body2);
+  cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::QUANT_VAR_ELIM_EQ);
+  finalTransEq.push_back(eqq);
+  Node beq = body1.eqNode(body2);
+  cdp->addStep(beq, ProofRule::TRANS, finalTransEq, {});
+  return true;
+}
+
 bool BasicRewriteRCons::ensureProofArithPolyNormRel(CDProof* cdp,
                                                     const Node& eq)
 {

diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h
@@ -180,6 +180,16 @@ class BasicRewriteRCons : protected EnvObj
    * @return true if added a closed proof of eq to cdp.
    */
   bool ensureProofMacroQuantPartitionConnectedFv(CDProof* cdp, const Node& eq);
+  /**
+   * Elaborate a rewrite eq that was proven by
+   * ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ.
+   *
+   * @param cdp The proof to add to.
+   * @param eq The rewrite proven by
+   * ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ.
+   * @return true if added a closed proof of eq to cdp.
+   */
+  bool ensureProofMacroQuantVarElimEq(CDProof* cdp, const Node& eq);
   /**
    * @param cdp The proof to add to.
    * @param eq The rewrite that can be proven by ProofRule::ARITH_POLY_NORM_REL.