Theorem Proving in Dependently-Typed Higher-Order Logic

Abstract

Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support.

We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

1 Introduction and Related Work

Theorem proving in higher-order logic (HOL) [5, 11] has been a long-running research strand producing multiple mature interactive provers [10, 13, 17] and automated provers [2, 4, 23]. Similarly, many, mostly interactive, theorem provers are available for various versions of dependent type theory (DTT) [7, 9, 15, 18]. However, it is (maybe surprisingly) difficult to develop theorem provers for dependently-typed higher-order logic (DHOL).

In this paper, we use HOL to refer to a version of Church’s simply-typed $\lambda$-calculus with a base type $\textsf{bool}$ for Booleans, simple function types $\rightarrow$, and equality $=_A:A\rightarrow A\rightarrow \textsf{bool}$. This already suffices to define the usual logical quantifiers and connectives.¹ Intuitively, it is straightforward to develop DHOL accordingly on top of the dependently-typed $\lambda$-calculus, which uses a dependent function type $\Pi x\!:\!A.~B$ instead of $\rightarrow$. However, several subtleties arise that seem deceptively minor at first but end up presenting fundamental theoretical issues. They come up already in the elementary expression for some dependent function $f:\Pi x\!:\!A.~B(x)$.

Firstly, the equality $f(x)\,=_{B(x)}\, f(y)$ is not even well-typed because the terms f(x) : B(x) and f(y) : B(y) do not have the same type. Intuitively, it is obvious that the type system can (and maybe should) be adjusted so that the equality $x=_A y$ between terms carries over to an equality $B(x)\,\equiv \,B(y)$ between types.² However, this means that the undecidability of equality leaks into the equality of types and thus into type-checking.

While some interactive provers successfully use undecidable type systems [6, 16], most formal systems for DTT commit to kee** type-checking decidable. The typical approach goes back to Martin-Löf type theory [14] and the calculus of constructions [8] and uses two separate equality relations, a decidable meta-level equality for use in the type-checker and a stronger undecidable one subject to theorem proving. Moreover, it favors the propositions-as-types representation and deemphasizes or omits a type of classical Booleans. This approach has been studied extensively [7, 9, 15] and is not the subject of this paper.

Instead, our motivation is to retain a single equality relation and classical Booleans. This is arguably more intuitive to users, especially to those outside the DTT community such as typical HOL users or mathematicians, and it is certainly much closer to the logics of the strongest available ATP systems. This means we have to pay the price of undecidable type-checking. The current paper was prompted by the observation that this price may be acceptable for two reasons:

• 1. If our ultimate interest is theorem proving, undecidability comes up anyway. Indeed, it is plausible that the cost of showing the well-typedness of a conjecture will be negligible compared to the cost of proving it.

• 2. As the strength of ATPs for HOL increases, the practical drawbacks of undecidable type-checking decrease, which indicates revisiting the trade-off from time to time. Indeed, if we position DHOL close to an existing HOL ATP, it is plausible that the price will, in practice, be affordable.

Secondly, even if we add a rule like “if $\vdash x=_A y$, then $\vdash B(x)\,\equiv \,B(y)$” to our type system, the above expression is still not well-typed: Above, the equality $x=_A y$ on the left of is needed to show the well-typedness of the equality $f(x)=_{B(x)}f(y)$ on the right. This intertwines theorem proving and type-checking even further. Concretely, we need a dependent implication, where the first argument is assumed to hold while checking the well-typedness of the second one. Formally, this means that to show , we require $\vdash F:\textsf{bool}$ and $F\vdash G:\textsf{bool}$. Similarly, we need a dependent conjunction. And if we are classical, we may also opt to add a dependent disjunction $F\vee G$, where $\lnot F$ is assumed in G. Naturally, dependent conjunction and disjunction are not commutative anymore. This may feel disruptive, but similar behavior of connectives is well-known from short-circuit evaluation in programming languages.

The meta-logical properties of dependent connectives are straightforward. However, interestingly, these connectives can no longer be defined from just equality. At least one of them (we will choose dependent implication) must be taken as an additional primitive in DHOL along with $=_A$.

Finally, the above generalizations require a notion of DHOL-contexts that is more complex than for HOL. HOL-contexts can be stratified into (a) a set of variable declarations $x_i:A_i$, and (b) a set of logical assumptions F possibly using the variables $x_i$. Moreover, the former are often not explicitly listed at all and instead inferred from the remainder of the sequent. But in DHOL, the well-formedness of an $A_i$ may now depend on previous logical assumptions. To linearize this inter-dependency, DHOL contexts must consist of a single list alternating between variable declarations and assumptions.

Contribution. Our contribution is twofold. Firstly, we introduce a new logic DHOL designed along the lines described above. Moreover, we further extend DHOL with predicate subtypes $A|_{p}$ for a predicate $p:A\rightarrow \textsf{bool}$ on the type A. Besides dependent types, these constitute a second important source of terms occurring in types. Because they also make ty** undecidable, they are often avoided. The most prominent exception is PVS [16], whose kernel essentially arises by adding predicate subtypes to HOL. In current HOL ITPs going back to [10], their use is usually restricted to the subtype definition principle: here a definition $b:=A|_{p}$ may occur on toplevel and is elaborated into a fresh type b that is axiomatized to mimic the subtype $A|_{p}$. Because we are committed to undecidable ty** anyway, predicate subtypes fit naturally into our approach.

Secondly, we develop and implement a sound and complete translation of DHOL into HOL. This setup allows the use of DHOL as the expressive user-facing language and HOL as the internal theorem-proving language. We position our implementation close to an existing HOL ATP, namely the LEO-III system. From the LEO-III perspective, DHOL serves as an additional input language that is translated into HOL by an external logic embedding tool [5 we prove the soundness and completeness of the translation. In Sect. 6 we describe how to use our translation and a HOL ATP to implement a theorem prover for DHOL.

2 Preliminaries: Higher-Order Logic

We introduce the syntax and rules of HOL. Our definitions are standard except that we tweak a few details in order to later present the extension to DHOL more succinctly. We use the following grammar for HOL:

A theory T is a list of base type declarations $a:\textsf{tp}$, typed constant declarations c : A, and named axioms $c\!:F$ asserting the formula F. A context $\Gamma$ has the same form except that no type variables are allowed. It is not strictly necessary to use named axioms and assumptions, but it makes our extensions to DHOL later on simpler. We write $\circ$ and $.$ for the empty theory and context, respectively. At this point, it is possible to normalize contexts into a set of variable declarations followed by a set of assumptions because the well-formedness of a type A can never depend on a variable or an assumption. But that property will change when going to DHOL, which is why we allow $\Gamma$ to alternate between variables and assumptions.

Types A are either user-declared types a, the built-in base type $\textsf{bool}$, or function types $A\rightarrow B$. Terms are constants c, variables x, $\lambda$-abstractions $\lambda x\!:\!A.~ t$, function applications $f\ t$, or obtained from the built-in $\textsf{bool}$-valued connectives $\,=_{A}\,$ or $\Rightarrow$. As usual [1], this suffices to define all the usual quantifiers and connectives $\textsf{true}$, $\textsf{false}$, $\lnot$, $\wedge$, $\vee$, $\forall$ and $\exists$. This includes $\Rightarrow$, but we make it a primitive here because we will change it in DHOL. As usual, denotes the capture-avoiding substitution of the variable x with the term t within expression E.

The type and proof system uses the judgments given below. Note that we need a meta-level judgment for the equality of types because $\,\equiv \,$ is not a $\textsf{bool}$-valued connective. On the contrary, the equality of terms $\vdash s\,=_{A}\, t$ is a special case of the validity judgment $\vdash F$. In HOL, $\,\equiv \,$ is trivial, and the judgment is redundant. But we include it here already because it will become non-trivial in DHOL.

Name	Judgment	Intuition
theories	$\vdash \,T\ \textsf{Thy}$	T is well-formed theory
contexts	$\vdash _T\Gamma \ \textsf{Ctx}$	$\Gamma$ is well-formed context
types	$\Gamma \vdash _TA\, \textsf{tp}$	A is well-formed type
ty**	$\Gamma \vdash _Tt :A$	t is a well-formed term of type well-formed type A
validity	$\Gamma \vdash _TF$	well-formed Boolean F is provable
equality of types	$\Gamma \vdash _TA\,\equiv \,B$	well-formed types A and B are equal

The rules are given in Fig. 1. We assume that all names in a theory or a context are unique without making that explicit in the rules. Following common practice, we further assume that HOL types are non-empty.

Fig. 1.

HOL Rules

3 Dependent Function Types

3.1 Language

We have carefully defined HOL in such a way that only a few surgical changes are needed to define DHOL. A consolidated summary of DHOL is given in Appendix A.2 in the extended preprint [20]. The grammar is as follows with unchanged parts :

Concretely, base types a may now take term arguments and simple function types $A\rightarrow B$ are replaced with dependent function types $\Pi x\!:\!A.~ B$. As usual we will retain the notation $A\rightarrow B$ for the latter if x does not occur free in B. DHOL is a conservative extension of HOL, and we recover HOL as the fragment of DHOL in which all base types a have arity 0.

Example 1 (Category Theory)

As a running example, we formalize the theory of a category in DHOL. It declares the base type obj for objects and the dependent base type for morphisms. Further it declares the constants id and $\texttt{comp}$ for identity and composition, and the axioms for neutrality. We omit the associativity axiom for brevity.

Here we use a few intuitive notational simplifications such as writing for binding two variables of the same type. We also use the notations for and $h\circ g$ for where the $\_$ denote inferable arguments of type .

The judgments stay the same and we only make minor changes to the rules, which we explain in the sequel. Firstly we replace all rules for $\rightarrow$ with the ones for $\Pi$:

Then we replace the rules for declaring, using, and equating base types with the ones where base types are applied to arguments:

The last of these is the critical rule via which term equality leaks into type equality. Thus, ty** of expressions may now depend on equality assumptions and thus ty** becomes undecidable.

Example 2 (Undecidability of Ty**)

Continuing Example 1, consider terms and for terms . Then holds iff , which holds iff . Depending on the axioms present, this may be arbitrarily difficult to prove.

Finally, we modify the rule for the non-emptiness of types: we allow the existence of empty dependent types and only require that for each HOL type in the image of the translation there exists one non-empty DHOL type translated to it (rather than requiring all dependent types translated to it to be non-empty). And we replace the ty** rule for implication with the dependent one. The proof rules for implications are unchanged.

Example 3 (Dependent Implication)

Continuing Example 1, consider the formula

which expresses that equal objects have equal identity morphisms. It is easy to prove. But it is only well-typed because the ty** rule for dependent implication allows using while type-checking , which requires deriving and thus .

All the usual connectives and quantifiers can be defined in any of the usual ways now. However, the details matter for the dependent versions of the connectives. In particular, we choose and in order to obtain the dependent versions of conjunction and disjunction, in which the well-formedness of G may depend on the truth or falsity of F, respectively.

3.2 Translation

We define a translation function $X\mapsto \overline{X}$ that maps any DHOL-syntax X to HOL-syntax. Its intuition is to erase type dependencies by translating all types $a\,t_1\,\ldots ,\,t_n$ to a and replacing every $\Pi$ with $\rightarrow$. To recover the information of the erased dependencies, we additionally define a partial equivalence relation (PER) ${A}^*$ on $\overline{A}$ for every DHOL-type A.

In general, a PER r on type U is a symmetric and transitive relation on U. This is equivalent to r being an equivalence relation on a subtype of U. The intuitive meaning of our translation is that the DHOL-type A corresponds in HOL to the quotient of the appropriate subtype of $\overline{A}$ by the equivalence ${A}^*$. In particular, the predicate ${A}^*\ t\ t$ captures whether t represents a term of type A. More formally, the correspondence is:

DHOL	HOL
type A	type $\overline{A}$ and PER ${A}^*:\overline{A}\rightarrow \overline{A}\rightarrow \textsf{bool}$
term t : A	term $\overline{t}:\overline{A}$ satisfying ${A}^*\ \overline{t}\ \overline{t}$

Definition 1 (Translation)

We translate DHOL-syntax by induction on the grammar. Theories and contexts are translated declaration-wise:

where $\overline{D}$ is a list of declarations.

The translation $\overline{\;a: \Pi x_1\!:\!A_1.~\ldots \Pi x_n\!:\!A_n.~\textsf{tp}}$ of a base type declaration is given by

Thus, a is translated to a base type of the same name without arguments and a trivial PER for every argument tuple. Intuitively, ${a}^* \ \overline{t_1}\ \ldots \ \overline{t_n}\ u\ u$ defines the subtype of the HOL-type a corresponding to the DHOL-type $a\ t_1\ \ldots \ t_n$.

Constant and variable declarations are translated by adding the assumptions that they are in the PER of their type, and axioms and assumptions are translated straightforwardly:

The cases of $\overline{A}$ and ${A}^*$ for types A are:

Finally, the cases for terms are straightforward except for, crucially, translating equality to the respective PER:

Example 4 (Translating Derived Connectives)

If we define $\textsf{true}$, $\textsf{false}$, $\lnot$ as usual in HOL and use the definition for dependent conjunction from above, it is straightforward to show that all DHOL-connectives are translated to their HOL-counterparts. For example, we have (up to logical equivalence in HOL) that $\overline{F\wedge G}=\overline{F}\wedge \overline{G}$.

We also define the quantifiers in the usual way, e.g., using $\forall x:A.F(x)\;:=\;\lambda x\!:\!A.~F(x)\,=_{A\rightarrow \textsf{bool}}\,\lambda x\!:\!A.~\textsf{true}$. Then applying our translation yields

This looks clunky, but (because ${A}^*$ is a PER as shown in Theorem 1) is equivalent to . Thus, DHOL-$\forall$ is translated to HOL-$\forall$ relativized using ${A}^*\ x\ x$. The corresponding rule $\overline{\exists x:A.F(x)}=\exists x:\overline{A}.{A}^*\ x\ x\wedge F(x)$ can be shown accordingly.

Example 5 (Categories in HOL)

We give a fragment of the translation of Example 1:

Here, for brevity, we have omitted , , and and have already used the translation rule for $\forall$ from Example 4. The result is structurally close to what a native formalization of categories in HOL would look like, but somewhat clunkier.

Fig. 2.

Additional Rules for Predicate Subtypes

4 Predicate Subtypes

To add predicate subtypes, we extend the grammar with the production . No new productions for terms are needed because the inhabitants of use the same syntax as those of A.

Example 6 (Isomorphisms)

We continue Example 1 and use predicate subtypes to write the type $\texttt{isomorphisms}\ u$ of automorphisms on u as a subtype of . We can define where the predicate p is given by

Adding subty** requires a few extensions to our type system. First we add a judgment $\Gamma \vdash _TA \,<:\,B$ and replace the lookup rules for variables and constants with their subty**-aware variants:

Then we add the rules given in Fig. 2. These induce an algorithm for deciding subty** relative to an oracle for the undecidable validity judgment. The latter enters the algorithm when two predicate subtypes are compared. Note that the type-equality rule for $A|_{p}|_{q}$ uses a dependent conjunction.

The resulting system is a conservative extension of the variants of HOL and DHOL without subty**: we recover these systems as the fragments that do not use $A|_{p}$. In particular, in that case $A \,<:\,B$ is trivial and holds iff $A\,\equiv \,B$ holds.

Finally, we extend our translation by adding the cases for predicate subtypes:

Definition 2 (Translation)

We extend Definition 1 with

5 Soundness and Completeness

Now we establish that our translation is faithful, i.e. sound and complete. We will use the terms sound and complete from the perspective of using a HOL-ATP for theorem proving in DHOL, e.g., sound means if $\overline{F}$ is a HOL-theorem, then F is a DHOL-theorem, and complete is the dual.³

The completeness theorem states that our translation preserves all DHOL-judgments. Moreover, the theorem statement clarifies the intuition behind the translations invariants:

Theorem 1 (Completeness)

We have

Additionally the substitution lemma holds, i.e.,

Proof

The proof proceeds by induction and can be found in Appendix B of the extended preprint [20].

The reverse direction is much trickier. To understand why, we look at two canaries in the coal mine that we have used to reject multiple intuitive but untrue conjectures:

Example 7 (Non-Injectivity of the Translation)

Continuing Example 1, assume terms and consider the identify functions and . Both are translated to the same HOL-term (because $I_u$ and $I_v$ only differ in the type indices, which are erased by our translation).

Consequently, the ill-typed DHOL-Boolean is translated to the HOL-Boolean , which is not only well-typed but even a theorem.

To better understand the underlying issue we introduce the notion of spurious terms. The well-typed translation $\overline{t}$ of a DHOL-term t is called spurious if t is ill-typed (otherwise it is called proper). Intuitively, we should be able to use the PERs ${A}^*$ to deal with spurious terms: to type-check t : A in DHOL, we want to use ${A}^*\ \overline{t}\ \overline{t}$ in HOL. But even that is tricky:

Example 8 (Trivial PERs for Built-In Base Types)

Consider the property ${\textsf{bool}}^*\ x\ x$. Our translation guarantees ${\textsf{bool}}^*\ \textsf{true}\ \textsf{true}$ and ${\textsf{bool}}^*\ \textsf{false}\ \textsf{false}$. Thus, we can use Boolean extensionality to prove in HOL that $\forall x:\textsf{bool}.\,{\textsf{bool}}^*\ x\ x$, making the property trivial. In particular, we can prove ${\textsf{bool}}^*\ \overline{b}\ \overline{b}$ for the spurious Boolean b from Example 7. Even worse, the property ${(\Pi x\!:\!A.~B)}^*\ x\ x$ is trivial in this way whenever it is for B and thus for all n-ary $\textsf{bool}$-valued function types.

More generally, this degeneration effect occurs for every base type that is built into both DHOL and HOL and that is translated to itself. $\textsf{bool}$ is the simplest example of that kind, and the only one in the setting described here. But reasonable language extensions like built-in base types a for numbers, strings, etc. would suffer from the same issue. This is because all of these types would come with built-in induction principles that derive a universal property from its ground instances, at which point ${a}^*\ x \ x$ becomes trivial.

Note, however, that the degeneration effect does not occur for user-declared base types. For example, consider a theory that declares a base type N for the natural numbers and an induction axiom for it. N would not be translated to itself but to a fresh HOL-type in whose induction axiom the quantifier $\forall$ is relativized by ${N}^*\ x\ x$. Consequently, ${N}^*\ x\ x$ is not trivial and can be used to reject spurious terms.

These examples show that we cannot expect the reverse directions of the statements in Theorem 1 to hold in general. However, we can show the following property that is sufficient to make our translation well-behaved:

Theorem 2 (Soundness)

Assume a well-formed DHOL-theory $\vdash \,T\ \textsf{Thy}$.

$$\begin{aligned} \text {If}\;\;\Gamma \vdash _TF:\textsf{bool}\;\;\text {and}\;\; \overline{\Gamma }\vdash _{\overline{T}}\overline{F}, \;\;\text {then}\;\; \Gamma \vdash _TF \end{aligned}$$

In particular, if $\Gamma \vdash _Ts:A$ and $\Gamma \vdash _Tt:A$ and $\overline{\Gamma }\vdash _{\overline{T}}{A}^*\ \overline{s}\ \overline{t}$, then $\Gamma \vdash \,s \,=_{A}\,t$.

Proof

The key idea is to transform a HOL-proof of $\overline{F}$ into one that is in the image of the translation, at which point we can read off a DHOL-proof of F. The full proof is given in Appendix B of the extended preprint [20].

Intuitively, the reverse directions of Theorem 1 holds once we establish that all involved expressions are well-typed in DHOL. Thus, we can use a HOL-ATP to prove DHOL-conjectures if we validate independently that the conjecture is well-typed all along. In the remainder of the section, we develop the necessary type-checking algorithm for DHOL.

Type-Checking. Inspecting the rules of DHOL, we observe that all DHOL-judgments would be decidable if we had an oracle for the validity judgment $\Gamma \vdash _TF$. Indeed, our DHOL-rules are already written in a way that essentially allows reading off a bidirectional type-checking algorithm. It only remains to split the ty** judgment $\Gamma \vdash _Tt:A$ into two algorithms for type-inference (which computes A from t) and type-checking (which takes t and A and returns yes or no) and to aggregate the rules for subty** into an appropriate pattern-match.

The construction is routine, and we have implemented the resulting algorithm in our MMT/LF logical framework [12, 19].⁴ The oracle for the validity judgment is provided by our translation and a theorem prover for HOL (see Sect. 6). It remains to show that whenever the algorithm calls the oracle for $\Gamma \vdash _TF$, we do in fact have that $\Gamma \vdash _TF:\textsf{bool}$ so that Theorem 2 is applicable. Formally, we show the following:

Theorem 3

Relative to an oracle for $\Gamma \vdash _TF$, consider a derivation of some DHOL-judgment, in which the children of each node are ordered according to the left-to-right order of the assumptions in the statement of the applied rule.

If the oracle calls are made in depth-first order, then each such call satisfies $\Gamma \vdash _TF:\textsf{bool}$.

Proof

We actually prove, by induction on derivations, the more general statement requires that each rule preserves the following preconditions:

Judgment	Precondition
$\vdash _T\Gamma \ \textsf{Ctx}$	$\vdash \,T\ \textsf{Thy}$
$\Gamma \vdash _TA\, \textsf{tp}$	$\vdash _T\Gamma \ \textsf{Ctx}$
$\Gamma \vdash _Tt:A$	$\Gamma \vdash _TA\,\textsf{tp}$ (post-condition when used as type-inference)
$\Gamma \vdash _TF$	$\Gamma \vdash _TF:\textsf{bool}$
$\Gamma \vdash _TA\,\equiv \,B$ or $\Gamma \vdash _TA\,<:\,B$	$\Gamma \vdash _TA\,\textsf{tp}$ and $\Gamma \vdash _TB\,\textsf{tp}$

Note that rules whose conclusion is a validity judgment can be ignored because they are replaced by the oracle anyway.

The most interesting case is the rule for $\Gamma \vdash _Ta\ s_1\ \ldots \ s_n\,\equiv \,a\ t_1\ \ldots t_n$. Here, the left-to-right order of assumptions is critical because $\Gamma \vdash _Ts_1\,=_{A_1}\,t_1$ may be needed to show, e.g., .

6 Theorem Prover Implementation

We have integrated our translation as a preprocessor to the HOL ATP LEO-III [23]. We chose this ATP because its existing preprocessor infrastructure already includes a powerful logic embedding tool [21, 22].However, with a little more effort, other HOL ATPs work as well.

Furthermore, we developed a bridge between the logical framework [19] and LEO-III (both of which are written in the same programming language).This allows us to use our -based type-checker for DHOL with our Leo-III-based theorem prover to obtain a full-fledge implementation of DHOL. Moreover, this system can immediately use ’s logic-independent frontend features like IDE and module system.

Alternatively, we can use LEO-III as a general purpose DHOL-ATP that accepts input in TPTP. Even though TPTP does not officially sanction DHOL as a logic, it anticipates dependent function types and already provides syntax for them (although—to our knowledge—no ATP system has made use of it so far). Concretely, TPTP represents the type $\Pi x\!:\!A.~B$ as >​[X:A]:B and a base type $a\ t_1\ldots \ t_n$ as  @ t1 ... @ tn. TPTP does not yet provide syntax for predicate subtypes, i.e., this approach is currently limited to the no-subty** fragment of DHOL. But extending the TPTP syntax with predicate subtypes would be straightforward, e.g., by using  ?| p to represent the type $A|_{p}$.

The encoding of the conjecture given in Example 3 using the theory from Example 1 is given at https://gl.mathhub.info/MMT/LATIN2/-/blob/devel/source/casestudies/2023-cade/Category Theory/category-theory-lemmas-dhol.p (which also includes further example conjectures relative to the same theory). Running the logic embedding tool translates it into the TPTP TH0 problem given at https://gl.mathhub.info/MMT/LATIN2/-/blob/devel/source/casestudies/2023-cade/Category Theory/category-theory-lemmas-hol.p. Unsurprisingly, LEO-III can prove this simple theorem easily.

Practical Evaluation. In order to evaluate the practical usefulness of the translation we studied various example conjectures about function composition in set theory and category theory. We considered 5 further lemmas based on the theory in Example 1 which are written directly in TPTP and can all be proven by E, Vampire and cvc5. We also studied various harder lemmas about function composition and category theory. Those examples are written in and take advantage of advanced features to improve readability, such as definitions, user-defined notations, and implicit arguments that are inferred by the prover.

The examples can be found at https://gl.mathhub.info/MMT/LATIN2/-/blob/devel/source/casestudies/2023-cade. The prover successfully type-checks all problems and translates them into TPTP problems to be solved by HOL ATPs.

Since LEO-III can solve none of the 6 function composition examples, we also tested other HOL ATPs on the generated TPTP problems. Running all HOL ATP provers supported at https://www.tptp.org/cgi-bin/SystemOnTPTP on the function composition problems shows that many provers can solve 3 of the problems, Vampire can solve 4 of them, and 5 out of the 6 conjectures can be solved by at least one HOL ATP.

We also studied 6 more difficult theorems about limits in category theory including the uniqueness, commutativity, and associativity of some limits. To better evaluate the usefulness of our translation, we also formalized these lemmas in native HOL (in ) and compared the results. Naturally, the DHOL formalization is significantly more readable and benefits from the more expressive type system that can help spot mistakes in the formalization. Running the HOL ATPs from https://www.tptp.org/cgi-bin/SystemOnTPTP on the generated TPTP problems (with 60 s timeout) yields the results in the table below (where we omit provers that proved none of the theorems in either formalization).

HOL ATP	lemma 1 proven		lemma 2 proven		lemma 3 proven
	DHOL	native HOL	DHOL	native HOL	DHOL	native HOL
agsyHOL	yes	no	no	no	yes	no
cocATP	yes	no	no	no	no	no
cvc5	yes	yes	no	no	yes	no
cvc5-SAT	yes	no	no	no	no	no
E	yes	yes	no	no	no	yes
HOLyHammer	yes	yes	no	no	yes	yes
Lash	yes	yes	no	no	no	no
LEO-II	yes	no	no	no	no	no
Leo-III	yes	yes	no	no	no	no
Leo-III-SAT	yes	yes	no	no	no	no
Satallax	yes	yes	no	no	yes	no
Vampire	yes	yes	no	no	no	yes
Zipperpin	yes	yes	no	no	yes	yes
total	13	9	0	0	5	4

HOL ATP	lemma 4 proven		lemma 5 proven		lemma 6 proven
	DHOL	native HOL	DHOL	native HOL	DHOL	native HOL
agsyHOL	no	no	no	no	no	no
cocATP	no	no	no	no	no	no
cvc5	no	yes	no	no	no	no
cvc5-SAT	no	no	no	no	no	no
E	no	yes	no	yes	no	yes
HOLyHammer	no	yes	no	no	no	yes
Lash	no	no	no	no	no	no
LEO-II	no	no	no	no	no	no
Leo-III	no	no	no	no	no	no
Leo-III-SAT	no	no	no	no	no	no
Satallax	no	no	yes	no	no	no
Vampire	no	yes	no	yes	no	yes
Zipperpin	no	yes	yes	yes	no	yes
total	0	5	2	3	0	4

Overall more problems generated from the native HOL formalization can be solved by some HOL ATP (5/6 compared to 3/6 for the DHOL formalization). The HOL ATPs found 25 successful proofs for the native HOL problems and 20 for the DHOL problems. This suggests that current HOL ATPs can prove native HOL problems somewhat better than their translated DHOL counterparts, but not much better. In 8 cases a prover can prove the DHOL conjecture but not the native HOL analogue, indicating that the two formalizations have different advantages.

Furthermore, our translation has so far been engineered for generality and soundness/completeness and not for ATP efficiency. Indeed, future work has multiple options to boost the ATP performance on translated DHOL, e.g., by

• develo** sufficient criteria for when simpler HOL theories can be produced

• inserting lemmas into the translated theories that guide proof search in ATPs, e.g., to speed up equality reasoning

• adding definitions to translated DHOL problems and develo** better criteria when to expand them

Thus, we consider the test results to be very promising. In particular, the translation could serve as a useful basis for type-checkers and hammer tools for DHOL ITPs.

7 Conclusion and Future Work

We have combined two features of standard languages, higher-order logic HOL and dependent type theory DTT, thereby obtaining the new dependently-typed higher-order logic DHOL. Contrary to HOL, DHOL allows for dependent function types. Contrary to DTT, DHOL retains the simplicity of classical Booleans and standard equality.

On the downside, we have to accept that DHOL, unlike both HOL and DTT, has an undecidable type system. Further work will show how big this disadvantage weighs in practical theorem proving applications. But we anticipate that the drawback is manageable, especially if, as in our case, an implementation of DHOL is coupled tightly with a strong ATP system. We accomplish this with a sound and complete translation from DHOL into HOL that enables using existing HOL ATPs to discharge the proof obligations that come up during type-checking. We have implemented our novel translation as a TPTP-to-TPTP preprocessor for HOL ATP systems and outlined the implementation of a type-checker and hammer tool for DHOL based on the resulting prover.

Moreover, once this design is in place, it opens up the possibility to add certain type constructors to DHOL that are often requested by users but difficult to provide for system developers because they automatically make ty** undecidable. We have shown an extension of DHOL with predicate subtypes as an example. Quotients, partial functions, or fixed-length lists are other examples that can be supported in future work.

We expect our translation remains sound and complete if DHOL is extended with other features underlying common HOL systems such as built-in types for numbers, the axiom of infinity, or the subtype definition principle. How to extend DHOL with a choice operator remains a question for future work — if solved, this would allow extending existing HOL ITPs to DHOL.