# A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions

Gilles Dowek

► To cite this version:

Gilles Dowek. A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions. 1990. hal-04228809

HAL Id: hal-04228809

https://inria.hal.science/hal-04228809v1

Preprint submitted on 4 Oct 2023

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 CC BY 4.0 - Attribution - International License
# A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions

Gilles Dowek

INRIA*

## Introduction

In [6] we have developed a complete proof synthesis method for the Calculus of Constructions which generalizes Huet's proof synthesis method for Church Higher Order Logic [8]. We study in this paper a restriction of the algorithm presented in [6] which is always terminating and a complete Vernacular [1] [2] for the Calculus of Constructions based on this algorithm. This restriction uses a second order pattern matching algorithm for the Calculus of Construction presented in [7] which generalizes Huet's second order pattern matching algorithm for simply typed λ-calculus [9] [10].

A preleminary version of this paper, which presented a complete Vernacular for a restriction of the Calculus of Construction has been presented in [5].

# 1 An Always Terminating Proof Synthesis Method

We consider a restriction of the method presented in [6].

Let Γ be a (non constrained, non quantified context) and T a proposition
$T = (x_1 : P_1)...(x_n : P_n)P$ (P atomic).

We consider the quantified context $\Gamma[\exists x : T]$.

If P is a sort.

If P is not a sort then for each $i \ 0 \le i \le n$ and for each variale w which is
either a universal variable $\Gamma$ or an $x_i$, $w : (y_1 : Q'_1)...(y_p : Q'_p)Q'$ ($Q'$ atomic),

We let:

$Q_1 = Q'_1$

$Q_2 = [y_1 : Q'_1]Q'_2$

...

$Q_q = [y_1 : Q'_1]...[y_{q-1} : Q'_{q-1}]Q'_q$

<footnote>*This research was partly supported by ESPRIT Basic Research Action “Logical Frameworks”.</footnote>
$$Q = [y_1 : Q'_1]...[y_q : Q'_q]Q'$$

$$w : (y_1 : Q_1)(y_2 : (Q_2 y_1))...(y_q : (Q_q y_1 \dots y_{q-1}))(Q y_1 \dots y_q)$$

We let:

$$\gamma = [\exists h_1 : (x_1 : P_1)...(x_i : P_i)Q_1;$$

$$\exists h_2 : (x_1 : P_1)...(x_i : P_i)(Q_2 (h_1 x_1 \dots x_i));$$

...;

$$\exists h_q : (x_1 : P_1)...(x_i : P_i)(Q_q (h_1 x_1 \dots x_i) ... (h_{q-1} x_1 \dots x_i));$$

$$(x_1 : P_1)...(x_i : P_i)(Q (h_1 x_1 \dots x_i) ... (h_q x_1 \dots x_i)) = (x_1 : P_1)...(x_n : P_n)P]$$

we consider the substitutions:

$$\{<x, \gamma, [x_1 : P_1]...[x_i : P_i](w (h_1 x_1 \dots x_i) ... (h_q x_1 \dots x_n)) >\}$$

We get the context $\Gamma\gamma$.

Then form left to right, for each $j$ such that $Q_j$ is not second order in $\Gamma[\exists y_1 : Q_1; \dots; \exists y_{j-1} : Q_{j-1}]$ we try to instanciate $h_j$ by a universal variable. The accounting equation is always a second-order-argument-restricted problem, we solve it.

Then the equation of the context is a second-order-argument-restricted problem we solve it.

At last from right to left, we try to instanciate the existential variables of the context by a universal variable or a term of the form $[x_1 : P_1]...[x_i : P_i]x_i$. Accounting equations are second-order-argument-restricted problem, we solve them.

**Proposition:** This algorithm is always terminating

**Definition:** Transitive Closure of a Proof Synthesis Method

We consider a proof synthesis method. We write $\Gamma \rightsquigarrow P$ the assertion that in the context $\Gamma$ a proof of $P$ is synthetized by the method. We consider also assertions $\Gamma \hookrightarrow P$ meaning intuitively that there exists a text in Vernacular which is a demonstration of $P$.

We want, a priori, to have only one rule that allows to synthesize the proof of a new proposition, using already proved ones. Actually we need also another rule, which allows to introduce explicitly an hypothesis or a variable. Indeed, let us imagine that we want to prove a proposition $A \to B$ in
introducing the hypothesis A then proving B. If a proof of B cannot be automatically synthesized and for instance we have to prove a lemma C (using the hypothesis A) before, we cannot let the system introduce automatically the hypothesis A, we have to do it by hand.

**Rule 1: Synthesis**

$$ \frac{\Gamma \hookrightarrow Q_1 \dots \Gamma \hookrightarrow Q_n \quad \Gamma[c_1:Q_1;\dots;c_n:Q_n] \rightsquigarrow P}{\Gamma \hookrightarrow P} \quad c_i \text{ not free in } P $$

**Rule 2: Explicit introduction**

$$ \frac{\Gamma[x:Q] \hookrightarrow P}{\Gamma \hookrightarrow (x:Q)P} $$

**Lemma:** If a proof synthesis method is sound then so is its transitive closure.

**Proof:** Let $\Gamma$ a context and $P$ a proposition such that we know a derivation of $\Gamma \hookrightarrow P$. By induction on the length of this derivation, we construct a proof $t$ of $P$ in $\Gamma$.

If the last rule of the derivation is the rule *Synthesis* we have by the soundness of the proof synthesis method a term $u$ such that:

$$ \Gamma[c_1:Q_1, \dots, c_n:Q_n] \vdash u : P $$

and by induction hypothesis terms $v_1, \dots, v_n$ such that:

$$ \Gamma \vdash v_i : Q_i $$

so:

$$ \Gamma \vdash u[c_1 \leftarrow v_1, \dots, c_n \leftarrow v_n] : P $$

If the last rule of the derivation is the rule *Explicit introduction* then $P = (x:U)V$ and we have by induction hypothesis a term $u$ such that:

$$ \Gamma[x:U] \vdash u : V $$

$$ \Gamma \vdash [x:U]u : P $$

**Definition:** *Transitively Complete Proof Synthesis Method*

A proof synthesis method is said to be *transitively complete* if for all context $\Gamma$ and proposition $P$ if there exists a term $t$ such that $\Gamma \vdash t : P$, then $\Gamma \hookrightarrow P$.
**Proposition:** The proof synthesis method presented above if transitively complete.

**Premises:**

## 2 An Allusive Vernacular

In the Elementary Vernacular [4] there is an instruction *Proof t.* where *t* is a term. When the proof checker meets the instruction *Proof t.* in a context Γ, it computes the type of *t* in Γ, eliminates the local elements declared since the last instruction *Statement*, checks that the type obtained that way is the same as the one given in the last instruction *Statement* (if it is not then it fails), then eliminates the local elements declared since the last instruction *Theorem* and adds this new theorem to the context.

We modify this Vernacular in replacing this instruction by *Using s1, ..., sn.* where *s1, ..., sn* are symbolic names. When the proof checker meets the instruction *Using s1, ..., sn.* in a context Γ, it computes, using the type given in the last instruction *Statement* and the local elements declared since this last instruction, the goal to be proved then looks for a proof of this goal using the premises {*s1, ..., sn*}, fails if it does not find one, then eliminates the local elements declared since the last instruction *Theorem* and adds this new theorem to the context.

**Proposition:** For all inhabited proposition *P*, there exists a text in Vernacular which denotes a proof of this proposition.

**Proof:** We construct such a text from a derivation of Γ ⊢ *P*.

* If the last rule used is the rule *Synthesis*, then there exists, by induction hypothesis, texts that define symbols *c*₁, ..., *c*ₙ proof of *Q*₁, ..., *Q*ₙ. Let <text> be their concatenation.

There exists also a set of premises <premises> of Γ[{c₁ : Q₁, ..., cₙ : Qₙ}] used in the synthesis of a proof of *P*. We build the text:

Remark <name>.

Statement *P*.

<text>

Using <premises>.

* If the last rule is the *Explicit introduction* then *P* = (*x* : *U*)*V*. By induction hypothesis *V* has a proof in Vernacular in the context Γ[*x* : *U*]
that uses a set <premises> of premises (*x* may belong to <premises>).
Let a text in Vernacular that proves *V* in this context:

Remark <name>.
<text 1>
Statement <statement>.
<text 2>
Using <premises>.

We transform this text in:

Remark <name>.
Variable/Hypothesis x:U.
<text 1>
Statement <statement>.
<text 2>
Using <premises>.

## References

[1] N.G. de Bruijn. "The Mathematical Vernacular, A Language For Mathematics With Typed Sets", Proceedings, Workshop on Programming Logic, Marstrand, Sweden, 1987

[2] N.G. de Bruijn. "The Mathematical Vernacular: Examples", Unpublished manuscript.

[3] T. Coquand, G. Huet. "The Calculus of Constructions." Information and Computation, Volume 76, pp 95-120, 1988.

[4] G. Dowek. "Naming and Scoping in a Mathematical Vernacular." Rapport de Recherche n° 1283, INRIA.

[5] G. Dowek. "A Proof Synthesis Algorithm for a Mathematical Vernacular in a Restriction of the Calculus of Constructions." To appear in Proceedings of the First Workshop on Logical Frameworks, Sophia-Antipolis, France, 1990.

[6] G. Dowek. "A Complete Proof Synthesis Method for Type Systems of the Cube."
[7] G.Dowek. "Second Order Matching is Decidable in Type Systems of the Cube." In preparation.

[8] G.Huet. "Constrained Resolution A Complete Method for Higher Order Logic", Phd Thesis, Case Western Reserve University, 1972.

[9] G. Huet. "Résolution d'équations dans les langages d'ordres 1,2, ..., ω." Thèse de Doctorat d'État, Université de Paris VII, 1976.

[10] G. Huet, B. Lang. "Proving and Applying Program Transformations Expressed with Second Order Patterns", Acta Informatica n° 11, p. 31-55, 1978.

[11] D. Simon. "Checking Natural Language Proofs." 9th International Conference on Automated Deduction. Argonne, Illinois, USA, May 1988, Lecture Notes in Computer Science n°310