Prover playgroundMilestone 4 · Proof by cases

Check every step.

Build a candidate, inspect its evidence, and ask the kernel to check it. Explore implication, conjunction, disjunction, falsity, and constructive negation.

Theorem statement

Outer context: ∅
A A

Hover over or focus an operator to underline each of its arguments.

Assume A, use that assumption, then discharge it. The final theorem has no open assumptions.

Inspect the proposition AST

This tree describes the statement. Negation ¬P expands to P → ⊥; the core AST has no negation node. The proof AST below describes the evidence offered for the statement.

{
  "kind": "implies",
  "from": {
    "kind": "atom",
    "name": "A"
  },
  "to": {
    "kind": "atom",
    "name": "A"
  }
}

Builder code

Untrusted constructors
intro("h", atom("A"),
  use("h")
)

This constructor expression describes the generated candidate below. Helpers create AST nodes; they cannot grant acceptance. The display is not an editable script.

Generated candidate
Inspect the generated AST
{
  "kind": "implies-intro",
  "assumption": {
    "id": "h",
    "proposition": {
      "kind": "atom",
      "name": "A"
    }
  },
  "body": {
    "kind": "assumption",
    "id": "h"
  }
}

Kernel result

Checked against the requested theorem

Not checked

Choose an example and press Check proof. A displayed candidate is not a checked theorem.

construct candidates. The checks assumption scope, each inference, and the requested conclusion. This constructive kernel supports atoms, implication, conjunction, disjunction, and falsity. Negation is shorthand; classical axioms, proof editing, and search come later.

Review the trust boundaryExplore conjunction and derived rulesExplore falsity and negationExplore disjunction and proof by cases
Reference: Proof AST. Abstract syntax tree.