Native PA foundations

A complete reader’s guide to the first-order arithmetic language, its six arithmetic axioms, every independently checked proof constructor, and every executable Peano Lab proof command.

6 arithmetic axioms · 25 kernel proof constructors · 34 documented commands · 19 commands used by this 557-theorem proof corpus

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

First, what is actually trusted?

A proof script is a human-readable recipe, not proof authority. Tactics, search, simplification, theorem names, dashboards, and generated explanations are untrusted proof builders. They propose an explicit certificate. The small independent kernel accepts a theorem only after checking that certificate against the exact original formula in the empty context.

native statement + tactic script + checked prerequisites
                    ↓ untrusted proof construction
               explicit proof certificate
                    ↓ independent kernel checker
             original theorem accepted — QED

Constructive by default. The quadratic-reciprocity corpus does not gain classical reasoning from a dashboard or a tactic. Double-negation elimination requires an explicitly authorized classical session and leaves a visible DNE certificate. A checked Cut shares evidence but adds no arithmetic assumption.

Why certificates are data, not authority · Follow the complete library trust path · Constructive versus explicitly classical checking

Terms: the complete arithmetic vocabulary

t ::= x | 0 | S(t) | t + u | t * u

The kernel understands variables, zero, successor, addition, and multiplication—nothing else. A numeral such as 3 is convenient notation for S(S(S(0))). Bound names become de Bruijn indices, so renaming a bound variable cannot change its mathematical meaning.

There are no primitive division, remainder, subtraction, exponentiation, lists, sets, primes, or residue symbols. Bigger mathematics is encoded using this same small term language.

Read the complete term grammar and parser conventions · Understand de Bruijn indices and capture avoidance

Formulas: first-order logic with equality

A ::= t = u | false | A -> B | A /\ B | A \/ B
    | forall x. A | exists x. A

These forms mean equality, contradiction, implication, conjunction, disjunction, universal quantification, and existential quantification. Negation is the conservative abbreviation ~A := A -> false, not an additional kernel constructor.

Familiar number-theoretic notation is relational shorthand: a ≤ b expands to exists k. b = a + k; a < b expands to exists k. b = a + S k; and divisibility expands to exists k. b = a * k. Every definition-aware theorem ultimately expands back to this exact grammar.

Full formula grammar · How order, divisibility, residues, and finite objects expand · Why mathematical definitions add no kernel axioms · Open the linked definition-aware edition

Arithmetic axioms PA1–PA6

These are the only named arithmetic axiom constants. Notice that both addition and multiplication recurse on their right argument: n + 0 = n follows immediately from PA3, whereas 0 + n = n needs induction.

Induction is a checked proof rule, not “PA7”

P(0),  forall n. P(n) -> P(S n)
────────────────────────────────
         forall n. P(n)

Each Ind constructor stores one concrete first-order motive and separate base and successor proofs. The kernel checks both; there is no object-language predicate variable and no unrestricted induction oracle.

Induction is a rule, not PA7 · See induction build the arithmetic ladder

DNE is explicitly classical, never silently constructive

((A -> false) -> false) -> A is represented only by an explicit DNE node. The ordinary constructive checker rejects it. An owner must separately authorize classical mode; it is not proof authority for this quadratic-reciprocity stack.

Read the exact constructive/classical boundary

All 25 native proof constructors

These are the complete, exact proof-certificate constructors accepted by the kernel, grouped by their mathematical rule. Signatures are generated from the actual frozen proof dataclasses; the displayed sequent explains what each constructor has to establish. Neither a tactic nor an engine-only administrative node appears in this inventory.

Context, implication, and checked sharing

Hyp(i)

Use a hypothesis already present in the current logical context.

Γ, A ⊢ A

Index zero selects the newest assumption; the checker rejects missing or malformed context indices.

Read the corresponding proof rule · Related commands: exact · assumption

ImpIntro(body)

Introduce an implication by proving its conclusion under a fresh assumption.

Γ, A ⊢ B  ⇒  Γ ⊢ A → B

The checker extends the context with the exact antecedent before it checks the body.

Read the corresponding proof rule · Related commands: intro

ImpElim(f, a)

Apply an established implication to an independently checked proof of its premise.

Γ ⊢ A → B; Γ ⊢ A  ⇒  Γ ⊢ B

This is ordinary modus ponens; both the function and its argument must match exactly.

Read the corresponding proof rule · Related commands: apply · specialize

Cut(proposition, conclusion, lemma, body)

Share a checked intermediate lemma with a continuation that may reuse it.

Γ ⊢ A; Γ, A ⊢ B  ⇒  Γ ⊢ B

The checker validates both branches. Cut is proof sharing, not a theorem oracle or another arithmetic axiom.

Read the corresponding proof rule · Related commands: use

Conjunction

AndIntro(left, right)

Establish a conjunction by constructing proofs of both component propositions.

Γ ⊢ A; Γ ⊢ B  ⇒  Γ ⊢ A ∧ B

Its left and right certificate branches are checked separately against the corresponding conjuncts.

Read the corresponding proof rule · Related commands: split

AndElimL(pair)

Project the left component from a proof of a conjunction.

Γ ⊢ A ∧ B  ⇒  Γ ⊢ A

The source must synthesize a genuine conjunction; no assumption about its right field is discarded unsafely.

Read the corresponding proof rule · Related commands: cases

AndElimR(pair)

Project the right component from a proof of a conjunction.

Γ ⊢ A ∧ B  ⇒  Γ ⊢ B

The checker first identifies both conjuncts and returns exactly the independently established right component.

Read the corresponding proof rule · Related commands: cases

Disjunction and contradiction

OrIntroL(proof)

Prove a disjunction by supplying a proof of its left alternative.

Γ ⊢ A  ⇒  Γ ⊢ A ∨ B

The expected target supplies the unchosen right alternative; no proof of that alternative is claimed.

Read the corresponding proof rule · Related commands: left

OrIntroR(proof)

Prove a disjunction by supplying a proof of its right alternative.

Γ ⊢ B  ⇒  Γ ⊢ A ∨ B

The expected target supplies the unchosen left alternative; the chosen branch must still be checked.

Read the corresponding proof rule · Related commands: right

OrElim(disjunction, left_case, right_case)

Reason by cases on a proved disjunction, establishing the same conclusion in both cases.

Γ ⊢ A ∨ B; Γ, A ⊢ C; Γ, B ⊢ C  ⇒  Γ ⊢ C

Both branches receive their own precise hypothesis and must prove the identical original conclusion.

Read the corresponding proof rule · Related commands: cases

BotElim(absurdity)

Derive any specified conclusion from an independently checked proof of contradiction.

Γ ⊢ ⊥  ⇒  Γ ⊢ A

Explosion is constructive logic: it consumes real evidence of bottom and never manufactures the contradiction.

Read the corresponding proof rule · Related commands: exfalso · cases

Quantifiers and explicit witnesses

ForallIntro(body)

Prove a universal statement using an arbitrary fresh rigid term variable.

Γ ⊢ P(x fresh)  ⇒  Γ ⊢ ∀x. P(x)

The context is shifted beneath the binder so the introduced eigenvariable cannot capture an outer variable.

Read the corresponding proof rule · Related commands: intro · induction

ForallElim(p, t)

Instantiate a proved universal formula at one well-scoped arithmetic term.

Γ ⊢ ∀x. P(x)  ⇒  Γ ⊢ P(t)

Capture-avoiding substitution replaces the quantified slot with the supplied term before comparison.

Read the corresponding proof rule · Related commands: specialize · forall_elim · apply

ExistsIntro(t, p)

Prove existence by exhibiting a concrete witness and checking its required property.

Γ ⊢ P(t)  ⇒  Γ ⊢ ∃x. P(x)

The certificate stores both the witness term and the proof of the exactly substituted body.

Read the corresponding proof rule · Related commands: exists

ExistsElim(p, body)

Open an existential hypothesis using a fresh witness that cannot escape into the conclusion.

Γ ⊢ ∃x. P(x); Γ, P(w fresh) ⊢ C  ⇒  Γ ⊢ C

The checker lifts the surrounding context and the target, preventing the private witness from leaking.

Read the corresponding proof rule · Related commands: cases

Equality, congruence, and transport

EqRefl(t)

Certify that a well-formed arithmetic term is equal to itself.

Γ ⊢ t = t

The checker constructs exactly the reflexive equation for the stored rigid kernel term.

Read the corresponding proof rule · Related commands: refl · simp

EqSym(proof)

Reverse the direction of an already checked equality proof.

Γ ⊢ s = t  ⇒  Γ ⊢ t = s

Only a certificate that actually synthesizes an equality can be reversed by this constructor.

Read the corresponding proof rule · Related commands: symm · rewrite

EqTrans(first, second)

Compose two checked equality proofs through exactly the same intermediate term.

Γ ⊢ r = s; Γ ⊢ s = t  ⇒  Γ ⊢ r = t

The middle expressions must agree syntactically after legitimate substitution; unrelated chains are rejected.

Read the corresponding proof rule · Related commands: trans

CongS(proof)

Lift an equality through the successor constructor on both sides.

Γ ⊢ s = t  ⇒  Γ ⊢ S(s) = S(t)

This is structural congruence for the sole unary arithmetic function in the native language.

Read the corresponding proof rule · Related commands: congr · norm_num

CongAdd(left, right)

Lift two component equalities through the binary addition constructor.

Γ ⊢ a = c; Γ ⊢ b = d  ⇒  Γ ⊢ a + b = c + d

Both argument certificates are checked; addition congruence does not assume commutativity or associativity.

Read the corresponding proof rule · Related commands: congr · norm_num

CongMul(left, right)

Lift two component equalities through the binary multiplication constructor.

Γ ⊢ a = c; Γ ⊢ b = d  ⇒  Γ ⊢ a · b = c · d

Both factor equalities need evidence; multiplication laws remain separate theorems or arithmetic axioms.

Read the corresponding proof rule · Related commands: congr · norm_num

EqSubst(motive, eq_proof, body_proof)

Transport a proved formula along an equality using an explicit one-variable motive.

Γ ⊢ s = t; Γ ⊢ P(s)  ⇒  Γ ⊢ P(t)

The stored Leibniz motive uses a distinguished de Bruijn slot; both substitutions are capture-avoiding.

Read the corresponding proof rule · Related commands: rewrite · simp

Arithmetic, induction, and explicit classicality

Axiom(name)

Introduce exactly one of the six fixed arithmetic axiom schemas PA1 through PA6.

Γ ⊢ PAi   where i ∈ {1, 2, 3, 4, 5, 6}

The checker reconstructs the precise named schema and rejects arbitrary theorem names or fabricated formulas.

Read the corresponding proof rule · Related commands: apply · rewrite · simp

Ind(motive, base, step)

Prove a concrete first-order induction instance from its zero and successor cases.

Γ ⊢ P(0); Γ ⊢ ∀n. P(n) → P(S n)  ⇒  Γ ⊢ ∀n. P(n)

The motive is an actual stored formula, never a predicate variable, a blanket axiom, or an unchecked induction oracle.

Read the corresponding proof rule · Related commands: induction

DNE(proposition)

State double-negation elimination for one concrete proposition in explicitly classical mode.

Γ ⊢ ((A → ⊥) → ⊥) → A   [classical only]

The ordinary constructive checker rejects every DNE node; only owner-authorized classical checking accepts it.

Read the corresponding proof rule · Related commands: apply

How the checker interprets inert proof data · Natural deduction, equality, and induction rules

The 19 tactics occurring in this proof corpus

The 557 quadratic-reciprocity theorem pages link every formal proof line to the corresponding command below. Peano Lab has additional supported commands; their cards are included too and clearly labeled as outside this particular proof slice.

apply · cases · congr · exact · exfalso · exists · have · induction · intro · left · norm_num · refl · rewrite · right · simp · specialize · split · symm · trans

A command’s goal effect describes the obligation a reader sees; its kernel evidence describes the explicit certificate that must ultimately survive independent checking. Every example below is a complete replay ending in ordinary qed.

Primitive tactics and session commands · 23

Primitive commands introduce or eliminate logical structure, manipulate equalities, build explicit witnesses, or manage an honest proof session. Commands such as undo restore state but never create a logical inference; use imports only an independently checked theorem.

intro · Introduce one implication premise or one universally quantified variable.

Used in the quadratic-reciprocity proof corpus

Syntax: intro [name]

Goal effect: For A -> B, adds the named A hypothesis and focuses B. For forall x. P, adds a fresh rigid variable and focuses P.

Kernel evidence: Replaces the focused hole by ImpIntro(?) or ForallIntro(?).

Complete executable example:

pa prove 0 = 0 -> 0 = 0
intro h
exact h
qed
Common mistakes and failure modes
  • The goal is neither an implication nor a universal quantifier.
  • The supplied name is already in use or is not a legal surface name.

Goals, holes, and proof constructors · Open this interactive tactic card

have · Prove a named local fact, then continue with that fact available.

Used in the quadratic-reciprocity proof corpus

Syntax: have h : P

Goal effect: Creates two ordered goals: first P in the current context, then the old target with the fresh hypothesis h : P.

Kernel evidence: Installs an engine-only proof-first cut. Before QED, capture-avoiding cut elimination compiles it to ordinary proof terms for the independent kernel.

Complete executable example:

pa prove 0 = 0
have h : 0 = 0
refl
exact h
qed
Common mistakes and failure modes
  • The command must have the exact shape `have h : P`.
  • The name is malformed or already names a variable or hypothesis.
  • The proposition is malformed or mentions a term variable outside the current scope.

How local intermediate facts compile · Open this interactive tactic card

suffices · Reduce the old target to a named fact, then prove that fact.

Available in Peano Lab; not used in this proof slice

Syntax: suffices h : P

Goal effect: Creates two ordered goals: first the old target with h : P available, then P in the original context.

Kernel evidence: Installs an engine-only continuation-first cut. Before QED, capture-avoiding cut elimination compiles it to ordinary proof terms for the independent kernel.

Complete executable example:

pa prove 0 = 0
suffices h : 0 = 0
exact h
refl
qed
Common mistakes and failure modes
  • The command must have the exact shape `suffices h : P`.
  • The name is malformed or already names a variable or hypothesis.
  • The proposition is malformed or mentions a term variable outside the current scope.

How local intermediate facts compile · Open this interactive tactic card

specialize · Add a concrete instance of a universally quantified hypothesis.

Used in the quadratic-reciprocity proof corpus

Syntax: specialize <hypothesis> <term>

Goal effect: Keeps the original universal hypothesis under a fresh internal name and adds its selected instance under the requested name.

Kernel evidence: Builds ForallElim for the instance and a local implication cut around the existing certificate hole.

Complete executable example:

pa prove (forall x. x = x) -> 0 = 0
intro h
specialize h 0
exact h
qed
Common mistakes and failure modes
  • The named hypothesis is missing or is not universally quantified.
  • The term is missing, malformed, or contains an unresolved metavariable.

Goals, holes, and proof constructors · Open this interactive tactic card

forall_elim · Spell the same universal-hypothesis elimination as specialize.

Available in Peano Lab; not used in this proof slice

Syntax: forall_elim <hypothesis> <term>

Goal effect: Adds the concrete instance to the context while retaining the universal fact.

Kernel evidence: Builds the same ForallElim-and-cut certificate as specialize; this is a pedagogical alias, not a new kernel rule.

Complete executable example:

pa prove (forall x. x = x) -> 1 = 1
intro h
forall_elim h 1
exact h
qed
Common mistakes and failure modes
  • The command needs exactly a hypothesis name and a concrete term.
  • The named hypothesis is not a forall formula.

Goals, holes, and proof constructors · Open this interactive tactic card

induction · Apply structural induction to a leading forall or a named rigid variable.

Used in the quadratic-reciprocity proof corpus

Syntax: induction <variable>

Goal effect: Replaces one goal by the zero case and the successor case; the latter has the step variable and an IH hypothesis.

Kernel evidence: Installs an Ind certificate with base and step holes. The step is wrapped by ForallIntro and ImpIntro; local-variable induction also uses ForallElim.

Complete executable example:

pa prove forall n. 0 + n = n
induction n
simp
simp [IH]
qed
Common mistakes and failure modes
  • The name is not a leading forall binder or a variable in the goal.
  • An unresolved term metavariable prevents construction of a fixed motive.

Concrete first-order induction motives · Open this interactive tactic card

apply · Use a local theorem, a PA axiom, or explicitly authorized DNE backwards.

Used in the quadratic-reciprocity proof corpus

Syntax: apply <hypothesis|PA1..PA6|DNE>

Goal effect: Matches the source conclusion against the goal and creates one subgoal for each implication premise; leading forall variables are inferred as metas.

Kernel evidence: Starts with Hyp, Axiom, or DNE, adds ForallElim nodes for inferred terms, then ImpElim nodes whose argument positions are new holes.

Complete executable example:

pa prove forall n. S n = 0 -> false
intro n
intro h
apply PA1
exact h
qed
Common mistakes and failure modes
  • The proof source is unknown or its conclusion does not match the goal.
  • DNE is rejected unless the session owner has enabled classical mode.

Goals, holes, and proof constructors · Open this interactive tactic card

split · Prove both halves of a conjunction.

Used in the quadratic-reciprocity proof corpus

Syntax: split

Goal effect: Replaces A /\ B by two ordered goals, first A and then B.

Kernel evidence: Replaces the hole by AndIntro(left-hole, right-hole).

Complete executable example:

pa prove 0 = 0 /\ 1 = 1
split
refl
refl
qed
Common mistakes and failure modes
  • The focused goal is not a conjunction.
  • Extra arguments are not accepted.

Goals, holes, and proof constructors · Open this interactive tactic card

left · Choose the left constructor of a disjunction.

Used in the quadratic-reciprocity proof corpus

Syntax: left

Goal effect: Replaces A \/ B by the single goal A.

Kernel evidence: Replaces the hole by OrIntroL(?).

Complete executable example:

pa prove 0 = 0 \/ 0 = 1
left
refl
qed
Common mistakes and failure modes
  • The focused goal is not a disjunction.
  • Choosing left does not prove the discarded right alternative.

Goals, holes, and proof constructors · Open this interactive tactic card

right · Choose the right constructor of a disjunction.

Used in the quadratic-reciprocity proof corpus

Syntax: right

Goal effect: Replaces A \/ B by the single goal B.

Kernel evidence: Replaces the hole by OrIntroR(?).

Complete executable example:

pa prove 0 = 1 \/ 0 = 0
right
refl
qed
Common mistakes and failure modes
  • The focused goal is not a disjunction.
  • Choosing right does not prove the discarded left alternative.

Goals, holes, and proof constructors · Open this interactive tactic card

cases · Eliminate a conjunction, disjunction, existential, or bottom hypothesis.

Used in the quadratic-reciprocity proof corpus

Syntax: cases <hypothesis>

Goal effect: A conjunction exposes both fields; a disjunction makes two branches; an existential opens a fresh witness; bottom closes the goal.

Kernel evidence: Builds the matching AndElim cut, OrElim, ExistsElim, or BotElim tree with holes exactly corresponding to the displayed branches.

Complete executable example:

pa prove (0 = 0 /\ 1 = 1) -> 0 = 0
intro h
cases h
exact h_left
qed
Common mistakes and failure modes
  • The hypothesis name is unknown.
  • Atomic, implication, universal, and equality hypotheses cannot be cased.

Goals, holes, and proof constructors · Open this interactive tactic card

exfalso · Reduce an arbitrary target to bottom (false).

Used in the quadratic-reciprocity proof corpus

Syntax: exfalso

Goal effect: Keeps the context and replaces the focused target by false.

Kernel evidence: Wraps the new hole in BotElim, so a proof of bottom can inhabit the old target.

Complete executable example:

pa prove false -> 0 = 1
intro h
exfalso
exact h
qed
Common mistakes and failure modes
  • The current goal is already bottom, so the command would make no progress.
  • Exfalso does not manufacture a contradiction; the new false goal remains.

Goals, holes, and proof constructors · Open this interactive tactic card

exists · Supply a witness for an existential goal.

Used in the quadratic-reciprocity proof corpus

Syntax: exists <term|?>

Goal effect: Replaces exists x. P(x) by P(witness). A bare ? creates a flexible, proof-wide term metavariable that later unification must resolve.

Kernel evidence: Replaces the hole by ExistsIntro(witness, proof-hole).

Complete executable example:

pa prove exists n. n = 0
exists 0
refl
qed
Common mistakes and failure modes
  • The focused goal is not existential or the witness term is malformed.
  • QED fails if a ? witness remains unresolved in the final certificate.

Witnesses and scoped metavariables · Open this interactive tactic card

refl · Close an equality whose two sides unify as the same term.

Used in the quadratic-reciprocity proof corpus

Syntax: refl

Goal effect: Removes the focused equality goal and may solve shared term metavariables.

Kernel evidence: Inserts EqRefl(term), then propagates any new metavariable substitution through every sibling goal and the whole partial certificate.

Complete executable example:

pa prove 0 = 0
refl
qed
Common mistakes and failure modes
  • The goal is not an equality.
  • The two rigid terms differ and cannot be made identical by solving metas.

Goals, holes, and proof constructors · Open this interactive tactic card

symm · Reverse the direction of an equality goal.

Used in the quadratic-reciprocity proof corpus

Syntax: symm

Goal effect: Changes the target from a = b to b = a.

Kernel evidence: Replaces the focused hole by EqSym(new-hole).

Complete executable example:

pa prove 0 = 1 -> 1 = 0
intro h
symm
exact h
qed
Common mistakes and failure modes
  • The focused goal is not an equality.
  • Repeated symmetry can cycle; repeat detects that cycle and stops.

Goals, holes, and proof constructors · Open this interactive tactic card

trans · Split an equality through a chosen middle term.

Used in the quadratic-reciprocity proof corpus

Syntax: trans <middle-term|?>

Goal effect: Replaces a = c by the ordered goals a = b and b = c.

Kernel evidence: Replaces the hole by EqTrans(left-hole, right-hole); a ? midpoint is one shared metavariable in both holes.

Complete executable example:

pa prove 0 = 1 -> 1 = 0 -> 0 = 0
intro h01
intro h10
trans 1
exact h01
exact h10
qed
Common mistakes and failure modes
  • The goal is not an equality or the middle term is missing/malformed.
  • A metavariable midpoint must be consistently solved across both subgoals.

Witnesses and scoped metavariables · Open this interactive tactic card

congr · Reduce equality of matching arithmetic constructors to their arguments.

Used in the quadratic-reciprocity proof corpus

Syntax: congr

Goal effect: S a = S b makes one goal a = b; a+b = c+d and a*b = c*d each make two.

Kernel evidence: Inserts CongS, CongAdd, or CongMul with one hole per component equality.

Complete executable example:

pa prove forall n m. n = m -> S n = S m
intro n
intro m
intro h
congr
exact h
qed
Common mistakes and failure modes
  • The focused target is not an equality.
  • The two sides do not share the same outer constructor S, +, or *.

Goals, holes, and proof constructors · Open this interactive tactic card

exact · Close the goal with one named context hypothesis.

Used in the quadratic-reciprocity proof corpus

Syntax: exact <hypothesis>

Goal effect: Removes the focused goal when the hypothesis formula unifies with it.

Kernel evidence: Replaces the hole by Hyp(index) and propagates any shared-meta solution.

Complete executable example:

pa prove 0 = 0 -> 0 = 0
intro h
exact h
qed
Common mistakes and failure modes
  • The command needs exactly one existing hypothesis name.
  • The named hypothesis does not match the current goal.

Goals, holes, and proof constructors · Open this interactive tactic card

assumption · Close with the first context hypothesis that matches the goal.

Available in Peano Lab; not used in this proof slice

Syntax: assumption

Goal effect: Scans the context deterministically from newest to oldest and removes the goal.

Kernel evidence: Inserts the matching Hyp(index), with proof-wide metavariable propagation.

Complete executable example:

pa prove 1 = 1 -> 1 = 1
intro h
assumption
qed
Common mistakes and failure modes
  • No context hypothesis matches the current goal.
  • The tactic accepts no hypothesis name; use exact h to choose explicitly.

Goals, holes, and proof constructors · Open this interactive tactic card

rewrite · Rewrite the first eligible occurrence using a context equation or PA axiom.

Used in the quadratic-reciprocity proof corpus

Syntax: rewrite [<-] <equation> [at <hypothesis>]

Goal effect: Without at, changes the goal; with at h, adds a rewritten version of h to the context. The <- marker reverses the selected equation.

Kernel evidence: Builds EqSubst with an explicit motive and equality proof. Rewriting a hypothesis additionally uses a local implication cut.

Complete executable example:

pa prove forall n. n = 0 -> S n = S 0
intro n
intro h
rewrite h
refl
qed
Common mistakes and failure modes
  • The equation is unknown, non-equational, or has no occurrence in that direction.
  • Rewriting is refused when it would cross a quantifier unsafely or metas remain.

Equality transport and simplification · Open this interactive tactic card

simp · Normalize with ordered PA3-PA6 rewrites plus explicitly named equations.

Used in the quadratic-reciprocity proof corpus

Syntax: simp [<equation-hypothesis>, <- <equation-hypothesis>, ...]

Goal effect: Simplifies the target deterministically. It closes a reflexive, exact, or structurally congruent equality normal form; otherwise one simplified goal remains.

Kernel evidence: Records every rewrite as EqSubst, adds ForallIntro when simplifying under leading quantifiers, and ends in EqRefl, Hyp, CongS/CongAdd/CongMul, or a hole.

Complete executable example:

pa prove forall n. n = 0 -> S n = S 0
intro n
intro h
simp [h]
qed
Common mistakes and failure modes
  • An explicit lemma is missing, duplicated, non-equational, or badly oriented.
  • The command fails transactionally if no rewrite or closing step makes progress.

Equality transport and simplification · Open this interactive tactic card

undo · Restore the exact proof state before the latest successful command.

Available in Peano Lab; not used in this proof slice

Syntax: undo

Goal effect: Restores goals, substitutions, certificate holes, and earlier history exactly.

Kernel evidence: Discards the most recent transaction's certificate changes; it creates no kernel proof node of its own.

Complete executable example:

pa prove 0 = 0
refl
undo
refl
qed
Common mistakes and failure modes
  • There is no successful history entry to restore.
  • Undo is a complete-line session command and cannot be nested in a tactical.

Transactional states and undo · Open this interactive tactic card

use · Bring one independently checked library theorem into the focused context.

Available in Peano Lab; not used in this proof slice

Syntax: use <library-theorem> [as <alias>]

Goal effect: Adds the closed theorem under its canonical name or a fresh chosen alias; ordinary specialize, apply, rewrite, exact, and simp commands can then use it.

Kernel evidence: Inserts a local implication cut backed by the theorem's closed certificate. QED contracts exposed cuts and checks the resulting closed proof against the original goal; the kernel never trusts theorem names.

Complete executable example:

pa prove forall n m. n + m = m + n
use add_comm
exact add_comm
qed
Common mistakes and failure modes
  • The library theorem is unknown or its replay certificate fails checking.
  • The alias is malformed or already names a variable or hypothesis.
  • The imported or live certificate exceeds its explicit node/depth budget.

Checked theorem reuse, without a theorem oracle · Open this interactive tactic card

Tactical composition and goal selection · 6

A tactical combines existing proof-building steps; it adds no kernel inference rule. Sequencing, alternatives, repetition, first-success search, all-goal traversal, and focused execution retain exact goal-to-certificate-hole correspondence and roll back failed transactions.

; · Run the right tactic on every goal created by the left tactic.

Available in Peano Lab; not used in this proof slice

Syntax: <tactic-1> ; <tactic-2>

Goal effect: The left tactic runs on the focus; each of its newly created goals then receives the right tactic, in order.

Kernel evidence: Splices the child certificates into their exact holes and publishes the whole compound command as one undo transaction.

Complete executable example:

pa prove 0 = 0 /\ 1 = 1
split; refl
qed
Common mistakes and failure modes
  • Either side is empty or grouping is unbalanced.
  • If any child fails, the entire compound command leaves the state unchanged.

How tactical composition works · Open this interactive tactic card

<|> · Try the left tactic, falling back on ordinary failure while malformed input aborts.

Available in Peano Lab; not used in this proof slice

Syntax: <tactic-1> <|> <tactic-2>

Goal effect: Publishes the left result when it succeeds; otherwise runs the right tactic on the exact original snapshot.

Kernel evidence: Keeps only the successful branch certificate and records one outer undo transaction.

Complete executable example:

pa prove 0 = 0
assumption <|> refl
qed
Common mistakes and failure modes
  • Either side is empty or grouping is unbalanced.
  • If both branches fail, the complete alternative fails without state leakage.

How tactical composition works · Open this interactive tactic card

repeat · Run a tactic until ordinary failure, no logical progress, or a revisited state.

Available in Peano Lab; not used in this proof slice

Syntax: repeat <tactic>

Goal effect: Applies the child repeatedly to the focused evolving state; the expected final failure is the stopping condition, not a failure of repeat.

Kernel evidence: Combines all successful child certificate edits into one transaction. A 256-step guard prevents runaway growth.

Complete executable example:

pa prove 0 = 0 -> 0 = 0
repeat intro
assumption
qed
Common mistakes and failure modes
  • The child tactic is missing.
  • Syntax and resource-limit errors propagate instead of pretending repeat succeeded.
  • A child that evades cycle detection for 256 steps triggers the termination guard.

How tactical composition works · Open this interactive tactic card

first · Run the first tactic in a left-to-right list that succeeds.

Available in Peano Lab; not used in this proof slice

Syntax: first [<tactic> | <tactic> | ...]

Goal effect: Each failed choice sees the same original state; the first success becomes visible.

Kernel evidence: Retains only the winning child certificate and collapses it to one undo transaction.

Complete executable example:

pa prove 0 = 0
first [assumption | refl]
qed
Common mistakes and failure modes
  • The brackets or choices are missing, empty, or unbalanced.
  • If every choice fails, first reports the last error and restores the snapshot.

How tactical composition works · Open this interactive tactic card

all_goals · Apply a tactic once to every goal that exists when the command begins.

Available in Peano Lab; not used in this proof slice

Syntax: all_goals <tactic>

Goal effect: Visits entry goals in order. New subgoals made by the child are preserved but are not recursively revisited by this same all_goals command.

Kernel evidence: Splices each child certificate at its original hole and publishes one transaction.

Complete executable example:

pa prove 0 = 0 /\ 1 = 1
split
all_goals refl
qed
Common mistakes and failure modes
  • The child tactic is missing.
  • Failure on any visited goal rolls back successes on all earlier goals.

How tactical composition works · Open this interactive tactic card

focus · Run one tactic on one selected goal without reordering the goal list.

Available in Peano Lab; not used in this proof slice

Syntax: focus <positive-goal-number> <tactic>

Goal effect: Uses one-based numbering from the displayed panel and leaves every other goal at its original position.

Kernel evidence: Runs the child against the selected certificate hole, then splices its result back into that exact position as one transaction.

Complete executable example:

pa prove 0 = 0 /\ 1 = 1
split
focus 2 refl
refl
qed
Common mistakes and failure modes
  • The goal number is missing, zero, negative, or outside the current list.
  • The selected child failure leaves every goal and hole unchanged.

How tactical composition works · Open this interactive tactic card

Why one tactical expression is one transaction

Checked arithmetic, bounded search, and advice · 5

Automation computes or searches, then constructs ordinary independently checked evidence. A bounded failure means only that this attempt exceeded its supported search or resource policy; it never proves a statement impossible. Advisory hint changes neither the goal nor the certificate.

norm_num · Normalize closed arithmetic inside an equality with checked certificates.

Used in the quadratic-reciprocity proof corpus

Syntax: norm_num

Goal effect: Replaces maximal variable-free subterms by canonical numerals in a fixed left-to-right order. It closes the goal when the normalized sides coincide; otherwise one normalized equality goal remains.

Kernel evidence: Checks a PA3-PA6 proof for every calculation and lifts those proofs through term congruence. The equality bridge is checked from either the empty context or exactly one normalized residual assumption.

Complete executable example:

pa prove forall n. n + (2 * 3) = n + 6
intro n
norm_num
qed
Common mistakes and failure modes
  • After optional leading forall binders, the goal is not an equality or contains an unresolved term metavariable.
  • Norm_num takes no arguments and never mines hypotheses for arithmetic facts.
  • A false closed equation, non-closing no-progress request, or an explicit input, value, work, proof, or time limit stops transactionally.

Checked arithmetic and advisory automation · Open this interactive tactic card

ring · Close an unconditional polynomial identity with a checked certificate.

Available in Peano Lab; not used in this proof slice

Syntax: ring

Goal effect: Reifies 0, successors, variables, addition, and multiplication into one deterministic sparse polynomial form and closes the goal only when both sides have the same form.

Kernel evidence: Builds an equality proof from independently checked commutative-semiring lemmas, reduces their proof-level beta redexes, and asks the kernel to check the generated certificate before changing the state.

Complete executable example:

pa prove forall n m. n + m = m + n
intro n
intro m
ring
qed
Common mistakes and failure modes
  • The focused goal is not an equality or still contains a term metavariable.
  • Ring takes no arguments; use trans and rewrite explicitly when a hypothesis matters.
  • Different normal forms or an explicit size, work, depth, or time limit stop transactionally.

Checked arithmetic and advisory automation · Open this interactive tactic card

compact_arith · Close a supported PA equality with a small, independently checked certificate.

Available in Peano Lab; not used in this proof slice

Syntax: compact_arith [equation, <- equation, ...]

Goal effect: Searches a bounded deterministic family of successor, addition, multiplication, and doubling recurrences. Only equations named explicitly in brackets may be used; the matching compact_arith? command previews a candidate without changing the goal.

Kernel evidence: Chooses the least-cost proof-tree candidate generated by this bounded attempt, constructs ordinary PA proof nodes, and asks the independent kernel to check the fragment before committing.

Complete executable example:

pa prove forall n. n + 1 = S n
intro n
compact_arith
qed
Common mistakes and failure modes
  • The focused goal is not a rigid equality, or a named assumption is not an equation.
  • No certificate was found in the bounded supported family; this is not an unprovability result.
  • A work, proof-size, depth, time, or host-recursion limit stops transactionally.

The compact arithmetic contract · Open this interactive tactic card

auto · Search a bounded deterministic tree and replay a certificate-valid primitive plan.

Available in Peano Lab; not used in this proof slice

Syntax: auto [positive-depth]

Goal effect: On success, closes the goals found by the winning plan. Exhausting a depth or node bound is reported as a limit, never as an unprovability result.

Kernel evidence: Speculative branches publish nothing. Only the winning ordinary primitive steps are replayed, and QED still invokes the independent kernel checker afterward.

Complete executable example:

pa prove forall n. 0 + n = n
auto 5
qed
Common mistakes and failure modes
  • Depth must be a positive integer; the default is 5.
  • No plan was found in the finite search or a depth/node bound was reached.

Bounded proof search and replay · Open this interactive tactic card

hint · Inspect the focused goal and suggest one supported immediate command.

Available in Peano Lab; not used in this proof slice

Syntax: hint

Goal effect: Does not change any goal. Its found, none, and limit statuses are deliberately advisory and never claim that a theorem is provable or unprovable.

Kernel evidence: Creates no certificate node and does not append proof history.

Complete executable example:

pa prove 0 = 0
hint
refl
qed
Common mistakes and failure modes
  • A limit status means inspection stopped; it is not a negative proof result.
  • The suggestion is text only and must still be executed and kernel-checked.

Checked arithmetic and advisory automation · Open this interactive tactic card

Why these commands are not decision procedures for all arithmetic

Read one complete proof from source text to kernel evidence

pa prove forall n. n + 0 = n
intro n
rewrite PA3
refl
qed

intro n contributes ForallIntro. rewrite PA3 specializes the checked PA3 constant with ForallElim and transports the equality using EqSubst. Finally, refl supplies EqRefl. Only qed asks the independent kernel to check the completed certificate against the original universal formula.

See the proof-state and transport explanation · Continue with a complete hand proof of addition commutativity · Open the live Peano proof lab

Where to go next