//
// We give a semi-formal description of each proof rule in proof_kinds files.
//
// Formulas and terms in all children, arguments, and conclusions are assumed to
// be in *witness* form (see expr/proof_skolem_cache.h).

//======================== Assume and Scope

// ======== Assumption (a leaf)
// Children: none
// Arguments: (F)
// --------------
// Conclusion: F
//
// This rule has special status, in that an application of assume is an
// open leaf in a proof that is not (yet) justified. An assume leaf is
// analogous to a free variable in a term, where we say "F is a free
// assumption in proof P" if it contains an application of F that is not
// bound by SCOPE (see below).
proofrule ASSUME 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker

// ======== Assumption (a leaf)
// Children: (P:F)
// Arguments: (F1, ..., Fn)
// --------------
// Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
//
// This rule has a dual purpose with ASSUME. It is a way to close
// assumptions in a proof. We require that F1 ... Fn are free assumptions in
// P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
// are bound by this application. For example, the proof node:
//   (SCOPE (ASSUME F) :args F)
// has the conclusion (=> F F) and has no free assumptions. More generally, a
// proof with no free assumptions always concludes a valid formula.
proofrule SCOPE 1 1: ::CVC4::theory::builtin::BuiltinProofRuleChecker

//======================== Node operations

// ======== Substitution
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (t, id?)
// ---------------------------------------------------------------
// Conclusion: (= t t.substitute(xn,tn). ... .substitute(x1,t1))
// Notice that the orientation of the premises matters.
proofrule SUBS 1: 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker

// ======== Rewrite
// Children: none
// Arguments: (t, id?)
// ----------------------------------------
// Conclusion: (= t Rewriter::rewrite(t))
proofrule REWRITE 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker

// NOTE: these technically rely on TRANS/TRUE_ELIM, which are UF

// ======== Substitution + Rewriting equality introduction
//
// In this rule, we provide a term t and conclude that it is equal to its
// rewritten form under a (proven) substitution.
//
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (t, id?)
// ---------------------------------------------------------------
// Conclusion: (= t t')
// where
//   t' is toWitness(Rewriter{id}(toSkolem(t).substitute(x1...xn,t1...tn)))
//   toSkolem(...) converts terms from witness form to Skolem form,
//   toWitness(...) converts terms from Skolem form to witness form.
//
// Notice that:
//   toSkolem(t') = Rewriter{id}(toSkolem(t).substitute(x1...xn,t1...tn))
// In other words, from the point of view of Skolem forms, this rule transforms
// t to t' by standard substitution + rewriting.
//
// The argument id is optional and specifies the identifier of the rewriter to
// be used (see theory/builtin/proof_checker.h).
macro MACRO_SR_EQ_INTRO 0: 1:2 ::CVC4::theory::builtin::BuiltinProofRuleChecker {
  (TRANS 
    (SUBS <children> t) 
    (REWRITE <t.substitute(x1,t1). ... .substitute(xn,tn)>))
}

// ======== Substitution + Rewriting predicate introduction
//
// In this rule, we provide a formula F and conclude it, under the condition
// that it rewrites to true under a proven substitution.
//
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (F, id?)
// ---------------------------------------------------------------
// Conclusion: F
// where 
//   Rewriter{id}(F.substitute(x1...xn,t1...tn)) == true
//
// Notice that we apply rewriting on the witness form of F, meaning that this
// rule may conclude an F whose Skolem form is justified by the definition of
// its (fresh) Skolem variables. Furthermore, notice that the rewriting and
// substitution is applied only within the side condition, meaning the rewritten
// form of the witness form of F does not escape this rule.
macro MACRO_SR_PRED_INTRO 0: 1:2 ::CVC4::theory::builtin::BuiltinProofRuleChecker {
  (TRUE_ELIM 
    (MACRO_SR_EQ_INTRO <children> F))
}

// ======== Substitution + Rewriting predicate elimination
//
// In this rule, if we have proven a formula F, then we may conclude its
// rewritten form under a proven substitution.
//
// Children: (P1:F, P2:(= x1 t1), ..., P_{n+1}:(= xn tn))
// Arguments: (id?)
// ----------------------------------------
// Conclusion: F'
// where
//   F' is toWitness(Rewriter{id}(toSkolem(F).substitute(x1...xn,t1...tn))).
//
// We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
macro MACRO_SR_PRED_ELIM 1: 0:1 {
  (TRUE_ELIM 
    (TRANS 
      (SYMM (MACRO_SR_EQ_INTRO <children>[1:] F)) 
      (TRUE_INTRO <children>[0])))
}

// ======== Substitution + Rewriting predicate transform
//
// In this rule, if we have proven a formula F, then we may provide a formula
// G and conclude it if F and G are equivalent after rewriting under a proven
// substitution.
//
// Children: (P1:F, P2:(= x1 t1), ..., P_{n+1}:(= xn tn))
// Arguments: (G, id?)
// ----------------------------------------
// Conclusion: G
// where 
//   Rewriter{id}(F.substitute(x1...xn,t1...tn)) ==
//   Rewriter{id}(G.substitute(x1...xn,t1...tn))
//
// Notice that we apply rewriting on the witness form of F and G, similar to
// MACRO_SR_PRED_INTRO.
macro MACRO_SR_PRED_TRANSFORM 1: 1:2 {
  (TRUE_ELIM 
    (TRANS 
      (MACRO_SR_EQ_INTRO <children>[1:] G)
      (SYMM (MACRO_SR_EQ_INTRO <children>[1:] F)) 
      (TRUE_INTRO <children>[0])))
}

// ======== Untrustworthy theory lemma
// Children: none
// Arguments: (F, tid)
// ---------------------------------------------------------------
// Conclusion: F
// where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
// This is a "coarse-grained" rule that is used as a placeholder if a theory
// did not provide a proof for a lemma or conflict.
proofrule THEORY_LEMMA 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker