# Reverse Engineering of HOL Proofs

Shuai Wang

July 2015 (revisited in Sep 2016)
# Project Proposal

Thesis submitted in accordance with the requirements of the ENS Cachan and INRIA as MPRI M1 internship report.

* Course: MPRI

* Level: M1

* Personal Tutor: Dr. David Baelde (ENS Cachan)

* Supervisor: Dr. Gilles Dowek

* Institute: INRIA

* Team: Deducteam

* Address: INRIA, 23 avenue d'Italie, CS 81321, 75214 Paris Cedex 13, France.

This internship is to analysis the translation of HOL-proofs to Dedukti in order to build
constructive proofs when possible. The goal of this project is a first quantitative analysis of
the proportion of proofs in usual classical mathematics that do not genuinely use the excluded
middle and that could be expressed constructively.

# Declaration Of Authorship

I declare that this thesis and the work presented in it are my own and has been generated by
me as the result of my own original research.

I confirm that:

* This work was done wholly or mainly while in candidature for a research degree at this University;

* Where any part of this thesis has previously been submitted for a degree or any other qualification at this University or any other institution, this has been clearly stated;

* Where I have consulted the published work of others, this is always clearly attributed;

* Where I have quoted from the work of others, the source is always given. With the exception of such quotations, this thesis is entirely my own work;

* I have acknowledged all main sources of help;

* Where the thesis is based on work done by myself jointly with others, I have made clear exactly what was done by others and what I have contributed myself;

Signed __________ Date __________
# Contents

<table><tr><td>Contents</td><td>iii</td></tr><tr><td>List of Figures</td><td>v</td></tr><tr><td>Acknowledgement</td><td>vi</td></tr><tr><td>Datasets, Code, and Reproducibility</td><td>vii</td></tr><tr><td>Nomenclature</td><td>vii</td></tr><tr><td>1 Introduction</td><td>1</td></tr><tr><td>2 Basics</td><td>2</td></tr><tr><td>2.1 Higher Order Logic</td><td>2</td></tr><tr><td>2.2 HOL Light</td><td>4</td></tr><tr><td>2.2.1 Introduction to HOL Light</td><td>4</td></tr><tr><td>2.2.2 Types and Terms</td><td>4</td></tr><tr><td>2.2.3 Constants and Connectives</td><td>4</td></tr><tr><td>2.2.4 Inference Rules of HOL Light</td><td>6</td></tr><tr><td>3 HOL Proof Checking with OpenTheory, Holide and Dedukti</td><td>8</td></tr><tr><td>3.1 OpenTheory and OpenTheory HOL Light</td><td>8</td></tr><tr><td>3.1.1 OpenTheory Version 6</td><td>9</td></tr><tr><td>3.2 λΠ-calculus and λΠ-calculus Modulo and Dedukti</td><td>10</td></tr><tr><td>3.3 Holide</td><td>12</td></tr><tr><td>3.3.1 Translation</td><td>13</td></tr><tr><td>3.3.2 Correctness</td><td>15</td></tr><tr><td>3.3.3 Holide2</td><td>15</td></tr><tr><td>4 Reverse Engineering of HOL Proofs</td><td>17</td></tr><tr><td>4.1 Double Negation Translation</td><td>18</td></tr><tr><td>4.2 Kernel Hacking for Reverse Engineering of HOL Proofs</td><td>19</td></tr></table>
<table>
  <tbody>
    <tr>
      <td>5</td>
      <td>HOLALA</td>
      <td>20</td>
    </tr>
    <tr>
      <td>5.1</td>
      <td>Kernel Hacking</td>
      <td>20</td>
    </tr>
    <tr>
      <td>5.1.1</td>
      <td>Logic Kernel</td>
      <td>20</td>
    </tr>
    <tr>
      <td>5.1.2</td>
      <td>Proof Logging</td>
      <td>22</td>
    </tr>
    <tr>
      <td>5.2</td>
      <td>Holide2x</td>
      <td>22</td>
    </tr>
    <tr>
      <td>5.2.1</td>
      <td>HOL Terms</td>
      <td>23</td>
    </tr>
    <tr>
      <td>5.2.2</td>
      <td>HOL Proofs</td>
      <td>23</td>
    </tr>
    <tr>
      <td>6</td>
      <td>Proof Analysis and Evaluation</td>
      <td>24</td>
    </tr>
    <tr>
      <td>6.1</td>
      <td>Workflow</td>
      <td>24</td>
    </tr>
    <tr>
      <td>6.2</td>
      <td>Proof Checking</td>
      <td>25</td>
    </tr>
    <tr>
      <td>6.3</td>
      <td>Proof Analysis</td>
      <td>27</td>
    </tr>
    <tr>
      <td>6.4</td>
      <td>ProofCloud</td>
      <td>28</td>
    </tr>
    <tr>
      <td>7</td>
      <td>Conclusion and Future Work</td>
      <td>33</td>
    </tr>
    <tr>
      <td>7.1</td>
      <td>Conclusion and Contribution</td>
      <td>33</td>
    </tr>
    <tr>
      <td>7.2</td>
      <td>Optimisation of proofs</td>
      <td>33</td>
    </tr>
    <tr>
      <td>7.3</td>
      <td>HOL-Modulo</td>
      <td>34</td>
    </tr>
    <tr>
      <td>7.4</td>
      <td>HOL-Tableaux</td>
      <td>34</td>
    </tr>
    <tr>
      <td>7.5</td>
      <td>ProofCloud</td>
      <td>35</td>
    </tr>
    <tr>
      <td>A</td>
      <td>Comparison of Sequent Calculus, Natural Deduction and HOL Light</td>
      <td>36</td>
    </tr>
    <tr>
      <td>B</td>
      <td>Proof of Law of Excluded Middle</td>
      <td>40</td>
    </tr>
    <tr>
      <td>B.1</td>
      <td>Law of Excluded Middle</td>
      <td>40</td>
    </tr>
    <tr>
      <td>B.2</td>
      <td>Diaconescu's Proof of Law of Excluded Middle</td>
      <td>40</td>
    </tr>
    <tr>
      <td>B.3</td>
      <td>A New Proof of Law of Excluded Middle</td>
      <td>41</td>
    </tr>
    <tr>
      <td>B.4</td>
      <td>Proof of ¬¬LEM</td>
      <td>42</td>
    </tr>
    <tr>
      <td>C</td>
      <td>Attempts of reverse engineering of HOL Light Proofs</td>
      <td>43</td>
    </tr>
    <tr>
      <td>C.1</td>
      <td>HOL-intermediate</td>
      <td>44</td>
    </tr>
    <tr>
      <td>C.2</td>
      <td>HOLIU</td>
      <td>44</td>
    </tr>
    <tr>
      <td>C.3</td>
      <td>HOLbot</td>
      <td>45</td>
    </tr>
    <tr>
      <td>D</td>
      <td>The Specification of ProofCloud</td>
      <td>46</td>
    </tr>
    <tr>
      <td>D.1</td>
      <td>The Specification of ProofCloud</td>
      <td>46</td>
    </tr>
    <tr>
      <td>Index</td>
      <td></td>
      <td>47</td>
    </tr>
  </tbody>
</table>
List of Tables

<table><tbody><tr><td>2.1</td><td>Primitive and Axiomatic Definitions of Connectives and Constants of Q<sub>0</sub></td><td>3</td></tr><tr><td>2.2</td><td>HOL Light Notations</td><td>5</td></tr><tr><td>2.3</td><td>Primitive Inference Rules of HOL Light [20]</td><td>6</td></tr><tr><td>2.4</td><td>HOL Light Deduced Inference Rules</td><td>7</td></tr><tr><td>3.1</td><td>OpenTheory version 5 Logic Kernel [21]</td><td>9</td></tr><tr><td>3.2</td><td>New and Updated Inference Rules of OpenTheory (version 6)</td><td>9</td></tr><tr><td>3.3</td><td>Differences between version 5 and version 6</td><td>10</td></tr><tr><td>3.4</td><td>Typing Rules of the λΠ-calculus</td><td>12</td></tr><tr><td>4.1</td><td>Properties of Translation Compared</td><td>19</td></tr><tr><td>5.1</td><td>Primitive and Axiomatic Definitions of Connectives and Constants Comparison</td><td>20</td></tr><tr><td>5.2</td><td>Additional Primitive Inference Rules of HOLALA</td><td>22</td></tr><tr><td>5.3</td><td>Size of Deductive Rules Between OpenTheory HOL Light and HOLALA</td><td>22</td></tr><tr><td>6.1</td><td>Version Correspondance of OpenTheory, Holide and HOLALA</td><td>25</td></tr><tr><td>6.2</td><td>Size of Article Files and Translation Time</td><td>26</td></tr><tr><td>6.3</td><td>Size of Dedukti Files and Proof Checking Time</td><td>26</td></tr><tr><td>6.4</td><td>Size and Frequency Analysis of Main Inference Rules of HOL Light and HOLALA Proofs</td><td>28</td></tr><tr><td>6.5</td><td>Comparison of Translation and Proof Checking</td><td>30</td></tr><tr><td>A.1</td><td>Example Proof of (p ∧ (p → q)) → q in Sequent Calculus, Natural Deduction and HOL Light</td><td>36</td></tr><tr><td>A.2</td><td>Inference System Comparison</td><td>39</td></tr></tbody></table>
# List of Figures

<table><tr><td>5.1</td><td>Dependency of Constants and Connectives Analysis</td><td>21</td></tr><tr><td>6.1</td><td>Workflow of HOLALA, Holide, OpenTheory and ProofCloud</td><td>24</td></tr><tr><td>6.2</td><td>Frequency of Main Inference Rules of OpenTheory Articles</td><td>29</td></tr><tr><td>6.3</td><td>Frequency of Main Inference Rules of HOLALA Articles</td><td>29</td></tr><tr><td>6.4</td><td>The Interface of ProofCloud</td><td>30</td></tr><tr><td>6.5</td><td>Dependency of Packages of OpenTheory</td><td>31</td></tr><tr><td>6.6</td><td>A Proof Page of ProofCloud</td><td>32</td></tr><tr><td>6.7</td><td>A Proof Checking Page of ProofCloud</td><td>32</td></tr><tr><td>C.1</td><td>Constants and Connectives Dependency Analysis and Design</td><td>44</td></tr></table>
Acknowledgement

The author wishes to thank Dr. Gilles Dowek, Mr. Ali Assaf, Mr. Frédéric Gilbert and Mr. Raphaël Cauderlier, members of Deducteam at INRIA and Dr. Benno van den Berg (ILLC, UvA) for their help during and after this project. The author would also like to thank all those who gave advice or comments during the past few months, especially those at the conferences and workshops (ESSLLI, UITP, AITP): Dr. Sven Linker, Mr. Eric Flaten, Mr. Letchi Akhmatov, Dr. Cezary Kaliszyk and anonymous reviewers.

This is a revisited version of the original report with many mistakes corrected. This re-
port also includes a detailed description of the latest version of ProofCloud, which was a side
project commered around end of the internship. ProofCloud was later developed as a new
platform after the author left INRIA.

Finally, the reference list was reviewed.
# Datasets, Code, and Reproducibility

For reproducibility, the following datasets and their code and documentation are available.
Unfortunately. They have not been maintained since early 2016.

1. Holide: The description is on GitHub https://airobert.github.io/holide/. The source code is in the repository https://github.com/airobert/holide.

2. HOLALA: Some description is on this GitHub page: https://airobert.github.io/holala/. The source code is available at https://github.com/airobert/holala.

3. ProofCloud: The main website is at https://airobert.github.io/proofcloud/ and the source code is hosted on GitHub at https://github.com/airobert/proofcloud.

The code, intermediate results, design of the interface are all free for use under the licence
CC-BY 4.0 provided that the author recieves credits via citation or acknowledgement.
# Chapter 1

# Introduction

In Logical Framework, proofs are defined using definitions of logical constants, connectives, quantifiers and axioms. Using a Logical Framework, the theories can be defined explicitly, making it possible to investigate which part of the theory is needed for each given proof. The process of reconstructing proofs in a given form is defined “reverse engineering of proofs”. This work is a first attempt to do such reverse engineering of higher order proofs. More specifically, this project first analyse which proofs in the HOL-light library are constructive. If so, we attempt to transform them in the weaker constructive system. This internship project aimed at such automatic analysis for proofs by picking constructive-compatible definitions and transform proofs using those definitions. As a consequence, rework all the chain from HOL-Light to Dedukti takes these modifications into account for proof checking. Several unsuccessful attempts have been made to change the kernel of HOL Light. Among them HOLALA extends the kernel of HOL Light by introducing the universal quantification and implication. It can classify proofs and perform structural and statistical analysis. The result is that 531 proofs out of 1199 (44%) in the HOL-light standard library are shown to be constructive. The evaluation results showed that HOLALA is a successful attempt to reduce the size of proof files, leading to an improvement of 41.81% in translation time and a speed-up of 38.04% in proof checking. Finally, all structural analysis and proof checking results were presented in a proof search engine, namely ProofCloud.

This report is organised as follows: Chapter 2 and Chapter 3 are an exposition of the tools used during this internship: HOL-Light, Dedukti and Holide. To perform double negation translation as described in Chapter 4, it is required to do some modification of the primitive symbols of OpenTheory HOL Light kernel. Chapter 5 present a modification of the OpenTheory HOL-Light system, namely HOLALA, which meant to change the definition of the connectives and quantifiers. Following that was the corresponding modifications of Holide. Chapter 6 presents some proof analysis results and the evaluation.
# Chapter 2

## Basics

### 2.1 Higher Order Logic

Higher Order Logic, also known as simple type theory (STT), is an extension of first order logic [13]. A term is considered either a variable (e.g. $x$), an abstraction (e.g. $\lambda x.x$) or an application (e.g. $(\lambda x.x) y$) of certain type. A variable following $\lambda$ is considered an argument of a function. Such variables are also considered as *bound*, otherwise *free*. The rest of the function is usually referred to as the *body*. The notation $x : \iota$ means that the term $x$ is of type $\iota$. The type of a term is recursively defined as $\iota$ (a type symbol, denoting the type of individuals) or $\iota \to \iota$ (a function type, the arrow is known as type constructor), or a boolean type (*bool* for short). Propositions are of type *bool*. Type notions are sometimes omitted for simplicity of representation. Restricted by typing, application has to agree also on their types. For example, $\lambda x : \iota.x$ which is of type $\iota \to \iota$ can be applied to $w : \iota$ but not $z : \iota \to \iota$. Such functions can be $\beta$-reduced through application to another term. Variables bound by $\lambda$ are considered only place-holders so terms are considered identical if they only differ for the names of their bound variables. For example $(\lambda x.yx)$ and $(\lambda s.ys)$. These terms are considered $\alpha$-convertible. $\beta$-reduction is simply to replace all the occurrences of the bound variable by the applied term in the “bod” of the function. For example, $(\lambda x.x)y$ would be $\beta$-reduced to $y$ (denoted as $(\lambda x.x)y \to_{\beta} y$). The notation $[y/x]$A is used to represent the result of replacing all the $x$ by $y$ in A. Thus, $(\lambda x.yx)z \to_{\beta} [z/x](yx) = yz$. The relation $\equiv_{\beta}$ is the reflexive, symmetric, transitive closure of $\to_{\beta}$, which is also referred to as equivalence up to $\beta$. For example, $(\lambda x.(\lambda y.y)x)w \equiv_{\beta} (\lambda y.y)w \equiv_{\beta} w$. $\lambda$-calculus can be used as representation of arithmetic, lists and more.

Higher order logic includes also some additional axioms and inference rules. Since most mathematical theories can be expressed in STT, it has been well investigated during the past few decades. As a result, automatic and interactive theorem provers have been developed for formal mathematics. Among the interactive theorem provers, the HOL family consists of several interactive theorem provers including HOL4 [33], HOL Light [20], ProofPower [29], HOL Zero [1], etc. Alongside, many higher order automatic theorem provers have also been developed [9, 28, 34].
The following is a brief introduction to the higher order logic system $Q_0$ [2]. $Q_0$ takes two primitive symbols, = and ι. Other constants and connectives are defined based on it. Table 2.1 illustrates a list of constants and connectives defined in $Q_0$. Note that $\forall x.A$ is an abbreviation of $\forall(\lambda x.A)$, which is also written as $\forall A$ in some contexts.

<table><caption>Table 2.1: Primitive and Axiomatic Definitions of Connectives and Constants of $Q_0$</caption><thead><tr><th>Symbol</th><th>Definition</th></tr></thead><tbody><tr><td>=</td><td>primitive</td></tr><tr><td>ι</td><td>primitive</td></tr><tr><td>↔</td><td>=</td></tr><tr><td>⊤</td><td>= = =</td></tr><tr><td>∀</td><td>λp.A = λp.⊤</td></tr><tr><td>⊥</td><td>λx.T = λx.x</td></tr><tr><td>∧</td><td>λxλy(λg.g⊤⊤ = λg.gxy)</td></tr><tr><td>→</td><td>λpq.(p = (p ∧ q))</td></tr><tr><td>∃</td><td>¬∀x¬A</td></tr><tr><td>∨</td><td>λxy.¬(¬x ∧ ¬y)</td></tr><tr><td>¬</td><td>λx.x = ⊥</td></tr><tr><td>∃!</td><td>(∃p) ∧ (∀xy.px ∧ py ⇒ x = y)</td></tr></tbody></table>

The higher order logic inference system $Q_0$ takes a list of axioms but has a single primitive inference rule, Rule R. The following illustrates a list of axioms of $Q_0$ followed by its only inference rule [2].

**Axiom 1.** $f⊤ ∧ f⊥ = ∀x.fx$

**Axiom 2.** $(x = y) = (fx = fy)$

**Axiom 3.** $(f = g) = ∀x.(fx = gx)$

**Axiom 4.** $(\lambda x.B)A = B$, where B is a primitive constant or variable distinct from x.

**Axiom 5.** $(\lambda x.x)A = A$

**Axiom 6.** $(\lambda x.(BC)A = ((\lambda x.B)A)(\lambda x.C)A)$

**Axiom 7.** $(\lambda x.(\lambda y.B))A = (\lambda y.((\lambda x.B)A))$, where y is distinct from x and from all variables in A.

**Axiom 8.** $(\lambda x.(\lambda x.B))A = \lambda x.B$

**Axiom 9.** $ι(= y) = y$

**Rule R.** $\frac{C \quad A = B}{C'} R$, where C' is C with one occurrence of A replaced by B, provided that the occurrence of A in C is not (an occurrence of a variable) immediately preceded by λ. [2].
To construct proofs, it is first required to understand the definition of a sequent. A sequent is in the form Γ ⊢ A, where Γ is the hypotheses and A the conclusion. Such sequent means that we can deduce A from Γ. Informally, a proof is a tree of sequents connected by inference rules. Based on the logic of $Q_0$, we can deduce some more inference rules corresponding to common logic connectives and constants, making it a usable inference system. One of the most used inference systems is Natural Deduction. It is commonly used in proof assistants including HOL Light.

## 2.2 HOL Light

### 2.2.1 Introduction to HOL Light

HOL Light is an open source interactive theorem prover and proof checker for higher order logic [20]. HOL Light is a simplified version of the original HOL [33] system with a small and reliable kernel. Similar to the HOL system, HOL Light takes advantage of the powerful functional programming language OCaml [20] and has a special notation system for logical connectives and constants which is presented in Table 2.2 in case of confusion.

### 2.2.2 Types and Terms

To understand how HOL Light works, it is necessary to understand how HOL Light defines types and terms. HOL Light terms are usually represented in backticks. For example, `x:A` means a variable x of type A. Each HOL Light term has a type defined recursively, which can be either a type variable, a boolean type or an arrow type. An arrow type is of the form $\alpha \to \beta$, which means that the function takes an argument of type $\alpha$ and returns a term of type $\beta$. A HOL Light term is a variable, a constant, an application or an lambda abstraction. For example, the type of $\lambda x : A. \top$ is $A \to bool$. The syntax of HOL Light is as follows [5]:

<table><tr><td>type variables</td><td>$\alpha, \beta$</td></tr><tr><td>type operators</td><td>$p$</td></tr><tr><td>types</td><td>$A, B ::= \alpha | p(A_1, ..., A_n)$</td></tr><tr><td>term variables</td><td>$x, y$</td></tr><tr><td>term constants</td><td>$c$</td></tr><tr><td>terms</td><td>$M, N ::= x | \lambda x : A.M | MN | c$</td></tr></table>

### 2.2.3 Constants and Connectives

HOL Light's logic is an extension of Church's simple type theory (STT) [7]. STT, together with polymorphic type variables and some axioms and inference rules, makes the logic of HOL Light. HOL Light has terms of type boolean, individual and function as well as polymorphic
<table><caption>Table 2.2: HOL Light Notations</caption><thead><tr><th>HOL Notation</th><th>Meaning</th><th>Logic Notation</th><th>Definition</th></tr></thead><tbody><tr><td>=</td><td>Equivalence</td><td>=</td><td>primitive</td></tr><tr><td>\</td><td>lambda</td><td>λ</td><td>built-in symbol</td></tr><tr><td>!</td><td>Universal Quantifier</td><td>∀</td><td>λp.A = λp.⊤</td></tr><tr><td>?</td><td>Existential Quantifier</td><td>∃</td><td>¬∀x¬A</td></tr><tr><td>~</td><td>Negation</td><td>¬</td><td>λp.p ⇒ ⊥</td></tr><tr><td>==></td><td>Implication</td><td>⇒</td><td>λpq.(p = (p ∧ q))</td></tr><tr><td><=></td><td>Bi-implication</td><td>↔</td><td>=</td></tr><tr><td>\</td><td>Disjunction</td><td>∨</td><td>λxy.¬(¬x ∧ ¬y)</td></tr><tr><td>∧</td><td>Conjunction</td><td>∧</td><td>λxλy(λg.g⊤⊤ = λg.gxy)</td></tr><tr><td>T</td><td>Truth</td><td>⊤</td><td>λp.p = λp.p</td></tr><tr><td>F</td><td>False</td><td>⊥</td><td>λx.T = λx.x</td></tr><tr><td>@</td><td>Hilbert's Choice Symbol</td><td>@</td><td>Constant</td></tr><tr><td>?!</td><td>Exist Unique</td><td>∃!</td><td>(∃p) ∧ (∀xy.px ∧ py ⇒ x = y)</td></tr></tbody></table>

type variables. There are constants with polymorphic types: equality (=) ¹and Hilbert's choice symbol (denoted as @) [20]. The choice symbol can be considered a function with a predicate as input, and return an element satisfying such predicate. It returns a random element if there is no such element. The choice symbol is used in the axiom of choice, which is in the center of the proof of the law of excluded middle to be presented in Section B.2.

$$ 
\begin{aligned}
&=: \alpha \rightarrow \alpha \rightarrow o \\
@ : & (\alpha \rightarrow o) \rightarrow \alpha
\end{aligned}
 $$

Here, the polymorphic type variables α of = would be instantiated to the type of the term(s) it is applied to. For instance, in the term ⊤ = ⊤, = is of type o → o → o<fnref n="2" />.

The constant = plays three roles in HOL Light:

### Definition

= is the first connective introduced HOL Light system. Its first use is to define other logical constants and connectives, as the role of equivalence (≡).

### Equality

In most cases, = is used to represent equivalence of two terms, including variables, constants, λ abstraction and application. Terms are of the same type on both sides of =.

### Bi-implication

In HOL Light, the bi-implication connector ↔ is redefined as equality since such case can be regarded as equality with type o → o → o.

<footnote n="1">¹s = t is a conventional concrete syntax for ((=)st).</footnote>

<footnote n="2">²This is also the type of bi-implication. Bi-implication (⇔) can be considered a special case of the polymorphic =</footnote>
### 2.2.4 Inference Rules of HOL Light

The definition of the logical symbols and the primitive inference rules are the very beginning of the HOL-Light library. This is known as the kernel of HOL-Light. More specifically, the kernel defines 10 primitive inference rules as in Table 2.3³.

<table><caption>Primitive Inference Rules of HOL Light</caption><tr><td>Structural</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">{A} &vdash; A</span><span style="display: inline-block; padding-top: 1px;">ASSUME</span></div></td></tr><tr><td>&lambda; Calulus</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma; &vdash; A = B</span><span style="display: inline-block; padding-top: 1px;">&Gamma; &vdash; &lambda;x.A = &lambda;x.B</span><span style="display: inline-block; padding-top: 1px;">ABS</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">(&lambda;x.A)x = A</span><span style="display: inline-block; padding-top: 1px;">BETA</span></div></td></tr><tr><td>Instantiation</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma;[x<sub>1</sub>,...,x<sub>n</sub>] &vdash; A[x<sub>1</sub>,...,x<sub>n</sub>]</span><span style="display: inline-block; padding-top: 1px;">&Gamma;[t<sub>1</sub>,...,t<sub>n</sub>] &vdash; A[t<sub>1</sub>,...,t<sub>n</sub>]</span><span style="display: inline-block; padding-top: 1px;">INST</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma;[&alpha;<sub>1</sub>,...,&alpha;<sub>n</sub>] &vdash; A[&alpha;<sub>1</sub>,...,&alpha;<sub>n</sub>]</span><span style="display: inline-block; padding-top: 1px;">&Gamma;[&gamma;<sub>1</sub>,...,&gamma;<sub>n</sub>] &vdash; A[&gamma;<sub>1</sub>,...,&gamma;<sub>n</sub>]</span><span style="display: inline-block; padding-top: 1px;">INST_TYPE</span></div></td></tr><tr><td>Bi-implication</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma; &vdash; A = B</span><span style="display: inline-block; padding-top: 1px;">&Delta; &vdash; A</span><span style="display: inline-block; padding-top: 1px;">EQ MP</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma; &cup; &Delta; &vdash; B</span><span style="display: inline-block; padding-top: 1px;">&Gamma; &vdash; A</span><span style="display: inline-block; padding-top: 1px;">&Delta; &vdash; B</span><span style="display: inline-block; padding-top: 1px;">DEDUCT_ANTISYM_RULE</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">(&Gamma; \ {B}) &cup; &Delta; \ {A}) &vdash; A = B</span><span style="display: inline-block; padding-top: 1px;">REFL</span></div></td></tr><tr><td>Equality</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma; &vdash; A = B</span><span style="display: inline-block; padding-top: 1px;">&Delta; &vdash; C = D</span><span style="display: inline-block; padding-top: 1px;">MK_COMB</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">&Gamma; &cup; &Delta; &vdash; A(C) = B(D)</span><span style="display: inline-block; padding-top: 1px;">&Gamma; &vdash; A = B</span><span style="display: inline-block; padding-top: 1px;">&Delta; &vdash; B = C</span><span style="display: inline-block; padding-top: 1px;">TRANS</span></div></td></tr></table>

<caption>Table 2.3: Primitive Inference Rules of HOL Light [20]</caption>

On the bases of the ten primitive inference rules we can deduce inference rules, referred to as derived inference rules" in contrast with "primitive inference rules" in this report (Table 2.4).

<footnote n="3">³To keep tables small, types are eliminated.</footnote>
<table><caption>Table 2.4: HOL Light Deduced Inference Rules</caption><thead><tr><th>Symbol</th><th>HOL Light Deduced Inference Rules</th></tr></thead><tbody><tr><td>⊤</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ⊤</span><span style="display: inline-block; padding-top: 1px;">TRUTH</span></div></td></tr><tr><td>⊥</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ⊥</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A</span><span style="display: inline-block; padding-top: 1px;">CONTR</span></div></td></tr><tr><td>∧</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A ∧ B</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A</span><span style="display: inline-block; padding-top: 1px;">CONJUNCT1</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A ∧ B</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ B</span><span style="display: inline-block; padding-top: 1px;">CONJUNCT2</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A</span><span style="display: inline-block; padding-top: 1px;">Δ ⊢ B</span><span style="display: inline-block; padding-top: 1px;">Γ ∪ Δ ⊢ A ∧ B</span><span style="display: inline-block; padding-top: 1px;">CONJ</span></div></td></tr><tr><td>∨</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A ∨ B</span><span style="display: inline-block; padding-top: 1px;">Γ ∪ (Γ<sub>1</sub> \ {A}) ∪ (Γ<sub>2</sub> \ {B})</span><span style="display: inline-block; padding-top: 1px;">C</span><span style="display: inline-block; padding-top: 1px;">DISJ CASES</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A ∨ B</span><span style="display: inline-block; padding-top: 1px;">DISJ1</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ B</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A ∨ B</span><span style="display: inline-block; padding-top: 1px;">DISJ2</span></div></td></tr><tr><td>⇒</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A → B</span><span style="display: inline-block; padding-top: 1px;">Γ ∪ Δ ⊢ B</span><span style="display: inline-block; padding-top: 1px;">MP</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ B</span><span style="display: inline-block; padding-top: 1px;">Γ \ {A} ⊢ A → B</span><span style="display: inline-block; padding-top: 1px;">DISCH</span></div></td></tr><tr><td>∀</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A[c/x]</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ ∀xA</span><span style="display: inline-block; padding-top: 1px;">GEN</span><span style="display: inline-block; padding-top: 1px;">if x is not free in Γ</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ∀xA</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A[t/x]</span><span style="display: inline-block; padding-top: 1px;">SPEC</span></div></td></tr><tr><td>∃</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A[t/x]</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ ∃xA</span><span style="display: inline-block; padding-top: 1px;">EXISTS</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ∃xA[x]</span><span style="display: inline-block; padding-top: 1px;">Δ, A ⊢ B</span><span style="display: inline-block; padding-top: 1px;">Γ ∪ Δ \ {A[v/x]} ⊢ B</span><span style="display: inline-block; padding-top: 1px;">CHOOSE</span></div></td></tr><tr><td>¬</td><td><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ¬A</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A → ⊥</span><span style="display: inline-block; padding-top: 1px;">NOT ELIM</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ¬A = ⊥</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ ¬A</span><span style="display: inline-block; padding-top: 1px;">EQF ELIM</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ A → ⊥</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ ¬A</span><span style="display: inline-block; padding-top: 1px;">NOT INTRO</span></div><div style="text-align: center;"><span style="display: inline-block; border-bottom: 1px solid black; padding-bottom: 1px;">Γ ⊢ ¬A</span><span style="display: inline-block; padding-top: 1px;">Γ ⊢ A = ⊥</span><span style="display: inline-block; padding-top: 1px;">EQF INTRO</span></div></td></tr></tbody></table>
Chapter 3

HOL Proof Checking with
OpenTheory, Holide and Dedukti

Higher order inference systems have played an important role in formal mathematics, software
verification and hardware verification. The necessity of proof checking follows from the need
of correctness of such systems and rooted in three reasons: 1) proof systems may have bugs
and may lead to errors in proofs but not apparent within the proof system themselves. 2)
Proofs nowadays can be huge, making impossible to check by hand. For example [18] takes
a team of scientists a few years to complete. 3) since Simple Type Theory is not sound and
complete [13], there is no guarantee for proofs in proof systems to be error free. Cousineau
and Dowek showed that Simple Type Theory can be embedded in the λΠ-calculus Modulo as
well as other Pure Type System (PTS) [10]. This laid the logic foundation of Dedukti [31],
a universal proof checker. On top of Dedukti, Holide [5] was developed to transform proofs
from OpenTheory to Dedukti.

3.1 OpenTheory and OpenTheory HOL Light

It is necessary to have a certain amount of proofs both for testing, transformation and evaluation purposes. In this project, some small proofs were written for testing and debugging reasons but most proofs were retrieved from the OpenTheory library [21]. Although proofs have been developed in HOL Light [20], HOL4 [33] and ProofPower [29], they each contain significant theory formalizations that are not accessible to each other [5, 21]. HOL Light has a formalization of complex analysis while HOL4 has a formalization of probability theory [20, 21, 33]. In contrast, ProofPower has a formalization of the Z specification language [21, 29]. Taking advantage of the similarity of the logic between these systems, OpenTheory has developed a standard article file format for serializing proofs of higher order logic [21]. Table 3.1 shows the OpenTheory logic kernel which has some small differences compared with the HOL Light kernel<fnref n="1" />. The OpenTheory<fnref n="2" /> is a cross-platform proof package

<footnote n="1">¹Note that AppThm Corresponds to MK_COMB in HOL Light, not AP_THM.</footnote>

<footnote n="2">²http://opentheory.gilith.com/</footnote>
manager for proofs in theorem provers of HOL family. OpenTheory is organised into packages by theory. Such theories include lists, natural numbers, functions, etc<fnref n="3" />. OpenTheory comes along with the idea of "theory engineering" and has inspired further exploration on theory management between HOL families [15,23] as well as the development of several projects [5,6] takes advantage of these packages. OpenTheory HOL-Light<fnref n="4" /> is a modified version of HOL Light with the ability to export standard theory library in the OpenTheory standard proof format (.art). The standard library of OpenTheory can be considered equivalent to the proofs in OpenTheory HOL Light [21].

<figure><img src="image_1.png" /><figcaption>Table 3.1: OpenTheory version 5 Logic Kernel [21]</figcaption></figure>

### 3.1.1 OpenTheory Version 6

OpenTheory expanded the logic kernel with four inference rules in version 6: *proveHyp*, *trans*, *sym* and *defineTypeOp* (as in Table 3.2). This made some software depending on it out of date. A full comparison table between version 5 and version 6 is adapted from the announcement<fnref n="5" />.

<figure><img src="image_2.png" /><figcaption>Table 3.2: New and Updated Inference Rules of OpenTheory (version 6)</figcaption></figure>

<footnote n="3">³http://opentheory.gilith.com/packages/</footnote>

<footnote n="4">⁴http://src.gilith.com/hol-light.html</footnote>

<footnote n="5">⁵The version 6 announcement is here:</footnote>

<footnote>http://www.gilith.com/pipermail/opentheory-users/2014-December/000461.html</footnote>
<table><caption>Table 3.3: Differences between version 5 and version 6</caption><thead><tr><th>Command</th><th>New or Updated</th><th>Description</th></tr></thead><tbody><tr><td>version</td><td>new</td><td>Specify the version of article files.</td></tr><tr><td>proveHyp trans sym</td><td>new</td><td>These three new commands provide an efficient implementation of three frequently used derived inference rules to produce more compact article files.</td></tr><tr><td>defineConstList</td><td>new</td><td>The command defineConstList prov with ides a more abstract principle for constant definition. This supports recent extensions to HOL4 and ProofPower.</td></tr><tr><td>hdTl</td><td>new</td><td>The command hdTl provides a destructor function for lists (an inverse to the existing cons command). Together with the new command defineConstList, making it possible to store constants in the dictionary.</td></tr><tr><td>defineTypeOp</td><td>updated</td><td>The command defineTypeOp has been changed so that the theorems giving the defining properties of the abstraction and representation functions have no free variables. They were:<br> ⊢ (abs (rep a)) = a;<br> ⊢ (rep(absr) = r) = φr<br> And they are now<br> ⊢ (λa. abs (rep a)) = λa. a;<br> ⊢ λr.φr = (λr. rep (abs r) = r)</td></tr><tr><td>pragma</td><td>new</td><td>The new command pragma allows a writer to ask for a reader to take some implementation-dependent action, e.g., to produce debug output.</td></tr></tbody></table>

## 3.2 λΠ-calculus and λΠ-calculus Modulo and Dedukti

λΠ-calculus is also known as LF. It is a typed λ-calculus with dependent types. The type of functions is written Πx : A.B. When x does not appear free in B, it can be denoted as A → B. An example of dependently typed term is the term λx : int.p : Πx : int. A x. This term means that the type of p depends on the integer x. Think of p as a piece of paper of size A x. If x is 4 then the paper p is of size A4. If there exist a paper of size A4, then the type A4 is inhabitable. λΠ-calculus is useful since through the Curry-Howard correspondence, it can represent a variety of logics [19]. There are several formalizations of simple type theory in λΠ-calculus such as [3], [30], [5] and [32]. The main idea of this approach is "propositions as types" and "proofs as terms". For each proposition φ in HOL, we have a type ||φ|| in λΠ-calculus. φ is provable if and only if the type ||φ|| is inhabitable. A proof of φ is translated as a term of type ||φ||. Thus, the correctness of the proof is equivalent to the well-typedness of the term [5]. A signature contains constants while a context is a list of variable declarations. The syntax of λΠ-calculus is as follows, where · represents empty signature or empty context.:
term | typet t = x | Type | Kind | Π x. t t | λ x. t t | t t

contexts Γ ::= · | Γ, x : A

signatures Σ ::= · | Σ, c : A

λΠ-calculus Modulo is λΠ-calculus combined with rewriting technique similar to Deduction Modulo. As an extension of λΠ-calculus, in λΠ-calculus Modulo, a signature contains constants as well as rewriting rules:

$$ \Sigma ::= \cdot | \Sigma, c : A | \Sigma, [\Gamma] M \leadsto N $$

In the formula above, $\Sigma, [\Gamma] M \leadsto N$ means to add the rewriting rule $M \leadsto N$ to the signature $\Sigma$ regarding the context $\Gamma$. To keep type checking decidable, the free variables on the right-hand-side must appear on the left-hand-side and the left-hand-side must follow the higher order pattern fragment [26] in rewrite rules [4, 5]. Deduction Modulo takes advantage of rewriting techniques. There are several notations to be introduced. Assuming $R$ is a set of rewriting rules, $\rightarrow_R$ represents induced reduction relation while $\rightarrow_R^+$ means transitive closure. In addition, $\rightarrow_R^*$ refers to reflexive transitive closure. $\equiv_R$ is denoted as the reflexive, symmetric, transitive closure [5]. This thesis follows the notation of [5] and uses $\beta\Sigma$ as the union of the $\beta$ rule with the rewrite rules of $\Sigma$. The reduction relation $\rightarrow_{\beta\Sigma}$ should be confluent and strongly normalizing. Table 3.4 contains the typing rules for λΠ-calculus Modulo [5].
$$ \frac{\Gamma \ context \ (x : A) \in \Gamma}{\Gamma \vdash x : A} \ Var $$

$$ \frac{\Gamma \ context \ (c : A) \in \Sigma}{\Gamma \vdash c : A} \ Const $$

$$ \frac{\Gamma \ context}{\Gamma \vdash \mathit{Type} : \mathit{Kind}} \ \mathit{Type} $$

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma, x : A \vdash B : s}{\Gamma \vdash \Pi x : A.B : s} \ \mathit{Prod} $$

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad \Gamma, x : A \vdash M : B}{\Gamma \vdash \lambda x : A.M : \Pi x : A.B} \ \mathit{Abs} $$

$$ \frac{\Gamma \vdash M : \Pi x : A.B \quad \Gamma \vdash N : A}{\Gamma \vdash M N : [N/x]B} \ \mathit{App} $$

$$ \frac{\Gamma \vdash M : A \quad \Gamma \vdash B : \mathit{Type} \quad A \equiv_{\beta\Sigma} B}{\Gamma \vdash M : B} \ \mathit{Conv} $$

$$ \frac{\Sigma \ signature \ .context}{.context} \ Emptyctx $$

$$ \frac{\Gamma \vdash A : \mathit{Type} \quad x \notin \Gamma}{\Gamma, x : A context} \ VarCxt $$

$$ \frac{.signature}{.context} \ Emptytsig $$

$$ \frac{\Sigma | \vdash A : s \quad c \notin \Sigma}{\Gamma, c : A signature} \ ConstSig $$

$$ \frac{\Sigma | \Gamma \vdash M : A \quad \Sigma | \Gamma \vdash N : A}{\Sigma[\Gamma]M \leadsto N signature} \ RewriteSig $$

<caption>Table 3.4: Typing Rules of the λΠ-calculus</caption>

Dedukti<fnref n="6" /> is a type checker based on λΠ-calculus modulo [31]. Being a logical framework, Dedukti allows the definition of different theories, for instance classical/constructive HOL and Calculus of Constructions [31]. With the help of Holide, CoqInE, Focalide and Krajono<fnref n="7" />, it can perform proof checking on Coq, FoCaLize and Matita proofs<fnref n="8" /> [6]. It has been evaluated to be an efficient and reliable proof checker.

## 3.3 Holide

Holide is translator from HOL proofs to Dedukti [31] developed by Ali Assaf and Guillaume Burel [5]. It accepts files in the OpenTheory standard proof format (.art) and produces files (.dk) for the Dedukti proof checker [5]. The first version translated OpenTheory standard

<footnote n="6">⁶Available at https://www.rocq.inria.fr/deducteam/Dedukti.</footnote>

<footnote n="7">⁷http://dedukti.gforge.inria.fr/</footnote>

<footnote n="8">⁸https://who.rocq.inria.fr/Ali.Assaf/research/krajono-deducteam-2015-slides.pdf</footnote>
library and performed proof checking [5]. This internship project also includes an upgrade
of Holide following the most recent updates of OpenTheory (version 6). The translation is
presented next.

3.3.1 Translation

A signature contains constants and rewriting rules while a context is a list of variable decla-
rations. The following are the translation of HOL types, HOL terms and HOL proofs.

**HOL Types** To translate HOL types we need to introduce a Dedukti type: Type as well as the follows constructors:

• type : Type

• bool : type

• ind : type

• arrow : type → type → type

HOL types could then be translated as Dedukti terms:

• |α| = α

• |bool| = bool

• |ind| = ind

• |A→ B| = arr |A||B|

For an n-ary HOL type operator p, which is of type $\underbrace{type \rightarrow \dots \rightarrow type}_{n} \rightarrow type$, an instance $p(A, \dots, A_n)$ is then translated to the term $p|A_1| \dots |A_n|$.

**HOL Terms** We define a new dependent type called *term*, which depends on a Dedukti type. eq and select are also introduced for equality and the choice operator respectively.

• term : type -> Type

• eq : Πα : type.term(arr α (arr α bool))

• select : Πα : type.term(arr (arr α bool)α)

To translate a HOL type A as a term, we have ||A|| = term |A|. For any HOL term M,
we have the translation |M| defined as follows:
• $|x| = x$

• $|MN| = |M||N|$

• $\lambda x : A.M| = \lambda x : ||A||.|M|$

• $|\langle=\rangle| = eq|A|$

• $|select_A| = select|A|$

Holide has also introduced a rewriting rule to ensure terms are well-typed [5].

$$[\alpha : type, \beta : type] term(arr \alpha \beta) \rightsquigarrow term\alpha \rightarrow term\beta$$

In addition, for every family of HOL constant $c$ of type $A$ with free variables $\alpha_1, \dots, \alpha_n$, we declare a new constant of type $\Pi\alpha_1 : type. \dots \Pi\alpha_n : type. ||A||$. And an instance of the constant $c_{A_1, \dots, c_{A_n}}$ by $c|A_1| \dots |A_n|$.

**HOL Proofs** Similar as terms, we introduce another constant with dependent type: proof : term bool → Type, indexed by the corresponding HOL proposition. For any context $\Gamma = \phi_1 \dots \phi_n$, we define $||\Gamma|| = h_{\phi_1} : ||\phi_1||, \dots, h_{\phi_n} : ||\phi_n||$, where $||\phi|| = proof\phi$ and $\phi_1 \dots \phi_n$ are fresh variables [5]. We declare the following constants:

• Refl : $\Pi\alpha : type. \Pi x : term\alpha. proof(eq\alpha x x)$

• FunExt : $\Pi\alpha, \beta : type. \Pi f, g : term(arrow\alpha\beta). \Pi x : term\alpha. proof(eq\beta(f x)(g x))) \rightarrow proof(eq(arrow\alpha\beta)f g)$

• AppThm : $\Pi\alpha, \beta : type. \Pi f, g : term(arrow\alpha\beta). \Pi x, y : term\alpha. proof(eq(arrow\alpha\beta)f g) \rightarrow proof(eq\alpha x y) \rightarrow proof(eq\beta(f x)(g y))$

• PropExt : $\Pi p, q : term\ bool. (proof q \rightarrow proof p) \rightarrow (proof q \rightarrow proof p) \rightarrow proof(eq\ bool p q)$

• EqMp : $\Pi p, q : term\ bool. proof(eq\ bool p q) \rightarrow proof p \rightarrow proof q$

The proofs can then be translated as:

The constant FunExt is short for *functional extensionality*<fnref n="9" />, which is used for the translation of both **AbsThm**s as well as the $\eta$ axiom [5]. Translation of rules are provided as follows, where $i$ is the index of proof $D_i$.

<footnote n="9">⁹Functional extensionality means that if two functions $f$ and $g$ are of type $A \rightarrow B$ and are equal on all values $x$ of type $A$, then $f$ and $g$ are equal.</footnote>
$$ \overline{\vdash t = t} \ \mathrm{refl} \ t \quad = \mathrm{Refl} \ |A||M|, \text{ where } M : A $$

$$ \frac{\Gamma \vdash t = u}{\Gamma \vdash (\lambda v.t) = (\lambda v.u)} \ \mathrm{absThm} \ v \quad = \mathrm{FunExt} |A||B||\lambda x : A.M||\lambda x : A.N|(\lambda x : |A|.|\mathcal{D}|) $$

$$ \frac{\Gamma \vdash f = g \quad \Delta \vdash x = y}{\Gamma \cup \Delta \vdash f x = g y} \ \mathrm{appThm} \quad = \mathrm{AppThm} |A||B||F||G||M||N||\mathcal{D}_1||\mathcal{D}_2| $$

$$ \overline{\vdash (\lambda v.t) u = t[u/v]} \ \mathrm{betaConv}((\lambda v.t) u) \quad = \mathrm{Refl} |B||M|, \text{ where M is of type B} $$

$$ \overline{\{\varphi\} \vdash \varphi} \ \mathrm{assume} \ \varphi \quad = h_{\phi}, \text{ where } h_{\phi} \text{ is a fresh variable} $$

$$ \frac{\Gamma \vdash \varphi \quad \Delta \vdash \psi}{(\Gamma \setminus \{\psi\}) \cup (\Delta \setminus \{\varphi\}) \vdash \varphi = \psi} \ \mathrm{deductAntisym} \quad = \mathrm{ProfExt} |\phi||\psi|(\lambda h_{\psi} : ||\psi||.|\mathcal{D}_1|)(\lambda h_{\phi} : ||\phi||.|\mathcal{D}_2|) $$

$$ \frac{\Delta \vdash \varphi \quad \Gamma \vdash \varphi = \psi}{\Gamma \cup \Delta \vdash \psi} \ \mathrm{eqMp} \quad = \mathrm{EqMp} |\phi||\psi||\mathcal{D}_1||\mathcal{D}_2| $$

$$ \frac{\Gamma \vdash \phi}{\Gamma[\theta] \vdash \phi[\theta]} \ \mathrm{TypeSubst} \quad = (\lambda \alpha_1 : \mathrm{type} \dots \lambda \alpha_m : \mathrm{type} . |D|) |A_1| \dots |A_m| $$

$$ \frac{\Gamma \vdash \phi}{\Gamma[\sigma] \vdash \phi[\sigma]} \ \mathrm{TermSubst} \quad = (\lambda x_1 : ||B|| \dots \lambda x_n : ||B_n|| . |D|) |M_1| \dots |M_n| $$

### 3.3.2 Correctness

Completeness is to guarantee that the translated HOL terms have correct types. While soundness states that if a proof term is well-typed in Dedukti, the proofs must be correct in HOL Light. The completeness and soundness gives the correctness of a translation and was proved in [5].

### 3.3.3 Holide2

Recent updates of the OpenTheory format as shown in Table 3.3 requires an update of the Holide program (although users can still use the old version of Holide by limiting the output of OpenTheory to version 5). Holide uses a modular translation of higher order logic to Dedukti which makes the translation possible to extend [5]. The following shows an extension of Holide's translation. In addition, the following constants were added to Holide2 for to translate proofs using sym, trans and proveHyp.

* Sym : Πα : type.Πx, y : α.proof(eq bool x y) → proof(eq bool y x)

* Trans : Πα : type.Πx, y, z : term αproof(eq α x y) → proof(eq α y z) → proof(eq α x z)

* ProveHyp : Πx, y : term bool.proof x → proof y → proof y

$$ \frac{\Gamma \vdash \varphi = \psi}{\Gamma \vdash \psi = \varphi} \ \mathrm{sym} \quad = \mathrm{Sym} |A||t_1||t_2| $$

$$ \frac{\Gamma \vdash s = t \quad \Delta \vdash t = u}{\Gamma \cup \Delta \vdash s = u} \ \mathrm{trans} \quad = \mathrm{Trans} |A||x||y||z||D_1||D_2| $$
$$ \frac{\Gamma \vdash \varphi \quad \Delta \vdash \psi \quad \text{proveHyp}}{\Gamma \cup (\Delta \setminus \{\varphi\}) \vdash \psi} = \text{ProveHyp} |x||y||D_1|\lambda x : ||t_1||.|D_2| $$

Similar as Holide, Holide2 takes HOL proofs in the OpenTheory article format (.art) of version 6 as input and outputs a Dedukti file (.dk). A comparison of Holide1 and Holide2 is shown in Table 6.2 and Table 6.3 in Chapter6
# Chapter 4

## Reverse Engineering of HOL Proofs

The relationship between classical inference systems and constructive (a.k.a intuitionistic) inference systems has been a longstanding field of research. The concept of intuitionism dates back to the discovery by Brouwer that classical mathematics do not correspond to the intuition we have of the mathematical objects. The discussion of classical and constructive reasoning continues after the discovery of some paradoxes and inconsistencies [14], especially Gödel's incompleteness theorem. Proving by contradiction in classical inference systems was also considered to be one of the sources of problems. In addition, classical reasoning would also lead to the lose of the witness property [12]. This showed the limitations of classical inference systems. Some thought classical reasoning should be allowed as long as it was finitistically justified while others insist to avoid non-constructive proofs [14]. In the middle the debate of intuitionism and classifcism lies the law of excluded middle (LEM). Depending on whether there is a proof for $P \lor \neg P$ for any $P$ or not, inference systems are classified in classical logic (if there is such a proof) or constructive logic. A proof is regarded constructive when it is not using the law of excluded middle. Constructive proofs can also be considered classical proofs without using the law of excluded middle rule. Logical Framework provides a means to present a logic as a signature in such a way that provability of a formula in the original logic reduces to a type inhabitation problem in the framework type theory. In Logical Framework, proofs are defined using definitions of logical constants, connectives, quantifiers and axioms. Using a Logical Framework, the theories are made explicit, making it possible to investigate which part of the theory is needed for each given proof. This analysis is called "reverse engineering proofs". For instance, it is possible to investigate which proofs do not use the excluded middle. If so, these proofs can be expressed in the weaker constructive system. This internship project aimed at such automatic analysis for higher order logic by picking constructive-compatible definitions and transform proofs using those definitions.

An alternative view of this is to consider classical proofs as constructive proofs by embedding classical constants, connectives and quantifiers in constructive logic. Embedding methods of similar fashion are usually referred to as "double negation translation" or "negative translation". Double negation translation has a history back to 1925 from Kolmogorov's
translation [24]. Pioneering work also includes Gödel's translation in 1933 and Gentzen's translation in 1936 [17]. In 2013, another translation was provided by Dowek [12]. Most recently, Gilbert and Hermant provided a minimal translation for First Order Logic Sequent Calculus as morphism [16]. A morphism is to define an embedding of classical connectives, constants and quantifiers so that formulas that are provable in classical logic have its transformed formula provable in constructive logic.

## 4.1 Double Negation Translation

Negative translation has a history back to Kolmogorov's translation [24], following that was Gödel's translation in 1933 [17] and Gentzen's translation in 1936. Most recently, Gilbert and Hermant provided a minimal translation for First Order Logic Sequent Calculus [16].

The first double negation translation was proposed by Kolmogorov by putting a double negation in front of every subformula [14]. Following Kolmogorov, a similar translation was presented by Gödel and Gentzen [14, 17, 22]<fnref n="1" />. Later in 1950s, Kuroda proposed another translation [25]. Most recently, Gilbert and Hermant presented a minimal translation [16]. The translation has been proved to be minimal for formulas that are not in the form of $A_0 \wedge A_0 \wedge \dots \wedge A_n$, namely barred formulas [16]. Barred formulas are those not in the form of $A_0 \wedge A_0 \wedge \dots \wedge A_n$. A translation which depends on the subformulas of the formula to be translated is proof-dependent. Although the translation varies, the development of double negation translation aims at simpler and more efficient translation without losing properties. Table 4.1 sums up some properties. The entry “Morphism” refers to whether a translation is a connective to connective translation making it a morphism<fnref n="2" />. However all of the translations require universal quantifier and implication to be primitively defined. This lead to the change of the kernel of OpenTheory HOL for the sake of double negation translation.

<footnote n="1">¹Note that Gödel's original translation also puts double negation in front of the translated terms of implication.</footnote>

<footnote n="2">²Kuroda's translation has an additional double negation in front of the whole proposition, making it not a morphism.</footnote>
<table><caption>Table 4.1: Properties of Translation Compared</caption><thead><tr><th>Property</th><th>Gödel-Gentzen</th><th>Kuroda</th><th>Gilbert-Hermant</th></tr></thead><tbody><tr><td>Translation</td><td>⊥<sup>gg</sup> = ⊥<br>⊤<sup>gg</sup> = ⊤<br>P<sup>gg</sup> = ¬¬P, for P atomic<br>A ∧<sup>gg</sup> B = A<sup>gg</sup> ∧ B<sup>gg</sup><br>A ∨<sup>gg</sup> B = ¬¬(A<sup>gg</sup> ∨ B<sup>g</sup>)<br>A ⇒<sup>gg</sup> B = (A<sup>gg</sup> ⇒ B<sup>gg</sup>)<br>¬<sup>gg</sup> A = ¬A<sup>gg</sup><br>∀<sup>gg</sup>xA = ∀xA<sup>gg</sup><br>∃<sup>gg</sup>xA = ¬¬∃xA<sup>gg</sup></td><td>⊥<sup>ku</sup> = ⊥<br>⊤<sup>ku</sup> = ⊤<br>P<sup>ku</sup> = P, for P atomic<br>A ∧<sup>ku</sup> B = A<sup>ku</sup> ∧ B<sup>ku</sup><br>A ∨<sup>ku</sup> B = (A<sup>ku</sup> ∨ B<sup>g</sup>)<br>A ⇒<sup>ku</sup> B = (A<sup>ku</sup> ⇒ B<sup>ku</sup>)<br>¬<sup>ku</sup> A = ¬A<sup>ku</sup><br>∀<sup>ku</sup>xA = ∀x¬¬A<sup>ku</sup><br>∃<sup>ku</sup>xA = ∃xA<sup>ku</sup></td><td>⊥<sup>m</sup> = ⊥<br>⊤<sup>m</sup> = ⊤<br>P<sup>ku</sup> = P, for P atomic<br>A ∧<sup>m</sup> B = A<sup>m</sup> ∧ B<sup>m</sup><br>A ∨<sup>m</sup> B = ¬¬(A<sup>m</sup> ∨ B<sup>m</sup>)<br>A ⇒<sup>m</sup> B = A<sup>m</sup> ⇒ ¬¬B<sup>m</sup><br>¬<sup>m</sup> A = ¬A<sup>m</sup><br>∀<sup>m</sup>xA = ∀x¬¬A<sup>m</sup><br>∃<sup>m</sup>xA = ¬¬∃xA<sup>m</sup></td></tr><tr><td>Proof-dependent</td><td>No</td><td>No</td><td>Yes</td></tr><tr><td>Γ ⊢<sup>c</sup> |A| → Γ ⊢<sup>i</sup> |A|</td><td>Yes</td><td>Yes</td><td>Yes</td></tr><tr><td>Γ ⊢<sup>c</sup> |A| → Γ ⊢<sup>i</sup> |A|</td><td>Yes</td><td>Yes</td><td>only if A is barred</td></tr><tr><td>Morphism</td><td>No</td><td>No</td><td>Yes</td></tr><tr><td>Minimal Translation</td><td>No</td><td>No</td><td>Yes</td></tr></tbody></table>

## 4.2 Kernel Hacking for Reverse Engineering of HOL Proofs

There are several reasons for removing equality as primitive symbols. The first and the most important being that all theoretical results of double negation translation so far are based on universal and implication. Having universal quantifier and implication would also make the system fundamentally more similar as other proof assistants which would make it easier to transport proofs between each other. In addition, such change would bring the system of HOL Light and Dedukti closer for further optimisation of proof checking since Dedukti's logic foundation is based on universal quantifier and implication. Several attempts have been made to modify the kernel but none of them lead to a successful result by the deadline of the project. Among them HOLALA is to be presented in Chapter 5 and the rest are attached in Appendix C.
# Chapter 5
## HOLALA

As introduced in Chapter 2, HOL Light has a reliable kernel where equality and related primitive inference rules are defined. Based on the logic kernel, other connectives and constants were introduced as axioms followed by derived inference rules. HOLALA is a modified version of OpenTheory HOL Light where the kernel consists of three primitive logic symbols and their corresponding inference rules with some modification of OpenTheory HOL Light's proof logging methods.

### 5.1 Kernel Hacking

#### 5.1.1 Logic Kernel

<table><caption>Table 5.1: Primitive and Axiomatic Definitions of Connectives and Constants Comparison</caption><thead><tr><th></th><th>Q<sub>0</sub></th><th>OpenTheory HOL Light</th><th>HOLALA</th></tr></thead><tbody><tr><td>=`</td><td>primitive</td><td>primitive</td><td>primitive</td></tr><tr><td>⇒</td><td>λpq.(p = (p ∧ q))</td><td>λpq.p ∧ q = p</td><td>primitive</td></tr><tr><td>∀</td><td>λp.A = λp.⊤</td><td>λp.p = λx.⊤</td><td>primitive</td></tr><tr><td>∃</td><td>¬∀x¬A</td><td>λp.∀q.(∀x.px ⇒ q) ⇒ q</td><td>λp.∀q.(∀x.px ⇒ q) ⇒ q</td></tr><tr><td>⊤</td><td>= = =</td><td>λp.p = λp.p</td><td>∀x.(x ⇒ x)</td></tr><tr><td>⊥</td><td>λx.T = λx.x</td><td>∀p.p</td><td>∀p.p</td></tr><tr><td>∧</td><td>λx.λy.(λg.g⊤⊤ = λg.gxy)</td><td>λpq.(λf.fpq) = λf.f⊤⊤</td><td>λpq.(∀x.(p ⇒ ((q ⇒ x) ⇒ x)))</td></tr><tr><td>∇</td><td>λxy.¬(¬x ∧ ¬y)</td><td>λpq.∀.(p ⇒ r) ⇒ ((q ⇒ r) ⇒ r)</td><td>λpq.∀.(p ⇒ r) ⇒ ((q ⇒ r) ⇒ r)</td></tr><tr><td>¬</td><td>λx.⊤ = λx.x</td><td>λp.p ⇒ ⊥</td><td>λp.p ⇒ ⊥</td></tr><tr><td>∃</td><td>¬∀x¬A</td><td>λp.∀q.(∀x.px ⇒ q) ⇒ q</td><td>λp.∀q.(∀x.px ⇒ q) ⇒ q</td></tr><tr><td>⇔</td><td>=</td><td>=</td><td>=</td></tr><tr><td>∃!</td><td>(∃p) ∧ (∀xy.px ∧ py ⇒ x = y)</td><td>(∃p) ∧ (∀xy.px ∧ py ⇒ x = y)</td><td>(∃p) ∧ (∀xy.px ∧ py ⇒ x = y)</td></tr></tbody></table>

The Logic kernel of OpenTheory HOL Light has some modification from HOL Light. HOLALA can be considered a modified version of OpenTheory HOL Light. HOLALA does not only take equality as primitive symbol but also implication and universal quantification. The logic kernel consists of three primitive logic symbols defined based on implication and universal quantifier, together with their corresponding inference rules. Table 5.1 presents the
<figure><img src="image_3.png" /><figcaption>Figure 5.1: Dependency of Constants and Connectives Analysis</figcaption></figure>

constants of the logic kernel of HOLALA in comparison with $Q_0$ and OpenTheory HOL Light. Compared with OpenTheory HOL Light, HOLALA also changed the definition of $\vdash$, and $\wedge$, making as many definitions of logic symbol as possible dependent on universal quantification and implication instead.

To summarise, Table 5.1 presents a comparison with $Q_0$, OpenTheory HOL Light and HOLALA. Figure 6.5 shows the dependency analysis of OpenTheory HOL Light and HOLALA. Note that the graph omits equality as the definition symbol $\equiv$ for the sake of simplicity. In practice, the equality plays the role of $\equiv$ in every single axiom in HOLALA.

New primitive rules corresponding to implication and universal quantifier are therefore transported in the kernel as in Table 5.2. An immediate benefit of such change is that deduction rules directly related to $\forall$ and $\rightarrow$ got shortened. Deductive rules defined in *bool.ml* would therefore need to be reproved. Table 5.3 shows the smallest proof<fnref n="1" /> using the four basic rules which are outside of the kernel in OpenTheory but primitive (within the kernel) in HOLALA. Following that are some examples of derived rules as well as a comparison of the size of a proof of the Law of Excluded Middle. It is clear that smallest proofs using MP, DISCH, GEN and SPEC has reduced a dramatic amount of steps each. Deduced rules such as CONJ, IMP_ANTISYM_RULE and DISJ1 also reduced a significant amount of steps. However for rules not dependent on such changes, for example TRUTH<fnref n="2" />, the size stays the same. It is also noted that proving the law of excluded middle takes a significant number of steps instead of just one. More evaluation will be presented in the next section.

Although such change lead to reduction of size in most cases, users would lose the original definition of the $\forall$ and $\rightarrow$. Proofs using these two definitions directly would therefore report errors. To fix it, these two definitions were proved as theorems after the introduction of the axiom of extensionality in HOLALA.

<footnote n="1">¹Such proofs takes branches obtained by only one step of the axiom rule and directly followed by the inference rule.</footnote>

<footnote n="2">²In both systems, TRUTH is taken as a proof using EQ MP, SYM, T_DEF and REFL. None of these rules are directly related to the changes made by HOLALA.</footnote>
$$ \frac{\Gamma \vdash A \to B \qquad \Delta \vdash A}{\Gamma \cup \Delta \vdash B} MP $$

$$ \frac{\Gamma \vdash A[c/x]}{\Gamma \vdash \forall x A} GEN \text{ if x is not free in } \Gamma $$

$$ \frac{\Gamma \vdash B}{\Gamma \setminus \{A\} \vdash A \to B} DISCH $$

$$ \frac{\Gamma \vdash \forall x A}{\Gamma \vdash A[t/x]} SPEC $$

<table><caption>Table 5.2: Additional Primitive Inference Rules of HOLALA</caption><thead><tr><th></th><th>OpenTheory HOL Light</th><th>HOLALA</th></tr></thead><tbody><tr><td>MP</td><td>113</td><td>3</td></tr><tr><td>DISCH</td><td>106</td><td>2</td></tr><tr><td>GEN</td><td>23</td><td>2</td></tr><tr><td>SPEC</td><td>140</td><td>2</td></tr><tr><td>CONJ</td><td>57</td><td>33</td></tr><tr><td>DISJ1</td><td>158</td><td>23</td></tr><tr><td>IMP_ANTISYM_RULE</td><td>156</td><td>7</td></tr><tr><td>TAUT ( ∀ p.(p ∨ ¬p))</td><td>341</td><td>165</td></tr></tbody></table>

<caption>Table 5.3: Size of Deductive Rules Between OpenTheory HOL Light and HOLALA</caption>

### 5.1.2 Proof Logging

OpenTheory HOL Light modified the kernel of HOL Light and made it possible to export proofs by introducing a proof type. Instead of recording only the hypothesis and conclusion of proofs as in HOL Light, OpenTheory HOL Light records each step of HOL Light and deletes them after exporting to articles. HOLALA takes a similar approach but replaces the proof of the theorem Law of Excluded Middle (LEM) by a LEM_proof as record of classicism. HOLALA therefore considers a proof being classical when it uses LEM. Instead of simply replacing the record of proofs by axiom proofs after exporting, HOLALA performs structural and statistical analysis and then takes the proof as a term of Lemma with corresponding results of analysis. Such analysis includes, detection of LEM, i.e. a sign of classical proof or constructive proof, size of proof, axioms used in a proof as well as classical and constructive lemmas used. Such improved proof logging and exporting technique leads to a search engine to be presented at the end of next chapter, namely ProofCloud.

## 5.2 Holide2x

HOLALA extends the logic kernel of HOL Light. Thus, a translation the following four inference rules is necessary. This is captured in another variant of Holide, namely Holide2x. The following is the modification of translation of types, terms and proofs. The translation
of HOL types remains the same but, to deal with universal quantifier and implication and their rules, Holide2x declares the imp andforall together with MP, DISCH, GEN and SPEC as constants.

5.2.1 HOL Terms

Similar to equality, universal quantification is also of polymorphic type. The translation of
terms using universal quantification and existential quantification would therefore then be:
|!(M : A)| = **forall**|A||M| and |M| = ⇒ N| = **imp**|M||N|.

• imp : term bool → term bool → term bool

• **forall** : Πα : type → term (arr α bool) → term bool

• | → | = imp

• |(!_A)| = **forall**|A|

5.2.2 HOL Proofs

There are only four new inference rules introduced. The translation of proofs using these rules
are in the same style as [5].

| $\frac{\Gamma \vdash A \to B \quad \Delta \vdash A}{\Gamma \cup \Delta \vdash B}$ MP $\big| = MP|A||B||\mathcal{D}_1||\mathcal{D}_2|$, where $\mathcal{D}_1$ and $\mathcal{D}_2$ are the proofs
of $A \to B$ and $A$ respectively.

| $\frac{\Gamma \vdash A[c/x] \quad \Gamma \cup \forall x A}{\Gamma \vdash A}$ GEN, if $x$ is not free in $\Gamma$ $\big| = \text{GEN}|A||c'|||\mathcal{D}'|$, where $c' = \lambda x : ||A||.|c|$, $\mathcal{D}$ is a proof of $A[c/x]$ and $\mathcal{D}' = \lambda x : ||A||.|\mathcal{D}|$

| $\frac{\Gamma \vdash \mathcal{B} \quad \Gamma \setminus \{A\} \vdash \mathcal{A} \to \mathcal{B}}{\Gamma \vdash \mathcal{A} \vdash \mathcal{B}}$ DISCH $\big| = \text{DISCH}|\mathcal{A}|\mathcal{B}|\mathcal{D}'|\mathcal{D}|$, where $\mathcal{D}'$ is a proof of $\mathcal{A}$ and $\mathcal{D}$ is a proof of $\mathcal{B}$

| $\frac{\Gamma \vdash \forall x A \quad \Gamma \vdash A[t/x]}{\Gamma \vdash SPEC}$ $\big| = SPEC|A|t'|u||\mathcal{D}|$, where $t' = \lambda x : ||A||.|t|$ and $\mathcal{D}$ is a proof of $\mathcal{B}$ respectively.

The four constants MP, DISCH, GEN and SPEC introduced are as below.

MP: Πp : term bool. Πq : term bool. proof(imp p q) → proof p → proof q

DISCH: Πp : term bool. Πq : term bool. proofp → proof q → proof(imp p q)

GEN : Πα : type. Πp' : (term α → term bool) . Πx : term α. proof(p' x ) → proof(forall λ x .p'x )

SPEC : Πα : type. Πt : (term α → term bool) . Πu : term α. proof(forall α t ) → proof(t u )

This extended version of Holide completes the workflow of proof checking of OpenTheory
packages. proofs in HOLALA can be exported to new article files ( .artx ) and then translated
as Dedukti files. Detailed evaluation and proof checking are to be presented in Chapter 6.
# Chapter 6

## Proof Analysis and Evaluation

In this section, the workflow of this project is first illustrated. Following that are some structural and statistical analysis of OpenTheory using Holide, HOLALA and Dedukti. In addition, specification of ProofCloud will be presented at the end of the chapter.

### 6.1 Workflow

<figure><img src="image_4.png" /><figcaption>Figure 6.1: Workflow of HOLALA, Holide, OpenTheory and ProofCloud</figcaption></figure>

This project uses many softwares of different versions. Before presenting the evaluation results, it is necessary to clarify the version correspondence and workflow of this project. On one hand, both OpenTheory repository and users can provide articles<fnref n="1" />. These article files are then converted to Dedukti files by Holide2. Then Dedukti performs proof checking and checking results goes into ProofCloud. On the other hand, proofs scripts can be loaded by HOLALA and perform proof analysis, then exported to HOLALA article files. These article files are then converted to Dedukti files by Holide2x. Similarly, Dedukti conduct proof check-

<footnote n="1">¹All articles in evaluation are assumed to be of OpenTheory version 6.</footnote>
ing. Lastly, results from HOLALA and Dedukti get stored in ProofCloud. ProofCloud is not only a representation of proof analysis and proof checking results but also a search engine for a modified OpenTheory standard library. More details of ProofCloud will be presented at the end of this chapter.

Development of software makes correspondence of versions challenging. A significant amount of time of the project was to update Holide as a result of the changes of OpenTheory format and the changes of logic kernel of HOLALA. The recent updates of OpenTheory from version 5 to version 6 lead to the update of Holide from version 1 to version 2. Although users can still use the old version of Holide by limiting the output of OpenTheory to version 5². Holide2 takes HOL proofs in the OpenTheory article format (.art) of version 6 as input and outputs a Dedukti file (.dk). After translation, dedukti takes the translated files as input and perform proof checking. HOLALA can be considered a modified version of OpenTheory HOL Light and generates articles of its own but can be considered an extended version 6 OpenTheory article. This brought about an alternative of Holide, namely Holide2x. All three of Holide1, Holide2 and Holide2x have been tested. The subsequent Table 6.1 displays the version correspondence clearly. Items in grey in the table are currently maintained by the author. The author has also contributed to the latest version of OpenTheory HOL Light on the import function making HOL Light import theorems from articles of version 6 correctly.

<table><caption>Table 6.1: Version Correspondence of OpenTheory, Holide and HOLALA</caption><thead><tr><th>Article Generator / Repository</th><th></th><th>Article File Extension</th><th>Translation Tool and Version</th><th>Verification Tool</th></tr></thead><tbody><tr><td>OpenTheory Repository</td><td>5</td><td>.art</td><td>Holide1</td><td></td></tr><tr><td>OpenTheory Repository</td><td>6</td><td>.art</td><td>Holide2</td><td rowspan="2">Dedukti</td></tr><tr><td>HOLALA</td><td></td><td>.artx</td><td>Holide2x</td></tr></tbody></table>

## 6.2 Proof Checking

The standard library in OpenTheory Repo grouped theorems into packages, including theorems of booleans, sets, lists, etc. The standard library (the base package, including 11 subpackages) was first verified in this project followed by all the packages in OpenTheory Repo. These tests were completed on a 64-bit Intel Core i5-4590 CPU @3.30GHz ×4 machine with 3.8GB RAM.

Above are two tables with the size of files and the time taken for translation and proof checking. Table 6.2 and Table 6.3 illustrates a comparison of version 1 and version 2 of

<footnote n="2">²Holide1 has checked the standard library of OpenTheory (version 5). The first release of Holide2 (in May 2015) could not translate articles in the lazylist package correctly due to a small mistake in translation of type variables. This has been corrected in most recent release of Holide2.</footnote>
<table><caption>Table 6.2: Size of Article Files and Translation Time</caption><thead><tr><th rowspan="2">Package</th><th colspan="2">Holide 1</th><th colspan="2">Holide 2</th></tr><tr><th>Size (KB)</th><th>Time (s)</th><th>Size (KB)</th><th>Time (s)</th></tr></thead><tbody><tr><td>base</td><td>1,436</td><td>19.35</td><td>1,194</td><td>19.42</td></tr><tr><td>cl</td><td>313</td><td>5.77</td><td>313</td><td>5.56</td></tr><tr><td>empty</td><td>0</td><td>0.20</td><td>0</td><td>0.00</td></tr><tr><td>gfp</td><td>136</td><td>1.42</td><td>112</td><td>1.35</td></tr><tr><td>lazy-list</td><td>1,390</td><td>31.43</td><td>1,391</td><td>31.78</td></tr><tr><td>modular</td><td>45</td><td>1.13</td><td>37</td><td>0.37</td></tr><tr><td>natural-bits</td><td>162</td><td>1.43</td><td>132</td><td>1.39</td></tr><tr><td>natural-divides</td><td>193</td><td>2.10</td><td>157</td><td>1.94</td></tr><tr><td>natural-fibonacci</td><td>130</td><td>1.31</td><td>108</td><td>1.24</td></tr><tr><td>natural-prime</td><td>140</td><td>1.46</td><td>116</td><td>1.34</td></tr><tr><td>parser</td><td>240</td><td>3.22</td><td>204</td><td>3.15</td></tr><tr><td>probability</td><td>26</td><td>0.30</td><td>23</td><td>0.23</td></tr><tr><td>stream</td><td>75</td><td>0.75</td><td>63</td><td>0.73</td></tr><tr><td>word10</td><td>86</td><td>0.76</td><td>71</td><td>0.62</td></tr><tr><td>word12</td><td>88</td><td>0.79</td><td>72</td><td>0.75</td></tr><tr><td>word16</td><td>131</td><td>1.60</td><td>107</td><td>0.77</td></tr><tr><td>word5</td><td>77</td><td>0.70</td><td>64</td><td>1.56</td></tr><tr><td><strong>Total</strong></td><td><strong>4,668</strong></td><td><strong>73.73</strong></td><td><strong>4,377</strong></td><td><strong>72.21</strong></td></tr></tbody></table>

<table><caption>Table 6.3: Size of Dedukti Files and Proof Checking Time</caption><thead><tr><th rowspan="2">Package</th><th colspan="2">Dedukti (Holide 1)</th><th colspan="2">Dedukti (Holide 2)</th></tr><tr><th>Size (KB)</th><th>Time (s)</th><th>Size (KB)</th><th>Time (s)</th></tr></thead><tbody><tr><td>base</td><td>4,681</td><td>10.63</td><td>4,440</td><td>9.74</td></tr><tr><td>cl</td><td>1,219</td><td>2.42</td><td>1,219</td><td>2.46</td></tr><tr><td>empty</td><td>0</td><td>0.00</td><td>0</td><td>0.00</td></tr><tr><td>gfp</td><td>400</td><td>0.73</td><td>375</td><td>0.65</td></tr><tr><td>lazy-list</td><td>5,718</td><td>13.31</td><td>5,717</td><td>13.11</td></tr><tr><td>modular</td><td>120</td><td>0.19</td><td>111</td><td>0.17</td></tr><tr><td>natural-bits</td><td>452</td><td>0.74</td><td>419</td><td>0.68</td></tr><tr><td>natural-divides</td><td>599</td><td>1.11</td><td>566</td><td>0.99</td></tr><tr><td>natural-fibonacci</td><td>378</td><td>0.67</td><td>354</td><td>0.60</td></tr><tr><td>natural-prime</td><td>408</td><td>0.72</td><td>388</td><td>0.65</td></tr><tr><td>parser</td><td>802</td><td>1.87</td><td>776</td><td>1.69</td></tr><tr><td>probability</td><td>72</td><td>0.12</td><td>69</td><td>0.11</td></tr><tr><td>stream</td><td>221</td><td>0.41</td><td>211</td><td>0.38</td></tr><tr><td>word10</td><td>234</td><td>0.38</td><td>216</td><td>0.29</td></tr><tr><td>word12</td><td>239</td><td>0.40</td><td>220</td><td>0.35</td></tr><tr><td>word16</td><td>396</td><td>0.80</td><td>364</td><td>0.36</td></tr><tr><td>word5</td><td>207</td><td>0.33</td><td>192</td><td>0.72</td></tr><tr><td><strong>Total</strong></td><td><strong>16,146</strong></td><td><strong>34.83</strong></td><td><strong>15,637</strong></td><td><strong>32.95</strong></td></tr></tbody></table>
translation by Holide and proof checking by Dedukti. Both article files and Dedukti files are
compressed by gzip to reduce the effect of syntax formatting and whitespace. Translation
and proof checking can be completed within two minutes and are considered to be efficient.
However, there is little difference in terms of efficiency. In addition, the increase of size after
translation is consistent with previous work [5].

For the first time, all OpenTheory packages passed proof checking by Holide2 and Dedukti.
This announced the completion of proof checking of all OpenTheory packages available. The
success of checking of all these packages also provides evidence that OpenTheory being a
reliable platform for higher order proofs as well as the correctness of updates of Holide1 and
Holide2. In addition, this project also provides evidence for the correctness of HOL Light
kernel and proofs from a different perspective compared with [27].

## 6.3 Proof Analysis

As described in Chapter 1, HOLALA changed the proof logging technique of OpenTheory HOL Light and made it possible to do structural and statistical analysis before exporting to article files. HOLALA considers proofs using Law of Excluded Middle as classical proof and constructive otherwise. HOLALA is a modified version of OpenTheory HOL Light and integrates the standard library of 1199 proofs. Among them, there are 531 constructive proofs and 668 classical proofs making 44.29% of them constructive proofs.

Taking axioms and lemmas as one step and all deduction steps as one step, we can calculate
the size of proofs (up to lemma). The size of proofs varies from a few steps to millions of
steps. As illustrated in Table 6.4, compared with OpenTheory HOL Light, there is an overall
reduction of size around 40.87%. This indicates that introducing frequently used inference
rules as primitive inference rules would sharply reduce the size of proofs.

Analysis of OpenTheory proofs (Figure 6.2) shows that two primitive deduction rules
(subst and eqmp) combined makes up to over 45% of all the rules used making it essential
to further investigate the subst and eqmp. One reason is that the kernel of OpenTheory
HOL Light is very small making INST and PINST, EQ MP and MK COMB widely used
in bool.ml and equal.ml<fnref n="3" />. This inspires further work on proof optimisation, especially on the
reduction of the use of the two commands, subst and eqMp, as described in Chapter 6.

In contrast, Figure 6.3 indicates that the introduction of MP, DISCH, GEN and SPEC
has not only reduced total size of article files but also cut the percentage of subst and eqmp
to around 24% resulting more balanced and less dependent deduction system. However, HO-
LALA’s changes have little impact on appthm, trans and sym.

During the project the author also noticed that many common deducted inference rules are

<footnote n="3">³OpenTheory HOL Light takes β-conversion rule as primitive inferences rules which helps reducing the use of EQ MP and INST.</footnote>
<table><caption>Table 6.4: Size and Frequency Analysis of Main Inference Rules of HOL Light and HOLALA Proofs</caption><thead><tr><th></th><th>OpenTheory HOL Light Count</th><th>HOLALA Count</th></tr></thead><tbody><tr><td>subst</td><td>93330</td><td>27217</td></tr><tr><td>eqmp</td><td>92264</td><td>31234</td></tr><tr><td>appthm</td><td>52994</td><td>49712</td></tr><tr><td>proveHyp</td><td>47597</td><td>12782</td></tr><tr><td>betaConv</td><td>21370</td><td>8152</td></tr><tr><td>absThm</td><td>15024</td><td>9088</td></tr><tr><td>trans</td><td>26616</td><td>25337</td></tr><tr><td>refl</td><td>26644</td><td>25061</td></tr><tr><td>deductAntisym</td><td>9528</td><td>1246</td></tr><tr><td>sym</td><td>9401</td><td>8469</td></tr><tr><td>assume</td><td>16950</td><td>8376</td></tr><tr><td>mp</td><td>0</td><td>9644</td></tr><tr><td>disch</td><td>0</td><td>9455</td></tr><tr><td>gen</td><td>0</td><td>6344</td></tr><tr><td>spec</td><td>0</td><td>11327</td></tr><tr><td>Total</td><td>411718</td><td>243444</td></tr></tbody></table>

dependent on INST and INST_TYPE (mostly used via PINST). Having INST or INST_TYPE increased the complexity for proof searching automation. Such inference rule should be thought twice whether to be kept as primitive inference rule.

Since article files are compressed. A more practical way to compare proof size is to consider the size of the article files. Article files are where proofs are stored. The size of both article files and Dedukti files scaled down a lot. Article files of HOLALA are only around 23.63% on average the size of article files of OpenTheory<fnref n="4" />. Leading to an improvement of 41.81% in translation time. Size of Dedukti files got reduced to about 64.33% with a speed improvement of 38.04%.

## 6.4 ProofCloud

ProofCloud<fnref n="5" /> is a proof retrieval engine for easy searching of verified higher order logic proofs<fnref n="6" />. It consists of a presentation of proofs and proof packages, the results of some statistical and structural analyses, together with their proof checking results. So far it has been populated with 1687 proofs from 6 packages of OpenTheory. Information of each proof and package is presented on separate webpages. Taking classical proofs as those using the axiom of choice,

<footnote n="4">⁴For fair comparison, article files and dedukti files are compressed with gzip separately and then the whole folder was compressed by as a tar.gz file. All article files are obtained from "/opentheory/article" directory. To remove the factor of optimisation by opentheory, articles are not combined to packages.</footnote>

<footnote n="5">⁵http://airobert.github.io/proofcloud/</footnote>

<footnote n="6">⁶In this revisited version of internship report, ProofCloud is only about proofs and proof analysis results of OpenTheory. It has nothing to do with Holide2x and HOLALA anymore.</footnote>
<figure><img src="image_5.png" /><figcaption>Figure 6.2: Frequency of Main Inference Rules of OpenTheory Articles</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 6.3: Frequency of Main Inference Rules of HOLALA Articles</figcaption></figure>
<table><caption>Table 6.5: Comparison of Translation and Proof Checking</caption><thead><tr><th></th><th>Size of Proof Files (KB)</th><th>Translation Time (s)</th></tr></thead><tbody><tr><td>HOL Light</td><td>5,376</td><td>55.98</td></tr><tr><td>HOLALA</td><td>3,460</td><td>32.57</td></tr><tr><td>Comparison</td><td>Reduced to 64.36%</td><td>Improved by 41.81%</td></tr></tbody></table><table><thead><tr><th></th><th>Size of Dedukti Files (KB)</th><th>Proof Checking Time (s)</th></tr></thead><tbody><tr><td>HOL Light</td><td>16,092</td><td>30.75</td></tr><tr><td>HOLALA</td><td>10,448</td><td>19.05</td></tr><tr><td>Comparison</td><td>Reduced to 64.92%</td><td>Improved by 38.04%</td></tr></tbody></table>

ProofCloud can distinguish between classical proofs and constructive proofs. Furthermore, it tracks the origin of classicism, in other words, which classical lemmas<fnref n="7" /> were used within the proof. With this ability, the amount as well as the percentage of classical proofs of a certain package is calculated and displayed on its (package) page. Users will also find a statistical analysis on the size of proofs and links to proof checking results. As far as the author knows, this is the only online proof retrieval engine of its kind.

<figure><img src="image_7.png" /><figcaption>Figure 6.4: The Interface of ProofCloud</figcaption></figure>

So far ProofCloud includes six OpenTheory packages in total. These packages are *base* (the standard library with some subpackages), *stream*, *probability*, *natural-bits*, *natural-divides*

<footnote n="7">⁷To avoid confusion, all theorems used to prove the conclusion are referred to as lemmas when referring to a specific theorem.</footnote>
and *natural-prime*. Other packages will be added in the near future. An analysis of the dependency of packages of OpenTheory is as shown in Figure 6.5. To load a package, it is required to load all the packages it depends on primarily. In addition, the package *modular* is a parametric theory and requires the *modular-witness* theory which defines a suitable signature. Similarly *gfp* is another parametric theory. These packages are being updated and therefore not included for now. The package *modular* and *gfp* and packages depending on them will be added to ProofCloud in the near future.

<figure><img src="image_8.png" /><figcaption>Figure 6.5: Dependency of Packages of OpenTheory</figcaption></figure>

ProofCloud includes also the proof checking results for all packages of OpenTheory. The standard library of OpenTheory grouped theorems into packages, including theorems of booleans, sets, lists, etc. The standard library (the base package, including 11 subpackages) was first verified in this project, followed by all the packages in the OpenTheory repository. For the first time, Holide and Dedukti successfully translated and checked all packages in OpenTheory. Table 6.2 illustrates the size of OpenTheory proof article files and the time taken for translation. Table 6.3 represents the size of translated files and the time taken for proof checking by Dedukti. We name the translators as Holide 1 and Holide 2 respectively corresponding to OpenTheory version 5 and 6 respectively in Table 6.2 and Table 6.3. Both article files and Dedukti files are compressed by *gzip* to reduce the effect of syntax formatting and whitespace. These benchmarks were generated on a 64-bit Intel Core i5-4590 CPU @3.30GHz ×4 PC with 3.8GB RAM. However, there is little difference in terms of the size of article files and the efficiency between OpenTheory 5 and 6 for proof checking. The size of proof articles were reduced by around 7% while the proof checking time was reduced by around 5%. Figure 6.7 gives an example of the proof checking page of the stream package. In addition, Appendix D presents the specification of ProofCloud for further contribution.
<figure><img src="image_9.png" /><figcaption>Figure 6.7: A Proof Checking Page of ProofCloud</figcaption></figure>

<figure><img src="image_10.png" /></figure>

Back to package page
# Chapter 7

# Conclusion and Future Work

## 7.1 Conclusion and Contribution

In this report, Chapter 2 and Chapter 3 are an exposition of the tools used during this internship: HOL-Light, Dedukti and Holide. To perform double negation translation, it is required to replace the primitive symbols of OpenTheory HOL Light kernel by implication and universal quantifier. Chapter 4 and Chapter 5 present a modification of the OpenTheory HOL-Light system, namely HOLALA, which meant to change the definition of the connectives and quantifiers, followed by the corresponding modifications of Holide. Chapter 6 presents proof analysis and the evaluation: statistical analysis shows that, 44% of the proofs are constructive. Structural analysis shows that introducing more symbols to the kernel leads to the reduction of proof size to around 64%, which result in an improvement of 41% in translation time and 38% in proof checking time. In addition, ProofCloud was developed as a representation of the analysis of HOL proofs. It is the only proof search engine of its kind.

## 7.2 Optimisation of proofs

Table 6.4 suggested that many common derived inference rules are dependent on INST and INST_TYPE. Having INST or INST_TYPE might increased the complexity for proof searching automation. It would also be necessary to analyze inference Rules and their dependency of all deduction rules for further optimisation. Another inference rule which worth examining is the BETA_CONV rule. This rule built based on INST and BETA in (OpenTheory) HOL Light. While in OpenTheory, BETA_CONV is taken as primitive inference rule. Having BETA_CONV as primitive rule would not only reduce the size of proof but also reduce complexity for proof search. As a direct contribution, it can be expected that introducing techniques other than the combination of BETA, INST and EQ MP to deal with beta reduction would not only reduce the size of proof tree but also make inference clearer and easier. A solution for this is to introduce Deduction Modulo. Having Deduction Modulo would also allow introducing of constants and connectives independent of systems making defining equality based on universal quantifier and implication possible. This lead to the design of
## 7.3 HOL-Modulo

Although HOLALA is a reasonable attempt at removing equality as primitive rule, it lead to a more interesting question: why not transform HOL Light to a theorem prover taking advantage of Deduction Modulo. In theory, this would be one solution of replacing the equality in HOL Light. Instead of having beta reduction, defining equality up to $\beta$ (instead of up to $\alpha$) would also make proof shorter and more portable to Dedukti. There are also a small amount of code sharable between HOL-Modulo and Dedukti, making the integration of HOL-Modulo and Dedukti possible. Further than the analysis in Section 6.2, having equality up to $\beta$ would replace the use of BETA_CONV and reduce a significant amount of INST and INST_TYPE and may provide a solution for removing INST and INST_TYPE in proofs, which would benefit proof searching. A first step is to re-implement term comparison function. Following that it is required to introduce rewrite rules as well some rewriting algorithms for term conversion and proof construction. In addition, proof searching methods could be optimized. Further than that, it would be an possible to integrate HOL-Modulo with Dedukti making Dedukti not only a proof checker but also a theorem prover. Since Simple Type Theory can be expressed in Deduction Modulo [10], it is promising that HOL-Modulo be a step towards replacing the current kernels of HOL families and make ProofCloud a representation of rewriting rules for theorem proving.

## 7.4 HOL-Tableaux

Proof automation in interactive theorem proving is important since it reduces interaction and human labour and increase efficiency and usability of theorem provers. However, automated theorem proving methods in HOL Light such as ITAUT, TAUT, MESON_TAC, ASM_MESON_TAC do not always produce effecient proofs. And sometimes proofs can be really huge, for example TAUT in Table 5.3. In some cases, proof searching can go really deep and time-consuming. Having noticed also that Sequent Calculus is equivalent to Natural Deduction [11] (See Table A.2) and Sequent Calculus has a lot similarity compared with Tableuax Methods, this project aims at taking advantage of Tableaux methods for better proof search and convert current proofs from HOL Light to better and simpler proofs. Some data analysis in this project gave a good hint that some proofs are too large and have to be simplified. Thus HOL-Tableaux would give these proofs a chance to get shorter in a smart way.
## 7.5 ProofCloud

The ProofCloud described in this revisited internship report differs from that of the original report. Originally ProofCloud was developed as a platform to represent some proof analysis results which were too big to be included as tables in the report. ProofCloud is now a complete and stand-alone platform that has nothing to do with HOLALA. Future work includes adding the remaining packages of OpenTheory to ProofCloud. Most recent updates of OpenTheory include also the names of proofs in packages. This would benefit the usability of ProofCloud. ProofCloud (version 3) is being developed with a new ontological representation using Web Ontology Language (OWL) for better representation of proofs and axioms and more.
# Appendix A

## Comparison of Sequent Calculus, Natural Deduction and HOL Light

Sequent Calculus, Natural Deduction are the two most widely used style of inference systems. Intuitionistic Natural Deduction can be derived in HOL Light. The following is an example proof in Sequent Calculus, Natural Deduction and HOL Light.

<table><caption>Table A.1: Example Proof of $(p \land (p \to q)) \to q$ in Sequent Calculus, Natural Deduction and HOL Light</caption><thead><tr><th>Sequent Calculus</th><th>Natural Deduciton and HOL Light</th></tr></thead><tbody><tr><td><div style="text-align: center; line-height: 1.2;">p &vdash; p axiom<br>  p, p &rarr; q &vdash; q<br>  (p &vdash; (p &rarr; q)) &vdash; q<br>  &vdash; (p &vdash; (p &rarr; q)) &rarr; q</div></td><td><div style="text-align: center; line-height: 1.2;">p &vdash; (p &rarr; q) &vdash; p &vdash; (p &rarr; q) axiom<br>  p &vdash; (p &rarr; q) &vdash; p &rarr; q &vdash; q &vdash; p &vdash; (p &rarr; q) &vdash; p &rarr; q &vdash; p &rarr; elim<br>  p &vdash; (p &rarr; q) &vdash; q &vdash; p &vdash; (p &rarr; q) &vdash; p &rarr; elim<br>  &vdash; (p &vdash; (p &rarr; q)) &rarr; q &rarr; intro</div></td></tr><tr><td></td><td><div style="text-align: center; line-height: 1.2;">p &vdash; (p &rarr; q) &vdash; p &vdash; (p &rarr; q) axiom<br>  p &vdash; (p &rarr; q) &vdash; p &rarr; q &vdash; q &vdash; p &vdash; (p &rarr; q) &vdash; p &rarr; elim<br>  p &vdash; (p &rarr; q) &vdash; p &rarr; q &vdash; q &vdash; p &vdash; (p &rarr; q) &vdash; p &rarr; elim<br>  &vdash; (p &vdash; (p &rarr; q)) &rarr; q &rarr; intro</div></td></tr></tbody></table>
<table><caption>Table A.2 is a comparison of Sequent Calculus, Natural Deduction and HOL Light's logic. There is only one HOL Light primitive inference rule in the table (ASSUME). All the others are deducted rules (deduced from primitive rules) as marked in double bar. Note that the *Axiom* rule in Natural Deduction corresponds to the *ASSUME* rule in HOL Light. As for DISCH, A is not required to be in Γ. In addition, HOL Light does not allow repeated terms in its Γ. Thus no contraction rule for HOL Light.</caption><thead><tr><th></th><th>Sequent Calculus (LJ)</th><th>Natural Deduction (NJ)</th><th>HOL Light</th></tr></thead><tbody><tr><td>Axiom</td><td>Γ, A ⊢ A axiom</td><td>Γ, A ⊢ A axiom</td><td>{A} ⊢ A ASSUME</td></tr><tr><td>⊤</td><td>Γ ⊢ ⊤ ⊤<sub>R</sub></td><td>Γ ⊢ ⊤ ⊤<sub>intro</sub></td><td>Γ ⊢ ⊤ TRUTH</td></tr><tr><td>⊥</td><td>Γ ⊢ A weak<sub>R</sub></td><td>Γ ⊢ ⊥ ⊤<sub>elim</sub></td><td>Γ ⊢ ⊥ ⊤<sub>CONTR</sub></td></tr><tr><td>Weak</td><td>Γ ⊢ Δ weak<sub>L</sub></td><td></td><td>Γ ⊢ B ADD_ASSUM</td></tr><tr><td></td><td>Γ, ⊤ ⊢ Δ ⊥<sub>L</sub></td><td></td><td></td></tr><tr><td>∧</td><td>Γ ⊢ A ∧ B ∧ elim<sub>1</sub><br>Γ ⊢ A ∧ B ∧ elim<sub>2</sub></td><td>Γ ⊢ A ∧ B ∧ elim<sub>1</sub><br>Γ ⊢ A ∧ B ∧ elim<sub>2</sub></td><td>Γ ⊢ A ∧ B CONJUNCT1<br>Γ ⊢ A ∧ B CONJUNCT2</td></tr><tr><td></td><td>Γ, A ∧ B ⊢ Δ ∧<sub>L</sub></td><td></td><td></td></tr><tr><td>⊤</td><td>Γ ⊢ A Γ ⊢ B ∧<sub>R</sub><br>Γ ⊢ A ∧ B</td><td>Γ ⊢ A Γ ⊢ B ∧<sub>intro</sub><br>Γ ⊢ A ∧ B</td><td>Γ ⊢ A Δ ⊢ B CONJ</td></tr><tr><td>⊤</td><td>Γ, A ⊢ Δ Γ, B ⊢ Δ</td><td></td><td>Γ, A ∨ B ⊢ Δ ∨<sub>L</sub></td></tr></tbody></table>
<table><thead><tr><th></th><th>Γ ⊔ A ∨ B</th><th>Γ, A ⊔ C</th><th>Γ, B ⊔ C</th><th>Γ ⊔ A ∨ B</th><th>Γ₁, A ⊔ C</th><th>Γ₂, B ⊔ C</th><th>DISJ_CASES</th></tr><tr><th></th><th></th><th>Γ ⊔ C</th><th></th><th>Γ ⊔ A</th><th></th><th></th><th></th></tr></thead><tbody><tr><th>→</th><td>Γ ⊔ A<br>Γ ⊔ A ∨ B<br>Γ ⊔ A ∨ B</td><td>Γ ⊔ A<br>Γ ⊔ A ∨ B<br>Γ ⊔ A ∨ B</td><td>vintrol1<br>vintrol2</td><td>Γ ⊔ A<br>Γ ⊔ A ∨ B<br>Γ ⊔ A ∨ B</td><td>Γ ⊔ A<br>Γ ⊔ A ∨ B<br>Γ ⊔ A ∨ B</td><td>DISJ1<br>DISJ2</td><td></td></tr><tr><th>→</th><td>Γ ⊔ A<br>Γ, A ⊔ Δ<br>Γ, A → B ⊔ Δ</td><td>Γ ⊔ A</td><td>elim</td><td>Γ ⊔ A → B<br>Γ ⊔ A</td><td>Δ ⊔ A<br>Γ ∪ Δ ⊔ B</td><td>MP</td><td></td></tr><tr><th>→</th><td>Γ, A ⊔ B<br>Γ ⊔ A → B</td><td>Γ, A ⊔ B<br>Γ ⊔ A → B</td><td>intro</td><td>Γ ⊔ B<br>Γ \ {A} ⊔ A → B</td><td>DISCH</td><td></td><td></td></tr><tr><th>→</th><td>Γ ⊔ A<br>Γ, A ⊔ ¬ A</td><td>Γ ⊔ ¬ A<br>Γ, A ⊔ ¬ elim</td><td>elim</td><td>Γ ⊔ ¬ A<br>Γ ⊔ A → ⊥<br>Γ ⊔ A = ⊥</td><td>NOT_ELIM<br>EQF_ELIM</td><td></td><td></td></tr><tr><th>→</th><td>Γ, A ⊔<br>Γ ⊔ ¬ A</td><td>Γ, A ⊔<br>Γ ⊔ ¬ A</td><td>intro</td><td>Γ ⊔ A → ⊥<br>Γ ⊔ A → ⊥<br>Γ ⊔ A = ⊥</td><td>NOT_INTRO<br>EQF_INTRO</td><td></td><td></td></tr><tr><th>→</th><td>Γ, A[t/x] ⊔ Δ<br>Γ, ∀ x A ⊔ Δ</td><td></td><td>elim</td><td></td><td></td><td></td><td></td></tr><tr><th>→</th><td>Γ ⊔ A[c/x]<br>Γ ⊔ ∀ x A</td><td>Γ ⊔ A[c/x]<br>Γ ⊔ ∀ x A</td><td>intro if x is not free in Γ</td><td></td><td>GEN if x is not free in Γ</td><td></td><td></td></tr><tr><th>→</th><td>Γ ⊔ ∀ x A<br>Γ ⊔ A[t/x]</td><td>Γ ⊔ ∀ x A<br>Γ ⊔ A[t/x]</td><td>elim</td><td></td><td>SPEC</td><td></td><td></td></tr></tbody></table>
<table><caption>Table A.2: Inference System Comparison</caption><tbody><tr><td>∃</td><td><table><tbody><tr><td>Γ, A[c/x] ⊢ Δ</td><td>∃<sub>L</sub></td></tr><tr><td>Γ ⊢ A[c/x] ∃<sub>R</sub></td><td>Γ ⊢ A[t/x] ∃<sub>intro</sub></td></tr><tr><td>Γ ⊢ ∃xA</td><td>Γ ⊢ ∃xA</td></tr></tbody></table></td><td><table><tbody><tr><td>Γ ⊢ A[t/x]</td><td>∃xA EXISTS</td></tr><tr><td>Γ ⊢ ∃xA</td><td>Γ ⊢ ∃xA</td></tr></tbody></table></td></tr><tr><td>Cut</td><td><table><tbody><tr><td>Γ ⊢ A</td><td>Γ, A ⊢ Δ</td><td>cut</td></tr><tr><td>Γ ⊢ Δ</td><td></td><td></td></tr></tbody></table></td><td><table><tbody><tr><td>Γ ⊢ ∃xA</td><td>Γ, A ⊢ B</td><td>∃elim</td></tr><tr><td>Γ ⊢ B</td><td></td><td></td></tr></tbody></table></td></tr><tr><td>Contr</td><td><table><tbody><tr><td>Γ, A, A ⊢ Δ</td><td>contr<sub>L</sub></td></tr><tr><td>Γ, A ⊢ Δ</td><td></td></tr></tbody></table></td><td></td></tr></tbody></table>
# Appendix B

# Proof of Law of Excluded Middle

## B.1 Law of Excluded Middle

Generally speaking, classical Logic has the law of excluded middle (LEM) as an axiom while the conclusion of LEM is not provable in constructive logic. LEM states that a proposition is either true or false. In other words, the statement $P \lor \neg P$ is a tautology:

**Axiom 10 (Law of Excluded Middle (LEM))**. $\forall p.p \lor \neg p$

In OpenTheory HOL Light, LEM is derived from functional extensionality and the axiom of choice.

## B.2 Diaconescu's Proof of Law of Excluded Middle

It has been proved in [8] that the axiom of choice implies the law of excluded middle using separation and extensionality. The choice symbol is as introduced in Section 2.2.3.

**Axiom 11 (Axiom of Choice)**. $\forall P.\forall x : A.Px \Rightarrow P(@)P$

**Axiom 12 (Axiom of Extensionality)**. $\forall f : (A \to B)\forall f : (A \to B).(\forall x.fx = gx) \Rightarrow f = g$

The proof idea can be summarized as follows. Taking $A = \{n \in \mathbb{N} : n = 0 \lor (n = 1 \land \phi)\}$ and $B = \{n \in \mathbb{N} : n = 1 \lor (n = 0 \land \phi)\}$. When $\phi$ is true, $A = \{0, 1\}$ and $B = \{0, 1\}$ but when $\phi$ is false, $A = \{0\}$ and $B = \{1\}$. Thus, in either case, neither of A nor B would be empty. Suppose $f$ is a choice function so that $f(A) \in A$ and $f(B) \in B$. There are two cases, $A = B$ or $A \neq B$. On one hand, if $A = \neg B$, then $\phi$. On the other hand, when $A \neq B$, suppose $\phi$, using extensionality, we can get $f A = f B$. However this would give us contradiction with the hypothesis. Therefore, $\neg \phi$. Since the two cases infers $\phi$ and $\neg \phi$ respectively, we can conclude that $\phi \lor \neg \phi$. This proof was implemented by Mark Adams in HOL Zero and there is an adapted version in HOL Light. A shorter proof is to be released in the most recent version of HOL Zero<fnref n="1" />.

<footnote n="1">¹This shorter proof was in an email with Mark on 31st May 2015.</footnote>
## B.3 A New Proof of Law of Excluded Middle

Diaconescu's proof is closely related to set theory. Here we introduce a new proof without concepts of set theory <fnref n="2" />. This proof is longer than the proofs in HOL Light and HOL Zero. To prove it, we first introduce three predicates:

$$P_0 = \lambda b : \mathit{bool}.((\top \wedge (b = \top)) \lor (b = \bot))$$

$$P_1 = \lambda b : \mathit{bool}.((t \wedge (b = \top)) \lor (b = \bot))$$

$$P_2 = \lambda b : \mathit{bool}.((\top \wedge (b = \top)) \lor (t \wedge (b = \bot)))$$

, where $t$ is a boolean variable. It is easy to prove that $P_0 \top = \top$, $P_1 \bot = \top$ and $P_2 \top = \top$. Using the inference rule EXISTS, we can prove $\exists P_0, \exists P_1$ and $\exists P_2$. The proof idea is to assume $@P_0$ as true first and prove $t \lor \neg t$ in both cases of $@P_1$ and $\neg @P_1$. Similarly, we assume $\neg @P_0$ for both cases of $@P_2$ and $\neg @P_2$.

$$\frac{\frac{\exists P_0 \quad \begin{array}{l} \mathsf{EXISTS} \\ \vdash @P_0 \lor \neg @P_0 \end{array}}{\begin{array}{l} \mathsf{Axiom of Choice} \\ \vdash t \lor \neg t \end{array}} \quad \frac{\Pi_1}{@P_0 \vdash t \lor \neg t} \quad \frac{\Pi_2}{\neg @P_0 \vdash t \lor \neg t} \quad \begin{array}{l} \mathsf{DISJ\_CASES} \\ \vdash t \lor \neg t \end{array}}$$

where $\Pi_1$ is as follows:

$$\frac{\frac{\exists P_1 \quad \begin{array}{l} \mathsf{EXISTS} \\ \vdash @P_1 \lor \neg @P_1 \end{array}}{\begin{array}{l} \mathsf{Axiom of Choice} \\ \vdash @P_0 \vdash t \lor \neg t \end{array}} \quad \frac{\Pi_{1.1}}{@P_1 \vdash t \lor \neg t} \quad \frac{\Pi_{1.2}}{@P_0, \neg @P_1 \vdash t \lor \neg t} \quad \begin{array}{l} \mathsf{DISJ\_CASES} \\ \vdash t \lor \neg t \end{array}}$$

where $\Pi_2$ is as follows:

$$\frac{\frac{\exists P_2 \quad \begin{array}{l} \mathsf{EXISTS} \\ \vdash @P_2 \lor \neg @P_2 \end{array}}{\begin{array}{l} \mathsf{Axiom of Choice} \\ \vdash @P_0 \vdash t \lor \neg t \end{array}} \quad \frac{\Pi_{2.1}}{\neg @P_0, \neg @P_2 \vdash t \lor \neg t} \quad \frac{\Pi_{2.2}}{\neg @P_0, \neg @P_2 \vdash t \lor \neg t} \quad \begin{array}{l} \mathsf{DISJ\_CASES} \\ \vdash t \lor \neg t \end{array}}$$

$\Pi_{1.2}$ is as follows. $\Pi_{1.1}$, $\Pi_{2.1}$ are $\Pi_{2.2}$ are similar.

$$\frac{t \vdash (\lambda b.\top \wedge (b = \top) \lor b.\bot))}{(\lambda b.((\top \wedge (b = \top)) \lor ((b = \bot)))) = \top, (\lambda b.((t \wedge (b = \top)) \lor ((b = \bot)))) = \bot \vdash (\lambda b.\top \wedge (b = \top) \lor (b = \bot))) = (\lambda b.\top \wedge (b = \top) \lor (b = \bot))}$$

$$\frac{t, (\lambda b.((\top \wedge (b = \top)) \lor ((b = \bot)))) = \top, (\lambda b.((t \wedge (b = \top)) \lor ((b = \bot)))) = \bot \vdash T = F}{(\lambda b.((\top \wedge (b = \top)) \lor ((b = \bot)))) = \top, (\lambda b.((t \wedge (b = \top)) \lor ((b = \bot)))) = \bot \vdash T \Rightarrow F}$$

$$\frac{(\lambda b.((\top \wedge (b = \top)) \lor ((b = \bot)))) = \top, (\lambda b.((t \wedge (b = \top)) \lor ((b = \bot)))) = \bot \vdash t \lor \neg t}{@P_0, \neg @P_1 \vdash t \lor \neg t}$$

<footnote n="2">²This proof is a joint work with Mr. Frédéric Gilbert and Mr. Raphaël Cauderlier and has been formalized in HOL Light.</footnote>
## B.4 Proof of ¬¬LEM

Most double negation translation translate LEM to ¬¬LEM or similar form, which is provable in constructive logic as presented follows:

<figure><img src="image_11.png" /></figure>

Having ¬¬LEM proved, we are able to replace the LEM in the original proofs.
# Appendix C

## Attempts of reverse engineering of HOL Light Proofs

In this chapter, several attempts are presented to change the kernel. There are several reasons for removing equality as primitive symbols. The first and the most important reason being all theoretical results of double negation translation so far are for first order logic and are based on universal and implication. Having universal quantifier and implication would also make the system fundamentally more similar as other proof assistants which would make it easier to transport proofs between each other. In addition, such change would bring the system of HOL Light and Dedukti closer for further optimisation of proof checking since Dedukti's logic foundation is based on universal quantifier and implication. We will present the design of HOL-intermediate, HOLIU and HOLbot. Among them, HOL-intermediate is a premier attempt of making as many symbols depending on implication and universal quantifier as possible. HOLIU has universal quantifier and implication as primitive connectives as well as the equivalent symbol ($\equiv$) but this experiment was not proved to be successful. HOLbot is a another view of the logic kernel with all common logic symbols taken as primitive. Both HOLIU and HOLbot inspired the proposal of HOL-Modulo. Figure C.1 illustrates the dependency of constants and connectives of OpenTheory HOL Light, HOL-intermediate and HOLIU. In contrast, not aiming at removing equality, HOLbot takes all constants and connectives as primitive symbols for reduction of proof size and proof automation.

Although none of them is able to remove equality from the kernel and introduce universal and implication as the only primitive quantifiers, these attempts are good exercises for kernel hacking of (OpenTheory) HOL Light. Also these attempts result in deeper understanding of the kernel and implementation details as well as the analysis of dependency of constants, connectives and inference rules and inspire further development of this project.

OpenTheory HOL Light has the same logic foundation (a.k.a logic kernel) as HOL Light but with a proof logging method in its kernel. It takes equality as the only primitive symbol and defines all the other logic connectives and constants based on it. The kernel includes also some primitive inference rules (as in Table 2.3) where all the other inference rules (as in Table 2.4) are based on.
<figure><img src="image_12.png" /><figcaption>Figure C.1: Constants and Connectives Dependency Analysis and Design</figcaption></figure>

## C.1 HOL-intermediate

HOL-intermediate was the premier experiment in this project. As a very first attempt to change the kernel, HOL-intermediate kept equality as primitive rule but tries to build all the rest on top of the universal quantifier and implication. Instead of having the two connectives, $\top$ and $\land$, depending on equality. These symbols were introduced on top of $\rightarrow$ and $\forall$ after changing $\top$ and $\land$ to $\top'$ and $\land'$. This way, there are as symbols as possible depending on $\rightarrow$ and $\forall$. All the derived inference rules corresponding to $\top$ and $\land$ were then proved again. The implementation of HOL-intermediate requires knowledge of the kernel of HOL Light, especially the understanding of introducing new symbols, proving deduction rules as well as dependency analysis. The successful load of HOL libraries marked the completion of this attempt. With the experience of HOL-intermediate, we then tried to introducing universal quantifier and implication, which lead the design and implementation of HOLALA as presented in Chapter 5.

## C.2 HOLIU

HOLIU is another attempt to have universal quantifier and implication as primitive symbol. However, after realising that it is hard to remove equality from the kernel, in this attempt, $\equiv$ was introduced instead of $=$, making it possible to define new symbols without using $=$ as primitive symbol. This way, $\forall$ and $\rightarrow$ depend only on equiv and were successfully introduced as primitive symbol. Following that, we define equality as the Leibniz's equality:

**Definition 1.** $\equiv \lambda xy. \forall P. P x \rightarrow P y$

Correspondingly, this leads to the introduction of the EQUIV rule:

$$ \frac{\Gamma \vdash A \equiv B}{\Gamma \vdash A = B} \text{ EQUIV} $$

As a result, we lose almost all primitive inference rules including the $\eta$ reduction, which is key to $\beta$-conversion. This also results in the failure of the introduction of the rest of all inference rules. Thus, this approach was proved unsuccessful. Although it would not be
working, if terms are equivalent to *beta* and we take rewrite rules instead of $≡$ for the use of definition, there might be a way to remove equality from the kernel. This attempt leads to the design of HOL-Modulo.

### C.3 HOLbot

It was noticed in Table 5.3 and Table 6.2 that proofs in HOL-Light can be really big in size. One of the reasons is that the size of the kernel is really small, resulting in many derived inference rules. During this project, it was noticed that a small kernel benefits proof checking and verification but can make proofs big. Table 5.3 shows that introducing universal quantifier and implication can reduce the size of derived inference rules. Having more primitive rules would enlarge the kernel but shorter proofs can be expected. HOLbot follows from this idea. It has been also noticed during discussions that Sequent Calculus has some similarities as Tableaux Method. Since Tableaux Method provides a fully automated proof searching approach, it would be interesting to know if extending the kernel would reduce the size of proofs discovered automatically. HOLbot will be further explored as HOL-Tableaux.
# Appendix D

# The Specification of ProofCloud

The following attributes are included in the webpages of each package:

## D.1 The Specification of ProofCloud

The following attributes are included in the webpages of each package:

* Package name

* Author of package

* Subpackages

* Date retrieved

* Total number of proofs

* Number of constructive proofs

* Number of classical proofs

* Percentage of constructive proofs

* Size of constructive proofs on average

* Size of classical proofs on average

* List of proofs (names and conclusions)

* Comments

For each package, there is also a page for verification (proof checking) information with the following entries:

* Software engineer for verification

* Software for verification

* Translation time

* Verification time

* PC Specification

* Comments

Each proof has its own page for structural, statistical and proof checking results with the attributes as follows:

* Theorem name

* Theorem conclusion

* Packagename

* Constructive proof (or not)

* Axioms

* Constructive lemmas (if any)

* Classical lemmas (if any)

* Package

* Comments
Bibliography

[1] Mark Adams. Introducing HOL zero. In *Mathematical Software-ICMS 2010*, pages 142-143. Springer, 2010.

[2] Peter B Andrews. An introduction to mathematical logic and type theory: To truth through proof. 1986.

[3] Andrew W Appel. Foundational proof-carrying code. In *Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on*, pages 247-256. IEEE, 2001.

[4] Ali Assaf. *A framework for defining computational higher-order logics*. PhD thesis, École Polytechnique, 2015.

[5] Ali Assaf and Guillaume Burel. Translating HOL to Dedukti. In *Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015.*, pages 74-88, 2015.

[6] Ali Assaf and Raphaël Cauderlier. Mixing HOL and Coq in Dedukti (Extended Abstract). In *Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015.*, pages 89-96, 2015.

[7] Henk Barendregt, Wil Dekkers, and Richard Statman. *Lambda calculus with types*. Cambridge University Press, 2013.

[8] Michael J Beeson. Constructive set theories. In *Foundations of Constructive Mathematics*, pages 162-201. Springer, 1985.

[9] Chad E. Brown. Satallax: An automatic higher-order prover. In *Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings*, pages 111-117, 2012.

[10] Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In *Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings*, pages 102-117, 2007.

[11] Gilles Dowek. *Proofs and algorithms: an introduction to logic and computability*. Springer Science & Business Media, 2011.

[12] Gilles Dowek. On the definition of the classical connectives and quantifiers. *Why is this a Proof?, Festschrift for Luiz Carlos Pereira*, 2015.

[13] William M Farmer. The seven virtues of simple type theory. *Journal of Applied Logic*, 6(3):267-286, 2008.
[14] Gilda Ferreira and Paulo Oliva. On the relation between various negative translations. *Logic, Construction, Computation, Ontos-Verlag Mathematical Logic Series*, 3(23):227–258, 2012.

[15] Thibault Gauthier and Cezary Kaliszyk. Matching concepts across HOL libraries. In *Intelligent Computer Mathematics*, pages 267–281. Springer, 2014.

[16] Frédéric Gilbert. A lightweight double-negation translation. In *LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning*, 2015.

[17] Kurt Gödel. Zur intuitionistischen arithmetik und zahlentheorie. *Ergebnisse eines mathematischen Kolloquiums*, 4(1933):34–38, 1933.

[18] Thomas C Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller. A revision of the proof of the Kepler conjecture. In *The Kepler Conjecture*, pages 341–376. Springer, 2011.

[19] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. *Journal of the ACM (JACM)*, 40(1):143–184, 1993.

[20] John Harrison. HOL light: An overview. In *Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings*, pages 60–66, 2009.

[21] Joe Hurd. The opentheory standard theory library. In *NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings*, pages 177–191, 2011.

[22] Hajime Ishihara. A note on the Gödel-Gentzen translation. *Mathematical Logic Quarterly*, 46(1):135–137, 2000.

[23] Cezary Kaliszyk and Alexander Krauss. Scalable lcf-style proof translation. In *Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings*, pages 51–66, 2013.

[24] Andrei Nikolaevich Kolmogorov. On the principle of excluded middle. *Mat. Sb*, 32(646-667):24, 1925.

[25] Sigekatu Kuroda et al. Intuitionistische untersuchungen der formalistischen logik. *Nagoya Mathematical Journal*, 2:35–47, 1951.

[26] Dale Miller. Unification of simply typed lambda-terms as logic programming. 1991.

[27] Magnus O Myreen, Scott Owens, and Ramana Kumar. Steps towards verified implementations of HOL Light. In *Interactive Theorem Proving*, pages 490–495. Springer, 2013.

[28] Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. *Isabelle/HOL: a proof assistant for higher-order logic*, volume 2283. Springer Science & Business Media, 2002.

[29] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. *Unifying Theories in ProofPower-Z*, pages 123–140. Springer, 2006.
[30] Florian Rabe. Representing isabelle in LF. In Karl Crary and Marino Miculan, editors, *Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice*, LFMTP 2010, Edinburgh, UK, 14th July 2010, volume 34 of EPTCS, pages 85–99, 2010.

[31] Ronan Saillard. Dedukti: a universal proof checker. In *Foundation of Mathematics for Computer-Aided Formalization Workshop, January 9-11 2013, Padova, Italy*, 2013.

[32] Carsten Schürmann and Mark-Oliver Stehr. An executable formalization of the HOL/Nuprl connection in the metalogical framework Twelf. In *Logic for Programming, Artificial Intelligence, and Reasoning*, pages 150–166. Springer, 2006.

[33] Konrad Slind and Michael Norrish. A brief overview of HOL4. In *Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings*, pages 28–32, 2008.

[34] Nik Sultana, Jasmin Christian Blanchette, and Lawrence C Paulson. LEO-II and Satallax on the Sledgehammer test bench. *Journal of Applied Logic*, 11(1):91–102, 2013.