The framework of proofgold is intuitionistic higher-order logic. This consists of a collection of simple types, simply typed terms and Curry-Howard style proof terms. A quick summary is given by the following grammar:
| Types (α, β) | ::= | Prop | Base n | (α → β) |
| Terms (s, t) | ::= | x | Prim n | (s t) | (λ x:α . t) | (s → t) | (∀ x:α . t) | (∃ x:α . t) | (s =α t) |
| Proofs (D, E) | ::= | u | Known s | (D E) | (D t) | (λ u:s . D) | (λ x:α . D) | (Ext α β) |
In the implementation there is an additional term case that references a term by its hashroot. Also, the term in the Known proof case is always referenced by the hash root of the (allegedly) known proposition. A proposition can be known because it is an axiom of the current theory or if it has been proven in the theory.
The last two term cases (∃ and =) are included only for convenience and as part of normalization ∃ and = are expanded away as follows:
| (∃ x:α . s) | expands to | (∀ p:Prop . (∀ x:α . s → p) → p) |
| (s =α t) | expands to | (∀ q:α → α → Prop. q s t → q t s) |
The proof terms have the standard Curry Howard meaning. The last case (Ext α β) corresponds to functional extensionality. For two types α and β, (Ext α β) is a proof term for (∀ f g : α → β . (∀ x : α . f x =β g x) → (f =α → β g)).
Proofgold can read drafts of documents (and signatures and theories) using a basic "assembly" language (using prefix notation). See the commands readdraft, commitdraft and publishdraft. This assembly language is summarized below.
If Base types will be used, then the text should
declare names for them as follows:
Base base0
...
Base basen-1
After this types can be written as follows:
| Assembly | Informal |
|---|---|
| Prop | Prop |
| basen | Base n |
| TpArr α β | (α → β) |
Closed terms that will be used often can be abbreviated
by Let declarations, as follows:
Let letname : α := s
The Let declarations are completely transparent and
are expanded away while reading the specification.
Proper definitions are declared as follows:
Def defname : α := s
These definitions are associated with the hash root of the
term s and this hash root is used when reading
specified terms.
Opaque definitions can also be declared by referencing the
hash root. This assumes
the definition has already been made and published in a
previous document.
Param hashroot defname : α
Terms can be specified as follows:
| Assembly | Informal |
|---|---|
| letname | (term declared using Let earlier) |
| defname | (term hash root declared using Def or Param earlier) |
| x | x (local variable in the scope of λ, ∀ or ∃) |
| Prim n | Prim n |
| Ap s t | (s t) |
| Lam x α t | (λ x : α . t) |
| Imp s t | (s → t) |
| All x α t | (∀ x : α . t) |
| Ex x α t | (∃ x : α . t) |
| Eq α s t | (s =α t) |
Axioms and previously proven theorems can be locally declared as follows:
Known knownname : s
The hash root of s is computed and checked to be in the collection
of already known propositions.
Proofs are specified as follows:
| Assembly | Informal |
|---|---|
| knownname | (declared using Known earlier) |
| u | u (proof variable in the scope of a λ) |
| PrAp D E | (D E) |
| TmAp D t | (D t) |
| PrLa u s D | (λ u : s . D) |
| TmLa x α D | (λ x : α . D) |
| Ext α β | (Ext α β) |