Object-level reasoning for embedded logics in HOL Light
I am actively developing 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.
Further information and background will be provided in a forthcoming publication.
What this library does
Assuming you have an inductively defined logic embedded 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 embedding 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 embedded logic.
What this library does NOT do
It does not allow you to perform any meta-level reasoning (such as cut-elimination proofs). It deals with shallow embeddings where 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.
The project is available on GitHub.
A detailed example can be found here.