Overview of commands for OpenTheory article files
1. Deduction Rules
- Equality is reflexive, symmetric, and transitive (for any type):
- Carry equality to more complicated terms
- Replace a statement by an equivalent statement:
applied to an argument is equal to the result of substituting the argument:
Rules about the relation between hypotheses and conclusion
- Implication is transitive.
- Implication is antisymmetric.
Mutual implication implies equivalence.
- Implication is reflexive. A statement implies itself.
Substitute type variables and free term variables by specific values
Interface with other packages or articles
The assumptions and theorems generated in this way are the result of
reading the article. If the article was processed without error, this
means that the theorems can be deduced from the assumptions.
- Introduce an assumption, which can be an unproved axiom or a statement to be proved in another article and to be
imported from there:
- Mark a theorem that has been derived for export, to be listed as a result of the theory or to be used in other articles:
Other commands that create theorems (see below)
Variables are characterized by name and type.
Constants can be of three kinds:
- A constant can be introduced by giving just a name, with the
intention of referring to a constant defined in another package or article.
- A constant can be introduced as an abbreviation for another more
Its definition becomes a theorem, and
it can be used in other packages or articles.
constants can be defined simultaneously, and this is combined with a substitution in a
the defineTypeOp operation,
two constants for the representation and abstraction function (rep and
When a constant of the second and third category is defined,
a Const object is generated on the stack.
To use such a constant several times, this object
must be saved to the dictionary and retrieved from there.
When comparing two terms for α-equivalence,
constants of the first category are considered equal if they have the
same name (and type).
Constants of the second category are considered equal if they have the
same name and were introduced with the same definition (up to
α-equivalence?) including identical types.
Constants of the third category are considered equal if they originate
from the same defineTypeOp operation?
(and have the same type).
Constants of different categories are never considered equal.
It is possible to define and use different constants with the same name. However
it is illegal to use two or more such constants which are not equal by
the above rules in
the assumptions and theorems that are the result of
reading the article.
The basic building blocks for terms are variables and constants.
To use them in a term, use the following commands:
Build more complicated terms
Such a term is either a λ-abstraction
or an application "f A":
Types are built up from more elementary types by using
type operators. Type variables and nullary type operators are used as the basic building
blocks. The following command applies a type operator to its argument
Similar as for constants, there are two ways to make a type operator:
The rules governing the use of such defined type
operators and the comparison between them are analogous to
the rules for constants.
- By name
- By an explicit definition
This definition implicitly defines also two constants rep
and abs, as mentioned above.
6. The dictionary and the stack; lists, strings, and numbers
Entries from the top of the stack can be stored in the dictionary
and later retrieved from there (either keeping them in the dictionary or removing them).
Lists are used to build parameters for other commands such as
the arguments of type operators or the elements of a substitution.
Deconstruction into head and tail:
are used as names for variables, constants, type variables,
and type operators;
in addition, they can be arguments for
the pragma command.
are used as indices into the dictionary; and
as an argument of the version command.
(In addition, they might be arguments for
the pragma command in future versions.)
7. Directives for the article reader
Günter Rote, Aug 2015