Inspecting proofs, sort-erased

A proof is what an unsat answer can be asked for, with Solver.getUnsatProof. This module takes one apart:

• Solver.Proof.view answers the root step as a Cvc.Proof.View, its rule a constructor and its premises and arguments fields;
• Solver.Proof.fold visits the distinct steps depth-first, with early exit, in any monad, and for step in proof do … does the same through ForIn;
• Solver.Proof.foldUp computes a value for every distinct step from its premises' values, which is the shape of anything that rebuilds a proof elsewhere;
• size, ruleCounts, freeAssumptions and trusted answer the usual questions.

Solver.Proofs.fold and Solver.Proofs.foldUp do the same over several proofs at once, sharing what they visit, which is what the components other than full answer: one proof per theory lemma, for instance.

Every traversal visits a step shared by many others once, as Cvc.Proof explains.

@[reducible, inline]

abbrev Cvc.Untyped.Solver.ProofView [Ω] (s : Solver) (pc : Proof.Component) : Type

A step of a sort-erased proof, taken apart: Cvc.Proof.View over sort-erased terms.

Equations

• s.ProofView pc = Cvc.Proof.View (s.Proof pc) Cvc.Untyped.Term Cvc.Untyped.Term

Decoding a step

def Cvc.Untyped.Solver.Proof.viewWith {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) {X : Type} (premises : Array X) : Proof.View X Term Term

The root step of p, taken apart, with premises standing for its premises.

What view and foldUp are built on: view passes the premises themselves, foldUp what it computed for them. premises is expected to hold one element per premise, in order, as getChildren does; a step whose premises do not match its rule's layout is other.

Equations

• p.viewWith premises = (Cvc.Untyped.Solver.Proof.decode?✝ p.getRule premises p.getArguments p.getRewriteRule?).getD (Cvc.Proof.View.other p.getRule premises p.getArguments)

def Cvc.Untyped.Solver.Proof.view {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : s.ProofView pc

The root step of p, taken apart: its rule a constructor, its premises and arguments fields.

Equations

• p.view = p.viewWith p.getChildren

Traversing

def Cvc.Untyped.Solver.Proof.fold {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) {m : Type → Type u_1} {σ : Type} [Monad m] (init : σ) (pre : s.Proof pc → s.ProofView pc → σ → m (FoldPre σ) := fun (x : s.Proof pc) (x_1 : s.ProofView pc) (s : σ) => pure (FoldPre.descend s)) (post : s.Proof pc → s.ProofView pc → σ → m (FoldPost σ) := fun (x : s.Proof pc) (x_1 : s.ProofView pc) (s : σ) => pure (FoldPost.continue s)) (revisit : Bool := false) : m σ

Folds over the distinct steps of p, depth-first, with early exit, in any monad.

Each step is handed over with its view. pre is called on reaching a step, before its premises, and can skip them or stop; post on leaving it, once its premises are done, and can stop. Both default to carrying on.

A step shared by several others is visited once, on the first path that reaches it, unless revisit is set — which can take exponentially long.

Equations

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

def Cvc.Untyped.Solver.Proof.foldUp {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) {m : Type → Type u_1} {β : Type} [Monad m] (f : s.Proof pc → Proof.View β Term Term → m β) : m β

Computes a value for every distinct step of p, bottom-up, and answers the root's.

f is handed each step with its view, the premises of which are the values already computed for them. It is called once per distinct step, so a sub-proof shared by many steps is computed once, which is what rebuilding a proof elsewhere wants. To end early, throw, in Except for instance.

Equations

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

@[instance_reducible]

instance Cvc.Untyped.Solver.Proof.instForInOfMonad {pc : Proof.Component} [Ω] {s : Solver} {m : Type → Type u_1} [Monad m] : ForIn m (s.Proof pc) (s.Proof pc)

for step in p do … visits the distinct steps of p in the order fold enters them.

break ends the loop.

Equations

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

Questions about a proof

def Cvc.Untyped.Solver.Proof.size {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : Nat

The number of distinct steps in p.

Equations

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

def Cvc.Untyped.Solver.Proof.ruleCounts {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : Array (ProofRule × Nat)

How many distinct steps of p apply each rule, rules in the order they are first reached.

Equations

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

def Cvc.Untyped.Solver.Proof.freeAssumptions {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : Terms

The assumptions p leaves open, in the order they are first reached.

These are the formulas of its ASSUME steps that no enclosing SCOPE discharges.

A proof cvc5 answers for the full component leaves none open, its root scope discharging the assertions. Below that scope, they are the assertions the refutation actually uses.

Equations

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

def Cvc.Untyped.Solver.Proof.trusted {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : s.Proofs pc

The distinct steps of p that cvc5 does not justify, in the order they are first reached.

These are its TRUST and TRUST_THEORY_REWRITE steps.

Equations

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

def Cvc.Untyped.Solver.Proofs.fold {pc : Proof.Component} [Ω] {s : Solver} (ps : s.Proofs pc) {m : Type → Type u_1} {σ : Type} [Monad m] (init : σ) (pre : s.Proof pc → s.ProofView pc → σ → m (FoldPre σ) := fun (x : s.Proof pc) (x_1 : s.ProofView pc) (s : σ) => pure (FoldPre.descend s)) (post : s.Proof pc → s.ProofView pc → σ → m (FoldPost σ) := fun (x : s.Proof pc) (x_1 : s.ProofView pc) (s : σ) => pure (FoldPost.continue s)) (revisit : Bool := false) : m σ

Solver.Proof.fold over several proofs at once, left to right.

A step they share is visited once in all.

Equations

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

def Cvc.Untyped.Solver.Proofs.foldUp {pc : Proof.Component} [Ω] {s : Solver} (ps : s.Proofs pc) {m : Type → Type u_1} {β : Type} [Monad m] (f : s.Proof pc → Proof.View β Term Term → m β) : m (Array β)

Solver.Proof.foldUp over several proofs at once, answering each proof's value, in order.

A step they share is computed once in all.

Equations

• ps.foldUp f = Cvc.Proof.foldUpWith (fun (x : s.Proof pc) => x.getChildren) (fun (q : s.Proof pc) (bs : Array β) => f q (q.viewWith bs)) ps