Getting Started with the CalcCheck Language

This page tries to help you getting started with writing formal proofs in the CalcCheck langauge. For help with the CalcCheckWeb web-app interface, see Getting Started with CalcCheckWeb.

Example (if this does not display correctly, choose Unicode (UTF-8) character encoding in your browser):

Theorem (15.17) “Self-inverse of unary minus”: - (- a) = a
Proof:
    - (- a)
  =⟨ “Identity of +” ⟩
    0 + - (- a)
  =⟨ “Unary minus” ⟩
    a + (- a) + - (- a)
  =⟨ “Unary minus” ⟩
    a + 0
  =⟨ “Identity of +” ⟩
    a

1. The keywords Thoerem and Proof are not indented at all.
2. Everything that is part of the theorem needs to be either after the keyword Theorem, or indented by at least two spaces on the following lines.
3. Proofs by calculation start on the line after the “Proof:”, and every part of the calculation needs to be indented by at least two spaces.
4. An equational calculation consists of a sequence of expressions, each on a line (or several lines) of it own, and these expressions are separated by hint lines
5. A hint line contains an equality symbol (later also other symbols, generally called calculation operator) followed by a hint enclosed in angle brackets ⟨ and ⟩. (There may be spaces between the calculation operator and the hint-opening bracket.)

   The hint inside is surrounded by spaces: There needs to be at least one space after the opening hint bracket, and at least one space before the closing hint bracket.

   The whole hint, including the hint-closing bracket, has to be indented at least two spaces beyond the indentation of the calculation operator.

6. The expressions in a calculation need to be indented at least two spaces more than the equality symbols of the hint lines.
7. The recommended style for calculations is to indent the hint lines by two spaces, and indent the expression lines by four spaces.
8. The hints between the hint brackets ⟨ and ⟩ are non-empty sequences of hint items, separated by commas or by “and”.

   In the beginning, each hint is restrict to contain only one hint item.

   Simple hint items are:

   • Theorem numbers following the style of LADM are delimited by parentheses and consist of numbers, dots, and occasional letters. Examples: (15.17), (15.25a). The enclosure always consists of round parentheses, and there are never any space characters inside.
   • Theorem names are delimited by opening and closing double quote characters “ and ”.
   • Simple keyword hint items, such as Substitution
   • Hint items of shape Fact `expr`, where expr is a variable-free Boolean expression that evaluates to true in the current setting.
   • Simple key phrase hint items, such as Induction hypothesis.
9. For information about how to input all these special characters in CalcCheckWeb, see Getting Started with CalcCheckWeb.
10. Multi-letter variable names are supported in a rather liberal way. Therefore, spaces around operators are necessary almost everywhere.