2
$\begingroup$

How are the fundamental approaches to proving theorems by LCF and Automath different? Considering their modern descendants - Isabelle for LCF and Coq for Automath, both rely on type checking to do proof checking.

Theorems in Isabelle have a theorem type and the only functions that can create instances of this theorem type are inference rules of the logic.

Theorems in Coq have a Prop type and the only way to create Props is by creating proof terms that have the proposition as their types.

If I'm not wrong, LCF and Automath were developed independently around the same time so there wasn't an influence from one to the other, but perhaps by coincidence, is LCF's (Isabelle's) Theorem just a more generic version of Automath's (Coq's) Prop?

I would appreciate it if you could also point out any other fundamental differences between LCF and Automath that have manifested into their modern successors.

$\endgroup$
1
$\begingroup$

The difference is in what kind of type theorem/Prop is.

In Isabelle, theorem is a type in the underlying implementation language, that is made abstract so that the only way to create an inhabitant of that type (i.e. a valid theorem) is in the end to resort to the primitives provided by the kernel. So it is the typing constraints of the implementation language together with the restricted primitives that forces you to inhabit only correct theorems. Also, in that setting proofs can be any program in the implementation language producing an object of type theorem, but they have no specific status, and cannot be manipulated directly.

On the contrary, Prop is a type in the theory of Coq, but not in its implementation language: if you look at the OCaml code, there is no such thing as a Prop type, only a type of terms. Verifying that a term (written in a specific language called Gallina, the proof/programming language of Coq) is indeed a valid proof is a job of a specific type-checker. This type-checker is the kernel. In that setting, proofs have a specific status, being syntactical objects of a given type of terms in the implementation, and as such can be manipulated, inspected and so on. In particular, the tactic languages are used to generate such proofs, which is not the same as directly constructing an inhabitant of theorem, because such terms will still in the end be inspected by the kernel, which is the only judge of what is a valid proof.

$\endgroup$
4
  • $\begingroup$ Thanks for the answer! Can you expand a little bit on how proofs cannot be manipulated directly in Isabelle, but can be in Coq? Perhaps a simple example? $\endgroup$ Jan 25 at 15:43
  • $\begingroup$ As for Coq, this manipulation is only accessible to advanced users, because you need to be able to play with the OCaml code of the kernel of Coq. But for instance the unification machinerie that is used to elaborate terms from the input syntax into terms acceptable for the kernel manipulates those as syntax trees, and can do things like reducing them, matching on their shape, and so on. Whereas in Isabelle, the type of proofs is by design not accessible, so for instance given a proof you cannot inspect how it was constructed. $\endgroup$ Jan 26 at 16:14
  • $\begingroup$ Thanks! I'm surprised the Prop sort isn't defined in Coq's OCaml code. Is it defined in Gallina then? Do you know where and how its defined? $\endgroup$ Feb 3 at 14:58
  • 1
    $\begingroup$ Prop is defined in the OCaml code, but it is not an OCaml type. Instead, it is a type at the level of Gallina. $\endgroup$ Feb 4 at 17:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.