Petros Papapanagiotou
Jacques Fleuriot
Artificial Intelligence Modelling Lab
Artificial Intelligence and its Applications Institute
School of Informatics, University of Edinburgh
This is a generic framework to perform object level reasoning with logics encoded in HOL Light.
It provides procedural tactics inspired by Isabelle's rule/erule/drule/frule.
It also supports correspondences with computational terms in the style of Curry-Howard.
An online tutorial with simple examples can be found HERE.
Further information and background will be provided in a forthcoming publication.
Assuming you have an inductively defined logic encoded in HOL, the library allows you to prove object level theorems within your embedded logic. All the boilerplate around rule matching and meta-level term management is taken care of automatically without any additional coding.
Assuming an encoding of a constructive correspondence of a logic to some computational calculus (in the style of Curry-Howard) the library additionally automates the construction of the terms as the proof progresses. This is accomplished through the use of metavariables and delayed instantiation.
In effect, this allows the construction of any program via proof using any logic correspondence that can be embedded in HOL Light in the ways described below.
It is worth noting that the tactics can be used programmatically as well, e.g. towards automated proof tools for the encoded logic.
It does not allow you to perform any meta-level reasoning (such as cut-elimination proofs), as the derivation semantics of the encoded logic are mapped to HOL implication. At this level it is not possible to reason about the semantics of the encoded logic.
The framework can run on top of a running HOL Light instance as any library. It does have certain dependencies as described below.
Essential requirements for the software to run:
- OCaml 4.07.0 minimum. The easiest way to install this is through opam.
- The HOL Light theorem prover. It comes with its own installation instructions.
The framework depends on the following HOL Light libraries:
- The Isabelle Light library. This also comes bundled with HOL Light by default.
- Additional HOL Light tools. This consists of snippets of code and libraries I have implemented. Although some of these were implemented in parallel to this project, they have a more general function and so are kept separately.
The fastest way to install is by checking out this fork of HOL Light:
git clone https://github.com/PetrosPapapa/hol-light.git
The fork contains the required libraries as submodules which can be checked out as follows:
git submodule update --init --recursive
Note, however, that the fork includes additional submodules from other projects, some of which may be private. This will result in errors when updating the submodules, but does not affect this particular library.
You can then follow the standard HOL Light installation instructions as you would with the regular HOL Light repository.
If you already have HOL Light up and running and want to add this library, you will need to clone the 2 required repositories as follows:
cd hol-light/
git clone https://github.com/PetrosPapapa/hol-light-tools.git tools
git clone https://github.com/PetrosPapapa/hol-light-embed.git embed
Once HOL Light is up and running and the library is installed, you can load it with the following command:
loads ("embed/sequent.ml");;The usage information below highlights the main available tools and functionality. This is much easier to follow in the context of the examples provided:
- Examples/CurryHoward.ml contains 2 encodings. The first one is a subset of propositional logic involving only conjunction and implication. The second is the Curry-Howard correspondence for the same logic. Some example interactive proofs are also included. The 2 embeddings can be contrasted to show how the same proofs can work with or without a computational correspondence. A full online tutorial explaining these encodings can be found HERE.
- Examples/ILL.ml includes a simple encoding of Intuitionistic Linear Logic and some packaged proofs.
- Examples/pas/ includes an encoding of the Propositions-as-Sessions correspondence described in this paper by Philip Wadler. This is a correspondence between Classical Linear Logic and a session type calculus named CP. The example also includes the implementation of some automated proof procedures for Classical Linear Logic to demonstrate how the tactics can be used programmatically. Example proofs can be found in Examples/pas/examples.ml.
The library can be used to perform object level reasoning with embedded logics. The examples provided above can put much of this information in context.
An online tutorial explaining the Curry Howard example can be found HERE.
A typical way of encoding a logic in HOL Light is through an inductive definition of its inference rules using new_inductive_definition. This involves the definition of a consequence operator (turnstile). Valid derivations are defined inductively using standard (classical) HOL implication.
The library currently only supports a sequent calculus style, although we have plans for a natural deduction setup in the future. It supports one-sided, two-sided, classical, and intuitionistic (single conclusion) sequents.
Although sequent parts can be modelled arbitrarily, the library provides extended support for multisets of terms. The following 2 operators can be used to define your multisets:
'is a prefix for a singleton multiset^is an infix operator for multiset union
Multisets allow high flexibility with the ordering of the terms. However, substructural logics without the Exchange rule obviously cannot be modelled in this way.
Correspondences generally involve computational terms (e.g. in lambda-calculus) annotated with logic terms (types). The library does not differentiate between terms and their annotations. Construction is only attempted on metavariables (see below).
In some cases (such as in correspondences of Classical Linear Logic) the whole sequent is also annotated with a process term. This can be accomplished by adding an additional argument to the consequence operator (turnstile).
The library anticipates 2 types of proofs:
- Regular / type-checking proofs: these involve object level lemmas where all computational annotations (if any) are provided already. In simple logics, this is just a regular object level proof, whereas in constructive logics these are essentially proofs that type check the given computational terms.
- Construction proofs: these involve proofs in logics with a computational correspondence where the annotations are not known in advance. The aim of the proof is to construct a computational term that corresponds to the derived type.
This is accomplished by initializing the unknown computational term as a metavariable. The best way to achieve that is to existentially quantify the term and then use
META_EXISTS_TAC. The rest of the proof can then proceed as any other proof. Once the (interactive) proof is completed, the instantiation of the term can be obtained viatop_inst(p())(wherep()is the toplevel HOL Light goal state).
In order to automate the meta-level term management and bookkeeping (particularly metavariables) the whole HOL Light proof system is essentially reconstructed. The aim is to allow the extension of the proof state with additional metadata.
This results to the introduction of a seqtactic as an extension of the standard HOL Light tactic. Associated proof tools are also extended as follows:
ETHEN,EEVERY,ETHENLetc. extend their counterpart HOL Light tacticalseseqextendseprove_seqextendsproveETAC(orSEQTAC) can lift atacticto become aseqtactic
The main tactics (of type seqtactic) are built in the spirit of Isabelle Light:
ruleseq: Backward reasoning - match the current goaleruleseq: Elimination reasoning - match the major assumption and the current goaldruleseq: Destruction reasoning - match and delete the major assumptionfruleseq: Forward reasoning - match and keep the major assumptionseqassumption: Match the current goal to one of the assumption
These extend their Isabelle Light counterparts by taking care of multiset matching and term construction automatically.
Any embedded rule (assuming Isabelle Light's meta-implication operator is used) can be applied using these tactics. Instantiation lists can be used to manipulate the particular application of the rule.
Contact: Petros Papapanagiotou – pe.p@ed.ac.uk - @PetrosPapapa
Distributed under the BSD 3-Clause Revised license. See LICENSE for more information.