HOL Light Embed

I have developed a generic framework to perform object level reasoning with embedded logics 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.

It is available under the BSD-3-Clause License on GitHub: https://github.com/PetrosPapapa/hol-light-embed

Additional information is available in this publication.

A step-by-step tutorial with a detailed example is available here.

What this library does

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 encoded 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.

What this library does NOT do

It does not allow you to perform any meta-level reasoning (such as cut-elimination proofs) as the derivation semantics of the logic are mapped to HOL implication. At this level it is not possible to reason about the semantics of the embedded logic.