Function certify

Source

pub fn certify(
    tree: &DerivationTree,
    ctx: &CertificationContext<'_>,
) -> KernelResult<Term>

Expand description

Certify a derivation tree, producing a kernel term.

Converts a proof (derivation tree) into a typed lambda calculus term via the Curry-Howard correspondence. The resulting term, when type-checked by the kernel, should have the type corresponding to the tree’s conclusion.

§Arguments

tree - The derivation tree to certify
ctx - The certification context (wraps kernel context)

§Returns

Ok(term) - The kernel term representing this proof
Err(_) - If certification fails (missing hypothesis, wrong premises, etc.)

§Curry-Howard Mapping

Inference Rule	Kernel Term
`Axiom` / `PremiseMatch`	`Term::Global(name)` (hypothesis lookup)
`ModusPonens`	`Term::App(certify(impl), certify(arg))`
`ConjunctionIntro`	`conj P Q p_proof q_proof`
`UniversalInst(w)`	`Term::App(forall_proof, w)`
`UniversalIntro { var, type }`	`Term::Lambda { param: var, ... }`
`StructuralInduction`	`Term::Fix { name, body: λn. match n ... }`
`Rewrite { from, to }`	`Eq_rec A from P proof to eq_proof`
`ExistentialIntro`	`witness A P w proof`

§Induction Handling

Structural induction produces fixpoint terms. The step case certification tracks the induction variable so that IH references become recursive calls.

§See Also

CertificationContext - The context passed to this function
DerivationTree - The input proof structure
InferenceRule - The rules being certified

certify