Documentation

Cvc.Proof

Proofs, whichever the layer #

What the two layers' proof APIs share: Proof.View, a proof step taken apart, and the traversals both layers build fold, foldUp and their ForIn instance on. Nothing here mentions a solver or a term; the layers instantiate it — Cvc.Untyped.Solver.Proof and Cvc.Typed.Solver.Proof.

A proof is a graph, not a tree. cvc5 shares a sub-proof between the steps that use it, so a step can be reached along many paths, and a traversal that does not remember what it has visited redoes the work every time — exponentially often in the worst case. Both traversals here visit each distinct step once, telling steps apart by identity.

Taking a step apart #

source
inductive Cvc.Proof.View (P F T : Type) :
Type

One step of a cvc5 proof: its rule as a constructor, its premises and arguments as fields.

The parameters say what the fields are, so that each layer picks its own, and so that a traversal can hand over a step whose premises are something else entirely:

  • P is a premise — a proof, or what a bottom-up traversal computed for one;
  • F is a formula — a sort-erased term, or a typed Term Bool;
  • T is a term of any sort.

The conclusion is not a field: it is the step's own result. Neither is an argument that only restates it, such as REORDERING's target clause or THEORY_REWRITE's equality.

A rule is decoded only when its step has the layout cvc5 documents; anything else is other, holding the step's premises and arguments as cvc5 gives them. So no step is lost, and a layout cvc5 changes degrades to other rather than to a wrong reading. Which rules are decoded can grow, and a rule moving out of other is the change to expect from one version to the next.

Which rules appear at all depends on cvc5's proof-granularity option. Coarse settings leave MACRO_… steps, which are other here; dsl-rewrite breaks rewriting down into dslRewrite, theoryRewrite and the equality rules.

  • assume {P F T : Type} (f : F) : View P F T

    ASSUME, an open leaf: concludes f, unless an enclosing scope discharges it.

  • scope {P F T : Type} (body : P) (discharged : Array F) : View P F T

    SCOPE: discharges discharged from body : F, concluding F₁ ∧ … ∧ Fₙ ⇒ F.

    When F is false, the conclusion is ¬(F₁ ∧ … ∧ Fₙ) instead.

  • evaluate {P F T : Type} (t : T) : View P F T

    EVALUATE: t = v, v being the value t evaluates to.

  • dslRewrite {P F T : Type} (rule : ProofRewriteRule) (premises : Array P) (instantiation : Array T) : View P F T

    DSL_REWRITE: an instance of the RARE rule rule, its variables instantiated in order.

    The premises are the rule's conditions, instantiated likewise. A variable with list semantics is instantiated with the list of terms it stands for.

  • theoryRewrite {P F T : Type} (rule : ProofRewriteRule) : View P F T

    THEORY_REWRITE: t = t', the conclusion, by the theory rewrite rule rule.

  • aciNorm {P F T : Type} : View P F T

    ACI_NORM: t = s, equal modulo associativity, commutativity, idempotence and identity.

  • absorb {P F T : Type} : View P F T

    ABSORB: t = z, z being a zero element t contains beneath its operator.

  • trust {P F T : Type} (id : Nat) (premises : Array P) (extra : Array T) : View P F T

    TRUST: a step cvc5 does not justify, id saying what kind of step it is.

    The premises, possibly none, entail the conclusion; extra is whatever further arguments cvc5 recorded. id is cvc5's internal trust identifier, which its API does not name.

  • trustTheoryRewrite {P F T : Type} (theory method : Nat) : View P F T

    TRUST_THEORY_REWRITE: an unchecked theory rewrite, the equality being the conclusion.

    theory identifies the theory whose rewriter applied and method the kind of rewriting; both are cvc5's internal identifiers, which its API does not name.

  • satRefutation {P F T : Type} (premises : Array P) : View P F T

    SAT_REFUTATION: false from the clauses premises, the SAT solver's unsat core.

  • resolution {P F T : Type} (left right : P) (polarity : Bool) (pivot : F) : View P F T

    RESOLUTION of left and right on pivot.

    The pivot occurs in left as is and in right negated when polarity is true, the other way round when it is false.

  • chainResolution {P F T : Type} (premises : Array P) (steps : Array (Bool × F)) : View P F T

    CHAIN_RESOLUTION: resolves premises left to right, step i on steps[i]'s pivot.

    Each step is a polarity and a pivot, as in resolution, and there is one step fewer than there are premises.

  • chainMResolution {P F T : Type} (premises : Array P) (steps : Array (Bool × F)) : View P F T

    CHAIN_M_RESOLUTION: chainResolution with factoring and reordering.

    The conclusion is the result of the resolution as a set of literals.

  • factoring {P F T : Type} (premise : P) : View P F T

    FACTORING: premise's clause, every literal's repetitions dropped.

  • reordering {P F T : Type} (premise : P) : View P F T

    REORDERING: premise's clause, its literals in the conclusion's order.

  • split {P F T : Type} (f : F) : View P F T

    SPLIT: f ∨ ¬f.

  • eqResolve {P F T : Type} (premise equiv : P) : View P F T

    EQ_RESOLVE: F₂ from premise : F₁ and equiv : F₁ = F₂.

  • modusPonens {P F T : Type} (premise implication : P) : View P F T

    MODUS_PONENS: F₂ from premise : F₁ and implication : F₁ ⇒ F₂.

  • notNotElim {P F T : Type} (premise : P) : View P F T

    NOT_NOT_ELIM: F from ¬¬F.

  • contra {P F T : Type} (premise negation : P) : View P F T

    CONTRA: false from premise : F and negation : ¬F.

  • andElim {P F T : Type} (premise : P) (index : Nat) : View P F T

    AND_ELIM: the conjunct at index of premise : F₀ ∧ … ∧ Fₙ, counting from zero.

  • andIntro {P F T : Type} (premises : Array P) : View P F T

    AND_INTRO: the conjunction of the premises' conclusions.

  • notOrElim {P F T : Type} (premise : P) (index : Nat) : View P F T

    NOT_OR_ELIM: ¬Fᵢ from premise : ¬(F₀ ∨ … ∨ Fₙ), i being index, from zero.

  • impliesElim {P F T : Type} (premise : P) : View P F T

    IMPLIES_ELIM: ¬F₁ ∨ F₂ from F₁ ⇒ F₂.

  • notImpliesElim1 {P F T : Type} (premise : P) : View P F T

    NOT_IMPLIES_ELIM1: F₁ from ¬(F₁ ⇒ F₂).

  • notImpliesElim2 {P F T : Type} (premise : P) : View P F T

    NOT_IMPLIES_ELIM2: ¬F₂ from ¬(F₁ ⇒ F₂).

  • equivElim1 {P F T : Type} (premise : P) : View P F T

    EQUIV_ELIM1: ¬F₁ ∨ F₂ from F₁ = F₂.

  • equivElim2 {P F T : Type} (premise : P) : View P F T

    EQUIV_ELIM2: F₁ ∨ ¬F₂ from F₁ = F₂.

  • notEquivElim1 {P F T : Type} (premise : P) : View P F T

    NOT_EQUIV_ELIM1: F₁ ∨ F₂ from F₁ ≠ F₂.

  • notEquivElim2 {P F T : Type} (premise : P) : View P F T

    NOT_EQUIV_ELIM2: ¬F₁ ∨ ¬F₂ from F₁ ≠ F₂.

  • xorElim1 {P F T : Type} (premise : P) : View P F T

    XOR_ELIM1: F₁ ∨ F₂ from F₁ ⊕ F₂.

  • xorElim2 {P F T : Type} (premise : P) : View P F T

    XOR_ELIM2: ¬F₁ ∨ ¬F₂ from F₁ ⊕ F₂.

  • notXorElim1 {P F T : Type} (premise : P) : View P F T

    NOT_XOR_ELIM1: F₁ ∨ ¬F₂ from ¬(F₁ ⊕ F₂).

  • notXorElim2 {P F T : Type} (premise : P) : View P F T

    NOT_XOR_ELIM2: ¬F₁ ∨ F₂ from ¬(F₁ ⊕ F₂).

  • iteElim1 {P F T : Type} (premise : P) : View P F T

    ITE_ELIM1: ¬C ∨ F₁ from ite C F₁ F₂.

  • iteElim2 {P F T : Type} (premise : P) : View P F T

    ITE_ELIM2: C ∨ F₂ from ite C F₁ F₂.

  • notIteElim1 {P F T : Type} (premise : P) : View P F T

    NOT_ITE_ELIM1: ¬C ∨ ¬F₁ from ¬(ite C F₁ F₂).

  • notIteElim2 {P F T : Type} (premise : P) : View P F T

    NOT_ITE_ELIM2: C ∨ ¬F₂ from ¬(ite C F₁ F₂).

  • notAnd {P F T : Type} (premise : P) : View P F T

    NOT_AND: ¬F₁ ∨ … ∨ ¬Fₙ from ¬(F₁ ∧ … ∧ Fₙ).

  • cnfAndPos {P F T : Type} (f : F) (index : Nat) : View P F T

    CNF_AND_POS: ¬f ∨ Fᵢ, f being F₀ ∧ … ∧ Fₙ and i index, counting from zero.

  • cnfAndNeg {P F T : Type} (f : F) : View P F T

    CNF_AND_NEG: f ∨ ¬F₁ ∨ … ∨ ¬Fₙ, f being F₁ ∧ … ∧ Fₙ.

  • cnfOrPos {P F T : Type} (f : F) : View P F T

    CNF_OR_POS: ¬f ∨ F₁ ∨ … ∨ Fₙ, f being F₁ ∨ … ∨ Fₙ.

  • cnfOrNeg {P F T : Type} (f : F) (index : Nat) : View P F T

    CNF_OR_NEG: f ∨ ¬Fᵢ, f being F₀ ∨ … ∨ Fₙ and i index, counting from zero.

  • cnfImpliesPos {P F T : Type} (f : F) : View P F T

    CNF_IMPLIES_POS: ¬f ∨ ¬F₁ ∨ F₂, f being F₁ ⇒ F₂.

  • cnfImpliesNeg1 {P F T : Type} (f : F) : View P F T

    CNF_IMPLIES_NEG1: f ∨ F₁, f being F₁ ⇒ F₂.

  • cnfImpliesNeg2 {P F T : Type} (f : F) : View P F T

    CNF_IMPLIES_NEG2: f ∨ ¬F₂, f being F₁ ⇒ F₂.

  • cnfEquivPos1 {P F T : Type} (f : F) : View P F T

    CNF_EQUIV_POS1: ¬f ∨ ¬F₁ ∨ F₂, f being F₁ = F₂.

  • cnfEquivPos2 {P F T : Type} (f : F) : View P F T

    CNF_EQUIV_POS2: ¬f ∨ F₁ ∨ ¬F₂, f being F₁ = F₂.

  • cnfEquivNeg1 {P F T : Type} (f : F) : View P F T

    CNF_EQUIV_NEG1: f ∨ F₁ ∨ F₂, f being F₁ = F₂.

  • cnfEquivNeg2 {P F T : Type} (f : F) : View P F T

    CNF_EQUIV_NEG2: f ∨ ¬F₁ ∨ ¬F₂, f being F₁ = F₂.

  • cnfXorPos1 {P F T : Type} (f : F) : View P F T

    CNF_XOR_POS1: ¬f ∨ F₁ ∨ F₂, f being F₁ ⊕ F₂.

  • cnfXorPos2 {P F T : Type} (f : F) : View P F T

    CNF_XOR_POS2: ¬f ∨ ¬F₁ ∨ ¬F₂, f being F₁ ⊕ F₂.

  • cnfXorNeg1 {P F T : Type} (f : F) : View P F T

    CNF_XOR_NEG1: f ∨ ¬F₁ ∨ F₂, f being F₁ ⊕ F₂.

  • cnfXorNeg2 {P F T : Type} (f : F) : View P F T

    CNF_XOR_NEG2: f ∨ F₁ ∨ ¬F₂, f being F₁ ⊕ F₂.

  • cnfItePos1 {P F T : Type} (f : F) : View P F T

    CNF_ITE_POS1: ¬f ∨ ¬C ∨ F₁, f being ite C F₁ F₂.

  • cnfItePos2 {P F T : Type} (f : F) : View P F T

    CNF_ITE_POS2: ¬f ∨ C ∨ F₂, f being ite C F₁ F₂.

  • cnfItePos3 {P F T : Type} (f : F) : View P F T

    CNF_ITE_POS3: ¬f ∨ F₁ ∨ F₂, f being ite C F₁ F₂.

  • cnfIteNeg1 {P F T : Type} (f : F) : View P F T

    CNF_ITE_NEG1: f ∨ ¬C ∨ ¬F₁, f being ite C F₁ F₂.

  • cnfIteNeg2 {P F T : Type} (f : F) : View P F T

    CNF_ITE_NEG2: f ∨ C ∨ ¬F₂, f being ite C F₁ F₂.

  • cnfIteNeg3 {P F T : Type} (f : F) : View P F T

    CNF_ITE_NEG3: f ∨ ¬F₁ ∨ ¬F₂, f being ite C F₁ F₂.

  • refl {P F T : Type} (t : T) : View P F T

    REFL: t = t.

  • symm {P F T : Type} (premise : P) : View P F T

    SYMM: t₂ = t₁ from t₁ = t₂, or t₂ ≠ t₁ from t₁ ≠ t₂.

  • trans {P F T : Type} (premises : Array P) : View P F T

    TRANS: t₁ = tₙ from the chain t₁ = t₂, …, tₙ₋₁ = tₙ.

  • cong {P F T : Type} (premises : Array P) (app : T) : View P F T

    CONG: f(t₁, …, tₙ) = f(s₁, …, sₙ) from tᵢ = sᵢ, app being f(t₁, …, tₙ).

    Used for operators of fixed arity, indexed ones and uninterpreted functions included.

  • naryCong {P F T : Type} (premises : Array P) (app : T) : View P F T

    NARY_CONG: cong for a variadic, associative operator such as and or +.

  • pairwiseCong {P F T : Type} (premises : Array P) (app : T) : View P F T

    PAIRWISE_CONG: cong for a variadic, pairwise operator, which today means distinct.

  • trueIntro {P F T : Type} (premise : P) : View P F T

    TRUE_INTRO: F = true from F.

  • trueElim {P F T : Type} (premise : P) : View P F T

    TRUE_ELIM: F from F = true.

  • falseIntro {P F T : Type} (premise : P) : View P F T

    FALSE_INTRO: F = false from ¬F.

  • falseElim {P F T : Type} (premise : P) : View P F T

    FALSE_ELIM: ¬F from F = false.

  • other {P F T : Type} (rule : ProofRule) (premises : Array P) (args : Array T) : View P F T

    Any other step, as cvc5 gives it: a rule not decoded, or a step whose layout was not expected.

    Which rules are decoded grows over time, so a pattern .other .SOME_RULE … stops matching once that rule is decoded: match on the step's rule instead for a rule not decoded.

Instances For
    source
    def Cvc.Proof.View.rule {P F T : Type} :
    View P F T → ProofRule

    The rule a step applies.

    Equations
    Instances For
      source
      def Cvc.Proof.View.premises {P F T : Type} :
      View P F T → Array P

      A step's premises, in the order cvc5 gives them.

      Equations
      Instances For
        source
        def Cvc.Proof.View.mapM {m : Type → Type u_1} {P P' F F' T T' : Type} [Monad m] (fp : P → m P') (ff : F → m F') (ft : T → m T') :
        View P F T → m (View P' F' T')

        Maps a step's premises, formulas and terms, in a monad.

        Equations
        Instances For
          source
          def Cvc.Proof.View.map {P P' F F' T T' : Type} (fp : P → P') (ff : F → F') (ft : T → T') (v : View P F T) :
          View P' F' T'

          Maps a step's premises, formulas and terms.

          Equations
          Instances For

            Traversing #

            source
            def Cvc.Proof.foldWith {m : Type → Type u_1} {P N σ : Type} [Monad m] [BEq P] [Hashable P] (kids : P → Array P) (present : P → N) (roots : Array P) (init : σ) (pre : N → σ → m (FoldPre σ)) (post : N → σ → m (FoldPost σ)) (revisit : Bool := false) :
            m σ

            Folds over the distinct steps reachable from roots, each presented as present builds it.

            What both layers' fold are built on. Depth-first: each step is entered — pre — then, unless that answered skip, its premises (kids) are folded over left to right, and then it is left — post. A step reached again is passed over entirely unless revisit is set, in which case it is entered every time it is reached, which can take exponentially long on a proof sharing many sub-proofs.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Cvc.Proof.foldUpWith {m : Type → Type u_1} {P β : Type} [Monad m] [BEq P] [Hashable P] (kids : P → Array P) (step : P → Array β → m β) (roots : Array P) :
              m (Array β)

              Computes a value for every distinct step reachable from roots, bottom-up.

              What both layers' foldUp are built on. step is handed a step and the values of its premises (kids), in order, and is called once per distinct step, so a sub-proof shared by many steps is computed once. Answers the roots' values, in order. Ending early is the monad's business, by throwing for instance.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For