TPS A higher-order theorem proving system
This page was created and is maintained by Chad E Brown.
Landau, Grundlagen der Analysis, Alternate Formal Versions
Below are links to different formal developments corresponding to Jutting's Automath encoding of Landau's Grundlagen der Analysis. A tar file containing the Automath files and tex files is available here.
Coq Versions
In 2009, I (Chad) ported the Grundlagen encoding to Coq. There are four versions available. They are available landau-coq.tar.gz.- Version 1: This version is the closest to the Automath version. The elements that were left primitive in Automath are also left primitive here. Aut-QE's Type is mapped to Coq's Type, and Aut-QE's Prop is mapped to Coq's Prop,
- Version 2: This is the same as version 1 except Aut-QE's Prop is mapped to Coq's Type. This demonstrates that impredicativity of Prop is not used.
- Version 3: This is like version 1 except most of the primitives have been defined in Coq. The only primitives that remain correspond to classical logic, extensionality principles, (definite) description, and proof irrelevance.
- Version 4: This is like version 3 except we assume classical logic, extensionality principles and proof irrelevance. After assuming these, all the remaining primitives can be defined.
Grundlagen Browser
You can now use your browser to examine the encoding of the Grundlagen in its original Automath form and in its Coq form. The names are long because I removed the sectioning (paragraaf) features from Automath and for my names I used a combination of the sections and subsections combined with the name. If you know part of the name Jutting used in his encoding, then you can search for it and click on the appropriate result. For example, searching for satz2 (Theorem 2) returns a long list of theorems. Clicking on the first result ( l_e_st_eq_landau_n_satz2) displays Theorem 2 in three formats: the Coq version, an Automath version with minimized contexts and the original Automath version. Both of them are shown using HTML math symbols, but you can change the output style to show them in a format similar to Coq, Twelf or Automath. Theorem 2 says that no positive integer (nat) is equal to its own successor (suc). The proof is by induction, and this is reflected by the fact that the head of the proof term contains an element named induction. In each version there is a button "Interactive Checker." Clicking on this button calls server side code to type check modulo some β-, δ-, and η-equivalences. If there are any leftover equivalences, the user is asked to verify the equivalences by expanding definitions (δ-reduction) and doing β- and η-reductions by hand. The way to do a reduction is to put your mouse over the redex (but not over a hyperlink) and click. Each signature element is hyperlinked to a page describing that signature element. For some signature elements, there are three versions shown: the Coq version, an Automath version with a minimized context, and the original Automath version. For the signature elements with the contexts cannot be minized, the Automath math version with minimized contexts is not shown. About half of Jutting's definitions included variables in the context of the definition that were not used in the type or the definition. I removed these extra context dependencies before translating to different versions (e.g., the version in Coq). For a concrete example, see some_t1.Simply Typed Version
In 2005, I (Chad) wrote lisp code to parse the Automath version in order to port the encoding. Using this, I automatically generated alternative Automath versions, including an Automath version without implicit arguments, where contexts are always freshly declared, there is only one big paragraaf and dependencies on arguments are reduced . I once had HTML pages giving the details of the simply typed version online, but the files are huge. If you want to see these details, please download this (1M) gzip'd tar file. It will expand into a (23M) directory called landau-tps which will contain HTML files. Start by having your browser view landau-tps/landau-tps.html. To get an idea of how the details look, click here.
HOTPTP Version
There is now a version of the original Automath encoding in the hotptp format. Click here for the gzipped file. A corresponding Automath version is here (gzipped).
Simply Typed Version in Detail
I also translated the Automath code into simply-typed lambda-terms as abbreviations. This page provides access to this simply-typed version. The syntax corresponds TPS in GENERIC mode. In principle, one should be able to copy formulas from this page and paste them directly into TPS.
Proof terms were not translated. Any dependence on proof terms was translated away. In particular, all theorems were translated without proof. One reason I made the translation was as a challenge to systems such as Omega and TPS. In these systems, one should be able to reconstruct the proofs interactively, automatically or in a mixture of these modes.
Automath types were translated as partial equivalence relations (pers) over simple types. Certain abbreviations for pers are used.
I assumed the base type I satisfies the Peano Axioms. I also assumed the existence of two basic constants _1 of type I and _SUC of type (II). The Automath type _NAT corresponds to the type I (or technically, as a per, the equality relation on I).
The only axioms after translation are description (at every type) and the Peano Axioms at type (I). The particular version of description is given by _ONEAX. The Peano Axioms are _AX3, _AX4, and _AX5 (induction, not to be confused with the theorem _INDUCTION). Interestingly, we do not need an axiom of choice, axiom of Boolean extensionality or axioms of functional extensionality. The Automath encoding does not use axioms of choice or Boolean extensionality. The Automath encoding DOES use axioms of functional extensionality (see _FISI) which translates into a theorem since we interpret function types as function pers, which are extensional even if the underlying function types are not extensional.
IF the translation is correct, THEN each theorem should be provable using only description and the Peano Axioms.
TPS A higher-order theorem proving system