Enum mm0b_parser::ProofCmd

pub enum ProofCmd {
    Term {
        tid: TermId,
        save: bool,
    },
    Ref(u32),
    Dummy(SortId),
    Thm {
        tid: ThmId,
        save: bool,
    },
    Hyp,
    Conv,
    Refl,
    Sym,
    Cong,
    Unfold,
    ConvCut,
    ConvSave,
    Save,
    Sorry,
}

A proof command, which acts on a stack machine with the following components:

• H: Vec<StackEl>: a “heap” consisting of indexable elements that can be copied onto the stack using Ref
• S: Stack<StackEl>: The main stack, which most operations push and pop from.
• HS: Vec<Expr>: The hypothesis list, which grows only on Hyp operations and collects the hypotheses of the theorem.

Variants

Term

Term t: H; S, e1, ..., en --> H; S, (t e1 .. en)
Save: H; S, e --> H, e; S, e
TermSave t = Term t; Save:
  H; S, e1, ..., en --> H, (t e1 .. en); S, (t e1 .. en)

Pop n elements from the stack and allocate a new term t applied to those expressions. When save is used, the new term is also saved to the heap (this is used if the term will ever be needed more than once).

Fields of Term

tid: TermId

The term to construct

save: bool

True if we should save to the heap

Ref(u32)

Ref i: H; S --> H; S, Hi
ConvRef i: H; S, e1 =?= e2 --> H; S   (where Hi is e1 = e2)

Get the i-th heap element.

• If it is e1 = e2, pop a convertibility obligation e1 =?= e2.
• Otherwise push it on the stack.

Dummy(SortId)

Dummy s: H; S --> H, x; S, x    alloc(x:s)

Allocate a new variable x of sort s, and push it to the stack and the heap.

Thm

Thm T: H; S, e1, ..., en, e --> H; S', |- e
  (where Unify(T): S; e1, ... en; e --> S'; H'; .)
Save: H; S, |- e --> H, |- e; S, |- e

Pop n elements from the stack and put them on the unify heap, then call the unifier for T with e as the target. The unifier will pop additional proofs from the stack if the UHyp command is used, and when it is done, the conclusion is pushed as a proven statement.

When Save is used, the proven statement is also saved to the heap.

Fields of Thm

tid: ThmId

The theorem to apply

save: bool

True if we should save to the heap

Hyp

Hyp: HS; H; S, e --> HS, e; H, |- e; S

This command means that we are finished constructing the expression e which denotes a statement, and wish to assume it as a hypothesis. Push e to the hypothesis stack, and push |- e to the heap.

Conv

Conv: S, e1, |- e2 --> S, |- e1, e1 =?= e2

Pop e1 and |- e2, and push |- e1, guarded by a convertibility obligation e1 =?= e2.

Refl

Refl: S, e =?= e --> S

Pop a convertibility obligation where the two sides are equal.

Sym

Symm: S, e1 =?= e2 --> S, e2 =?= e1

Swap the direction of a convertibility obligation.

Cong

Cong: S, (t e1 ... en) =?= (t e1' ... en') --> S, en =?= en', ..., e1 =?= e1'

Pop a convertibility obligation for two term expressions, and push convertibility obligations for all the parts. The parts are pushed in reverse order so that they are dealt with in declaration order in the proof stream.

Unfold

Unfold: S, (t e1 ... en) =?= e', e --> S, e =?= e'
  (where Unify(t): e1, ..., en; e --> H'; .)

Pop e and (t e1 ... en) =?= e' from the stack and run the unifier for t (which should be a definition) to make sure that (t e1 ... en) unfolds to e. Then push e =?= e'.

ConvCut

ConvCut: S, e1 =?= e2 --> S, e1 = e2, e1 =?= e2

Pop a convertibility obligation e1 =?= e2, and push a convertability assertion e1 = e2 guarded by e1 =?= e2.

ConvSave

ConvSave: H; S, e1 = e2 --> H, e1 = e2; S

Pop a convertibility proof e1 = e2 and save it to the heap.

Save

Save: H; S, s --> H, s; S, s

Save the top of the stack to the heap, without popping it.

Sorry

Sorry: S, e -> S, |- e
ConvSorry: S, e1 =?= e2 -> S

• Sorry: Pop an expression e from the stack, and push |- e. This step exists only for debugging purposes and incomplete proofs, it is not a valid step under any circumstances, and verifiers are free to pretend it doesn’t exist.

• ConvSorry: Pop a convertibility obligation e1 =?= e2. This reuses the Sorry command, and depends on the type of the head of stack for its behavior.

Implementations

impl ProofCmd

pub fn write_to(self, w: &mut impl Write) -> Result<()>

Serialize a ProofCmd to the given writer. Uses the PROOF_* commands in mmb::export::cmd.

Trait Implementations

impl Clone for ProofCmd

fn clone(&self) -> ProofCmd

Returns a copy of the value.

pub fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for ProofCmd

impl Debug for ProofCmd

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl TryFrom<(u8, u32)> for ProofCmd

type Error = ParseError

The type returned in the event of a conversion error.

fn try_from((cmd, data): (u8, u32)) -> Result<Self, Self::Error>

Performs the conversion.