Proof Checker Pro

End punctuation is optional. References are optional when the compiler can infer exactly which earlier lines you mean.

• Declare an inductive type with inductive BinaryTree, one constructor per line, and end. Constructor fields use forms such as InternalNode(left: BinaryTree, right: BinaryTree).
• Define a structurally recursive function with recursive count(tree: BinaryTree): Natural, one constructor equation per line, and end. Use by definition of count to unfold one equation in a proof.
• Induct on t begins structural induction for a universal goal over a declared inductive type. Open a nonrecursive constructor with BaseCase Leaf and a recursive constructor with InductiveCase InternalNode(Left, Right).
• Immediately after an inductive case, write For induction assume:, followed by exactly one induction hypothesis for each immediate recursive part. The hypotheses become numbered proof lines.
• Close a constructor case with therefore P(InternalNode(Left, Right)) by induction case. After every constructor is complete, close with therefore (∀ t in BinaryTrees)P(t) by induction.
• Pretend Bob is a Creature or Let Bob be an arbitrary Creature opens an arbitrary-object world.
• Pretend X, Y are Numbers or Let X, Y be arbitrary Numbers opens several arbitrary-object worlds at once.
• Make believe S(Bob) or Assume S(Bob) opens a make-believe world.
• S(Bob) → M(Bob) by UI I applies a rule and cites an axiom.
• X < Y → F(X) < F(Y) by UI may instantiate several leading quantifiers at once; the source reference may be omitted when it is unambiguous.
• M(Bob) by detachment 2, 3 cites proof lines.
• therefore S(Bob) → V(Bob) by MB 6 closes a make-believe world.
• therefore (∀ c in Creatures)(S(c) → V(c)) by UG 7 closes an arbitrary-object world.
• Pretend Ari is a witness with P(Ari) by EI I or Let Ari be a witness such that P(Ari) opens an existential-witness world.
• 2(2J^2 + 2J) + 1 = N^2 by algebra checks polynomial algebra, using available equations such as 2J + 1 = N.
• For contradiction assume ¬P opens a pretend world and changes the current goal to Contradiction. After deriving one, therefore P by contradiction closes the world.
• Contradiction from lines 4, 7 is valid when one cited line negates the other, including complementary comparisons such as X < Y and X ≥ Y. Write simply Contradiction when there is only one contradictory pair available.
• Case 1: Make believe P by cases III opens the first branch of a proof by cases. Nested branches may use labels such as Case 1a and Case 1b.
• After establishing the goal in a branch, therefore R by case finishes that branch. Finish Case 1a before beginning Case 1b.
• After both sibling branches are finished, therefore R by cases III combines them; the checker finds the two matching branch conclusions.

Compiler convention: quantified variables and definition parameters begin lowercase; introduced individuals such as Bob begin uppercase. A quantifier may omit its type when the surrounding proof determines it; two explicitly different types still conflict.

Several variables may share a quantifier, as in (∀ x, y)(x < y → F(x) < F(y)). Function terms may be nested, as in F(G(x)). Definitions may have several parameters, as in Between(x, y, z).

Other rule names: EI, EG, and introduction, and elimination, or introduction, case, cases, De Morgan, double negation, iff introduction, and iff elimination.

Shorthand becomes notation as you type: \forall, \exists, \neg, \not, /\, \/, ->, <->, <=, and >=. The words and and or are also accepted inside formulas.