Inspecting proofs, typed

The sort-erased Cvc.Untyped.Proof with formulas typed: a step's view holds its formulas — an assumption, a pivot, a clause-form input — as Term Bool, and freeAssumptions answers them so.

A term that is not a formula — REFL's term, CONG's application, a rewrite's instantiation — stays sort-erased, as Solver.Proof.getArguments does: a rule fixes no sort for it, so there is no index to give it, and Untyped.Term.typeCheck is the way to put one on.

The decoding is the sort-erased one; each formula is then checked to be Boolean, and a step whose formulas are not falls back to other, so a Term Bool here is never a guess.

@[reducible, inline]

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

A step of a typed proof, taken apart: formulas as Term Bool, other terms sort-erased.

Equations

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

Decoding a step

def Cvc.Typed.Solver.Proof.viewWith {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) {X : Type} (premises : Array X) : Proof.View X (Term Bool) Untyped.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, and so is one with a formula that is not Boolean.

Equations

• p.viewWith premises = (Cvc.Proof.View.mapM pure Cvc.Typed.Solver.Proof.formula?✝ pure (p.relax.viewWith premises)).getD (Cvc.Proof.View.other p.getRule premises p.getArguments)

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

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

Equations

• p.view = p.viewWith p.getChildren

Traversing

def Cvc.Typed.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.Typed.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 Bool) Untyped.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.Typed.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.Typed.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.Typed.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.Typed.Solver.Proof.freeAssumptions {pc : Proof.Component} [Ω] {s : Solver} (p : s.Proof pc) : Terms Bool

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.Typed.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.Typed.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.Typed.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 Bool) Untyped.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