# Checking Zenon Modulo Proofs in Dedukti

Raphaël Cauderlier, Pierre Halmagrand

► To cite this version:

Raphaël Cauderlier, Pierre Halmagrand. Checking Zenon Modulo Proofs in Dedukti. Fourth Workshop on Proof eXchange for Theorem Proving (PxTP), Aug 2015, Berlin, Germany. hal-01171360

HAL Id: hal-01171360

https://inria.hal.science/hal-01171360

Submitted on 3 Jul 2015

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# Checking Zenon Modulo Proofs in Dedukti *

Raphaël Cauderlier Pierre Halmagrand

Cnam - Inria

Paris, France

raphael.cauderlier@inria.fr pierre.halmagrand@inria.fr

Dedukti has been proposed as a universal proof checker. It is a logical framework based on the λΠ-calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs produced by Zenon Modulo, an extension of the tableau-based first-order theorem prover Zenon to deduction modulo and typing. Zenon Modulo is applied to the verification of programs in both academic and industrial projects. The purpose of our embedding is to increase the confidence in automatically generated proofs by separating untrusted proof search from trusted proof verification.

## 1 Introduction

Program verification using deductive methods has become a valued technique among formal methods, with practical applications in industry. It guarantees a high level of confidence regarding the correctness of the developed software with respect to its specification. This certification process is generally based on the verification of a set of proof obligations, generated by deductive verification tools. Unfortunately, the number of proof obligations generated may be very high. To address this issue, deductive verification tools often rely on automated deduction tools such as first-order Automated Theorem Provers (ATP) or Satisfiability Modulo Theories solvers (SMT) to automatically discharge a large number of those proof obligations. For instance, Boogie is distributed with the SMT Z3 [4] and the Why3 platform with Alt-Ergo [16]. After decades of constant work, ATP and SMT have reached a high level of efficiency and now discharge more proof obligations than ever. At the end, many of these program verification tools use their corresponding ATP or SMT as oracles. The main concern here is the level of confidence users give to them. These programs are generally large software, consisting of dozens of thousands of lines of code, and using some elaborate heuristics, with some ad hoc proof traces at best, and with a simple "yes or no" binary answer at worst.

A solution, stated by Barendregt and Barendsen [3] and pursued by Miller [19] among others, relies on the concept of proof certificates. ATP and SMT should be seen as proof-certificate generators. The final "yes or no" answer is therefore left to an external proof checker. In addition, Barendregt and Barendsen proposed that proof checkers should satisfy two principles called the De Bruijn criterion and the Poincaré principle. The former states that proof checkers have to be built on a light and auditable kernel. The latter recommends that they distinguish reasoning and computing and that it should not be necessary to record pure computational steps.

Relying on an external proof checker to verify proofs strongly increases the trust we give them, but it also provides a common framework to express proofs. A profit made by using this common framework is the possibility to share proofs coming from different theorem provers, relying on different proof systems. But nothing comes for free, and using the same proof checker does not guarantee in general that we can

<footnote>*This work has received funding from the BWare project (ANR-12-INSE-0010) funded by the INS programme of the French National Research Agency (ANR).</footnote>
share proofs because formulæ and proofs can be translated in incompatible ways. Translation of proofs must rely on a shallow embedding in the sense proposed by Burel [10]: it reuses the features of the target language. It does not introduce new axioms and constants for logical symbols and inference rules. Connectives and binders of the underlying logic of ATP are translated to their corresponding connectives and binders in the target language. In addition, a shallow embedding preserves the computational behavior of the original ATP and the underlying type system of the logic.

In this paper, we present a shallow embedding of Zenon Modulo proofs into the proof checker Dedukti, consisting of an encoding of a typed classical sequent calculus modulo into the $\lambda\Pi$-calculus modulo ($\lambda\Pi^\equiv$ for short). Zenon Modulo [13] is an extension to deduction modulo [15] of the first-order tableau-based ATP Zenon [8]. It has also been extended to support ML polymorphism by implementing the TFF1 format [5]. Dedukti [7] is a proof checker that implements $\lambda\Pi^\equiv$, a proof language that has been proposed as a proof standard for proof checking and interoperability. This embedding is used to certify proofs in two different projects: FoCaLiZe [17], a programming environment to develop certified programs and based on a functional programming language with object-oriented features, and BWare [14], an industrial research project that aims at providing a framework for the automated verification of proof obligations coming from the B method [1]. The main benefit of Zenon Modulo and Dedukti relies on deduction modulo. Deduction modulo is an extension of first-order logic that allows reasoning modulo a congruence relation over propositions. It is well suited for automated theorem proving when dealing with theories since it turns axioms into rewrite rules. Using rewrite rules during proof search instead of reasoning on axioms lets provers focus on the challenging part of proofs, speeds up the tool and reduces the size of final proof trees [12].

Zenon was designed to support FoCaLiZe as its dedicated deductive tool and to generate proof certificates for Coq. Extension to deduction modulo constrains us to use a proof checker that can easily reason modulo rewriting. Dedukti is a good candidate to meet this specification. A previous embedding of Zenon Modulo proofs into Dedukti, based on a $\neg\neg$ translation [13], was implemented as a tool to translate classical proofs into constructive ones. This tool has the benefit to be shallower since it does not need add the excluded middle as an axiom into the target logic defined in Dedukti, but in return this transformation may be very time-consuming [12] and was not scalable to large proofs like those produced in BWare. The closest related work is the shallow embedding of resolution and superposition proofs into Dedukti proposed by Burel [10] and implemented in iProver Modulo [9]. Our embedding is close enough to easily share proofs of Zenon Modulo and iProver Modulo in Dedukti, at least for the subset of untyped formulæ.

The first contribution presented in this paper consists in the encoding into $\lambda\Pi^\equiv$ of typed deduction modulo and a set of translation functions into $\lambda\Pi^\equiv$ of theories expressed in this logic. Another contribution of this paper is the extension to deduction modulo and types of the sequent-like proof system LLproof which is the output format of Zenon Modulo proofs. The latter contribution is the embedding of this proof system into $\lambda\Pi^\equiv$ and the associated translation function for proofs coming from this system.

This paper is organized as follows: in Sec. 2, we introduce typed deduction modulo; in Sec. 3, we present $\lambda\Pi^\equiv$, its proof checker Dedukti, and a canonical encoding of typed deduction modulo in $\lambda\Pi^\equiv$; in Sec. 4 we introduce the ATP Zenon Modulo, the proof system LLproof used by Zenon Modulo to output proofs; and the translation scheme implemented as the new output of Zenon Modulo; finally, in Sec. 5, we present some examples and results to assess our implementation.
## 2 Typed Deduction Modulo

The Poincaré principle, as stated by Barendregt and Barendsen [3], makes a distinction between deduction and computation. Deduction may be defined using a set of inference rules and axioms, while computation consists mainly in simplification and unfolding of definitions. When dealing with axiomatic theories, keeping all axioms on the deduction side leads to inefficient proof search since the proof-search space grows with the theory. For instance, proving the following statement:

$$fst(a, a) = snd(a, a)$$

where a is a constant, and fst and snd are defined by:

$$\forall x, y. \text{fst}(x, y) = x$$

$$\forall x, y. \text{snd}(x, y) = y$$

and with the reflexivity axiom:

$$\forall x. x = x$$

using a usual automated theorem proving method such as tableau, will generate some useless boilerplate proof steps, whereas a simple unfolding of definitions of fst and snd directly leads to the formula $a = a$.

Deduction modulo was introduced by Dowek, Hardin and Kirchner [15] as a logical formalism to deal with axiomatic theories in automated theorem proving. The proposed solution is to remove computational arguments from proofs by reasoning modulo a decidable congruence relation $\equiv$ on propositions. Such a congruence may be generated by a confluent and terminating system of rewrite rules (sometimes extended by equational axioms).

In our example, the two definitions may be replaced by the rewrite rules:

$$\text{fst}(x, y) \rightarrow x$$

$$\text{snd}(x, y) \rightarrow y$$

And we obtain the following equivalence between propositions:

$$(\text{fst}(a, a) = \text{snd}(a, a)) \equiv (a = a)$$

Reasoning with several theories at the same time is often necessary in practice. For instance, in the BWare project, almost all proof obligations combine the theory of booleans, arithmetic and set theory. In this case, we have to introduce an expressive enough type system to ensure that an axiom about booleans, for instance $\forall x. x = \text{true} \lor x = \text{false}$, will not be used with a term that has another type. An input format for ATP called TFF1 [5] has been proposed recently by Blanchette and Paskevich to deal with first-order problems with polymorphic types. We propose to extend this format to deduction modulo.

We now introduce the notion of typed rewrite system, extending notations of Dowek et al. [15]. In the following, $FV(t)$ stands for the set of free variables of $t$ where $t$ is either a TFF1 term or a TFF1 formula.

### Definition (Typed Rewrite System)

A term rewrite rule is a pair of TFF1 terms $l$ and $r$ together with a TFF1 typing context $\Delta$ denoted by $l \rightarrow_{\Delta} r$, where $FV(r) \subseteq FV(l) \subseteq \Delta$. It is well-typed in a theory $\mathcal{T}$ if $l$ and $r$ can be given the same type $A$ in $\mathcal{T}$ using $\Delta$ to type free variables. A proposition rewrite rule is a pair of TFF1 formulæ $l$ and $r$ together with a typing context $\Delta$ denoted by $l \rightarrow_{\Delta} r$, where $l$ is an atomic formula and $r$ is an arbitrary formula,
<table><caption>Figure 1: Syntax of TFF1≡</caption><tr><td>Types</td><td>τ ::= α<br>| T(τ<sub>1</sub>,...,τ<sub>m</sub>)</td><td>(type variable)<br>(type constructor)</td></tr><tr><td>Terms</td><td>e ::= x<br>| f(τ<sub>1</sub>,...,τ<sub>m</sub>;e<sub>1</sub>,...,e<sub>n</sub>)</td><td>(term variable)<br>(function)</td></tr><tr><td>Formulae</td><td>φ ::= T | ⊥<br>| ¬φ | φ<sub>1</sub> ∧ φ<sub>2</sub> | φ<sub>1</sub> ∨ φ<sub>2</sub> | φ<sub>1</sub> ⇒ φ<sub>2</sub> | φ<sub>1</sub> ⇔ φ<sub>2</sub><br>| e<sub>1</sub> = τ e<sub>2</sub><br>| P(τ<sub>1</sub>,...,τ<sub>m</sub>;e<sub>1</sub>,...,e<sub>n</sub>)<br>| ∀x : τ. φ(x) | ∃x : τ. φ(x)<br>| ∀<sub>type</sub>α : type. φ(α) | ∃<sub>type</sub>α : type. φ(α)</td><td>(true, false)<br>(logical connectors)<br>(term equality)<br>(predicate)<br>(term quantifiers)<br>(type quantifiers)</td></tr><tr><td>Context</td><td>Δ ::= ∅<br>| Δ,x : τ</td><td>(empty context)<br>(declaration)</td></tr><tr><td>Theory</td><td>Γ ::= ∅<br>| Γ, T/m<br>| Γ, f : Πα. t → τ<br>| Γ, P : Πα. t → o<br>| Γ, name : φ<br>| Γ, l → Δr</td><td>(empty theory)<br>(m-ary type constructor declaration)<br>(function declaration)<br>(predicate declaration)<br>(axiom)<br>(rewrite rule)</td></tr></table>

and where $FV(r) \subseteq FV(l) \subseteq \Delta$. It is well-typed in a theory $\mathcal{T}$ if both $l$ and $r$ are well-formed formulæ in $\mathcal{T}$ using $\Delta$ to type free variables.

A typed rewrite system is a set $\mathcal{R}$ of proposition rewrite rules along with a set $\mathcal{E}$ of term rewrite rules. Given a rewrite system $\mathcal{R}\mathcal{E}$, the relation $\equiv_{\mathcal{R}\mathcal{E}}$ denotes the congruence generated by $\mathcal{R}\mathcal{E}$. It is well-formed in a theory $\mathcal{T}$, if all its rewrite rules are well-typed in $\mathcal{T}$.

The notion of TFF1 theory can be extended with rewrite rules; we call the resulting logic TFF1$^{≡}$. Its syntax is given in Fig. 1.

## 3 Dedukti

The $\lambda\Pi$-calculus [2] is the simplest Pure Type System featuring dependent types. It is commonly used as a logical framework for encoding logics [18]. The $\lambda\Pi$-calculus modulo, presented in Fig. 2, is an extension of the $\lambda\Pi$-calculus with rewriting. The $\lambda\Pi$-calculus modulo (abbreviated as $\lambda\Pi^{≡}$) has successfully been used to encode many logical systems (Coq [6], HOL, iProver Modulo [10], FoCaLiZe) using shallow embeddings.

In $\lambda\Pi^{≡}$, conversion goes beyond simple $\beta$-equivalence since it is extended by a custom rewrite system. When this rewrite system is both strongly normalizing and confluent, each term gets a unique (up to $\alpha$-conversion) normal form and both conversion and type-checking become decidable. Dedukti is an implementation of this decision procedure.

Burel [10] defines two encodings of deduction modulo in Dedukti: a deep encoding $|\varphi|$ in which logical connectives are simply declared as Dedukti constants and a shallow encoding $||\varphi|| := \text{prf} |\varphi|$ using a decoding function prf for translating connectives to their impredicative encodings. In Sec. 3.1 and Sec. 3.2, we extend these encodings to TFF1$^{≡}$.
### Syntax

$$s ::= \text{Type} | \text{Kind}$$

$$t ::= x \mid t \mid \lambda x : t.t \mid \Pi x : t.t \mid s$$

$$\Delta ::= \emptyset \mid \Delta, x : t$$

$$\Gamma ::= \emptyset \mid \Gamma, x : t \mid \Gamma, t \leftrightarrow \Delta t$$

### Well-formdness

$$\overline{\emptyset \vdash} \text{ (Empty)} \qquad \frac{\Gamma \vdash \Gamma \vdash A : s \qquad x \notin \Gamma \qquad \text{(Decl)}}{\Gamma, x : A \vdash} \qquad \frac{\Gamma, \Delta \vdash l : A \qquad \Gamma, \Delta \vdash r : A \qquad FV(r) \subseteq FV(l) \subseteq \Delta \qquad \Gamma, l \leftrightarrow \Delta r \vdash}{\Gamma, l \leftrightarrow \Delta r \vdash} \qquad \text{(Rew)}$$

### Typing

$$\frac{\Gamma \vdash \quad \frac{\Gamma \vdash x : A \in \Gamma}{\Gamma \vdash x : A} \quad \text{(Var)}}{\Gamma \vdash \text{Type} : \text{Kind}} \qquad \text{(Sort)}$$

$$\frac{\Gamma \vdash t_1 : \Pi x : A.B(x) \qquad \Gamma \vdash t_2 : A \qquad \text{(App)}}{\Gamma \vdash t_1 t_2 : B(t_1)} \qquad \frac{\Gamma \vdash A : \text{Type} \qquad \Gamma, x : A \vdash t : B(x) \qquad \Gamma, x : A \vdash B(x) : s \qquad \text{(Abs)}}{\Gamma \vdash \lambda x : A.t(x) : \Pi x : A.B(x)}$$

$$\frac{\Gamma \vdash A : \text{Type} \qquad \Gamma, x : A \vdash B(x) : s \qquad \text{(Prod)}}{\Gamma \vdash \Pi x : A.B(x) : s} \qquad \frac{\Gamma \vdash t : A \qquad \Gamma \vdash B : s \qquad A \equiv_{\beta} B \qquad \text{(Conv)}}{\Gamma \vdash t : B}$$

<caption>Figure 2: The $\lambda\Pi$-calculus modulo</caption>

## 3.1 Deep Embedding of Typed Deduction Modulo in Dedukti

In Fig. 3, for each symbol of our first-order typed logic, we declare its corresponding symbol into $\lambda\Pi^\equiv$. In $\lambda\Pi^\equiv$, types cannot be passed as arguments (no polymorphism) so we have to translate TFF1$^\equiv$ types as Dedukti terms. The Dedukti type of translated TFF1$^\equiv$ types is type and we can see an inhabitant of type as a Dedukti type thanks to the term function.

In Fig. 4, we define a direct translation of TFF1$^\equiv$ in Dedukti. It is correct in the following sense:

* if the theory $\mathcal{T}$ is well-formed in TFF1$^\equiv$, then $|\mathcal{T}| \vdash$.

* if $\tau$ is a well-formed TFF1$^\equiv$ type in a theory $\mathcal{T}$, then $|\mathcal{T}| \vdash |\tau| : \text{type}$.

* if $t$ is a TFF1$^\equiv$ term of type $\tau$ in a theory $\mathcal{T}$, then $|\mathcal{T}| \vdash |t| : \text{term}|\tau|$.

* if $\varphi$ is a well-formed TFF1$^\equiv$ formula in a theory $\mathcal{T}$, then $|\mathcal{T}| \vdash |\varphi| : \text{Prop}$.

## 3.2 From Deep to Shallow

Following Burel [10], we add rewrite rules defining the decoding function prf in Fig. 5 using the usual impredicative encoding of connectives. This transforms our deep encoding of TFF1$^\equiv$ into a shallow encoding in which all connectives are defined by the built-in constructions of $\lambda\Pi^\equiv$.

This encoding is better suited for sharing proofs with other ATP because it is less sensible to small modifications of the logic. Any proof found, for example, by iProver Modulo is directly usable as an (untyped) proof in the shallow encoding.
## Primitive Types

Prop : Type      prf : Prop → Type      type : Type      term : type → Type

## Primitive Connectives

⊤ : Prop      ⊥ : Prop

¬ : Prop → Prop      - ∧ : Prop → Prop → Prop

¬ ∨ : Prop → Prop → Prop      - ⇒ : Prop → Prop → Prop

¬ ⇔ : Prop → Prop → Prop      ∀ : Πα : type.(term α → Prop) → Prop

∀ type : (type → Prop) → Prop      ∃ : Πα : type.(term α → Prop) → Prop

∃ type : (type → Prop) → Prop      = : Πα : type.term α → term α → Prop

<caption>Figure 3: Dedukti Declarations of TFF1≡ Symbols</caption>

## Translation Function for Types

|α| := α      |T(τ₁, ..., τₘ)| := T |τ₁| ... |τₘ|

## Translation Function for Terms

|x| := x      |f(τ₁, ..., τₘ; e₁, ..., eₙ)| := f |τ₁| ... |τₘ| |e₁| ... |eₙ|

## Translation Function for Formulæ

|⊤| := ⊤      |⊥| := ⊥

|¬φ| := ¬|φ|      |φ₁ ∧ φ₂| := |φ₁| ∧ |φ₂|

|φ₁ ∨ φ₂| := |φ₁| ∨ |φ₂|      |φ₁ ⇒ φ₂| := |φ₁| ⇒ |φ₂|

|φ₁ ⇔ φ₂| := |φ₁| ⇔ |φ₂|      |e₁ = τ e₂| := |e₁| = |τ| |e₂|

|∀x : τ. φ| := ∀ |τ| (λx : term |τ|. |φ|)      |∃x : τ. φ| := ∃ |τ| (λx : term |τ|. |φ|)

|∀type α : type. φ| := ∀type (λα : type . |φ|)      |∃type α : type. φ| := ∃type (λα : type . |φ|)

|P(τ₁, ..., τₘ; e₁, ..., eₙ)| := P |τ₁| ... |τₘ| |e₁| ... |eₙ|

## Translation Function for Typing Contexts

|∅| := ∅      |Δ, x : τ| := |Δ|, x : term |τ|

## Translation Function for Theories

|∅| := Γ₀ where Γ₀ is the Dedukti context of Fig. 3

m times

|T, T/m| := |T|, T : type → ... → type → type

|T, f : Π(α₁, ..., αₘ). (τ₁, ..., τₙ) → τ| := |T|, f : Πα₁ : type...Παₘ : type. term |τ₁| → ... → term |τₙ| → |τ|

|T, P : Π(α₁, ..., αₘ). (τ₁, ..., τₙ) → o| := |T|, P : Πα₁ : type...Παₘ : type. term |τ₁| → ... → term |τₙ| → Prop

|T, name : φ| := |T|, name : prf |φ|

|T, l → Δ r| := |T|, |l| ↪→ Δ |r|

<caption>Figure 4: Translation Functions from TFF1≡ to λΠ≡</caption>

# 4 Zenon Modulo

Zenon Modulo [13] is an extension to deduction modulo [15] of the first-order tableau-based automated theorem prover Zenon [8]. It has also been improved to deal with typed formulæ and TFF1 input files. In this paper, we focus on the output format of Zenon Modulo. After finding a proof using its tableau-based proof-search algorithm [8], Zenon translates its proof tree into a low level format called LLproof, which
$$ \text{prf} \top \quad \leftrightarrow \quad \Pi P : \text{Prop. prf } P \to \text{prf } P $$

$$ \text{prf} \bot \quad \leftrightarrow \quad \Pi P : \text{Prop. prf } P $$

$$ \text{prf} (\neg A) \quad \leftrightarrow \quad \text{prf } A \to \text{prf } \bot $$

$$ \text{prf} (A \land B) \quad \leftrightarrow \quad \Pi P : \text{Prop. (prf } A \to \text{prf } B \to \text{prf } P) \to \text{prf } P $$

$$ \text{prf} (A \lor B) \quad \leftrightarrow \quad \Pi P : \text{Prop. (prf } A \to \text{prf } P) \to (\text{prf } B \to \text{prf } P) \to \text{prf } P $$

$$ \text{prf} (A \Rightarrow B) \quad \leftrightarrow \quad \text{prf } A \to \text{prf } B $$

$$ \text{prf} (A \Leftrightarrow B) \quad \leftrightarrow \quad \text{prf} ((A \Rightarrow B) \land (B \Rightarrow A)) $$

$$ \text{prf} (\forall \tau P) \quad \leftrightarrow \quad \Pi x : \text{term } \tau. \text{prf} (P x) $$

$$ \text{prf} (\forall_{\text{type}} P) \quad \leftrightarrow \quad \Pi \alpha : \text{type. prf} (P \alpha) $$

$$ \text{prf} (\exists \tau P) \quad \leftrightarrow \quad \Pi P : \text{Prop. } (\Pi x : \text{term } \tau. \text{prf} (P x) \to \text{prf } P) \to \text{prf } P $$

$$ \text{prf} (\exists_{\text{type}} P) \quad \leftrightarrow \quad \Pi P : \text{Prop. } (\Pi \alpha : \text{type. prf} (P \alpha) \to \text{prf } P) \to \text{prf } P $$

$$ \text{prf} (x =_{\tau} y) \quad \leftrightarrow \quad \Pi P : (\text{term } \tau \to \text{Prop. prf} (P x) \to \text{prf} (P y)) $$

<caption>Figure 5: Shallow Definition of Logical Connectives in Dedukti</caption>

is a classical sequent-like proof system. This format is used for Zenon proofs before their automatic translation to Coq. LLproof is a one-sided sequent calculus with explicit contractions in every inference rule, which is close to an upside-down non-destructive tableau method.

We present in Figs. 6 and 7 the new proof system LLproof$^≡$, an adaptation of Zenon output format LLproof [8] to deduction modulo and TFF1 typing.

Normalization and deduction steps may interleave anywhere in the final proof tree. This leads to the introduction of the congruence relation $\equiv_{\mathcal{R}\mathcal{E}}$ inside rules of Figs. 6 and 7: if the formula $P$ is in normal form (with respect to $\mathcal{R}\mathcal{E}$), we denote by $[P]$ any formula congruent to $P$ modulo $\equiv_{\mathcal{R}\mathcal{E}}$.

Extension of LLproof to TFF1 typing leads to the introduction of four new rules for quantification over type variables $\exists_{\text{type}}$, $\neg\forall_{\text{type}}$, $\forall_{\text{type}}$ and $\neg\exists_{\text{type}}$, and also to introduce some type information into

<figure><img src="image_2.png" /><figcaption>Figure 6: LLproof$^≡$ Inference Rules of Zenon Modulo (part 1)</figcaption></figure>
Quantifier Rules

$$ \frac{\Gamma, \exists_{\text{type}} \alpha : \text{type. } P(\alpha), P(\tau) \vdash \bot \quad \exists_{\text{type}} \Gamma, [\exists_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot}{\Gamma, [\exists_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot} \quad \frac{\Gamma, \neg \forall_{\text{type}} \alpha : \text{type. } P(\alpha), \neg P(\tau) \vdash \bot \quad \neg \forall_{\text{type}} \Gamma, [\neg \forall_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot}{\Gamma, [\neg \exists_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot} \quad \text{where } \tau \text{ is a} \\ \text{fresh type constant} $$

$$ \frac{\Gamma, \forall_{\text{type}} \alpha : \text{type. } P(\alpha), P(\beta) \vdash \bot \quad \forall_{\text{type}} \Gamma, [\forall_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot}{\Gamma, [\forall_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot} \quad \frac{\Gamma, \exists_{\text{type}} \alpha : \text{type. } P(\alpha), \neg P(\beta) \vdash \bot \quad \neg \exists_{\text{type}} \Gamma, [\neg \exists_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot}{\Gamma, [\neg \exists_{\text{type}} \alpha : \text{type. } P(\alpha)] \vdash \bot} \quad \text{where } \beta \text{ is} \\ \text{any closed type} $$

$$ \frac{\Gamma, \exists x : \tau. P(x), P(c) \vdash \bot \quad \exists \Gamma, [\exists x : \tau. P(x)] \vdash \bot}{\Gamma, [\exists x : \tau. P(x)] \vdash \bot} \quad \frac{\Gamma, \neg \forall x : \tau. P(x), \neg P(c) \vdash \bot \quad \neg \forall \Gamma, [\neg \forall x : \tau. P(x)] \vdash \bot}{\Gamma, [\neg \forall x : \tau. P(x)] \vdash \bot} \quad \text{where } c : \tau \text{ is a} \\ \text{fresh constant} $$

$$ \frac{\Gamma, \forall x : \tau. P(x), P(t) \vdash \bot \quad \forall \Gamma, [\forall x : \tau. P(x)] \vdash \bot}{\Gamma, [\forall x : \tau. P(x)] \vdash \bot} \quad \frac{\Gamma, \neg \exists x : \tau. P(x), \neg P(t) \vdash \bot \quad \neg \exists \Gamma, [\neg \exists x : \tau. P(x)] \vdash \bot}{\Gamma, [\neg \exists x : \tau. P(x)] \vdash \bot} \quad \text{where } t : \tau \text{ is} \\ \text{any closed term} $$

Special Rules

$$ \frac{\Delta, t_1 \neq \tau'_1 u_1 \vdash \bot \quad \dots \quad \Delta, t_n \neq \tau'_n u_n \vdash \bot}{\Gamma, [P(\tau_1, \dots, \tau_m; t_1, \dots, t_n)], [\neg P(\tau_1, \dots, \tau_m; u_1, \dots, u_n)] \vdash \bot} \quad \text{Pred} $$

$$ \text{where } \Delta = \Gamma \cup \{P(\tau_1, \dots, \tau_m; t_1, \dots, t_n), \neg P(\tau_1, \dots, \tau_m; u_1, \dots, u_n)\} $$

$$ \frac{\Delta, t_1 \neq \tau'_1 u_1 \vdash \bot \quad \dots \quad \Delta, t_n \neq \tau'_n u_n \vdash \bot}{\Gamma, [f(\tau_1, \dots, \tau_m; t_1, \dots, t_n) \neq \tau f(\tau_1, \dots, \tau_m; u_1, \dots, u_n)] \vdash \bot} \quad \text{Fun} $$

$$ \text{where } \Delta = \Gamma \cup \{f(\tau_1, \dots, \tau_m; t_1, \dots, t_n) \neq \tau f(\tau_1, \dots, \tau_m; u_1, \dots, u_n)\} $$

$$ \frac{\Delta, H_{11}, \dots, H_{1m} \vdash \bot \quad \dots \quad \Delta, H_{n1}, \dots, H_{nq} \vdash \bot}{\Gamma, [C_1], \dots, [C_p] \vdash \bot} \quad \text{Ext(name, args, } C_1, \dots, C_p, H_{11}, \dots, H_{nq}) $$

$$ \text{where } \Delta = \Gamma \cup \{C_1, \dots, C_p\} $$

<caption>Figure 7: LLproof≡ Inference Rules of Zenon Modulo (part 2)</caption>

other rules dealing with equality or quantification. For instance, equality of two closed terms $t$ and $u$, both of type $\tau$, is denoted by $t =_{\tau} u$. For predicate and function symbols, we first list types, then terms, separated by a semi-colon.

Finally, last difference regarding rules presented in [8] is the removal of rules “definition” and “lemma”. Zenon Modulo, unlike Zenon, does not need to explicitly unfold definitions and the lemma constructions have been removed.

## 4.1 Translation of Zenon Modulo Proofs into $\lambda\Pi^≡$

We present in Fig. 8 a deep embedding of LLproof≡ into $\lambda\Pi^≡$. We declare a constant for each inference rule, except for special rules Pred and Fun which have a dependency on the arity $n$ of their underlying predicate and function. Fortunately, they can be expressed with the following Subst inference rule which corresponds to the substitution in a predicate $P$ of a subterm $t : \tau'$ by another $u : \tau'$:

$$ \frac{\Gamma, P(\vec{t}; t), t \neq_{\tau'} u \vdash \bot \quad \Gamma, P(\vec{t}; t), P(\vec{t}; u) \vdash \bot}{\Gamma, P(\vec{t}; t) \vdash \bot} \quad \text{Subst} $$
### Zenon Modulo Rules

$R_{\perp}$: prf $\perp \to$ prf $\perp$

$R_{\neg\top}$: prf $(\neg\top) \to$ prf $\perp$

$R_{\lambda\alpha}$: $\Pi P$: Prop. prf $P \to$ prf $(\neg P) \to$ prf $\perp$

$R_{Cut}$: $\Pi P$: Prop. (prf $P \to$ prf $\perp$) $\to$ (prf $(\neg P) \to$ prf $\perp$) $\to$ prf $\perp$

$R_{\neq}$: $\Pi\alpha$: type. $\Pi t$: term $\alpha$. prf $(t \neq \alpha t) \to$ prf $\perp$

$R_{Sym}$: $\Pi\alpha$: type. $\Pi t, u$: term $\alpha$. prf $(t = \alpha u) \to$ prf $(u \neq \alpha t) \to$ prf $\perp$

$R_{\neg\neg}$: $\Pi P$: Prop. (prf $P \to$ prf $\perp$) $\to$ prf $(\neg\neg P) \to$ prf $\perp$

$R_{\wedge}$: $\Pi P, Q$: Prop. (prf $P \to$ prf $Q \to$ prf $\perp$) $\to$ prf $(P \wedge Q) \to$ prf $\perp$

$R_{\vee}$: $\Pi P, Q$: Prop. (prf $P \to$ prf $\perp$) $\to$ (prf $Q \to$ prf $\perp$) $\to$ prf $(P \vee Q) \to$ prf $\perp$

$R_{\Rightarrow}$: $\Pi P, Q$: Prop. (prf $(\neg P) \to$ prf $\perp$) $\to$ (prf $Q \to$ prf $\perp$) $\to$ prf $(P \Rightarrow Q) \to$ prf $\perp$

$R_{\Leftarrow}$: $\Pi P, Q$: Prop. (prf $(\neg P) \to$ prf $(\neg Q) \to$ prf $\perp$) $\to$ (prf $P \to$ prf $Q \to$ prf $\perp$) $\to$ prf $(P \Leftarrow Q) \to$ prf $\perp$

$R_{\neg\wedge}$: $\Pi P, Q$: Prop. (prf $(\neg P) \to$ prf $\perp$) $\to$ (prf $(\neg Q) \to$ prf $\perp$) $\to$ prf $(\neg(P \wedge Q)) \to$ prf $\perp$

$R_{\neg\vee}$: $\Pi P, Q$: Prop. (prf $(\neg P) \to$ prf $(\neg Q) \to$ prf $\perp$) $\to$ prf $(\neg(P \vee Q)) \to$ prf $\perp$

$R_{\neg\Rightarrow}$: $\Pi P, Q$: Prop. (prf $P \to$ prf $(\neg Q) \to$ prf $\perp$) $\to$ prf $(\neg(P \Rightarrow Q)) \to$ prf $\perp$

$R_{\neg\Leftarrow}$: $\Pi P, Q$: Prop. (prf $(\neg P) \to$ prf $Q \to$ prf $\perp$) $\to$ (prf $P \to$ prf $(\neg Q) \to$ prf $\perp$) $\to$ prf $(\neg(P \Leftarrow Q)) \to$ prf $\perp$

$R_{\exists}$: $\Pi\alpha$: type. $\Pi P$: (term $\alpha \to$ Prop). $(\Pi t$: term $\alpha$. (prf $(P t) \to$ prf $\perp$)) $\to$ prf $(\exists \alpha P) \to$ prf $\perp$

$R_{\forall}$: $\Pi\alpha$: type. $\Pi P$: (term $\alpha \to$ Prop). $\Pi t$: term $\alpha$. (prf $(P t) \to$ prf $\perp$) $\to$ prf $(\forall \alpha P) \to$ prf $\perp$

$R_{\neg\exists}$: $\Pi\alpha$: type. $\Pi P$: (term $\alpha \to$ Prop). $\Pi t$: term $\alpha$. (prf $(\neg(P t)) \to$ prf $\perp$) $\to$ prf $(\neg(\exists \alpha P) \to$ prf $\perp$)

$R_{\neg\forall}$: $\Pi\alpha$: type. $\Pi P$: (term $\alpha \to$ Prop). $(\Pi t$: term $\alpha$. (prf $(\neg(P t)) \to$ prf $\perp$)) $\to$ prf $(\neg\forall \alpha P) \to$ prf $\perp$

$R_{\exists_{type}}$: $\Pi P$: (type $\to$ Prop). $(\Pi\alpha$: type. (prf $(P \alpha) \to$ prf $\perp$)) $\to$ prf $(\exists_{type} P) \to$ prf $\perp$

$R_{\forall_{type}}$: $\Pi P$: (type $\to$ Prop). $\Pi\alpha$: type. (prf $(P \alpha) \to$ prf $\perp$) $\to$ prf $(\forall_{type} f) \to$ prf $\perp$

$R_{\neg\exists_{type}}$: $\Pi P$: (type $\to$ Prop). $\Pi\alpha$: type. (prf $(\neg(P \alpha)) \to$ prf $\perp$) $\to$ prf $(\neg(\exists_{type} P)) \to$ prf $\perp$

$R_{\neg\forall_{type}}$: $\Pi P$: (type $\to$ Prop). $(\Pi\alpha$: type. (prf $(\neg(P \alpha)) \to$ prf $\perp$)) $\to$ prf $(\neg(\forall_{type} P)) \to$ prf $\perp$

$R_{Subst}$: $\Pi\alpha$: type. $\Pi P$: (term $\alpha \to$ Prop). $\Pi t, u$: term $\alpha$. (prf $(t \neq \alpha u) \to$ prf $\perp$) $\to$ (prf $(P u) \to$ prf $\perp$) $\to$ prf $(P t) \to$ prf $\perp$

<caption>Figure 8: LLproof$^\equiv$ in $\lambda\Pi^\equiv$</caption>

The special rules Pred and Fun can be easily decomposed into $n$ applications of the Subst rule. For instance, for a binary predicate $P$, from (we omit to repeat the context $\Gamma$)

$$ \frac{\frac{\Pi_1}{t_1 \neq \tau' u_1 \perp \perp} \qquad \frac{\Pi_2}{t_2 \neq \tau'' u_2 \perp \perp}}{P(\tau; t_1, t_2), \neg P(\tau; u_1, u_2) \perp \perp} \text{Pred} $$

we obtain

$$ \frac{\frac{\Pi_1}{t_1 \neq \tau' u_1 \perp \perp} \qquad \frac{\Pi_2}{t_2 \neq \tau'' u_2 \perp \perp} \qquad \overline{P(\tau; u_1, u_2)}}{P(\tau; t_1, t_2), \neg P(\tau; u_1, u_2) \perp \perp} \text{Ax} \text{Subst} $$

In Fig. 9, we present the translation function for LLproof$^\equiv$ sequents and proofs into $\lambda\Pi^\equiv$. Let us present a simple example. We want to translate this proof tree:

$$ \Pi := \frac{\frac{\Pi_P}{\Gamma, P \vee Q, P \perp \perp} \qquad \frac{\Pi_Q}{\Gamma, P \vee Q, Q \perp \perp}}{\Gamma, P \vee Q \perp \perp} \lor (P, Q) $$
Translation Function for Sequents

$$|[\varphi_1], \dots, [\varphi_n] \vdash \perp| := x_{\varphi_1} : \text{prf} |\varphi_1|, \dots, x_{\varphi_n} : \text{prf} |\varphi_n|$$

Translation Function for Proofs

$$ \left| \begin{array}{c} \Pi_1 \\ \Delta, H_{11}, \dots, H_{1m} \vdash \perp \\ \vdots \\ \Gamma, C_1, \dots, C_p \vdash \perp \end{array} \quad \begin{array}{c} \Pi_n \\ \Delta, H_{n1}, \dots, H_{nq} \vdash \perp \end{array} \quad \text{Rule}(\text{Arg}_1, \dots, \text{Arg}_r) \right| \\ := \\ \begin{array}{l} \text{RRule} \quad |\text{Arg}_1| \dots |\text{Arg}_r| \\ \qquad (\lambda x_{H_{11}} : \text{prf} |H_{11}| \dots \lambda x_{H_{1m}} : \text{prf} |H|_{1m} | \Pi_1|) \\ \\ \vdots \\ \\ (\lambda x_{H_{n1}} : \text{prf} |H_{n1}| \dots \lambda x_{H_{nq}} : \text{prf} |H_{nq}| | \Pi_n|) \\ x_{C_1} \dots x_{C_p} \end{array} $$

<caption>Figure 9: Translation Functions for LLproof≡ Proofs into $\lambda\Pi^≡$</caption>

where $\Pi_P$ and $\Pi_Q$ are respectively proofs of sequents $\Gamma, P \vdash \perp$ and $\Gamma, Q \vdash \perp$, and where we annotate rule names with its parameters. Then, by applying the translation procedure of Figs. 4 and 9, we obtain the Dedukti term

$$R_{\lor} |P| |Q| (\lambda x_P : \text{prf } |P| . |\Pi_P|) (\lambda x_Q : \text{prf } |Q| . |\Pi_Q|) x_{P \lor Q}$$

where the notation $|x|$ means the translation of $x$ into $\lambda\Pi^≡$, and $x_P$ is a variable declared of type $\text{prf } |P|$. We then check that $\Pi$ is a proof of the sequent $\Gamma, P \lor Q \vdash \perp$ in a TFF1$^≡$ theory $\mathcal{T}$, by checking that $|\mathcal{T}|, |\Gamma, P \lor Q \vdash \Pi| : \text{prf} \perp$ in $\lambda\Pi^≡$.

More generally, for any LLproof$^≡$ proof $\Pi$ and any sequent $\Gamma \vdash \perp$, we check that $\Pi$ is a proof of $\Gamma \vdash \perp$ by checking the $\lambda\Pi^≡$ typing judgment $|\mathcal{T}|, |\Gamma| \vdash |\Pi| : \text{prf} \perp$.

## 4.2 Shallow Embedding of LLproof$^≡$

The embedding of LLproof$^≡$ presented in Fig. 8 can also be lifted to a shallow embedding. In Fig. 13 of Appendix A, we present rewrite rules that prove all constants corresponding to LLproof$^≡$ inference rules into the logic presented in Sec. 3. This has been written in Dedukti syntax and successfully checked by Dedukti (see the file modulologic.dk distributed with the source code of Zenon Modulo<fnref n="1" />). The only remaining axiom is the law of excluded middle. This shows the soundness of LLproof$^≡$ relatively to the consistency of the logic of Sec. 3.

# 5 Experimental Results

Zenon Modulo helps to automatically discharge proof obligations in particular in the two projects Fo-CaliZe [17] and BWare [14]. We present in this section some examples of theories, and simple related properties, that are handled successfully by Zenon Modulo, and its translation to Dedukti.

<footnote n="1">¹https://www.rocq.inria.fr/deducteam/ZenonModulo/</footnote>
Declarations

bool/0

false : bool

true : bool

~ : bool → bool

- && - : bool → bool → bool

- || - : bool → bool → bool

if. - then - else - : Πα. bool → α → α → α

Rewrite rules

true && a → a

a && true → a

false && a → false

a && false → false

a && a → a

a && (b && c) → (a && b) && c

~ true → false

~ false → true

~ ( ~ a ) → a

~ ( a || b ) → ( ~ a ) && ( ~ b )

~ ( a && b ) → ( ~ a ) || ( ~ b )

true || a → true

a || true → true

false || a → a

a || false → a

a || a → a

a || (b || c) → (a || b) || c

a && (b || c) → (a && b) || (a && c)

(a || b) && c → (a && c) || (b && c)

if_α true then t else e → t

if_α false then t else e → e

Extension deduction rules

$$
\frac{\Gamma, \neg P(\text{true}) \vdash \perp \quad \Gamma, \neg P(\text{false}) \vdash \perp}{\Gamma, [\neg \forall b : \text{bool. } P(b)] \vdash \perp} \text{Ext(bool-case-}\neg\neg, P)
$$

$$
\frac{\Gamma, P(\text{true}) \vdash \perp \quad \Gamma, P(\text{false}) \vdash \perp}{\Gamma, [\exists b : \text{bool. } P(b)] \vdash \perp} \text{Ext(bool-case-}\neg\exists, P)
$$

<caption>Figure 10: A TFF1<sup>=</sup> Theory of Booleans</caption>

5.1 Application to FoCaLiZe

FoCaLiZe is a framework for specifying, developing and certifying programs. The specification language is first-order logic and proofs can be discharged to Zenon or Zenon Modulo. The FoCaLiZe compiler produces both a regular program written in OCaml and a certificate written either in Coq or in Dedukti (but only the Dedukti output can be used from Zenon Modulo).

In FoCaLiZe, specifications usually rely a lot on the primitive type bool so it is important that
Zenon Modulo deals with booleans efficiently. In order to prove all propositional tautologies, it is enough
to add the following rules for reasoning by case on booleans (together with truth tables of connectives):

$$
\frac{\Gamma, \neg P(\text{true}) \vdash \perp \quad \Gamma, \neg P(\text{false}) \vdash \perp}{\Gamma, [\neg \forall b : \text{bool. } P(b)] \vdash \perp} \text{Ext(bool-case-}\neg\neg, P)
$$

$$
\frac{\Gamma, P(\text{true}) \vdash \perp \quad \Gamma, P(\text{false}) \vdash \perp}{\Gamma, [\exists b : \text{bool. } P(b)] \vdash \perp} \text{Ext(bool-case-}\neg\exists, P)
$$

However, we get a much smaller proof-search space and smaller proofs by adding common alge-
braic laws as rewrite rules. In Fig. 10, we define a theory of booleans in TFF1<sup>=</sup>. This theory handles
idempotency and associativity of conjunction and disjunction but not commutativity because the rule
$$ \lambda x_1 : \mathbf{prf}(\neg(\forall \mathbf{bool} (\lambda x : \mathbf{term bool} . \forall \mathbf{bool} (\lambda y : \mathbf{term bool} . x \&\& y = \mathbf{bool} y \&\& x))))). $$

$$ R_{\mathbf{bool-case-}\neg\forall} $$

$$ (\lambda x : \mathbf{term bool} . \forall \mathbf{bool} (\lambda y : \mathbf{term bool} . x \&\& y = \mathbf{bool} y \&\& x)) $$

$$ (\lambda x_2 : \mathbf{prf}(\neg(\forall \mathbf{bool} (\lambda y : \mathbf{term bool} . y = \mathbf{bool} y)))). $$

$$ R_{\neg\forall} \mathbf{bool} $$

$$ (\lambda y : \mathbf{term bool} . y \neq \mathbf{bool} y) $$

$$ (\lambda a : \mathbf{term bool} . $$

$$ \lambda x_3 : \mathbf{prf}(a \neq \mathbf{bool} a). $$

$$ R \neq \mathbf{bool} a x_3) $$

$$ x_2) $$

$$ (\lambda x_4 : \mathbf{prf}(\neg(\forall \mathbf{bool} (\lambda y : \mathbf{term bool} . \mathbf{false} = \mathbf{bool} \mathbf{false}))))). $$

$$ R_{\neg\forall} \mathbf{bool} $$

$$ (\lambda y : \mathbf{term bool} . \mathbf{false} = \mathbf{bool} \mathbf{false}) $$

$$ (\lambda a : \mathbf{term bool} . $$

$$ \lambda x_5 : \mathbf{prf}(\mathbf{false} \neq \mathbf{bool} \mathbf{false}). $$

$$ R \neq \mathbf{bool} \mathbf{false} x_5) $$

$$ x_4) $$

$$ x_1 $$

<caption>Figure 11: Proof Certificate for Commutativity of Conjunction in Dedukti</caption>

$a \&\& b \leftrightarrow b \&\& a$ would lead to a non terminating rewrite system; therefore, commutativity is a lemma with the following proof:

$$ \frac{\begin{array}{c} \overline{a \neq \mathbf{bool} a \vdash \bot} \\ \neg\forall y : \mathbf{bool} . y = \mathbf{bool} y \vdash \bot \end{array}}{\neg\forall x, y : \mathbf{bool} . x \&\& y = \mathbf{bool} y \&\& x \vdash \bot} \stackrel{\neg\forall}{\overline{\neg\forall y : \mathbf{bool} . \mathbf{false} = \mathbf{bool} \mathbf{false} \vdash \bot}} \stackrel{\neg\forall}{\overline{\mathbf{Ext}(\mathbf{bool-case-}\neg\forall)}} $$

The translation of this proof in Dedukti is shown in Fig. 11.

## 5.2 Application to Set Theory

The BWare project is an industrial research project that aims to provide a framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method [1]. The B method relies on a particular set theory with types. In the context of the BWare project, this typed set theory has been encoded into WhyML, the native language of Why3 [16]. To call Zenon Modulo, Why3 translates proof obligations and the B theory into TFF1 format. If it succeeds in proving the proof obligation, Zenon Modulo produces a proof certificate containing both the theory and the term, following the model presented in Fig. 12.

The BWare project provides a large benchmark made of 12,876 proof obligations coming from industrial projects. The embedding presented in this paper allowed us to verify with Dedukti all the 10,340 proof obligations that are proved by Zenon Modulo.

Let us present a small subset of this set theory, and a simple example of LLproof$\equiv$ proof produced by Zenon Modulo. The theory consists of three axioms that have been turned into rewrite rules. We define constructors: a type constructor set, the membership predicate $\in$, equality on sets $=_{set}$, the empty set $\emptyset$ and difference of sets $-$. For readability, we use an infix notation and let type parameters of functions and predicates in subscript. We want to prove the property

$$ \forall_{\mathbf{type}\alpha} : \mathbf{type} . \forall s : \mathbf{set}\alpha . s -_{\alpha} s =_{\mathbf{set}\alpha} \emptyset_{\alpha} $$
<figure><img src="image_3.png" /><figcaption>Figure 12: Proof Certificate for a B Set Theory Property in Dedukti</figcaption></figure>
with the theory:

set- /1

- ∈ - : Πα. setα → setα → Prop

- =set- : Πα. setα → setα → Prop

Ø_ : Πα. setα

- - - : Πα. setα → setα → setα

s =setα t → ∀x : α. x ∈α s ⇔ x ∈α t

x ∈α Øα → ⊥

x ∈α s -α t → x ∈α s ∧ x /∈α t

The LLproof proof tree generated by Zenon Modulo is (we omit to repeat context Γ):

$$
\begin{array}{c}
\begin{array}{c@{\quad}c@{\quad}c}
  & \overline{c_2 \in \tau c_1, c_2 \notin \tau c_1 \vdash \perp} & Ax \\
  & \multicolumn{2}{c}{\wedge} \\
  & \overline{c_2 \in \tau c_1 - \tau c_1, \neg(c_2 \in \tau \emptyset_{\tau}) \vdash \perp} & \neg \Leftrightarrow \\
  \multicolumn{1}{c}{\neg(c_2 \in \tau c_1 - \tau c_1), c_2 \in \tau \emptyset_{\tau} \vdash \perp} & &
\end{array} \\
\begin{array}{c}
  \neg((c_2 \in \tau c_1 - \tau c_1) \Leftrightarrow (c_2 \in \tau \emptyset_{\tau}) \vdash \perp) \\
  \neg(c_1 - \tau c_1 = \text{setr } \emptyset_{\tau}) \vdash \perp \\
  \neg(\forall s : \text{setr. } s - \tau s = \text{setr } \emptyset_{\tau}) \vdash \perp \\
  \neg(\forall_{\text{type}} \alpha : \text{type. } \forall s : \text{seta. } s - \alpha s = \text{seta } \emptyset_{\alpha}) \vdash \perp
\end{array}
\quad
\begin{array}{c}
  \neg \forall \\
  \neg \\
  \neg \\
  \neg
\end{array}
\end{array}
$$

We obtain the proof certificate of Fig. 12 checkable by Dedukti, using the file modulologic.dk, and
that is successfully checked.

6 Conclusion

We have presented a shallow embedding of Zenon Modulo proofs into Dedukti. For this encoding, we
have needed to embed into λΠ≡ an extension to deduction modulo of the underlying logic of the TFF1
format, denoted by TFF1≡. We then defined LLproof≡, the extension to TFF1≡ of the proof system
LLproof, which is the output format of Zenon Modulo. Finally, we have embedded LLproof≡ into λΠ≡
by giving the translation function for proofs. This embedding is shallow in the sense that we have reused
the features of the target language and have not declared new constants for connectives and inference
rules. The only axiom that we have added is the law of excluded middle.

This embedding has helped us to verify a large set of proof obligations coming from two different
projects. FoCaLiZe can now benefit from deduction modulo to improve program verification when dealing with theories. In BWare, this work allowed us to certify all the proofs generated by Zenon Modulo.

Our work is closely related to the embedding of iProver Modulo proofs into Dedukti [10]. The two main differences are the assumption of the excluded middle and the extension of the logic to deal with ML-style polymorphism. Because these shallow encodings are close, we could easily share proofs of untyped formulæ with iProver Modulo.

We do not have to trust the full implementation of Zenon Modulo but only the translation of TFF1≡
problems to λΠ≡ discussed in Sec. 3 and, of course, Dedukti. In the case of FoCaLiZe, we go even
further by using an external translator, Focalide [11]. Hence Zenon Modulo requires no confidence
in that context. As future work, we want to export this model. To achieve that, deduction tools must
be able to read Dedukti in addition to write some. This model improves the confidence on automated
deduction tools because it is no more possible to introduce inconsistency inside a proof certificate. In
addition, in case of the verification of several formulæ, it should be possible to inject terms coming from
different tools inside the same Dedukti file. A first experiment with Zenon Modulo and iProver Modulo
in FoCaLiZe would be an interesting proof of concept.
References

[1] Jean-Raymond Abrial (1996): *The B-Book, Assigning Programs to Meanings*. Cambridge University Press, doi:10.1017/CBO9780511624162.

[2] Hendrik Pieter Barendregt, Wil Dekkers & Richard Statman (2013): *Lambda calculus with types*. Cambridge University Press, doi:10.1017/CBO9781139032636.

[3] Henk Barendregt & Erik Barendsen (2002): *Autarkic Computations in Formal Proofs*. Journal of Automated Reasoning (JAR) 28, doi:10.1023/A:1015761529444.

[4] Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K Rustan M Leino (2006): *Boogie: A modular reusable verifier for object-oriented programs*. In: *Formal Methods for Components and Objects*, Springer, doi:10.1007/11804192_17.

[5] Jasmin Christian Blanchette & Andrei Paskevich (2013): *TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism*. In: *Conference on Automated Deduction (CADE)*, LNCS 7898, Springer, doi:10.1007/978-3-642-38574-2_29.

[6] Mathieu Boespflug & Guillaume Burel (2012): *CoqInE: translating the calculus of inductive constructions into the λΠ-calculus modulo*. In: *Proof Exchange for Theorem Proving (PxTP)*.

[7] Mathieu Boespflug, Quentin Carbonneaux & Olivier Hermant (2012): *The λΠ-Calculus Modulo as a Universal Proof Language*. In: *Proof Exchange for Theorem Proving (PxTP)*.

[8] Richard Bonichon, David Delahaye & Damien Doligez (2007): *Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs*. In: *Logic for Programming Artificial Intelligence and Reasoning (LPAR)*, LNCS/LNAI 4790, Springer, doi:10.1007/978-3-540-75560-9_13.

[9] Guillaume Burel (2011): *Experimenting with Deduction Modulo*. In: *Conference on Automated Deduction (CADE)*, LNCS/LNAI 6803, Springer, doi:10.1007/978-3-642-22438-6_14.

[10] Guillaume Burel (2013): *A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo*. In: *International Workshop on Proof Exchange for Theorem Proving (PxTP)*.

[11] Raphaël Cauderlier: *Focalide*. https://www.rocq.inria.fr/deducteam/Focalide.

[12] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): *Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps*. In: *International Workshop on the Implementation of Logics (IWIL)*.

[13] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand & Olivier Hermant (2013): *Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo*. In: *Logic for Programming Artificial Intelligence and Reasoning (LPAR)*, LNCS/ARCoSS 8312, Springer, doi:10.1007/978-3-642-45221-5_20.

[14] David Delahaye, Catherine Dubois, Claude Marché & David Mentré (2014): *The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations*. In: *Abstract State Machines, Alloy, B, VDM, and Z (ABZ)*, LNCS, Springer, doi:10.1007/978-3-662-43652-3_26.

[15] Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003): *Theorem Proving Modulo*. Journal of Automated Reasoning (JAR) 31, doi:10.1023/A:1027357912519.

[16] Jean-Christophe Filliâtre & Andrei Paskevich (2013): *Why3 - Where Programs Meet Provers*. In: *European Symposium on Programming (ESOP)*, doi:10.1007/978-3-642-37036-6_8.

[17] Thérèse Hardin, François Pessaux, Pierre Weis & Damien Doligez (2009): *FoCaLiZe reference manual*.

[18] Robert Harper, Furio Honsell & Gordon Plotkin (1993): *A Framework for Defining Logics*. Journal of the ACM 40, doi:10.1145/138027.138060.

[19] Dale Miller (2011): *A proposal for broad spectrum proof certificates*. In: *Certified Programs and Proofs (CPP)*, Springer, doi:10.1007/978-3-642-25379-9_6.
# A Appendix: Shallow Embedding of LLproof≡ System into Dedukti

<figure><img src="image_4.png" /><figcaption>Figure 13: Shallow Embedding of LLproof into Dedukti</figcaption></figure>

The deep embedding of LLproof≡ presented in Sec. 4.1 is well-typed with respect to the deep embedding.
bedding of typed deduction modulo presented in Sec. 3.1. Using the shallow embedding presented in Sec. 3.2, we can prove all the rules declared in Fig. 8 by rewriting the $R_{rule}$ symbols using only one axiom: the law of excluded middle. These proofs are listed in Fig. 13 where the $\Box$ symbol is used to delimit proofs.