Equational Reasoning in Algebraic Structures: a Complete Tactic

Luís Cruz-Filipe^{1,2} and Freek Wiedijk^{1}

1NIII, University of Nijmegen, Netherlands and ^{2}CLC, Lisbon, Portugal

Abstract

We present rational, a Coq tactic for equational reasoning in abelian groups, commutative rings, and fields. We give an mathematical description of the method that this tactic uses, which abstracts from Coq specifics.

We prove that the method that rational uses is correct, and that it is complete for groups and rings. Completeness means that the method succeeds in proving an equality if and only if that equality is provable from the the group/ring axioms. Finally we characterize in what way our method is incomplete for fields.

Contents

1 Introduction 2 1.1 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Background 3 2.1 The mechanism of rational . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Object level and meta-level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 The semantic level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 The syntactic level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.5 The interpretation relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

3 Lifting 11 3.1 Lifting to variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Lifting expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3 Properties of lifting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.4 Permutation of lifting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

4 Completeness of rational: rings 22 4.1 Normal forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 4.2 The normalization function . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.3 Properties of P and N . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.4 The substitution lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.5 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

5 Completeness of rational: groups 35

6 Partial completeness of rational: fields 37 6.1 Correctness and completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

7 Remarks on the implementation 39

8 Conclusions 39

A Proof of Equality (19) 40

1 Introduction

One of the main aims of the Foundations group at the University of Nijmegen is to help making formalization of mathematics practical and attractive. For this reason a library of formal mathematics for the Coq system [3] – called the C-CoRN library [4] – has been developed to exercise the technology of proof formalization. This library started as a formalization of the Fundamental Theorem of Algebra in the so-called FTA project, but then was extended with a formalization of basic analysis up to the Fundamental Theorem of Calculus, and currently other subjects are being added to it as well.

To support the formalization work for the C-CoRN library, a tactic called rational was implemented. It automatically proves equations from the field axioms. Later this tactic was generalized to prove equations in rings and groups as well. The tactic uses the approach of reflection from [1], in particular the variant of reflection called partial reflection described in [7]. The generalization to rings and groups uses the application of partial reflection called hierarchical reflection in [5].

The tactic has two parts: the first part is a Coq formalization of normalization of polynomial expressions over a field, and the second part is an ML program that constructs a proof term for a given equation. This means that the tactic contains two – quite different – programs. On the one hand there is the program that computes the normal form of a polynomial expression. This program is written in the Coq type theory, and is proved correct as part of the Coq formalization. On the other hand there is the program that calculates a proof term from an equation, which is written in ML.

The correctness of the rational tactic is guaranteed by the way that it works: if it finds a proof of an equation, then that proof is automatically checked by Coq. Failure, however, can arise from two different situations:

(1) the ML program cannot find a term that corresponds to the problem.

(2) the ML program returns a term that does not have the expected behavior.

In turn, the second situation can arise in two cases:

(2a) although the original terms are provably equal, the normalization procedure cannot determine that;

(2b) the original terms are in fact not provably equal.

This paper studies the behavior of rational from a theoretical point of view.

• It gives a mathematical description of the algorithm implicit in the ML part of the rational tactic, and proves that this algorithm is correct.

• It describes under what conditions the tactic is complete.

Now completeness can mean two things here: either one can consider the set of equations that hold in all fields, or one can consider the equations that can be proved from the field axioms. It happens to be the case that both sets of equations are the same [2].

The first point means that situation (1) cannot occur. In the second point, we establish completeness for groups and rings, excluding also situation (2a). Unfortunately this result only extends partially to fields, but we can still give a simple condition which, if fulfilled, also excludes this situation.

As a consequence, when a call to rational fails no proof of the goal exists that follows exclusively from the structure’s axioms. This is extremely useful in interactive proof development, since it enables the user to detect wrong paths much earlier.

The mathematics in this paper has not been formalized. Formalizing takes an order of a magnitude more work than just doing the proofs in the informal – old style – way, and it is not clear what the benefit of formalization would be in this case (apart from the fact that one then would be certain that the proofs are correct).

The description in this paper of the rational tactic is kept as independent of Coq as possible. The algorithms and results that we describe are not specific to Coq or even to type theory, they can be used with any proof assistant.

This paper is self-contained in the sense that everything that is used is defined as well. However, it does not go into detail about partial/hierarchical reflection or the details of the rational tactic. For this we refer to two earlier papers, [7] and [5].

We begin by describing the mechanism of rational in more detail. Then we discuss the several layers of expressions we need to study this mechanism.

Section 3 formally describes the ML part of the tactic and proves a number of results about it, among which the correctness of the code. In Section 4 we introduce the normalization function for rings and prove its completeness. This proof generalizes almost directly to groups, as explained in Section 5. Finally, Section 6 analyzes the more complex case of fields, focusing on why the previous proof cannot be adapted to this situation, and presents an alternative completeness result.

The tactic described here is a simplified version of that in [5], and in Section 7 we explain how the same theorems can be generalized to the implemented tactic. We conclude with an overview of what was achieved in Section 8.

1.1 Related work

Most proof assistants have automation tools that provide the functionality of rational for rings, and many also have them for fields (for instance, the standard library of Coq provides both these functionalities with the ring and field tactics, see [3]). This automation is always implemented (like rational is) by putting polynomials into a normal form.

The main difference between our approach and these other implementations of the same idea is that we do the normalization in a very structured and systematic way. We define addition and multiplication functions that are meant to operate on monomials and polynomials that are already in normal form. These functions are then the ‘building blocks’ of our normalization function. This enables us to easily prove the correctness of the normalization function, which we need to use the reflection method.

2 Background

In this section we lay the bricks for the work we propose to do. We begin by describing the way rational works in detail, after which we summarize the parts of [6], [7] and [5] that are essential for the remainder of the paper.

2.1 The mechanism of rational

The rational tactic proves equalities in an algebraic structure A through the use of a type of syntactic expressions E together with an interpretation relation.

][_{ρ} ⊆ E × A

In this, ρ is a valuation that maps the variables in the syntactic expressions to values in A. The relation e ][_{ρ} a means that the syntactic expression e is interpreted under the valuation ρ by the object a.

The type E is an inductive type, and therefore it is possible to recursively define a normalization function N on the type of syntactic expressions:

N : E → E

One can prove the following two lemmas

\begin{matrix}e ][_{ρ} a ⇒ N (e) ][_{ρ} a \\ e ][_{ρ} a ∧ e ][_{ρ} b ⇒ a =_{A} b \end{matrix}

and together these lemmas give a method to prove equalities between terms that denote elements of A.

For instance, suppose that one wants to prove a =_{A} b. One finds e, f and ρ with e ][_{ρ} a and f ][_{ρ} b, and one checks whether N (e) = N (f). If this is the case then it follows that a =_{A} b.

For from the first lemma we find that N (e) ][_{ρ} a and N (f) ][_{ρ} b, and then the second lemma gives this desired equality.

2.2 Object level and meta-level

To describe the behavior of rational we need to look at terms of several kinds. This section explains these different kinds of terms in turn, so that the remainder of the paper can be easily understood.

Throughout this paper we deal with algebraic structures (groups, rings and fields). And, as we are working with formal systems, we also have terms that are interpreted in these algebraic structures. To complicate things, we use the method of reflection which means that the notion of ‘term’ both occurs on the meta-level as well as on the object level. In this section we will clarify this. We will identify various instances of ‘number zero’ as an example to explain the situation.

Let us start with the object level. We have three kinds of objects that have a ‘zero’.

• The natural numbers and the integers. First of all, we have the natural numbers ℕ. In the natural numbers there is a unique object which is the natural number zero.

The equality that one uses for the natural numbers is Leibniz equality. This means that the zero of the natural numbers does not have different representations: there is only one zero.

The integers are like the natural numbers: there is exactly one integer zero, and one uses Leibniz equality to compare integers.

• The elements of the algebraic structures. Each group, ring, or field A has a zero as well. However, as we use setoids for these algebraic structures (so we can model quotients in a constructively valid way), an algebraic structure can have more than one object that represents the zero of that structure. In other words, for an algebraic structure we use setoid equality instead of Leibniz equality.

For instance, suppose we construct the real numbers as Cauchy sequences of rational numbers. Then every Cauchy sequence that converges to zero represents the zero of these ‘Cauchy reals’. These sequences are then all ‘setoid equal’ to each other, but can be distinguished using Leibniz equality.

• Field expressions. Finally we have the set E of terms generated by the field operations: +, −, × and /. This is an inductively generated set of syntactic objects. In this set there is a unique term for ‘zero’. For these ‘field expressions’ we also use Leibniz equality.

Note that although these objects that we call field expressions are terms, they exist on the object level (as a set of mathematical objects, like the natural numbers) and not on the meta-level (as linguistic constructions).

We also have the meta-level. In the formal language that we use to talk about all these objects, we have terms denoting these objects. This means there is still another kind of zero:

• Terms on the meta-level. For the integers there is a constant in the language that denotes the integer zero. This symbol is a linguistic construction that differs from the integer zero itself, in that it exists on the meta-level instead of at the object level.

Similarly, there is a function in the language that maps each algebraic structure to a zero element of that structure. Again, the symbol for this function is different from those zero elements itself, in that it exists on the meta-level. Note that this function denotes one specific zero of the structure among all the elements that are setoid equal to it. Finally, in the case of the field expressions, the basic terms denoting them on the meta-level are very similar to the objects themselves. Still one should distinguish the two.

On the terms of the language there are two notions of equality. There is syntactic identity, and there is βδι-equality or convertibility. (These equalities are used to talk about the language, and cannot be expressed in the language itself.)

Consider the function ‘zring’ that maps the integers into a given ring. Then if one applies this function to the integer zero, one gets a term that is syntactically different from the term that denotes the zero of the ring. However it is convertible to this term, by βδι-reduction (δreduction means unfolding the definition of a function, and ι-reduction means unfolding of a recursive definition.)

We will almost everywhere use syntactic identity in this paper. The only conversion that we will refer to is βδι-reduction of a few basic functions: subtraction, the zring function and exponentiation with a constant natural number. Of all other functions the definition will never be unfolded.

We also have two kinds of ‘terms’, which are quite different. There are the ‘field expressions’ on the object level, and there are the terms denoting elements of a field on the meta-level. In both cases one builds these terms with the field operations: +, −, × and /. However they exist on different levels (the method of mimicking part of the meta-level on the object level is called reflection). Also, the field expressions are very trivial: they can only involve variables and the field operations. But the meta-level terms can involve any type of sub-term, as long as the full term denotes an element of the field. For instance in the field of real numbers \sqrt{zring(2)} is an acceptable meta-level term, but there is nothing like a square root in field expressions.

The distinction between these two different kinds of terms can be illustrated with two relations that are defined in this paper. The relation <_{E} is defined on the field expressions in Definition 2.17. The relation ≺_{A} is defined on meta-level terms denoting elements of the field A in Definition 2.12. Note that this second relation does not respect convertibility: 1_{A}^{0} (‘one to the power zero’) is convertible with 1_{A}, but 1_{A} ≺_{A} 1_{A}^{0} while 1_{A} ⊀_{A} 1_{A}.

To summarize, we have three quite different kinds of objects that have a zero (integers, elements in an algebraic structure, and field expressions), and we should distinguish between these objects on the object level and terms denoting them on the meta-level.

Also we have four kinds of equality: between the objects on the object level we have Leibniz equality and setoid equality (and we can write those equalities in our language), while between the terms on the meta-level we have syntactic identity and βδι-equality (and those two relations are not in the language).

2.3 The semantic level

We now summarize the Algebraic Hierarchy of C-CoRN [6], on top of which rational works.

Definition 2.1 A setoid structure over A is a relation =_{A}: A → A → Prop (denoted infix) satisfying:

Set_{1} : ∀_{x:A}.x =_{A} x
Set_{2} : ∀_{x,y:A}.x =_{A} y → y =_{A} x
Set_{3} : ∀_{x,y,z:A}.x =_{A} y → y =_{A} z → x =_{A} z

Furthermore, we distinguish subtypes [A → A] and [A → A → A] of A → A and A → A → A, respectively, satisfying

Set_{4} : ∀_{f:[A→A]}.∀_{x,x′:A}.x =_{A} x′ → f(x) =_{A} f(x′)

Set_{5} : ∀_{f:[A→A→A]}.∀_{x,x′,y,y′:A}.x =_{A} x′ → y =_{A} y′ → f(x, y) =_{A} f(x′, y′)

We will speak of a setoid A to mean a type A with a setoid structure over A.

Definition 2.2 A group structure over A is a setoid structure over A together with a tuple ⟨0_{A}, +_{A}, −_{A}⟩ where 0_{A} : A, +_{A} : [A → A → A] and −_{A} : [A → A] (we will write +_{A} using the usual infix notation) satisfying:

SG : ∀_{x,y,z:A}.(x +_{A} y) +_{A} z =_{A} x +_{A} (y +_{A} z)
M_{1} : ∀_{x:A}.x +_{A} 0 =_{A} x
M_{2} : ∀_{x:A}.0 +_{A} x =_{A} x
G_{1} : ∀_{x:A}.x +_{A} (−_{A}x) =_{A} 0
G_{2} : ∀_{x:A}.(−_{A}x) +_{A} x =_{A} 0
AG : ∀_{x,y:A}.x +_{A} y =_{A} y +_{A} x

Notice that axiom M_{2} (respectively G_{2}) can be proved from M_{1} (resp. G_{1}) and AG. But in the construction of the Algebraic Hierarchy AG is introduced last.

By a group A we mean a type A with a group structure over it.

Definition 2.3 Let A be a group. We define −_{A} : A → A → A by

x −_{A} y := x +_{A} (−_{A}y).

The following is trivial, and allows us to write −_{A} : [A → A → A].

Proposition 2.4 −_{A} satisfies Set_{5}.

Definition 2.5 A ring structure over A is a group structure over A together with a tuple ⟨1_{A}, ×_{A}⟩ where 1_{A} : A, ×_{A} : [A → A → A] (we will write ×_{A} using the usual infix notation) satisfying the following.

R_{1} : ∀_{x,y,z:A}.(x ×_{A} y) ×_{A} z =_{A} x ×_{A} (y ×_{A} z)
R_{2} : ∀_{x:A}.x ×_{A} 1 =_{A} x
R_{3} : ∀_{x:A}.1 ×_{A} x =_{A} x
R_{4} : ∀_{x,y:A}.x ×_{A} y =_{A} y ×_{A} x
R_{5} : ∀_{x,y,z:A}.x ×_{A} (y +_{A} z) =_{A} (x ×_{A} y) +_{A} (x ×_{A} z)

As before, axiom R_{3} can be proved from R_{2} and R_{4}.

By a ring A we mean a type A with a ring structure over it.

Definition 2.6 Let A be a ring. We define two functions zring_{A} : ℤ → A and nexp_{A} : A → ℕ → A inductively as follows:

zring_{A}(0) := 0_{A}  (1)
zring_{A}(n + 1) := zring_{A}(n) +_{A} 1_{A}, for n ≥ 0  (2)
zring_{A}(n − 1) := zring_{A}(n) −_{A} 1_{A}, for n ≤ 0  (3)

nexp_{A}(x, 0) := 1_{A}  (4)
nexp_{A}(x, n + 1) := x ×_{A} nexp_{A}(x, n)  (5)

We denote zring_{A}(n) by \underline{n}_{A} and nexp_{A}(x, n) by x^{n}.

The following is again trivial to prove.

Proposition 2.7 For every n, the function ·^{n} : A → A satisfies Set_{4}.

Based on this result, we will often see x^{n} as the application of ·^{n} : [A → A] to x.

Definition 2.8 A field structure over A is a ring structure over A together with an operation ·^{−1} : Π_{x:A}.x ≠ 0 → A (we denote (·^{−1} x H) simply by x^{−1}, leaving the proof term implicit) satisfying

F : x ≠ 0 → x ×_{A} x^{−1} =_{A} 1_{A}.

By a field A we mean a type A with a field structure over it.

Definition 2.9 Let A be a field. We define /_{A} : A → Π_{y:A}.y ≠ 0 → A by

x/_{A}y := x ×_{A} (y^{−1}).

The following is trivial:

Proposition 2.10 /_{A} satisfies Set′_{5}:

Set′_{5} : ∀_{x,x′,y,y′:A}.y ≠ 0 → y′ ≠ 0 → x =_{A} x′ → y =_{A} y′ → x/_{A}y =_{A} x′/_{A}y′

We will sometimes abuse notation and refer to Set′_{5} as an instance of Set_{5}, and refer to /_{A} as an operation of type [A → A → A].

Definition 2.11 A proof of t_{1} =_{A} t_{2} from the field axioms in an environment Γ is a sequence φ_{1}, …, φ_{n} of equalities such that φ_{n} is t_{1} =_{A} t_{2} and, for i = 1, …, n, one of the following holds.

– φ_{i} is an instance of one of the axioms Set_{1}, SG, M_{1}, M_{2}, G_{1}, G_{2}, AG or R_{1}–R_{5}.

– φ_{i} is an instance of axiom F and the hypothesis of this axiom is in Γ.

– φ_{i} is an instance of one of the axioms Set_{2}–Set_{5} and the hypothesis(es) of the axiom are included in {φ_{1}, …, φ_{i−1}}.

We will often not mention Γ explicitly, but assume that all the proofs are done in an environment containing all the necessary inequalities. The reason for this (and for choosing the term “environment” rather than “context”) is that rational only looks at the equality being proved and assumes all needed inequalities hold anyway.

Definition 2.12 Let A be a type. We define the relation ≺_{A} on the terms of type A as the least relation satisfying:

1. t ≺_{A} f(t) for f : [A → A] (in particular, in a group one has t ≺_{A} −_{A}t and in a ring t ≺_{A} t^{n} for n : ℕ);

2. t_{i} ≺_{A} f(t_{1}, t_{2}) for f : [A → A → A] and i = 1, 2 (in particular, f can be one of +_{A}, −_{A} or ×_{A} in a group or ring);

3. if A is a field, then t_{i} ≺_{A} t_{1}/_{A}t_{2} for i = 1, 2.

(Notice the implicit requirement t_{2} ≠ 0 in the clause t_{i} ≺_{A} t_{1}/_{A}t_{2}.)

Proposition 2.13 ≺_{A} is a well founded relation.

Proof. By definition, if t_{1} ≺_{A} t_{2} then t_{1} is a subterm of t_{2}; since “being a subterm of” is a well founded relation, so is ≺_{A}. □

Notation 2.14 From now on, we will omit the subscript A in the symbols denoting the algebraic operations, since no ambiguity is introduced. However, we will write =_{A} to emphasize the distinction between this defined equality and the one induced by βδι-reduction on the set of lambda terms of type A.

2.4 The syntactic level

We now introduce the syntactic counterpart to the type of fields, which is the type of expressions that rational works with. Definition 2.15 The syntactic type E of expressions is the inductive type generated by the following grammar:

E ::= ℤ | 𝕍_{0} | 𝕍_{1}(E) | E + E | E × E | E/E

where 𝕍_{i} = {v_{j}^{i}|j ∈ ℕ} for i = 0, 1. Definition 2.16 We define the following abbreviations on expressions:

−e := e × (−1)  (6)
e_{1} − e_{2} := e_{1} + (−e_{2})  (7)
e^{0} := 1  (8)
e^{n+1} := e × e^{n}  (9)

Notice that these abbreviations are done only on the meta-level; when we write e.g. e_{1} − e_{2} we are speaking about the expression e_{1} + (e_{2} × (−1)).

At some stage we will need an order on E. Definition 2.17 The order on E is defined as follows, where ⋆ stands for +, × or /.

(i) v_{i}^{0} <_{E} v_{j}^{0} if i < j; (ii) v_{i}^{0} <_{E} e whenever e is i : ℤ, e_{1} ⋆ e_{2} or v_{i}^{1}(e′); (iii) i <_{E} j if i < j (i, j : ℤ); (iv) i <_{E} e whenever e is e_{1} ⋆ e_{2} or v_{i}^{1}(e′);

(v) e_{1} ⋆ e_{2} <_{E} e′_{1} ⋆ e′_{2} whenever e_{1} <_{E} e′_{1} or e_{1} = e′_{1} and e_{2} <_{E} e′_{2} (lexicographic ordering); (vi) e_{1} + e_{2} <_{E} e whenever e is e′_{1} × e′_{2}, e′_{1}/e′_{2} or v_{i}^{1}(e′); (vii) e_{1} × e_{2} <_{E} e whenever e is e′_{1}/e′_{2} or v_{i}^{1}(e′); (viii) e_{1}/e_{2} <_{E} e whenever e is v_{i}^{1}(e′); (ix) v_{i}^{1}(e_{1}) <_{E} v_{j}^{1}(e_{2}) whenever i < j or i = j and e_{1} <_{E} e_{2}. In other words, expressions are recursively sorted by first looking at their outermost operator

x <_{E} i <_{E} e + f <_{E} e × f <_{E} e/f <_{E} v(e)

and then sorting expressions with the same operator using a lexicographic ordering. For example, if x <_{𝕍_{0}} y and u <_{𝕍_{1}} v, then

x <_{E} y <_{E} 2 <_{E} 34 <_{E} x/4 <_{E} u(x + 3) <_{E} u(2 × y) <_{E} v(x + 3).

2.5 The interpretation relation

The correspondence between the syntactic and the semantic levels is made via an interpretation relation, described in detail in [7] and [5]. It is this relation that allows us to speak of correctness and completeness of rational, which is what we want to do.

Substitutions

The definition of E includes families of variables so that we can speak about arbitrary expressions in a field, and not only about those that only mention the field operations. Therefore, the interpretation of an expression is dependent on an assignment of values to the variables, which we will call a substitution.

Definition 2.18 A substitution from a type of variables 𝕍 to a type T is a finite (partial) function from 𝕍 to T.

Notation 2.19 The domain of a substitution ρ will be denoted by dom(ρ) or simply by domρ. We will use the usual notation [v := t] for the substitution that replaces v with t.

The following definitions and results are standard from the theory of finite functions.

Definition 2.20 Let ρ, σ be substitutions from 𝕍 to T. If ρ and σ coincide on the intersection of their domains (in particular, if their domains are disjoint), we define the union ρ∪σ to be the only substitution θ with domain domρ ∪ domσ such that θ(v) = ρ(v), for v ∈ domρ, and θ(v) = σ(v) for v ∈ domσ.

Definition 2.21 Let ρ, σ be substitutions from 𝕍 to T. We say that ρ is contained in σ, denoted by ρ ⊆ σ, if there is a substitution θ from 𝕍 to T such that σ = ρ ∪ θ.

Proposition 2.22 For all 𝕍 and T, ⊆ is a partial order on the set of substitutions from 𝕍 to T.

Proof. Trivial. □

Proposition 2.23 Let ρ, σ be substitutions from 𝕍 to T such that ρ ⊆ σ. Then σ(v) = ρ(v) for every v ∈ domρ.

Proof. By definition of ⊆, there is a substitution θ such that σ = ρ ∪ θ; by definition of ∪, since v ∈ domρ, σ(v) = (ρ ∪ θ)(v) = ρ(v). □

Definition 2.24 A substitution ρ is injective if, for any two distinct variables x and y in 𝕍, the terms ρ(x) and ρ(y) are syntactically distinct.

From now on, we assume a fixed field A.

Definition 2.25 A substitution pair over A is a pair ρ = ⟨ρ_{0}, ρ_{1}⟩ where ρ_{0} and ρ_{1} are injective substitutions from, respectively, 𝕍_{0} to A and 𝕍_{1} to [A → A].

The results about substitutions generalize in the obvious way to substitution pairs.

Definition 2.26 Let ρ be a substitution pair over A. We say that ρ is contained in σ, denoted by ρ ⊆ σ, if ρ_{i} ⊆ σ_{i} for i = 0, 1.

Proposition 2.27 ⊆ is a reflexive and transitive relation on the set of substitution pairs over A.

Proposition 2.28 Let ρ, σ be substitution pairs over A such that ρ ⊆ σ. Then σ_{i}(v_{k}^{i}) = ρ_{i}(v_{k}^{i}) for i = 0, 1 and v_{k}^{i} ∈ domρ_{i}.

Interpretation of expressions

Definition 2.29 Let ρ be a substitution pair over A. The interpretation relation ][_{ρ} ⊆ E × A is defined inductively by:

ρ_{0}(v_{i}^{0}) =_{A} t → v_{i}^{0} ][_{ρ} t  (10)
\underline{k} =_{A} t → k ][_{ρ} t  (11)
e_{1} ][_{ρ} t_{1} ∧ e_{2} ][_{ρ} t_{2} ∧ t_{1} + t_{2} =_{A} t → e_{1} + e_{2} ][_{ρ} t  (12)
e_{1} ][_{ρ} t_{1} ∧ e_{2} ][_{ρ} t_{2} ∧ t_{1} × t_{2} =_{A} t → e_{1} × e_{2} ][_{ρ} t  (13)
e_{1} ][_{ρ} t_{1} ∧ e_{2} ][_{ρ} t_{2} ∧ t_{2} ≠ 0 ∧ t_{1}/t_{2} =_{A} t → e_{1}/e_{2} ][_{ρ} t  (14)
e ][_{ρ} t_{1} ∧ ρ_{1}(v_{i}^{1})(t_{1}) =_{A} t → v_{i}^{1}(e) ][_{ρ} t  (15)

Notice that by omitting (14) we obtain an interpretation relation over rings; omitting also (13) and (11) for k ≠ 0 we obtain an interpretation relation over groups.

Lemma 2.30 The abbreviated expressions (Definition 2.16) satisfy the following relations.

e ][_{ρ} t_{1} ∧ −t_{1} =_{A} t → −e ][_{ρ} t  (16)
e_{1} ][_{ρ} t_{1} ∧ e_{2} ][_{ρ} t_{2} ∧ t_{1} − t_{2} =_{A} t → e_{1} − e_{2} ][_{ρ} t  (17)
e ][_{ρ} t_{1} ∧ t_{1}^{n} =_{A} t → e^{n} ][_{ρ} t  (18)

Proof.

(16) Recall that −e = e × (−1). By Set_{1}, −1 =_{A} −1; hence −1 ][_{ρ} −1 by (11). By hypothesis e ][_{ρ} t_{1}. Finally, since −t_{1} =_{A} t, one has t_{1} × (−1) =_{A} t, whence e × (−1) ][_{ρ} t by (13).

(17) By definition, e_{1} − e_{2} = e_{1} + (−e_{2}). By hypothesis, e_{1} ][_{ρ} t_{1} and e_{2} ][_{ρ} t_{2}. Since −t_{2} =_{A} −t_{2} by Set_{1}, one has that −e_{2} ][_{ρ} −t_{2} by (16). By hypothesis t_{1} − t_{2} =_{A} t, that is (by definition of −_{A}), t_{1} + (−t_{2}) =_{A} t. Hence, by (12) e_{1} + (−e_{2}) ][_{ρ} t.

(18) By induction on n. If n is 0, then by (8) e^{n} = 1. By hypothesis t_{1}^{0} =_{A} t, or simply 1 =_{A} t since t_{1}^{0} = 1 by (4). Hence 1 ][_{ρ} t by (11).

Consider now n = m + 1; then e^{n} = e × e^{m} by (9). By hypothesis t_{1}^{m+1} =_{A} t, that is to say, t_{1} × t_{1}^{n} =_{A} t according to (5). But e ][_{ρ} t_{1} by hypothesis, and also e^{m} ][_{ρ} t_{1}^{m} by induction hypothesis; hence e × e^{m} ][_{ρ} t by (13).

□

Lemma 2.31 Let e : E, t : A and ρ, σ be substitution pairs for A with ρ ⊆ σ such that e ][_{ρ} t; then e ][_{σ} t.

Proof. By induction on the proof of e ][_{ρ} t.

1. e = v_{i}^{0} and ρ_{0}(v_{i}^{0}) =_{A} t: since ρ ⊆ σ, Proposition 2.28 implies that σ_{0}(v_{i}^{0}) =_{A} t, and by (10) also v_{i}^{0} ][_{σ} t.

2. e = n and \underline{n} =_{A} t: then n ][_{σ} t follows by (11).

3. e = e_{1} + e_{2}, e_{1} ][_{ρ} t_{1}, e_{2} ][_{ρ} t_{2} and t_{1} + t_{2} =_{A} t; by induction hypothesis e_{1} ][_{σ} t_{1} and e_{2} ][_{σ} t_{2}, whence e_{1} + e_{2} ][_{σ} t follows from (12).

4. e = e_{1} × e_{2}: analogous using (13).

5. e = e_{1}/e_{2}: similar from (14), noticing that the side condition t_{2} ≠ 0 is also given by hypothesis.

6. e = v_{i}^{1}(e′), e′ ][_{ρ} t′ and ρ_{1}(v_{i}^{1})(t′) =_{A} t: since σ_{1}(v_{i}^{1}) = ρ_{1}(v_{i}^{1}) by Proposition 2.28, also σ_{1}(v_{i}^{1})(t′) =_{A} t. By induction hypothesis e′ ][_{σ} t′, whence v_{i}^{1}(e′) ][_{σ} t by (15).

□

Lemma 2.32 Let e : E, t, t′ : A and ρ be a substitution pair for A such that e ][_{ρ} t and e ][_{ρ} t′. Then the following hold.

(i) t =_{A} t′;

(ii) if e ][_{ρ} t and e ][_{ρ} t′ can be proved without using (14), and no divisions occur in either t or t′, then t =_{A} t′ can be proved without using the axiom F.

Proof. By induction on ][_{ρ} (Coq checked). □

3 Lifting

We now start looking at the actual implementation of rational, focusing on the ML program inside it. This program computes a partial inverse to the interpretation relation described above, that is, given a term t : A, with A a field, it returns an expression e and a substitution pair ρ such that e ][_{ρ} t. In this section we formally describe this program as a function lift and prove its correctness.

3.1 Lifting to variables

The first step is to define what to do when we meet a term that is not built from the field operations, e.g. a variable x or an expression like \sqrt{2}.

Definition 3.1 Let t : A and ρ be a substitution pair over A. Then lift_{𝕍_{0}}(t, ρ) = ⟨v, σ⟩, v ∈ 𝕍_{0}, is defined by:

• if there is an i such that ρ_{0}(v_{i}^{0}) = t, then v = v_{i}^{0} and σ = ρ;

• else, let k be minimal such that ρ_{0}(v_{k}^{0}) is not defined and take v = v_{k}^{0} and σ_{0} = ρ_{0} ∪[v_{k}^{0} := t], σ_{1} = ρ_{1}.

The behavior of lift_{𝕍_{0}} can be described as follows: given a term t and a substitution ρ, it checks whether there is a variable v_{i}^{0} such that ρ_{0}(v_{i}^{0}) = t. In the affirmative case, it returns this variable and ρ; else it extends ρ_{0} with a fresh variable which is interpreted to t and returns this variable and the resulting substitution. Notice that the result is deterministic, since there is at most one variable i satisfying ρ_{0}(v_{i}^{0}) = t.

Lemma 3.2 Let t and ρ be as in Definition 3.1, and suppose that lift_{𝕍_{0}}(t, ρ) = ⟨v, σ⟩. Then ρ ⊆ σ.

Proof. Immediate: either σ = ρ, and we invoke reflexivity of ⊆ (Proposition 2.27), or ⟨σ_{0}, σ_{1}⟩ = ⟨ρ_{0} ∪ [v_{k}^{0} := t], ρ_{1}⟩ with v_{k}^{0} ∉ domρ_{0}, which directly satisfies the definition of ⊆. □

Lemma 3.3 Let t and ρ be as in Definition 3.1, and suppose that lift_{𝕍_{0}}(t, ρ) = ⟨v, σ⟩. Then v ][_{σ} t.

Proof. By definition of lift_{𝕍_{0}}, there are two cases:

• There is an i such that ρ_{0}(v_{i}^{0}) = t, and then also ρ_{0}(v_{i}^{0}) =_{A} t by Set_{1}, whence v_{i}^{0} ][_{ρ} t by (10). Since in this case v = v_{i}^{0} and σ = ρ, the thesis follows.

• There is no such i; then v = v_{k}^{0} where k ∉ domρ_{0}, and σ_{0} = ρ_{0} ∪[v_{k}^{0} := t]. Then, by definition of ∪, σ_{0}(v_{k}^{0}) = t and we can conclude as above that v_{k}^{0} ][_{σ} t using Set_{1} and (10).

□

Definition 3.4 Let f : [A → A] and ρ be a substitution pair over A. Then lift_{𝕍_{1}}(f, ρ) = ⟨v, σ⟩, v ∈ 𝕍_{1}, is defined by:

• if there is an i such that ρ_{1}(v_{i}^{1}) = f, then v = v_{i}^{1} and σ = ρ;

• else, let k be minimal such that ρ_{1}(v_{k}^{1}) is not defined and take v = v_{k}^{1} and σ_{0} = ρ_{0}, σ_{1} = ρ_{1} ∪ [v_{k}^{1} := t].

Lemma 3.5 Let t and ρ be as in Definition 3.4, and suppose that lift_{𝕍_{1}}(t, ρ) = ⟨v, σ⟩. Then ρ ⊆ σ.

Proof. Analogous to the proof of Lemma 3.2. □

Lemma 3.6 Let f : [A → A] and ρ be a substitution pair over A and suppose that lift_{𝕍_{1}}(f, ρ) = ⟨v, σ⟩. Suppose that t ][_{ρ} e; then v(t) ][_{σ} f(e).

Proof. By definition of lift_{𝕍_{1}}, there are again two cases:

• There is an i such that ρ_{1}(v_{i}^{1}) = f; then ρ_{1}(v_{i}^{1})(t) =_{A} f(t) by Set_{1}, whence v_{i}^{1}(e) ][_{ρ} f(t) by (15). Since in this case v = v_{i}^{1} and σ = ρ, the thesis follows.

• There is no such i; then v = v_{k}^{1} where k ∉ domρ_{1}, and σ_{1} = ρ_{1} ∪[v_{k}^{1} := t]. Then, by definition of ∪, σ_{1}(v_{k}^{1}) = f and we can conclude as above that v_{k}^{1}(e) ][_{σ} f(t) using Set_{1} and (15).

□

3.2 Lifting expressions

We can now define lift.

Definition 3.7 Let t : A and ρ be a substitution pair over A. Then lift(t, ρ) is recursively defined as follows.

lift(\underline{n}, ρ) = ⟨n, ρ⟩  n : ℤ closed
lift(t_{1} ⋆ t_{2}, ρ) = ⟨e_{1} ⋆ e_{2}, σ⟩ where \{ \begin{matrix}⋆ ∈ \{+, −, ×, /\} \\ ⟨e_{1}, θ⟩ = lift(t_{1}, ρ) \\ ⟨e_{2}, σ⟩ = lift(t_{2}, θ) \end{matrix}
lift(−t, ρ) = ⟨−e, σ⟩  where ⟨e, σ⟩ = lift(t, ρ)
lift(t^{n}, ρ) = ⟨e^{n}, σ⟩  where \{ \begin{matrix}n : ℕ is closed \\ ⟨e, σ⟩ = lift(t, ρ) \end{matrix}
lift(f(t), ρ) = ⟨v_{i}^{1}(e), θ⟩ where \{ \begin{matrix}⟨e, σ⟩ = lift(t, ρ) \\ ⟨v_{i}^{1}, θ⟩ = lift_{𝕍_{1}}(f, σ) \end{matrix}
lift(t, ρ) = lift_{𝕍_{0}}(t, ρ) otherwise

The two last clauses also define lift(\underline{n}, ρ) and lift(t^{n}, ρ) when n is not a closed term.

Notice that on every recursive call of lift the argument decreases w.r.t ≺_{A}; since ≺_{A} is well founded by Proposition 2.13, this is a valid definition.

Lemma 3.8 Let ρ be a substitution pair for A. For all t : A and e : E, if ⟨e, σ⟩ = lift(t, ρ), then ρ ⊆ σ.

Proof. By induction on ≺_{A}.

1. t is minimal for ≺_{A}:

(a) t = \underline{n} with n : ℤ closed. Then σ = ρ.

(b) otherwise ⟨e, σ⟩ = lift_{𝕍_{0}}(t, ρ). By Lemma 3.2, ρ ⊆ σ.

2. t = f(t′) with f : [A → A].

(a) f is −_{A}: immediate by induction hypothesis.

(b) f is ·^{n} with n is a closed term: then the result follows by induction hypothesis.

(c) otherwise, e = v_{i}^{1}(e′) with ⟨e′, θ⟩ = lift(t′, ρ) and ⟨v_{i}^{1}, σ⟩ = lift_{𝕍_{1}}(f, θ). By induction hypothesis ρ ⊆ θ; by Lemma 3.5 θ ⊆ σ; by transitivity ρ ⊆ σ.

3. t = t_{1} ⋆ t_{2} with ⋆ ∈ {+, −, ×, /}: then e = e_{1} ⋆ e_{2} with ⟨e_{1}, θ⟩ = lift(t_{1}, ρ) and ⟨e_{2}, σ⟩ = lift(t_{1}, θ).

By induction hypothesis, ρ ⊆ θ and θ ⊆ σ; since ⊆ is transitive (Proposition 2.27), ρ ⊆ σ.

□

The following is the main result so far: it expresses the correctness of the ML program inherent to rational. Given a term t and a substitution ρ, the program computes an expression e and a new substitution σ such that e ][_{σ} t.

Theorem 3.9 Let t : A and ρ be a substitution pair over A, and take ⟨e, σ⟩ = lift(t, ρ). Then e ][_{σ} t.

Proof. By induction on ≺_{A}.

1. t is minimal for ≺_{A}:

(a) t = \underline{n} with n : ℤ closed. Then, by definition of lift, e = n and σ = ρ. By Set_{1}, \underline{n} =_{A} \underline{n}, and by (11) n ][_{ρ} \underline{n}.

(b) otherwise ⟨e, σ⟩ = lift_{𝕍_{0}}(t, ρ). By Lemma 3.3, it follows that e ][_{σ} t.

2. t = f(t′) with f : [A → A].

(a) f is −_{A}: then ⟨e, σ⟩ = ⟨−e′, σ⟩ with ⟨e′, σ⟩ = lift(t′, ρ). By induction hypothesis, e′ ][_{σ} t′; since −t′ = −t′ by Set_{1}, −e′ ][_{σ} −t′ by (16).

(b) f is ·^{n} with n closed: then ⟨e, σ⟩ = ⟨(e′)^{n}, σ⟩ with ⟨e′, σ⟩ = lift(t′, ρ). By induction hypothesis, e′ ][_{σ} t′; since (t′)^{n} = (t′)^{n} by Set_{1}, (e′)^{n} ][_{σ} (t′)^{n} by (18).

(c) otherwise e = v_{i}^{1}(e′) with ⟨e′, θ⟩ = lift(t′, ρ) and ⟨v_{i}^{1}, σ⟩ = lift_{𝕍_{1}}(f, θ). By induction hypothesis e′ ][_{θ} t′; Lemma 3.6 allows us to conclude that f(e′) ][_{σ} v_{i}^{1}(t′).

3. t = t_{1} ⋆ t_{2} with ⋆ ∈ {+, −, ×, /} (if ⋆ − /, then also t_{2} ≠ 0): then e = e_{1} ⋆ e_{2} with ⟨e_{1}, θ⟩ = lift(t_{1}, ρ) and ⟨e_{2}, σ⟩ = lift(t_{1}, θ).

By induction hypothesis, e_{1} ][_{θ} t_{1}; by Lemma 3.8, θ ⊆ σ, whence by Lemma 2.31 also e_{1} ][_{σ} t_{1}.

Also by induction hypothesis, e_{2} ][_{θ} t_{2}. Furthermore, Set_{1} implies t_{1} ⋆ t_{2} =_{A} t_{1} ⋆ t_{2}, hence e_{1} ⋆ e_{2} ][_{θ} t_{1} ⋆ t_{2} by either (12), (17), (13) or (14), according to whether ⋆ is respectively +, −, × or /; in the last case, the extra condition t_{2} ≠ 0 also holds.

□

Notice that this result is still valid if A is a group or a ring, as can be seen by removing the corresponding cases in this proof and checking that it remains valid.

3.3 Properties of lifting

The remainder of this section is concerned with other properties of the ML program, and of lift, that are needed for the rest of the paper.

First, lifting is idempotent on the second component: if lifting e with ρ returns t and σ, and θ is any substitution extending σ (in particular, σ itself), then lift(t, θ) = ⟨e, θ⟩.

Lemma 3.10 Let t : A, e : E and ρ, σ, θ be substitution pairs over A such that ⟨e, σ⟩ = lift(t, ρ) and σ ⊆ θ. Then lift(t, θ) = ⟨e, θ⟩.

Proof. By induction on ≺_{A}.

1. t is minimal for ≺_{A}:

(a) t = \underline{n} with n : ℤ closed. Then lift(\underline{n}, ρ) = ⟨n, ρ⟩ and lift(\underline{n}, θ) = ⟨n, θ⟩; hence the thesis holds.

(b) otherwise ⟨e, σ⟩ = lift_{𝕍_{0}}(t, ρ). Then e = v_{i}^{0} for some i, and by Lemma 3.3, σ_{0}(v_{i}^{0}) = t. Since σ ⊆ θ, θ_{0}(v_{i}^{0}) = t by Lemma 2.31, and, according to the definition of lift_{𝕍_{0}}, lift_{𝕍_{0}}(t, θ) = ⟨v_{i}^{0}, θ⟩.

2. t = f(t′) with f : [A → A].

(a) f is −_{A}: then ⟨e, σ⟩ = ⟨−e′, σ⟩ with ⟨e′, σ⟩ = lift(t′, ρ). By induction hypothesis, lift(t′, θ) = ⟨e′, θ⟩, whence lift(−t′, θ) = ⟨−e′, θ⟩.

(b) f is ·^{n} and n is closed: then ⟨e, σ⟩ = ⟨(e′)^{n}, σ⟩ with ⟨e′, σ⟩ = lift(t′, ρ). By induction hypothesis, lift(t′, θ) = ⟨e′, θ⟩, and it follows that lift((t′)^{n}, θ) = ⟨(−e′)^{n}, θ⟩.

(c) otherwise e = v_{i}^{1}(e′) with ⟨e′, σ′⟩ = lift(t′, ρ) and ⟨v_{i}^{1}, σ⟩ = lift_{𝕍_{1}}(f, σ′). By induction hypothesis, lift(t′, θ) = ⟨e′, θ⟩; by Lemma 3.6, σ_{1}(v_{i}^{1}) = f and hence θ_{1}(v_{i}^{1}) = f by Lemma 2.31. Therefore, the definition of lift_{𝕍_{1}} ensures that lift_{𝕍_{1}}(f, θ) = ⟨v_{i}^{1}, θ⟩ and lift(f(t′), θ) = ⟨v_{i}^{1}(e′), θ⟩.

3. t = t_{1} ⋆ t_{2} with ⋆ ∈ {+, −, ×, /}: then e = e_{1} ⋆ e_{2} with ⟨e_{1}, σ_{1}⟩ = lift(t_{1}, ρ) and ⟨e_{2}, σ⟩ = lift(t_{1}, σ_{1}).

By Lemma 3.8, σ_{1} ⊆ σ, hence σ_{1} ⊆ θ; then, by induction hypothesis, lift(t_{1}, θ) = ⟨e_{1}, θ⟩. Also by induction hypothesis, lift(t_{2}, θ) = ⟨e_{2}, θ⟩. It follows that lift(t_{1} ⋆ t_{2}, θ) = ⟨e_{1} ⋆ e_{2}, θ⟩.

□

All variables in the expression output by lift can be interpreted by the corresponding substitution.

Lemma 3.11 Let t : A and ρ be a substitution pair over A. If lift(t, ρ) = ⟨e, σ⟩, then v_{k}^{i} ∈ dom(σ_{k}) for all variables v_{k}^{i} occurring in e.

Proof. By induction on t according to ≺_{A}.

1. t is minimal for ≺_{A}.

(a) t = \underline{n}: then e = n and no variables occur in e, so the result vacuously holds.

(b) otherwise ⟨e, σ⟩ = lift_{𝕍_{0}}(t, ρ) and the result is immediate by definition of lift_{𝕍_{0}}.

2. t = f(t′) with f : [A → A].

(a) f is −_{A}: then e = e′ and lift(t′, ρ) = ⟨e′, σ⟩. Any variable v_{k}^{i} occurring in e must occur in e′, and by induction hypothesis v_{k}^{i} ∈ dom(σ_{i}).

(b) f is ·^{n} with n closed: analogous.

(c) otherwise there exist a natural number j, an expression e′ and a substitution pair θ such that lift(t′, ρ) = ⟨e′, θ⟩, lift_{𝕍_{1}}(f, θ) = ⟨v_{j}^{1}, σ⟩ and e = v_{j}^{1}(e′). If v_{k}^{i} is a variable occurring in e, then either v_{k}^{i} = v_{j}^{1} and the result holds by definition of lift_{𝕍_{1}} or v_{k}^{i} occurs in e′; in the latter case, by induction hypothesis v_{k}^{i} ∈ dom(θ_{i}), and since θ ⊆ σ also v_{k}^{i} ∈ dom(σ_{i}).

3. t = t_{1} ⋆ t_{2} with ⋆ ∈ {+, −, ×, /}: then e = e_{1} ⋆ e_{2} and there is a substitution pair θ such that lift(t_{1}, ρ) = ⟨e_{1}, θ⟩ and lift(t_{2}, θ) = ⟨e_{2}, σ⟩. Suppose v_{k}^{i} occurs in e; then it either occurs in e_{1} or in e_{2}. In the first case, by induction hypothesis v_{k}^{i} ∈ dom(θ_{i}), and since θ ⊆ σ also v_{k}^{i} ∈ dom(σ_{i}). The second case follows directly from the induction hypothesis.

□

3.4 Permutation of lifting

To prove properties of rational, we need to consider situations when the same terms are lifted in different orders. This section proves some results about the corresponding outputs: under quite general hypotheses, they differ only in the names of the variables.

Definition 3.12 Let ρ, σ be substitution pairs for A. We say that σ is obtained from ρ by a renaming of variables if there is a pair ξ = ⟨ξ_{0}, ξ_{1}⟩ of permutations of ℕ such that, for i = 0, 1, the following conditions hold:

• ξ_{i}(k) ≠ k → v_{k}^{i} ∈ dom(ρ_{i});

• for all k, σ_{i} (v_{ξ_{i}(k)}^{i}) ≃ ρ_{i}(v_{k}^{i}) (that is, either they are both undefined or they are both defined and coincide).

We denote this situation by σ = ρ^{ξ} and say that ξ is a renaming of variables for ρ (or simply ξ is a renaming of variables, if the ρ is not relevant). Also, we will abuse notation and write dom(ξ_{i}) = {k|ξ_{i}(k) ≠ k} for i = 0, 1; it follows that ξ_{i}(j) = j if j ∉ dom(ξ_{i}). The first condition then becomes simply dom(ξ_{i}) ⊆ dom(ρ_{i}).

Notice that the second condition totally defines σ, since each ξ_{i} is a permutation. For this reason, we will also use the notation σ = ρ^{ξ} as a definition of σ.

Another important consequence is that, if σ = ρ^{ξ}, then dom(σ_{i}) = dom(ρ_{i}) for i = 0, 1.

Proposition 3.13 The relation R(ρ, σ) defined as “σ is obtained from ρ by a renaming of variables” is an equivalence relation.

Proof.

• Reflexivity: just take ξ = ⟨(), ()⟩.

• Symmetry: suppose σ = ρ^{ξ} for some ξ; then, since each ξ_{i} is a bijection, trivially ρ = σ^{⟨ξ_{0}^{−1},ξ_{1}^{−1}⟩}.

• Transitivity: suppose σ = ρ^{ξ} and θ = σ^{ξ′}; then θ = ρ^{ξ′∘ξ} where ξ′ ∘ ξ denotes pointwise composition. In fact, for i = 0, 1, and for every k, θ_{i} (v_{ξ′∘ξ(k)}^{i}) ≃ σ_{i} (v_{ξ(k)}^{i}) ≃ ρ_{i}(v_{k}^{i}).

Finally, suppose that, for some k, v_{k}^{i} ∉ dom(ρ_{i}); then ξ_{i}(k) = k and, since dom(σ_{i}) = dom(ρ_{i}), also v_{k}^{i} ∉ dom(σ_{i}) and hence ξ′_{i} ∘ ξ_{i}(k) = ξ′_{i}(k) = k. But then ξ′_{i} ∘ ξ_{i}(k) ≠ k → v_{k}^{i} ∈ dom(ρ_{i}).

□

Definition 3.14 Let ξ be a renaming of variables and e, e′ : E. We say that e′ is obtained from e by ξ, denoted (e′) = e^{ξ}, if e′ is obtained from e by replacing each occurrence of v_{k}^{i} by v_{ξ_{i}(k)}^{i}, i = 0, 1.

Lemma 3.15 Let ρ be a substitution pair for A and ξ be a renaming of variables for ρ. For every t : A, if lift(t, ρ) = ⟨e, σ⟩ then lift(t, ρ^{ξ}) = ⟨e^{ξ}, σ^{ξ}⟩.

Proof. By induction on ≺_{A}.

1. t is minimal for ≺_{A}:

(a) t = \underline{n}: then e = n, σ = ρ, lift(t, ρ^{ξ}) = ⟨n, ρ^{ξ}⟩ and the conclusion trivially holds.

(b) otherwise, e = lift_{𝕍_{0}}(t, ρ) and we have to distinguish two cases. Suppose there is an i such that ρ_{0}(v_{i}^{0}) = t. Then e = v_{i}^{0} and σ = ρ; but by Definition 3.12 ρ_{0}^{ξ} (v_{ξ_{0}(i)}^{0}) = ρ_{0}(v_{i}^{0}), so lift(t, ρ^{ξ}) = ⟨v_{ξ_{0}(i)}^{0}, ρ^{ξ}⟩, and by definition v_{ξ_{0}(i)}^{0} = (v_{i}^{0})^{ξ}.

Otherwise, pick k minimal such that v_{k}^{0} ∉ dom(ρ_{0}). Then e = v_{k}^{0} and σ = ⟨ρ_{0} ∪ [v_{k}^{0} := t], ρ_{1}⟩. But then lift(t, ρ^{ξ}) = ⟨v_{k}^{0}, σ′⟩ with σ′ = ⟨ρ_{0}^{ξ} ∪ [v_{k}^{0} := t], ρ_{1}^{ξ}⟩: since dom(ρ_{0}) = dom(ρ_{0}^{ξ}) (see remark after Definition 3.12), k is also the minimal natural number satisfying v_{k}^{0} ∉ dom(ρ_{0}^{ξ}); furthermore, there can be no i such that ρ_{0}^{ξ}(v_{i}^{0}) = t because ρ_{0}^{ξ}(v_{i}^{0}) = ρ_{0}(v_{ξ_{0}^{−1}(i)}^{0}). But k ∉ dom(ξ_{0}), so v_{k}^{0} = v_{k}^{0}^{ξ} and σ′ = σ^{ξ}.

2. t = f(t′) with f : [A → A].

(a) f is −_{A}: then there is an expression e′ such that lift(t′, ρ) = ⟨e′, σ⟩ and e = −e′. By induction hypothesis, lift(t′, ρ^{ξ}) = ⟨(e′)^{ξ}, σ^{ξ}⟩ and hence lift(t, ρ^{ξ}) = ⟨e^{ξ}, σ^{ξ}⟩.

(b) f is ·^{n} with n closed: analogous.

(c) otherwise there exist an expression e′, an index i and a substitution pair θ such that lift(t′, ρ) = ⟨e′, θ⟩, lift_{𝕍_{1}}(f, θ) = ⟨v_{i}^{1}, σ⟩ and e = v_{i}^{1}(e′). By induction hypothesis, lift(t′, ρ^{ξ}) = ⟨(e′)^{ξ}, θ^{ξ}⟩. Suppose there is an k such that θ_{1}(v_{k}^{1}) = f. Then i = k and σ = θ; but by Definition 3.12 θ_{1}^{ξ} (v_{ξ_{1}(i)}^{1}) = θ_{1}(v_{i}^{1}) = f, so lift_{𝕍_{1}}(f, θ^{ξ}) = ⟨v_{ξ_{1}(i)}^{1}, θ^{ξ}⟩. Trivially v_{ξ_{1}(i)}^{1} = (v_{i}^{1})^{ξ};

since θ = σ, lift(t, ρ^{ξ}) = ⟨v_{i}^{1}(e′)^{ξ}, σ^{ξ}⟩, which establishes the result. Otherwise, i is the minimal k such that v_{k}^{1} ∉ dom(θ_{1}) and σ = ⟨θ_{0}, θ_{1} ∪ [v_{i}^{1} := f]⟩. But then lift_{𝕍_{1}}(f, θ^{ξ}) = ⟨v_{i}^{1}, σ′⟩ with σ′ = ⟨θ_{0}^{ξ}, θ_{1}^{ξ} ∪ [v_{i}^{1} := f]⟩: since dom(θ_{1}) = dom(θ_{1}^{ξ}) (second condition in Definition 3.12), i is also the minimal k satisfying v_{k}^{1} ∉ dom(θ_{1}^{ξ}); furthermore, there can be no k such that ρ_{1}^{ξ}(v_{k}^{1}) = f, since θ_{1}^{ξ}(v_{k}^{1}) = θ_{1}(v_{ξ_{1}^{−1}(k)}^{1}). But

then σ′ = σ^{ξ}; since i = ξ_{1}(i), we also have in this situation that lift(t, ρ^{ξ}) = ⟨v_{i}^{1}(e′)^{ξ}, σ^{ξ}⟩.

3. t = t_{1} ⋆ t_{2} with ⋆ ∈ {+, −, ×, /}: then there are expressions e_{1}, e_{2} and a substitution pair θ such that lift(t_{1}, ρ) = ⟨e_{1}, θ⟩, lift(t_{2}, θ) = ⟨e_{2}, σ⟩ and e = e_{1} ⋆ e_{2}.

By induction hypothesis lift(t_{1}, ρ^{ξ}) = ⟨e_{1}^{ξ}, θ^{ξ}⟩. But then the induction hypothesis applies again, and lift(t_{2}, θ^{ξ}) = ⟨e_{2}^{ξ}, σ^{ξ}⟩. Hence, lift(t_{1} ⋆ t_{2}, ρ^{ξ}) = ⟨(e_{1}^{ξ}) ⋆ (e_{2}^{ξ}), σ^{ξ}⟩ and trivially (e_{1}^{ξ}) ⋆ (e_{2}^{ξ}) = e^{ξ}.

□

We now prove some lemmas about the order in which terms are lifted.

Lemma 3.16 Let t : A, f : [A → A] and ρ be a substitution pair for A. Suppose lift_{𝕍_{0}}(t, ρ) = ⟨v_{i}^{0}, σ⟩ and lift_{𝕍_{1}}(f, ρ) = ⟨v_{j}^{1}, θ⟩. Then lift_{𝕍_{1}}(f, σ) = ⟨v_{j}^{1}, ⟨σ_{0}, θ_{1}⟩⟩ and lift_{𝕍_{0}}(t, θ) = ⟨v_{i}^{0}, ⟨σ_{0}, θ_{1}⟩⟩.

Proof. Let τ be an arbitrary substitution pair. From the definition of lift_{𝕍_{0}} (Definition 3.1), one sees that the result of lift_{𝕍_{0}}(u, τ) always has τ_{1} as the second component of the substitution pair in the output and the remaining values do not depend on τ_{1}. Therefore, σ = ⟨σ_{0}, ρ_{1}⟩.

Similarly, from the definition of lift_{𝕍_{1}} (Definition 3.4), one sees that τ_{0} is the first component of the substitution pair in the result of lift_{𝕍_{1}}(g, τ), the other values being independent of τ_{0}. Therefore, θ = ⟨ρ_{0}, θ_{1}⟩.

But then lift_{𝕍_{1}}(f, σ) = lift_{𝕍_{1}}(f, ⟨σ_{0}, ρ_{1}⟩) = ⟨v_{j}^{1}, ⟨σ_{0}, θ_{1}⟩ and lift_{𝕍_{0}}(t, θ) = lift_{𝕍_{0}}(t, ⟨ρ_{0}, θ_{1}⟩) = ⟨v_{i}^{0}, ⟨σ_{0}, θ_{1}⟩⟩. □

Lemma 3.17 Let t_{1}, t_{2} : A and ρ be a substitution pair for A. Suppose that

lift_{𝕍_{0}}(t_{1}, ρ) = ⟨v_{i}^{0}, σ⟩
lift_{𝕍_{0}}(t_{2}, σ) = ⟨v_{j}^{0}, θ⟩
lift_{𝕍_{0}}(t_{2}, ρ) = ⟨v_{j′}^{0}, σ′⟩
lift_{𝕍_{0}}(t_{1}, σ′) = ⟨v_{i′}^{0}, θ′⟩

Then there is a renaming of variables ξ for θ such that ξ_{1} = (), dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅, θ′ = θ^{ξ}, i′ = ξ_{0}(i) and j′ = ξ_{0}(j).

Proof. There are four cases to consider.

If t_{1} and t_{2} are (syntactically) equal, then ξ = ⟨(), ()⟩ trivially establishes the thesis: in this case j′ = i and σ′ = σ, whence i′ = j and θ′ = θ; furthermore, since we are in a special case of Lemma 3.10, also j = i and i′ = j′.

Let us now assume that t_{1} and t_{2} are different. Suppose first that there is a variable v_{k}^{0} such that ρ_{0}(v_{k}^{0}) = t_{1}; then i = k and again σ = ρ, from which we can deduce j′ = j and σ′ = σ. But from Lemma 3.2, ρ ⊆ σ, hence from Lemma 3.10 also i′ = i and θ′ = θ; therefore ξ can again be taken to be ⟨(), ()⟩.

A symmetric argument proves the case where there is a variable v_{k}^{0} such that ρ_{0}(v_{k}^{0}) = t_{2}. Finally, suppose that for no k either ρ_{0}(v_{k}^{0}) = t_{1} or ρ_{0}(v_{k}^{0}) = t_{2}. Then i is the minimal natural

number satisfying v_{i}^{0} ∉ dom(ρ_{0}) and σ = ⟨ρ_{0} ∪ [v_{i}^{0} := t_{1}], ρ_{1}⟩. By definition of ∪, there is still no k such that σ_{0}(v_{k}^{0}) = t_{2}, whence j is the least natural number such that v_{j}^{0} ∉ dom(σ_{0}) and θ = ⟨σ_{0} ∪ [v_{j}^{0} := t_{2}], σ_{1}⟩.

On the other hand, j′ is also the least natural satisfying v_{j′}^{0} ∉ dom(ρ_{0}), so j′ = i and σ′ = ⟨ρ_{0} ∪ [v_{i}^{0} := t_{2}], ρ_{1}⟩. Then dom(σ′_{0}) = dom(ρ_{0}) ∪ {i} = dom(σ_{0}), whence necessarily i′ = j and θ′ = ⟨σ′_{0} ∪ [v_{j}^{0} := t_{2}], σ′_{1}⟩. It then trivially follows that the renaming of variables ⟨(i j), ()⟩ satisfies all the desired conditions. □

Lemma 3.18 Let f_{1}, f_{2} : [A → A] and ρ be a substitution pair for A. Suppose that

lift_{𝕍_{1}}(f_{1}, ρ) = ⟨v_{i}^{1}, σ⟩
lift_{𝕍_{1}}(f_{2}, σ) = ⟨v_{j}^{1}, θ⟩
lift_{𝕍_{1}}(f_{2}, ρ) = ⟨v_{j′}^{1}, σ′⟩
lift_{𝕍_{1}}(f_{1}, σ′) = ⟨v_{i′}^{1}, θ′⟩

Then there is a renaming of variables ξ for θ such that ξ_{0} = (), dom(ξ_{1}) ∩ dom(ρ_{1}) = ∅, θ′ = θ^{ξ}, i′ = ξ_{1}(i) and j′ = ξ_{1}(j).

Proof. The proof is exactly analogous to that of Lemma 3.17, interchanging the indices 0 and 1 of the variables and substitutions. □

Lemma 3.19 Let t_{1}, t_{2} : A, e_{1}, e′_{1}, e_{2}, e′_{2} : E and ρ, σ, σ′, θ, θ′ be substitution pairs for A satisfying the following relations.

lift(t_{1}, ρ) = ⟨e_{1}, σ⟩
lift_{𝕍_{0}}(t_{2}, σ) = ⟨e_{2}, θ⟩
lift_{𝕍_{0}}(t_{2}, ρ) = ⟨e′_{2}, σ′⟩
lift(t_{1}, σ′) = ⟨e′_{1}, θ′⟩

Then there is a renaming of variables ξ for θ such that:

(i) ξ_{1} = () and dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅; (ii) θ′ = θ^{ξ} and e′_{i} = e_{i}^{ξ} for i = 1, 2.

Proof. By induction on t_{1} according to ≺_{A}.

1. t_{1} is minimal for ≺_{A}.

(a) t_{1} = \underline{n}: then e_{1} = n, σ = ρ whence trivially e′_{2} = e_{2}, σ′ = θ and also e′_{1} = e_{1} and θ′ = θ; thus ξ = ⟨(), ()⟩ trivially satisfies (i) and (ii).

(b) otherwise lift(t_{1}, ρ) = lift_{𝕍_{0}}(t_{1}, ρ) and Lemma 3.17 establishes the result.

2. t_{1} = f(t) with f : [A → A].

(a) f is −_{A}: then e_{1} = −e where ⟨e, σ⟩ = lift(t, ρ); similarly e′_{1} = −e′ where ⟨e′, θ′⟩ = lift(t, σ′). By induction hypothesis there is a renaming of variables ξ for θ such that ξ_{1} = (), dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅, θ′ = θ^{ξ}, e′ = e^{ξ} and e′_{2} = e_{2}^{ξ}. The only thing left to show is that e′_{1} = e_{1}^{ξ}; but this is trivial, since e_{1} = e and e′_{1} = −e′. Therefore ξ is the desired renaming of variables.

(b) f is ·^{n} with n is closed: analogous.

(c) otherwise e_{1} = v_{i}^{1}(e) with lift(t, ρ) = ⟨e, τ⟩ and lift_{𝕍_{1}}(f, τ) = ⟨v_{i}^{1}, σ⟩; also e′_{1} = v_{j}^{1}(e′) with lift(t, σ′) = ⟨e′, τ′⟩ and lift_{𝕍_{1}}(f, τ′) = ⟨v_{j}^{1}, θ′⟩. By Lemma 3.16, θ = ⟨θ_{0}, σ_{1}⟩ and lift_{𝕍_{0}}(t_{2}, τ) = ⟨e_{2}, ⟨θ_{0}, τ_{1}⟩⟩. By induction hypothesis, there is a renaming of variables ξ for ⟨θ_{0}, τ_{1}⟩ such that ξ_{1} = (), dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅, τ′ = ⟨θ_{0}, τ_{1}⟩^{ξ}, e′ = e^{ξ} and e′_{2} = e_{2}^{ξ}. It remains to show that e′_{1} = e_{1}^{ξ}; but τ′ = ⟨θ_{0}, τ_{1}⟩^{ξ} and ξ_{1} = () imply τ′_{1} = τ_{1}. Similar considerations as made in the proof of Lemma 3.16 make it clear that θ′_{1} = τ′_{1} and j = i. Hence the thesis follows.

3. t_{1} = u⋆v with ⋆ ∈ {+, −, ×, /}: then there are expressions e_{u} and e_{v} and a substitution pair τ such that lift(u, ρ) = ⟨e_{u}, τ⟩, lift(v, τ) = ⟨e_{v}, σ⟩ and e = e_{u} ⋆e_{v}. Also, there are expressions e′_{u} and e′_{v} and a substitution pair τ′ such that lift(u, σ′) = ⟨e′_{u}, τ′⟩, lift(v, τ′) = ⟨e′_{v}, θ′⟩ and e′ = e′_{u} ⋆ e′_{v}. Consider now lift_{𝕍_{0}}(t_{2}, τ) = ⟨e_{2}^{∗}, τ^{∗}⟩. By induction hypothesis, there is a renaming of variables ξ for τ^{∗} satisfying (i) such that e′_{2} = e_{2}^{∗}^{ξ}, e′_{u} = e_{u}^{ξ} and τ′ = τ^{∗}^{ξ}. Let now lift(v, τ^{∗}) = ⟨e_{v}^{∗}, θ^{∗}⟩. Induction hypothesis now implies that there is a renaming of variables ξ′ for θ such that ξ′_{1} = (), dom(ξ′_{0}) ∩ dom(τ_{0}) = ∅, e_{2}^{∗} = e_{2}^{ξ′}, e_{v}^{∗} = e_{v}^{ξ′} and θ^{∗} = θ^{ξ′} (see Figure 1).

\xymatrix{ & ρ \ar[dl]_{u} \ar[dr]^{t_{2}} \\ τ \ar[d]_{v} \ar[dr]^{t_{2}} &  & σ′ \ar[d]_{u} \\ σ \ar[d]_{t_{2}} & τ^{∗} \ar@{.>}[r]^{ξ} \ar[d]_{v} & τ′ \ar[d]_{v} \\ θ \ar@{.>}[r]^{ξ′} & θ^{∗} \ar@{.>}[r]^{ξ} & θ′}

Figure 1: Induction step on the proof of Lemma 3.19. An arrow from ρ to ρ′ with label t means that ρ′ is obtained by lift(t, ρ).

We now prove that ξ ∘ ξ′ is the desired renaming of variables.

• Trivially, ξ_{1} ∘ ξ′_{1} = (); since ρ ⊆ τ, if v_{k}^{0} ∈ dom(ρ_{0}) then ξ_{0}(k) = k and ξ′_{0}(k) = k, hence dom(ξ_{0} ∘ ξ′_{0}) ∩ dom(ρ_{0}) = ∅.

• By hypothesis, e′_{2} = e_{2}^{∗}^{ξ} and e_{2}^{∗} = e_{2}^{ξ′}, whence e′_{2} = e_{2}^{ξ∘ξ′}.

• By Lemma 3.15, lift(v, τ′) = lift(v, (τ^{∗})^{ξ}) = ⟨(e_{v}^{∗})^{ξ}, (θ^{∗})^{ξ}⟩, which is ⟨(e_{v}^{ξ′})^{ξ}, (θ^{ξ′})^{ξ}⟩. In other words, lift(v, τ′) = ⟨e_{v}^{ξ∘ξ′}, θ^{ξ∘ξ′}⟩. Also, dom(ξ′_{0}) ∩ dom(τ_{0}) = ∅, hence no variable occurring in e_{u} is in the domain of ξ_{0} by Lemma 3.11. Therefore, e′_{u} = e_{u}^{ξ} = (e_{u}^{ξ′})^{ξ} = e_{u}^{ξ∘ξ′}, whence e′ = e^{ξ∘ξ′}.

Thus ξ ∘ ξ′ is the desired renaming of variables.

□

Lemma 3.20 Let t : A, f : [A → A], e, e′ : E, i, i′ : ℕ and ρ, σ, σ′, θ, θ′ be substitution pairs for A satisfying the following relations.

lift(t, ρ) = ⟨e, σ⟩
lift_{𝕍_{1}}(f, σ) = ⟨v_{i}^{1}, θ⟩
lift_{𝕍_{1}}(f, ρ) = ⟨v_{i′}^{1}, σ′⟩
lift(t, σ′) = ⟨e′, θ′⟩

Then there is a renaming of variables ξ for θ such that:

(i) ξ_{0} = () and dom(ξ_{1}) ∩ dom(ρ_{1}) = ∅;

(ii) θ′ = θ^{ξ}, e′ = e^{ξ} and i′ = ξ_{1}(i).

Proof. By induction on t according to ≺_{A}.

1. t is minimal for ≺_{A}.

(a) t = \underline{n}: then e = n, σ = ρ whence trivially i′ = i, σ′ = θ and also e′ = e and θ′ = θ; thus ξ = ⟨(), ()⟩ trivially satisfies (i) and (ii).

(b) otherwise lift(t, ρ) = lift_{𝕍_{0}}(t, ρ). By Lemma 3.16, ⟨(), ()⟩ also satisfies both (i) and (ii).

2. t = g(t_{0}) with g : [A → A].

(a) g is −_{A}: again analogous to the corresponding case in the proof of Lemma 3.19.

(b) g is ·^{n} with n is closed: analogous.

(c) otherwise e = v_{j}^{1}(e_{0}) with lift(t_{0}, ρ) = ⟨e_{0}, τ⟩ and lift_{𝕍_{1}}(g, τ) = ⟨v_{j}^{1}, σ⟩; also e′ = v_{j′}^{1}(e′_{0}) with lift(t, σ′) = ⟨e′_{0}, τ′⟩ and lift_{𝕍_{1}}(g, τ′) = ⟨v_{j′}^{1}, θ′⟩.

3. t_{1} = u⋆v with ⋆ ∈ {+, −, ×, /}: then there are expressions e_{u} and e_{v} and a substitution pair τ such that lift(u, ρ) = ⟨e_{u}, τ⟩, lift(v, τ) = ⟨e_{v}, σ⟩ and e = e_{u} ⋆e_{v}. Also, there are expressions e′_{u} and e′_{v} and a substitution pair τ′ such that lift(u, σ′) = ⟨e′_{u}, τ′⟩, lift(v, τ′) = ⟨e′_{v}, θ′⟩ and e′ = e′_{u} ⋆ e′_{v}.

If we define lift_{𝕍_{1}}(f, τ) = ⟨v_{i^{∗}}^{1}, τ^{∗}⟩ and lift_{𝕍_{1}}(g, τ^{∗}) = ⟨v_{j^{∗}}^{1}, θ^{∗}⟩, we can draw the picture on Figure 2. Again, by induction hypothesis, there is a renaming of variables ξ for τ^{∗} satisfying (i) such that i′ = ξ_{1}(i^{∗}), e′_{0} = e_{0}^{ξ} and τ′ = τ^{∗}^{ξ}. By Lemma 3.18, there is a renaming of variables ξ′ for θ such that ξ′_{0} = (), dom(ξ′_{1}) ∩ dom(τ_{1}) = ∅, i^{∗} = ξ′_{1}(i), j^{∗} = ξ′_{1}(j) and θ^{∗} = θ^{ξ′}.

Once again, ξ ∘ ξ′ is the desired renaming of variables.

• Trivially, ξ_{0} ∘ ξ′_{0} = (); since ρ ⊆ τ, if v_{k}^{1} ∈ dom(ρ_{1}) then ξ_{1}(k) = k and ξ′_{1}(k) = k, hence dom(ξ_{1} ∘ ξ′_{1}) ∩ dom(ρ_{1}) = ∅.

\xymatrix{ & ρ \ar[dl]_{t_{0}} \ar[dr]^{f} \\ τ \ar[d]_{g} \ar[dr]^{f} &  & σ′ \ar[d]_{t_{0}} \\ σ \ar[d]_{f} & τ^{∗} \ar@{.>}[r]^{ξ} \ar[d]_{g} & τ′ \ar[d]_{g} \\ θ \ar@{.>}[r]^{ξ′} & θ^{∗} \ar@{.>}[r]^{ξ} & θ′}

Figure 2: Last case of the proof of Lemma 3.20. An arrow from ρ to ρ′ with label t means that ρ′ is obtained by either lift(t, ρ) or lift_{𝕍_{1}}(t, ρ).

• By hypothesis, i′ = ξ_{1}(i^{∗}) and i^{∗} = ξ′(i), whence i′ = ξ ∘ ξ′(i).

• lift(g(t_{0}), τ^{∗}) = ⟨v_{j^{∗}}^{1}(e_{0}), θ^{∗}⟩: since τ ⊆ τ^{∗} by Lemma 3.5, lift(t_{0}, τ^{∗}) = ⟨e_{0}, τ^{∗}⟩ due to Lemma 3.10; the rest follows by definition of lift_{𝕍_{1}}(g, τ^{∗}). Similar considerations show that lift(g(t_{0}), τ′) = ⟨v_{j′}^{1}(e′_{0}), θ′⟩.

By Lemma 3.15, lift(g(t_{0}), τ′) = lift(g(e_{0}), τ^{∗}^{ξ}) = ⟨v_{j^{∗}}^{1}(e_{0})^{ξ}, θ^{∗}^{ξ}⟩; hence θ′ = θ^{∗}^{ξ} and v_{j′}^{1}(e′_{0}) = v_{j^{∗}}^{1}(e_{0})^{ξ}.

From θ′ = θ^{∗}^{ξ} and θ^{∗} = θ^{ξ′} we can deduce that θ′ = θ^{ξ∘ξ′}.

Finally we show that v_{j′}^{1}(e′_{0}) = v_{j}^{1}(e_{0})^{ξ∘ξ′}. Obviously, v_{j}^{1}(e_{0})^{ξ∘ξ′} = v_{ξ∘ξ′(j)}^{1}(e_{0}^{ξ∘ξ′}). From

v_{j′}^{1}(e′_{0}) = v_{j^{∗}}^{1}(e_{0})^{ξ} we get first that j′ = ξ_{1}(j^{∗}), and since j^{∗} = ξ′_{1}(j) we conclude that ξ_{1} ∘ ξ′_{1}(j) = j′. Also e′_{0} = e_{0}^{ξ}; since dom(ξ′_{0}) ∩ dom(τ_{0}) = ∅, no variable occurring in e_{0} is in the domain of ξ′_{0} by Lemma 3.11. Therefore, e′_{0} = e_{0}^{ξ} = (e_{0}^{ξ′})^{ξ} = e_{0}^{ξ∘ξ′}.

Thus ξ ∘ ξ′ is the desired renaming of variables.

□

Lemma 3.21 Let t_{1}, t_{2} : A, e_{1}, e′_{1}, e_{2}, e′_{2} : E and ρ, σ, σ′, θ, θ′ be substitution pairs for A satisfying the following relations.

lift(t_{1}, ρ) = ⟨e_{1}, σ⟩
lift(t_{2}, σ) = ⟨e_{2}, θ⟩
lift(t_{2}, ρ) = ⟨e′_{2}, σ′⟩
lift(t_{1}, σ′) = ⟨e′_{1}, θ′⟩

Then there is a renaming of variables ξ for θ such that:

(i) dom(ξ_{i}) ∩ dom(ρ_{i}) = ∅ for i = 1, 2;

(ii) θ′ = θ^{ξ} and e′_{i} = e_{i}^{ξ} for i = 1, 2.

Proof. By induction on t_{1} with respect to ≺_{A}; most cases can be dealt with as in the proof of Lemma 3.19. First, notice that the only steps where use was made of the fact that e_{2} was obtained from t_{2} by lift_{𝕍_{0}} were the cases where t_{1} was minimal for ≺_{A} and not of the form \underline{n} or t_{1} = f(t). In all other cases, proving that dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅ made use only of the induction hypothesis, so that replacing 0 by 1 in that subproof yields a valid proof of dom(ξ_{1}) ∩ dom(ρ_{1}) = ∅ from the induction hypothesis. Therefore, we only need to consider those two cases.

If t_{1} is minimal for ≺_{A} and not of the form \underline{n}, then lift(t_{1}, ρ) = lift_{𝕍_{0}}(t_{1}, ρ) and lift(t_{1}, σ′) = lift_{𝕍_{0}}(t_{1}, σ′). Lemma 3.19 then allows us to conclude that there is a renaming of variables ξ for θ′ such that ξ_{1} = (), dom(ξ_{0}) ∩ dom(ρ_{0}) = ∅ and θ = θ′^{ξ} and e_{i} = e′_{i}^{ξ} for i = 1, 2. Then ξ^{−1} satisfies our requirements: since ξ_{0} is a permutation, dom(ξ_{0}^{−1}) = dom(ξ_{0}) and therefore dom(ξ_{0}^{−1}) ∩ dom(ρ_{0}) = ∅; dom(()) = ∅, hence dom(ξ_{0}^{−1}) ∩ dom(ρ_{0}) = ∅; θ′ = θ^{ξ^{−1}} follows from the second case in the proof of Lemma 3.13; and e′_{i} = e_{i}^{ξ^{−1}} follows from the definition of inverse.

If t_{1} = f(t), then there are expressions e, e′, natural numbers i, i′ and substitution pairs τ, τ′ such that lift(t, ρ) = ⟨e, τ⟩, lift_{𝕍_{1}}(f, τ) = ⟨v_{i}^{1}, σ⟩, e_{1} = v_{i}^{1}(e), lift(t, σ′) = ⟨e′, τ′⟩, lift_{𝕍_{1}}(f, τ′) = ⟨v_{i′}^{1}, θ⟩ and e′_{1} = v_{i′}^{1}(e′).

We once again let lift(t_{2}, τ) = ⟨e_{2}^{∗}, τ^{∗}⟩ and lift_{𝕍_{1}}(f, τ^{∗}) = ⟨v_{i^{∗}}^{1}, θ^{∗}⟩ (see Figure 3). By induction

\xymatrix{ & ρ \ar[dl]_{t} \ar[dr]^{t_{2}} \\ τ \ar[d]_{f} \ar[dr]^{t_{2}} &  & σ′ \ar[d]_{t} \\ σ \ar[d]_{t_{2}} & τ^{∗} \ar@{.>}[r]^{ξ} \ar[d]_{f} & τ′ \ar[d]_{f} \\ θ \ar@{.>}[r]^{ξ′} & θ^{∗} \ar@{.>}[r]^{ξ} & θ′}

Figure 3: Last case of the proof of Lemma 3.21. An arrow from ρ to ρ′ with label t means that ρ′ is obtained by either lift(t, ρ) or lift_{𝕍_{1}}(t, ρ).

hypothesis there is a renaming of variables ξ for τ^{∗} such that (i) holds, τ′ = τ^{∗}^{ξ}, e′ = e^{ξ} and e′_{2} = e_{2}^{ξ}. By Lemma 3.20 there is a renaming of variables ξ′ for θ such that ξ′_{0} = (), dom(ξ′_{1}) ∩ dom(τ_{1}) = ∅, θ^{∗} = θ^{ξ′}, e_{2}^{∗} = e_{2}^{ξ′} and i^{∗} = ξ′_{1}(i).

In a similar way to the proof of the last case of Lemma 3.20, we can conclude that θ′ = θ^{ξ∘ξ′}, i′ = ξ_{1}(i^{∗}) and e′ = e^{ξ∘ξ′}. Then trivially v_{i′}^{1}(e′) = v_{i}^{1}(e)^{ξ∘ξ′}. Finally, if v_{k}^{i} ∈ dom(ρ_{i}), then v_{k}^{i} ∈ dom(τ_{i}), hence ξ′_{i}(k) = k, ξ_{i} ∘ ξ′_{i}(k) = ξ(k) = k and dom(ξ_{i}) ∩ dom(ρ_{i}) = ∅. □

Lemma 3.22 Let t_{1}, t_{2}, t_{3} : A, e_{1}, e_{2}, e′_{2}, e_{3}, e′_{3} : E and ρ, σ, σ′, θ, θ′ be substitution pairs for A satisfying the following relations.

lift(t_{2}, ∅) = ⟨e_{2}, σ⟩
lift(t_{3}, σ) = ⟨e_{3}, θ⟩
lift(t_{1}, ∅) = ⟨e_{1}, ρ⟩
lift(t_{2}, ρ) = ⟨e′_{2}, σ′⟩
lift(t_{3}, σ′) = ⟨e′_{3}, θ′⟩

Then there exist a substitution pair τ and a renaming of variables ξ for τ such that:

(i) θ ⊆ τ;

(ii) θ′ = τ^{ξ} and e′_{i} = e_{i}^{ξ} for i = 2, 3.

Proof. Define lift(t_{1}, σ) = ⟨e_{1}^{∗}, ρ^{∗}⟩. By Lemma 3.21, there is a renaming of variables ξ for τ^{∗} such that σ′ = ρ^{∗}^{ξ}, e_{1} = e_{1}^{∗}^{ξ} and e′_{2} = e_{2}^{ξ}.

Define lift(t_{3}, ρ^{∗}) = ⟨e_{3}^{∗}, θ^{∗}⟩. Then, by Lemma 3.15, e′_{3} = e_{3}^{∗}^{ξ} and θ′ = θ^{∗}^{ξ}.

Now take lift(t_{1}, θ) = ⟨e′_{1}, τ⟩. By Lemma 3.21 there is a renaming of variables ξ′ for τ such that also e_{3}^{∗} = e_{3}^{ξ′} and θ^{∗} = τ^{ξ′}.

It then follows that ξ ∘ ξ′ is the desired renaming of variables.

The situation is graphically depicted in Figure 4. □

\xymatrix{ & ∅ \ar[dl]_{t_{2}} \ar[dr]^{t_{1}} \\ σ \ar[d]_{t_{3}} \ar[dr]^{t_{1}} &  & ρ \ar[d]_{t_{2}} \\ θ \ar[d]_{t_{1}} & ρ^{∗} \ar@{.>}[r]^{ξ} \ar[d]_{t_{3}} & σ′ \ar[d]_{t_{3}} \\ τ \ar@{.>}[r]^{ξ′} & θ^{∗} \ar@{.>}[r]^{ξ} & θ′}

Figure 4: Proof of Lemma 3.22. An arrow from ρ to ρ′ with label t means that ρ′ is obtained by lift(t, ρ).

4 Completeness of rational: rings

We now move to the Coq portion of the tactic. We identify a subset of the set of expressions which we call normal forms. Then we define a normalization function N that assigns to any expression e an expression N (e) in normal form. In this section we prove the fundamental properties of this function.

In this first stage we will forget about division and work only with the subset of expressions interpretable in a ring. Section 6 discusses how these definitions can be generalized for fields and how the results we show here can be transposed to the general case.

4.1 Normal forms

The intuition for the normal forms is as follows. A normal form is a polynomial where all terms have been multiplied, so that it is written as a sum of products of atomic terms (integers, variables of arity 0 or variables of arity 1 applied to a normal form). To guarantee uniqueness of the normal form we further require that these terms be ordered.

We begin by defining monomials and polynomials. These can be seen in a precise way as lists of expressions; hence we can identify the subset of monomials and polynomials whose lists are ordered. These will be our normal forms.

Definition 4.1 The sets of monomials and polynomials are inductively defined by the following grammar:

M′ ::= ℤ | 𝕍_{0} × M′ | 𝕍_{1}(P′) × M′
P′ ::= ℤ | M′ + P′

Notice that M′ ⊆ E and P′ ⊆ E.

Definition 4.2 For every m : M′ we define:

1. the list of variables of m, |m|;

2. the coefficient of m, ∥m∥.

\begin{matrix}| · | : M′ & → & list(E) & ∥ · ∥ : M′ & → & ℤ \\ i & ↦ & [] & i & ↦ & i \\ v_{i}^{0} × m & ↦ & v_{i}^{0} :: m & v_{i}^{0} × m & ↦ & ∥m∥ \\ v_{i}^{1}(p′) × m & ↦ & v_{i}^{1}(p′) :: m & v_{i}^{1}(p′) × m & ↦ & ∥m∥ \end{matrix}

Definition 4.3 For every p : P′ we define the list of monomials of p as follows:

| · | : P′ → list(list(E))
i ↦ []
m + p ↦ |m| :: |p|

Definition 4.4 We define the following mutually recursive predicates over M′ and P′.

(i) ord_{M′}(m) holds if |m| is an ordered list (with the ordering from Definition 2.17).

(ii) ord_{P′}(p) holds if |p| is ordered (using the lexicographic ordering for each element of |p|) and |p| does not contain repetitions.

(iii) wf_{M′} is defined recursively as follows:

• wf_{M′}(i) holds for i ≠ 0;

• wf_{M′}(v_{i}^{0} × m) ⟺ wf_{M′}(m);

• wf_{M′}(v_{i}^{1}(p) × m) ⟺ (wf_{M′}(m) ∧ nf_{P′}(p)).

(iv) nf_{M′}(m) holds if either m = 0 or wf_{M′}(m) ∧ ord_{M′}(m) holds.

(v) wf_{P′} is defined recursively as follows:

• wf_{P′}(i) holds for i ∈ ℤ;

• wf_{P′}(m + p) ⟺ (wf_{P′}(p) ∧ nf_{M′}(m)).

(vi) nf_{P′}(p) holds iff wf_{P′}(p) ∧ ord_{P′}(p) holds.

Definition 4.5 The set M of monomials in normal form is defined as

M = {m : M′ | nf_{M′}(m)}.

The set P of polynomials in normal form, or simply of normal forms, is defined as

P = {p : P′ | nf_{P′}(p)}.

We will use the definitions of ∥m∥, |m| and |p| above also for monomials and polynomials in normal form.

Definition 4.6 Let m : M and p : P. The coefficient of m in p, denoted by ∥p∥_{m}, is recursively defined as follows.

∥ · ∥ : P × M → ℤ
i, j ↦ i
i, m ↦ 0
m′ + p, m ↦ \{ \begin{matrix}∥m′∥ & if |m′| = |m| \\ ∥p∥_{m} & else \end{matrix}

The first clause in this definition may look somewhat strange; the idea is that we only look at |m| to define ∥p∥_{m}, and thus any integer should correspond to the independent term of p.

The reason for introducing the operations | · | and ∥ · ∥ is that they totally characterize normal forms.

Lemma 4.7 Let m, m′ : M. Then m = m′ ⟺ ∥m∥ = ∥m′∥ ∧ |m| = |m′|.

Proof. Straightforward. The direct implication is immediate, since both |·| and ∥·∥ are functions. For the converse, assume that |m| = |m′|. Then m and m′ share the same variables (counting repetitions); since they are ordered, these must appear in exactly the same order. If we also assume that ∥m∥ = ∥m′∥, then their integer coefficient is also the same, whence m = m′. □

Lemma 4.8 Let p, q : P. Then p = q ⟺ ∀m : M.∥m∥_{p} = ∥m∥_{q}.

Proof. The direct implication is again immediate, since ∥ · ∥ is a function. For the converse, assume that ∥m∥_{p} = ∥m∥_{q} for all m; then every monomial occurring in p also occurs in q with the same coefficient, and reciprocally. But |p| and |q| are both ordered, hence p = q. □

4.2 The normalization function

The normalization function is not defined directly, but by means of a number of auxiliary functions. This makes it easier to state and prove results about it.

Definition 4.9 ·_{Mℤ} is defined by:

·_{Mℤ} : M × ℤ → M
m, 0 ↦ 0
i, j ↦ i × j
x × m, j ↦ x × (m ·_{Mℤ} j)

Proposition 4.10 ·_{Mℤ} satisfies the following properties:

(i) ∥m ·_{Mℤ} i∥ = ∥m∥ × i;

(ii) |m ·_{Mℤ} 0| = [];

(iii) |m ·_{Mℤ} i| = |m| for i ≠ 0;

(iv) ·_{Mℤ} is well defined, i.e. its output is in M;

(v) if m ][_{ρ} t, then m ·_{Mℤ} i ][_{ρ} t × i.

Proof. The first two properties follow directly from the definition; for the third, just notice that, if i ≠ 0, then ×_{Mℤ} translates to the identity on the list of variables of m. From these three properties, the fourth then follows: if i = 0, then this is a consequence of 0 : M; else only the coefficient of m changes, hence nf_{M′}(m ·_{Mℤ} i) still holds. The last property is proved by straightforward induction (Coq checked). □

Definition 4.11 ·_{M𝕍} is defined by:

·_{M𝕍} : M × (𝕍_{0} ∪ 𝕍_{1}(P)) → M
i, y ↦ (y × 1) ·_{Mℤ} i
x × m, y ↦ \{ \begin{matrix}x × (m ·_{M𝕍} y) & x <_{E} y \\ y × x × m & otherwise \end{matrix}

Proposition 4.12 ·_{M𝕍} satisfies the following properties:

(i) ∥m ·_{M𝕍} x∥ = ∥m∥; (ii) if m ≠ 0, then |m ·_{M𝕍} x| is the sorted list obtained from m and x;

(iii) ·_{M𝕍} is well defined;

(iv) if m ][_{ρ} t and x ][_{ρ} t′, then m ·_{M𝕍} x ][_{ρ} t × t′.

Proof. If m = 0 these properties follow from Proposition 4.10, so assume m ≠ 0. The first property follows directly from the definition; for the second, just notice that ·_{M𝕍} translates to the algorithm of straight insertion on lists. From these two properties, the third then follows: the elements of |m| are not changed by ·_{M𝕍} and x is either v_{i}^{0} or v_{i}^{1}(p) with p : P, hence m ·_{M𝕍} x satisfies wf_{M′}. Also the correctness of straight insertion guarantees that |m ·_{M𝕍} x| is sorted if m is. The last property is again proved by straightforward induction using Proposition 4.10 (Coq checked). □

Definition 4.13 ·_{MM} is defined by:

·_{MM} : M × M → M
i, m ↦ m ·_{Mℤ} i
x × m, m′ ↦ (m ·_{MM} m′) ·_{M𝕍} x

Proposition 4.14 ·_{MM} satisfies the following properties:

(i) ∥m ·_{MM} m′∥ = ∥m∥ × ∥m′∥;

(ii) if m, m′ ≠ 0, then |m ·_{MM} m′| is the sorted list obtained by merging |m| with |m′|;

(iii) ·_{MM} is well defined;

(iv) if m ][_{ρ} t and m′ ][_{ρ} t′, then m ·_{MM} m′ ][_{ρ} t × t′.

Proof. The first property again follows directly from the definition of ·_{MM} and Propositions 4.10 and 4.12. The second holds because ·_{MM} simply implements straight insertion sort on the list obtained by appending |m| to |m′|. From these two the third property follows, and the last one is again proved by straightforward induction using Propositions 4.10 and 4.12 (Coq checked). □

The next function is of a different nature: it takes two monomials m and m′ that coincide as lists (that is, |m| = |m′|) and returns the monomial obtained by adding them. Obviously this is only well defined under the assumption that |m| = |m′|.

Definition 4.15 Let Δ_{M} denote the subset of M × M defined by

Δ_{M} = {⟨m, m′⟩ ∈ M × M | |m| = |m′|}.

+_{MM} is defined as follows.

+_{MM} : Δ_{M} → M
i, j ↦ i + j
x × m, x × m′ ↦ (m +_{MM} m′) ·_{M𝕍} x

Notice that this definition covers all cases because of the structure of Δ_{M}.

Proposition 4.16 +_{MM} satisfies the following properties:

(i) ∥m +_{MM} m′∥ = ∥m∥ + ∥m′∥;

(ii) m +_{MM} m′ = 0 if ∥m∥ + ∥m′∥ = 0;

(iii) |m +_{MM} m′| = |m| = |m′| otherwise; (iv) +_{MM} is well defined;

(v) if m ][_{ρ} t and m′ ][_{ρ} t′, then m +_{MM} m′ ][_{ρ} t + t′.

Proof. The first condition is straightforward from the definition of +_{MM}. The second and third follow from this definition and Proposition 4.12; and from these the fourth is a direct consequence. Finally the last point is again proved by induction using Proposition 4.12 (Coq checked). □

In the sequence we will need the following notations. We will denote by <_{M} the lexicographic ordering on list(E) obtained from <_{E}. Given two lists l, w of expressions, we write l ⊆ w to mean that l is a sublist of w, i.e. all elements of l occur in w and in the same order.

Definition 4.17 +_{PM} is defined as follows.

+_{PM} : P × M → P
i, j ↦ i + j
i, m ↦ m + i
m + p, j ↦ m + (p +_{PM} j)
m + p, m′ ↦ \{ \begin{matrix}m + (p +_{PM} m′) & |m| <_{M} |m′| \\ p +_{PM} (m +_{MM} m′) & |m| = |m′| \\ m′ + m + p & else \end{matrix}

Proposition 4.18 +_{PM} satisfies the following properties:

(i) if |m| = |m′|, then ∥p +_{PM} m∥_{m′} = ∥p∥_{m′} + ∥m∥;

(ii) if |m| ≠ |m′|, then ∥p +_{PM} m∥_{m′} = ∥p∥_{m′};

(iii) |p +_{PM} m| ⊆ l, where l is the list obtained by appending |m| to |p| and sorting the result;

(iv) +_{PM} is well defined;

(v) if p ][_{ρ} t and m′ ][_{ρ} t′, then p +_{PM} m′ ][_{ρ} t + t′.

Proof. The two first properties follow from the definition of +_{PM} (in the first case also appealing to Proposition 4.16).

The third property is proved by induction. The basis is trivial; for the induction step we need to consider two cases. Let p = m′ + p′; if |m| ≠ |m′|, then the algorithm reduces again to straight insertion of an element in a list (since the only difference is in the case |m| = |m′|). If |m| = |m′|, then |m′ +_{MM} m| = |m| by Proposition 4.16, so we can use the induction hypothesis to conclude that this call returns a q such that |q| is the straight insertion of |m′| in |p′|, which is |m′| :: |p′| (since m′ + p : P), and this is a sublist of |m| :: |m| :: |p′|, which would be the outcome of the straight insertion of |m| in |m′| :: |p′| (since |m| = |m′|). Hence also in this case the thesis holds.

The fourth property is a consequence of the previous ones, since a sublist of an ordered list is ordered. The last property is proved by induction (Coq checked). □

Definition 4.19 +_{PP} is defined as follows.

+_{PP} : P × P → P
i, q ↦ q +_{PM} i
m + p, q ↦ (p +_{PP} q) +_{PM} m

Proposition 4.20 +_{PP} satisfies the following properties:

(i) for all m, ∥p +_{PP} q∥_{m} = ∥p∥_{m} + ∥q∥_{m}; (ii) |p +_{PP} q| ⊆ l, where l is the list obtained by appending |q| to |p| and sorting the result;

(iii) +_{PP} is well defined;

(iv) if p ][_{ρ} t and q ][_{ρ} t′, then p +_{PP} q ][_{ρ} t + t′.

Proof. The first property is proved by induction on p. If p = i, then either m = j for some j ∈ ℤ and the thesis holds by the first part of Proposition 4.18 or else |m| ≠ |i| and the thesis holds by the second part of Proposition 4.18. If p = m′ + p′, then by induction hypothesis ∥p′ +_{PP} q∥_{m} = ∥p′∥_{m} + ∥q∥_{m} and there are two cases. If |m′| = |m|, then ∥p∥_{m} = ∥m′∥ and ∥p′∥_{m} = 0 (since |p| does not have repetitions), and by the first part of Proposition 4.18 ∥(p′ +_{PP} q) +_{PM} m′∥_{m} = ∥p′ +_{PP} q∥_{m} + ∥m′∥ = ∥p′∥_{m} + ∥q∥_{m} + ∥m′∥ = ∥q∥_{m} + ∥m′∥ = ∥q∥_{m} + ∥p∥_{m}. If |m′| ≠ |m| then ∥p∥_{m} = ∥p′∥_{m} and by the second part of Proposition 4.18 ∥(p′ +_{PP} q)+_{PM} m′∥_{m} = ∥p′∥_{m} + ∥q∥_{m} = ∥p∥_{m} + ∥q∥_{m}.

The second and third properties are proved from Proposition 4.18 by straightforward induction. The last property is similar (Coq checked). □

The last operations have no analogue in sorting algorithms. We will use juxtaposition to denote the sorted merge of two lists.

Definition 4.21 ·_{PM} is defined as follows.

·_{PM} : P × M → P
i, m′ ↦ 0 +_{PM} (m′ ·_{Mℤ} i)
m + p, m′ ↦ (p ·_{PM} m′) +_{PM} (m ·_{MM} m′)

Proposition 4.22 ·_{PM} satisfies the following properties:

(i) for all m, ∥p ·_{PM} m′∥_{m} = ∥p∥_{m^{∗}} × ∥m′∥ if there is^{1} an m^{∗} such that |m| = |m^{∗}||m′| and 0 otherwise;

(ii) p ·_{PM} 0 = 0;

(iii) if m′ ≠ 0, then |p ·_{PM} m′| is the sorted list whose elements are obtained by appending |m′| to each element of p and sorting the result;

(iv) ·_{PM} is well defined;

(v) if p ][_{ρ} t and m′ ][_{ρ} t′, then p ·_{PM} m′ ][_{ρ} t × t′.

Proof. The first property is a straightforward induction on p using Propositions 4.18 and 4.14 (notice that ·_{Mℤ} is a special case of ·_{MM}). The second property can be proved directly by induction, since 0 ·_{MM} 0 = 0 and 0 +_{PM} 0.

The third property is also proved by induction on p. If p = i then the result follows from Propositions 4.10 and 4.18. If p = m+p′, then (m+p′)·_{PM} m′ = (p·_{PM} m′)+_{PM} (m·_{MM} m′). Since |p′| does not have any repeated elements, by induction hypothesis neither does |p ·_{PM} m′| (since its elements are the image of the elements of |p| via an injective function). By Proposition 4.14, |m ·_{MM} m′| is the sorted list whose elements are either in |m| or in |m′|, and this does not occur in |p ·_{PM} m′|. Hence the thesis follows from Proposition 4.18.

The fourth property is straightforward since ·_{MM} and +_{PM} are both well defined. The last one is again proved by induction on p (Coq checked). □

Definition 4.23 ·_{PP} is defined as follows.

·_{PP} : P × P → P
i, q ↦ q ·_{PM} i
m + p, q ↦ (q ·_{PM} m) +_{PP} (p ·_{PP} q)

1Notice that there may exist at most one such m^{∗}.

Proposition 4.24 ·_{PP} satisfies the following properties:

(i) for all m ∈ M, ∥p ·_{PP} q∥_{m} = ∑ ∥p∥_{m_{1}}∥q∥_{m_{2}}, where the sum ranges over all m_{1} ∈ |p| ∪ {1} and m_{2} ∈ |q| ∪ {1} for which |m| = |m_{1}||m_{2}|;

(ii) ·_{PP} is well defined;

(iii) if p ][_{ρ} t and q ][_{ρ} t′, then p ·_{PP} q ][_{ρ} t × t′.

Proof. We prove the first property by induction. If p = i then the result follows from Proposition 4.22, since then m_{1} can only be 1 (|p| is the empty list). If p = m′+p′, then by Proposition 4.20 ∥(q ·_{PM} m′) +_{PP} (p′ ·_{PP} q)∥_{m} = ∥q ·_{PM} m′∥_{m} + ∥p′ ·_{PP} q∥_{m}; the result now follows from induction hypothesis and Proposition 4.22.

The second property is trivial; the last is proved by induction (Coq checked). □

Definition 4.25 The normalization function N is defined as follows, where E^{∗} denotes the type of expressions that do not use division.

N : E^{∗} → P
i ↦ i
v_{i}^{0} ↦ v_{i}^{0} × 1 + 0
e + f ↦ N (e) +_{PP} N (f)
e × f ↦ N (e) ·_{PP} N (f)
v_{i}^{1}(e) ↦ v_{i}^{1}(N (e)) × 1 + 0

Proposition 4.26 N satisfies the following properties:

(i) N is well defined;

(ii) if e ][_{ρ} t then N (e) ][_{ρ} t.

Proof. The first part is a straightforward induction. N (i) and N (v_{i}^{0}) are in normal form by definition of P; N (e + f) and N (e × f) are in normal form by induction hypothesis and Propositions 4.20 and 4.24; and N (v_{i}^{1}(e)) is in normal form by definition of P and induction hypothesis.

The second property is a straightforward induction (Coq checked). □

Corollary 4.27 Let t, t′ : A and define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). If N (e) = N (e′), then t =_{A} t′ can be proved from the ring axioms and unfolding of the definitions of −, zring and nexp.

Proof. Let e and e′ be as defined above and suppose that N (e) = N (e′). By Lemma 3.9, both e ][_{ρ} t and e′ ][_{ρ} t′. By Proposition 4.26 also N (e) ][_{ρ} t and N (e′) ][_{ρ} t′. Since N (e) = N (e′), we have that N (e) ][_{ρ} t and N (e) ][_{ρ} t′, whence t =_{A} t′ by Lemma 2.32. □

4.3 Properties of P and N

We now show that ⟨P, +_{PP}, 0, ·_{PP}, 1⟩ is a ring (w.r.t. syntactic equality). This will be essential later on, where we will use the properties of these operations without comment.

Lemma 4.28 For all m, m′ : M, m ·_{MM} m′ = m′ ·_{MM} m.

Proof. By Lemma 4.7, it is sufficient to show that ∥m ·_{MM} m′∥ = ∥m′ ·_{MM} m∥ and |m ·_{MM} m′| = |m′ ·_{MM} m|. But both of these are consequences of Proposition 4.14, commutativity of addition and uniqueness of sort. □

Lemma 4.29 Let p, q, r : P. Then the following hold:

(i) p +_{PP} 0 = p

(ii) p +_{PP} (q +_{PP} r) = (p +_{PP} q) +_{PP} r

(iii) p +_{PP} q = q +_{PP} p

(iv) p +_{PP} (p ·_{PP} (−1)) = 0

Proof. Remember that p = q ⟺ ∀m : M.∥m∥_{p} = ∥m∥_{q} (Proposition 4.8). Let m : M be arbitrary; then, by Proposition 4.20, the following are immediate:

(i) ∥p +_{PP} 0∥_{m} = ∥p∥_{m} + ∥0∥_{m} = ∥p∥_{m}

(ii) ∥p +_{PP} (q +_{PP} r)∥_{m} = ∥p∥_{m} + ∥q +_{PP} r∥_{m} = ∥p∥_{m} + ∥q∥_{m} + ∥r∥_{m} = ∥p +_{PP} q∥_{m} + ∥r∥_{m} = ∥(p +_{PP} q) +_{PP} r∥_{m}.

(iii) ∥p +_{PP} q∥_{m} = ∥p∥_{m} + ∥q∥_{m} = ∥q∥_{m} + ∥p∥_{m} = ∥q +_{PP} p∥_{m}.

(iv) Given m : M, ∥p +_{PP} (p ·_{PP} (−1))∥_{m} = ∥p∥_{m} + ∥p ·_{PP} (−1)∥_{m}, so it suffices to show that ∥p ·_{PP} (−1)∥_{m} = −∥p∥_{m}. By Proposition 4.24, ∥p ·_{PP} (−1)∥_{m} = ∑ ∥p∥_{m_{1}}∥ − 1∥_{m_{2}}. Now in this sum m_{2} can only assume value 1, whence m_{1} = m and the previous expression reduces to ∥p∥_{m}(−1) = −∥p∥_{m}.

□

Lemma 4.30 Let p, q, r : P. Then the following hold:

(i) p ·_{PP} 0 = 0

(ii) p ·_{PP} 1 = p

(iii) p ·_{PP} (q ·_{PP} r) = (p ·_{PP} q) ·_{PP} r

(iv) p ·_{PP} q = q ·_{PP} p

Proof. Again we appeal to Proposition 4.8.

We begin by proving commutativity. For any m : M, ∥p ·_{PP} q∥_{m} = ∑ ∥p∥_{m_{1}}∥q∥_{m_{2}} = ∑ ∥q∥_{m_{2}}∥p∥_{m_{1}} = ∥q ·_{PP} p∥_{m} where the sums range over all m_{1} ∈ |p| ∪ {1} and m_{2} ∈ |q| ∪ {1} for which |m| = |m_{1}||m_{2}|; the equalities hold by Proposition 4.24.

p ·_{PP} 0 = 0 is proved straightforwardly by induction, using Proposition 4.22.

Next, p ·_{PP} 1 = 1 ·_{PP} p = p ·_{PM} 1. For any m : M, |m| = |m||1|, hence by Proposition 4.22 ∥p ·_{PM} 1∥_{m} = ∥p∥_{m} × ∥1∥ = ∥p∥_{m}, hence p ·_{PP} 1 = p.

Finally, for associativity, we again obtain from Proposition 4.24 that, for m : M, ∥p ·_{PP} (q ·_{PP} r)∥_{m} = ∑ ∥p∥_{m_{1}}∥q ·_{PP} r∥_{m_{2}} = ∑ ∥p∥_{m_{1}} (∑ ∥q∥_{m_{2}^{1}}∥r∥_{m_{2}^{2}}) = ∑ ∥p∥_{m_{1}}∥q∥_{m_{2}^{1}}∥r∥_{m_{2}^{2}}

The last expression is completely symmetric on p, q and r, since the last sum in fact ranges over all m_{1}, m_{2}^{1} and m_{2}^{2} such that |m| = |m_{1}||m_{2}^{1}||m_{2}^{2}| with m_{1} ∈ |p| ∪ {1}, m_{2}^{1} ∈ |q| ∪ {1} and m_{2}^{2} ∈ |r| ∪ {1}. Therefore, from associativity and commutativity of sums and products of integers, we immediately get that ∥p ·_{PP} (q ·_{PP} r)∥_{m} = ∥r ·_{PP} (p ·_{PP} q)∥_{m}, and applying commutativity of ·_{PP} twice we get the desired result. □

Lemma 4.31 Let p, q, r : P. Then p ·_{PP} (q +_{PP} r) = (p ·_{PP} q) +_{PP} (p ·_{PP} r).

Proof. Once again, if m : M then ∥p·_{PP} (q+_{PP} r)∥_{m} = ∑ ∥p∥_{m_{1}}∥q+_{PP} r∥_{m_{2}} = ∑ ∥p∥_{m_{1}}(∥q∥_{m_{2}} + ∥r∥_{m_{2}}) = ∑ ∥p∥_{m_{1}}∥q∥_{m_{2}} + ∑ ∥p∥_{m_{1}}∥r∥_{m_{2}} = ∥(p ·_{PP} q) +_{PP} (p ·_{PP} r)∥_{m} □

Lemma 4.32 Let m : M \ ℤ and p : P. Then N (m) = m + 0 and N (p) = p.

Proof. We prove both results by simultaneous induction on m and p.

If m = v_{i}^{0} × i then N (m) = N (v_{i}^{0}) ·_{PP} N (i) = (v_{i}^{0} × 1 + 0) ·_{PP} i = v_{i}^{0} × i + 0 = m + 0, where the last-but-one equality is simply computation of ·_{PP}. If m = v_{i}^{1}(p) × i then N (m) = N (v_{i}^{1}(p)) ·_{PP} N (i) = (v_{i}^{1}(N (p)) × 1 + 0) ·_{PP} i = v_{i}^{1}(p) × i + 0 = m + 0, where the last-but-one equality follows from computation and induction hypothesis for p.

If m = v_{i}^{0} ×m′, then notice first that m′ ·_{MM} (v_{i}^{0} ×1) = m: ∥m′ ·_{MM} (v_{i}^{0} ×1)∥ = ∥m′∥×1 = ∥m′∥ by Proposition 4.14 and |m′ ·_{MM} (v_{i}^{0} × 1)| is the list obtained by inserting v_{i}^{0} at the right position in |m′|, which is by definition |m| (since this list is sorted), hence by Lemma 4.7 the result holds. Using this fact, the induction hypothesis and Lemmas 4.30 and 4.29, we see that the thesis holds.

N (m) = N (v_{i}^{0}) ·_{PP} N (m′)
= (v_{i}^{0} × 1 + 0) ·_{PP} (m′ + 0)
= (m′ + 0) ·_{PM} (v_{i}^{0} × 1) +_{PP} (0 ·_{PP} (e′ + 0))
= (m′ + 0) ·_{PM} (v_{i}^{0} × 1) +_{PP} 0
= (m′ + 0) ·_{PM} (v_{i}^{0} × 1)
= 0 ·_{PM} (v_{i}^{0} × 1) +_{PM} m′ ·_{MM} (v_{i}^{0} × 1)
= (0 +_{PM} (v_{i}^{0} × 1) ·_{Mℤ} 0) +_{PM} m′ ·_{MM} (v_{i}^{0} × 1)
= (0 +_{PM} 0) +_{PM} (m′ ·_{MM} (v × 1))
= 0 +_{PM} m
= m + 0.

If m = v_{i}^{1}(p) × m′, then by induction hypothesis N (v_{i}^{1}(p)) = v_{i}^{1}(N (p)) × 1 + 0 = v_{i}^{1}(p) + 0 and the previous chain of equalities holds replacing v_{i}^{1}(p) + 0 for v_{i}^{0} everywhere.

Now suppose that p is an integer; then N (p) = p by definition. Else take p = m + q; by induction hypothesis N (q) = q and N (m) = m + 0, hence

N (m + q) = N (m) +_{PP} N (q)
= (m + 0) +_{PP} q
= (0 +_{PP} q) +_{PM} m
= q +_{PM} m

by Lemma 4.29; but by definition of P, |m| cannot occur in |q| and must be smaller (w.r.t. <_{M}), hence the last expression reduces to m + q, or p. □

Corollary 4.33 N is idempotent, i.e., for every e : E^{∗}, N (N (e)) = N (e).

Proof. Since N (e) : P, the previous lemma is applicable, yielding the result. □

4.4 The substitution lemma

In this subsection, we show that the following “substitution lemma” holds: if, in two expressions that normalize to the same, some variables get uniformly renamed, then the resulting expressions also normalize to the same term.

This is proven in two steps.

Lemma 4.34 Let e : E and ξ be a renaming of variables. Then N (e^{ξ}) = N (N (e)^{ξ}).

Proof. By induction on e.

Suppose e = i; then N (N (i)^{ξ}) = N (i^{ξ}) = N (i) = N (i^{ξ}).

Now let e = v_{i}^{0}. Then N (N (e)^{ξ}) = N ((v_{i}^{0} × 1 + 0)^{ξ}) = N (v_{ξ_{0}(i)}^{0} × 1 + 0) = N (v_{ξ_{0}(i)}^{0}) ·_{PP} 1 +_{PP}

0 = N (v_{ξ_{0}(i)}^{0})) = N ((v_{i}^{0})^{ξ}) by virtue of Propositions 4.29 and 4.30.

If e = v_{i}^{1}(e′), then we use the induction hypothesis to show that

N (N (v_{i}^{1}(e′))^{ξ}) = N ((v_{i}^{1}(N (e′)) × 1 + 0)^{ξ})
= N (v_{ξ_{1}(i)}^{1}(N (e′)^{ξ}) × 1 + 0)
= N (v_{ξ_{1}(i)}^{1}(N (e′)^{ξ})) ·_{PP} 1 +_{PP} 0
= N (v_{ξ_{1}(i)}^{1}(N (e′)^{ξ}))
= v_{ξ_{1}(i)}^{1}(N (N (e′)^{ξ})) × 1 + 0
=^{IH} v_{ξ_{1}(i)}^{1}(N (e′^{ξ})) × 1 + 0
= N (v_{ξ_{1}(i)}^{1}(e′^{ξ}))
= N ((v_{i}^{1}(e′))^{ξ})

For the case e = e_{1} ⋆ e_{2}, with ⋆ = +, ×, we need besides the induction hypothesis the equality

N ((p ⋆ q)^{ξ}) = N ((p ⋆_{PP} q)^{ξ})  (19)

for all p, q : P. The proof of this is included in the Appendix; its use is marked here by ∗.

N (N (e_{1} ⋆ e_{2})^{ξ}) = N ((N (e_{1}) ⋆_{PP} N (e_{2}))^{ξ})
=^{∗} N ((N (e_{1}) ⋆ N (e_{2}))^{ξ})
= N (N (e_{1})^{ξ} ⋆ N (e_{2})^{ξ})
= N (N (e_{1})^{ξ}) ⋆_{PP} N (N (e_{2})^{ξ})
=^{IH} N (e_{1}^{ξ}) ⋆_{PP} N (e_{2}^{ξ})
= N (e_{1}^{ξ} ⋆ e_{2}^{ξ})
= N ((e_{1} ⋆ e_{2})^{ξ})

□

With this we can prove the main result of this section:

Theorem 4.35 Let e, e′ : E be expressions such that N (e) = N (e′) and let ξ be a renaming of variables. Then N (e^{ξ}) = N (e′^{ξ}).

Proof. According to the previous lemma, N (e^{ξ}) = N (N(e)^{ξ}) = N (N(e′)^{ξ}) = N (e′^{ξ}). □

4.5 Completeness

We are now ready to state our main result.

Theorem 4.36 Let t, t′ : A be such that the equality t =_{A} t′ can be proved (in the sense of Definition 2.11) only from the ring axioms and unfolding of the definitions of −, zring and nexp in t and t′. Define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). Then N (e) = N (e′).

The proof of this is split in several stages.

Lemma 4.37 Let t, t′ : A be terms such that t′ is obtained from t by unfolding the definitions of −, zring and ·^{n} (n closed) in t. Let lift(t, ρ) = ⟨e, σ⟩ and lift(t′, ρ) = ⟨e′, σ′⟩. Then σ = σ′ and N (e) = N (e′).

Proof. For − and ·^{n} this is immediate, since terms using these constructors are lifted to expressions using the corresponding abbreviations whose definition coincides with those of − and ·^{n}.

For zring the proof is by induction^{2}: \underline{0} unfolds to 0, both of which are lifted to 0; \underline{n + 1} is lifted to n+_{ℤ}1, which is in normal form, whereas \underline{n}+1 is lifted to n+1 which normalizes to N (n)+_{PP}1 = n +_{ℤ} 1; finally, \underline{n − 1} is lifted to n + 1 × (−1), which normalizes to N (n) +_{PP} 1 ·_{PP} (−1) = n −_{ℤ} 1.

□

Lemma 4.38 Let t, t′ : A be such that t =_{A} t′ is an instance of one of the axioms Set_{1}, SG, M_{1}, M_{2}, G_{1}, G_{2}, AG or R_{i} with 1 ≤ i ≤ 5. Define ⟨e, τ⟩ = lift(t, ∅) and ⟨e′, τ′⟩ = lift(t′, τ). Then N (e) = N (e′).

Proof. All these proofs are very similar, being a consequence of Lemmas 4.29 and 4.30. We detail a few:

Set_{1} Then t = t′; by Lemma 3.10 e′ = e, and obviously N (e) = N (e).

SG Then t = (t_{1} + t_{2}) + t_{3} and t′ = t_{1} + (t_{2} + t_{3}). Let lift(t_{1}, ∅) = ⟨e_{1}, ρ⟩, lift(t_{2}, ρ) = ⟨e_{2}, σ⟩ and lift(t_{3}, σ) = ⟨e_{3}, θ⟩. Then lift(t_{1} + t_{2}, ∅) = ⟨e_{1} + e_{2}, σ⟩ and lift((t_{1} + t_{2}) + t_{3}, ∅) =

⟨(e_{1} + e_{2}) + e_{3}, θ⟩.

Furthermore, since ρ ⊆ σ ⊆ θ by Lemma 3.8, Lemma 3.10 yields lift(t_{1}, θ) = ⟨e_{1}, θ⟩, lift(t_{2}, θ) = ⟨e_{2}, θ⟩ and lift(t_{3}, σ) = ⟨e_{3}, θ⟩, whence lift(t_{2} + t_{3}, θ) = ⟨e_{2} + e_{3}, θ⟩ and lift(t_{1} +

(t_{2} + t_{3}), θ) = ⟨e_{1} + (e_{2} + e_{3}), θ⟩.

Then N ((e_{1} + e_{2}) + e_{3}) = N (e_{1} + e_{2}) +_{PP} N (e_{3}) = (N (e_{1}) +_{PP} N (e_{2})) +_{PP} N (e_{3}) =

N (e_{1}) +_{PP} (N (e_{2}) +_{PP} N (e_{3})) = N (e_{1}) +_{PP} N (e_{2} + e_{3}) = N (e_{1} + (e_{2} + e_{3})).

G_{1} Then t = t_{1} + (−t_{1}) and t′ = 0. Let lift(t_{1}, ∅) = ⟨e_{1}, ρ⟩; then by Lemma 3.10 also lift(t_{1}, ρ) = ⟨e_{1}, ρ⟩, hence e = e_{1} + (e_{1} × (−1)); by definition lift(0, ρ) = ⟨0, ρ⟩, so e′ = 0.

Now N (e_{1}+(e_{1}×(−1))) = N (e_{1})+_{PP}(N (e_{1})·_{PP}(−1)) = 0 = N (0), according to Lemma 4.29.

R_{5} In this case t = t_{1} × (t_{2} + t_{3}) and t′ = (t_{1} × t_{2}) + (t_{1} × t_{3}). Reasoning in an analogous way to the case of SG above, we conclude that e = e_{1} × (e_{2} + e_{3}) and e′ = (e_{1} × e_{2}) + (e_{1} × e_{3}). By Lemma 4.30, N (e_{1} × (e_{2} + e_{3})) = N (e_{1}) ·_{PP} (N (e_{2}) +_{PP} N (e_{3})) = N (e_{1}) ·_{PP} N (e_{2}) +_{PP}

N (e_{1}) ·_{PP} N (e_{3}) = N ((e_{1} × e_{2}) + (e_{1} × e_{3})).

□

Lemma 4.39 Let t_{1}, t_{2} : A be such that, if ⟨e_{1}, ρ⟩ = lift(t_{1}, ∅) and ⟨e_{2}, σ⟩ = lift(t_{2}, ρ), then N (e_{1}) = N (e_{2}). Define ⟨e′_{2}, σ′⟩ = lift(t_{2}, ∅) and ⟨e′_{1}, ρ′⟩ = lift(t_{1}, σ′). Then N (e′_{1}) = N (e′_{2}).

Proof. Let e_{1}, e′_{1}, e_{2} and e′_{2} be as given. By Lemma 3.21 there is a renaming of variables ξ such that e′_{i} = e_{i}^{ξ} for i = 1, 2; but then

N (e′_{1}) = N (e_{1}^{ξ}) = N (e_{2}^{ξ}) = N (e′_{2})

using the hypothesis N (e_{1}) = N (e_{2}) and Theorem 4.35. □

Lemma 4.40 Let t_{1}, t_{2}, t_{3} : A and define

⟨e_{1}, ρ⟩ = lift(t_{1}, ∅)  ⟨e′_{2}, σ′⟩ = lift(t_{2}, ∅)
⟨e_{2}, σ⟩ = lift(t_{2}, ρ)  ⟨e′_{3}, θ′⟩ = lift(t_{3}, σ′)

Assume that N (e_{1}) = N (e_{2}) and N (e′_{2}) = N (e′_{3}). Define ⟨e_{3}, θ⟩ = lift(t_{3}, ρ). Then N (e_{1}) = N (e_{3}).

2In this paragraph we write +_{ℤ} to emphasize the distinction between addition of integers and addition of expressions.

Proof. Let e_{1}, e_{2}, e′_{2}, e_{3} and e′_{3} be as given and define ⟨e′′_{3}, θ′′⟩ = lift(t_{3}, σ). By Lemma 3.22, there exists a renaming of variables ξ such that e′′_{3} = e′_{3}^{ξ} and e_{2} = e′_{2}^{ξ}. By Lemma 3.21 there is another renaming of variables ξ′ such that e_{3} = e′′_{3}^{ξ′} and dom(ξ′_{i}) ∩ dom(ρ_{i}) = ∅ (see Figure 5). Then,

\xymatrix{ & ∅ \ar[dl]_{t_{2}} \ar[dr]^{t_{1}} \\ σ′ \ar[d]_{t_{3}} \ar@{.>}[dr]^{ξ} &  & ρ \ar[dl]_{t_{2}} \ar[d]_{t_{3}} \\ θ′ \ar@{.>}[dr]^{ξ} & σ \ar[d]_{t_{3}} & θ \\  & θ′′ \ar@{.>}[ur]^{ξ′}}

Figure 5: Proof of Lemma 4.40

N (e_{3}) = N (e′′_{3}^{ξ′}) = N (e′_{3}^{ξ′∘ξ}) = N (e′_{2}^{ξ′∘ξ}) = N (e_{2}^{ξ′}) = N (e_{1}^{ξ′}) = N (e_{1})

using the hypotheses N (e_{1}) = N (e_{2}) and N (e′_{2}) = N (e′_{3}) together with Theorem 4.35 and the equalities above stated. The last equality follows from the fact that dom(ξ′_{i}) ∩ dom(ρ_{i}) = ∅: by Lemma 3.11 every variable v_{k}^{i} occurring in e_{1} is in dom(ρ_{i}), so e_{1} = e_{1}^{ξ′}. □

Lemma 4.41 Let t_{1}, t_{2} : A be such that, if ⟨e_{1}, ρ⟩ = lift(t_{1}, ∅) and ⟨e_{2}, σ⟩ = lift(t_{2}, ρ), then N (e_{1}) = N (e_{2}). Let f : [A → A] be other than ·^{n} with n closed and define ⟨e′_{1}, ρ′⟩ = lift(f(t_{1}), ∅) and ⟨e′_{2}, σ′⟩ = lift(f(t_{2}), ∅). Then N (e′_{1}) = N (e′_{2}).

Proof. We have to consider two cases. If f is the unary inverse (−), then immediately e′_{1} = −e_{1}, ρ′ = ρ and hence e′_{2} = −e_{2}; in this case, N (e′_{1}) = N (−e_{1}) = N (e_{1} × (−1)) = N (e_{1}) ·_{PP} (−1) = N (e_{2}) ·_{PP} (−1) = N (e_{2} × (−1)) = N (−e_{2}) = N (e′_{2}).

Else, e′_{1} = v_{i}^{1}(e_{1}) with lift_{𝕍_{1}}(f, ρ) = ⟨v_{i}^{1}, ρ′⟩ and e′_{2} = v_{i}^{1}(e′′_{2}), with lift(t_{2}, ρ′) = ⟨e′′_{2}, σ′⟩ (since by Lemma 3.8 ρ′ ⊆ σ′, σ′_{1}(v_{i}^{1}) = f and thus lift_{𝕍_{1}}(f, σ′) = ⟨v_{i}^{1}, σ⟩).

By Lemma 3.20 there is a renaming of variables ξ such that e′′_{2} = e_{2}^{ξ} and dom(ξ_{i})∩dom(ρ_{i}) = ∅. Hence N (e′_{2}) = N (v_{i}^{1}(e′′_{2})) = v_{i}^{1}(N (e′′_{2})) × 1 + 0 = v_{i}^{1}(N (e_{2}^{ξ})) × 1 + 0 = v_{i}^{1}(N (e_{1}^{ξ})) × 1 + 0 = v_{i}^{1}(N (e_{1})) × 1 + 0 = N (v_{i}^{1}(e_{1})) = N (e′_{1}), using Theorem 4.35 together with the assumption N (e_{1}) = N (e_{2}) and the fact that e_{1} = e_{1}^{ξ} by virtue of Lemma 3.11 and dom(ξ_{i}) ∩ dom(ρ_{i}) = ∅.

□

Lemma 4.42 Let t_{1}, t_{2}, t_{3}, t_{4} : A and define

⟨e_{1}, ρ⟩ = lift(t_{1}, ∅)  ⟨e_{3}, θ⟩ = lift(t_{3}, ∅)
⟨e_{2}, σ⟩ = lift(t_{2}, ρ)  ⟨e_{4}, τ⟩ = lift(t_{4}, θ)

Assume that N (e_{1}) = N (e_{2}) and N (e_{3}) = N (e_{4}) and let

⟨e, γ⟩ = lift(t_{1} ⋆ t_{3})  ⟨e′, γ′⟩ = lift(t_{2} ⋆ t_{4})

where ⋆ is + or ×. Then N (e) = N (e′).

Proof. By definition of lift, e = e_{1} ⋆ e′_{3} with ⟨e′_{3}, γ⟩ = lift(t_{3}, ρ). Also, e′ = e′_{2} ⋆ e′_{4}, with ⟨e′_{2}, γ′′⟩ = lift(t_{2}, γ) and ⟨e′_{4}, γ′⟩ = lift(t_{4}, γ′′).

\xymatrix{ &  & ∅ \ar[dl]_{t_{1}} \ar[dr]^{t_{3}} \\  & ρ \ar[dl]_{t_{2}} \ar[dr]^{t_{3}} &  & θ \ar[dr]^{t_{4}} \ar@{.>}[dl]_{ξ} \\ σ \ar@{.>}[dr]^{ξ′} &  & γ \ar[dl]_{t_{2}} \ar[dr]^{t_{4}} &  & τ \ar@{.>}[dl]_{ξ} \\  & γ′′ \ar[dr]^{t^{4}} &  & γ′′′ \ar@{.>}[dl]_{ξ′′} \\  &  & γ′}

Figure 6: Proof of Lemma 4.42

Take lift(t_{4}, γ) = ⟨e′′_{4}, γ′′′⟩.

According to Lemma 3.22, there exists a renaming of variables ξ such that e′_{3} = e_{3}^{ξ} and e′′_{4} = e_{4}^{ξ}. By Lemma 3.21, there is a renaming of variables ξ′ such that e′_{2} = e_{2}^{ξ′} and dom(ξ′_{i}) ∩ dom(ρ_{i}) = ∅ (and hence e_{1} = e_{1}^{ξ′} due to Lemma 3.11). Again by Lemma 3.21, there exists a renaming of variables ξ′′ such that e′_{4} = e′′_{4}^{ξ′′} and dom(ξ′′_{i}) ∩ dom(γ_{i}) = ∅ (so that e′_{3} = e′_{3}^{ξ′′}) (see Figure 6).

Then, N (e′) = N (e′_{2}⋆e′_{4}) = N (e′_{2})⋆_{PP}N (e′_{4}) = N (e_{2}^{ξ′})⋆_{PP}N (e′′_{4}^{ξ′′}) = N (e_{2}^{ξ′})⋆_{PP}N (e_{4}^{ξ′′∘ξ}) = N (e_{1}^{ξ′}) ⋆_{PP} N (e_{3}^{ξ′′∘ξ}) = N (e_{1}) ⋆_{PP} N (e′_{3}^{ξ′′}) = N (e_{1}) ⋆_{PP} N (e′_{3}) = N (e_{1} ⋆ e′_{3}) = N (e) using the hypotheses and Theorem 4.35. □

Definition 4.43 A normal proof of t =_{A} t′ is a proof of t =_{A} t′ where Set_{4} is never applied with ·^{n} (n closed) and Set_{5} is never applied with −.

Lemma 4.44 Suppose that t =_{A} t′ can be proved only from the ring axioms and unfolding of the definitions of −, zring and nexp in t and t′. Then there exists a normal proof of t =_{A} t′.

Proof. By induction on the length of the proof of t =_{A} t′. The only non-trivial cases are those when the last axiom to be applied is Set_{4} with ·^{n} (n closed) or Set_{5} with −.

Suppose we prove t_{1}^{n} =_{A} t_{2}^{n} from t_{1} =_{A} t_{2} using Set_{4}. We proceed by induction. If n = 0, then we can replace the whole proof by (Set_{1} 1), and folding produces t_{1}^{0} =_{A} t_{2}^{0}. If n = k + 1, we first find a normal proof of t_{1}^{k} =_{A} t_{2}^{k} using the induction hypothesis (for n) and a normal proof of t_{1} =_{A} t_{2} using the induction hypothesis for the lemma. Then we apply Set_{5} to get t_{1} × t_{1}^{k} =_{A} t_{2} × t_{2}^{k}; folding ·^{k+1} on the last equality produces the desired proof.

Finally, if we prove t_{1} − t_{3} =_{A} t_{2} − t_{4} from t_{1} =_{A} t_{2} and t_{3} =_{A} t_{4} using Set_{5}, we first find normal proofs of t_{1} =_{A} t_{2} and t_{3} =_{A} t_{4} (induction hypothesis), apply Set_{4} to the latter to get −t_{3} =_{A} −t_{4} and apply Set_{5} to get t_{1} + (−t_{3}) =_{A} t_{2} + (−t_{4}), which is the desired equality with the definition of − unfolded. □

Theorem 4.45 Let t, t′ : A and e, e′ : E be as in Theorem 4.36 and assume furthermore that there is a normal proof of the equality t =_{A} t′. Then N (e) = N (e′).

Proof. By induction on the length of the normal proof of t =_{A} t′.

If t =_{A} t′ is an instance of one of the axioms Set_{1}, SG, M_{1}, M_{2}, G_{1}, G_{2}, AG or R_{i} with 1 ≤ i ≤ 5, then by Lemma 4.38 N (e) = N (e′).

Suppose t =_{A} t′ is proved by Set_{2} from t′ =_{A} t. Then we can apply Lemma 4.39 and the induction hypothesis to conclude that the thesis holds.

Suppose t =_{A} t′ is proved by Set_{3} from t =_{A} t_{1} and t_{1} =_{A} t′. Then we can apply Lemma 4.40 and the induction hypothesis to conclude that the thesis holds.

Suppose t =_{A} t′ is proved from t_{1} =_{A} t_{2} by Set_{4} and f is not ·^{n} with n closed. Then by Lemma 4.41 and the induction hypothesis the thesis holds.

Suppose t =_{A} t′ is proved from t_{1} =_{A} t_{2} and t_{3} =_{A} t_{4} by Set_{5} and f is not −. Then by Lemma 4.42 and the induction hypothesis the thesis holds.

If t_{1} and t_{2} can be obtained from t and t′ by unfolding the definitions of −, ·^{n} and zring, then by Lemma 4.37 lift(t_{1}, ∅) = lift(t, ∅) = ⟨e, ρ⟩ and lift(t_{2}, ρ) = lift(t′, ρ) = ⟨e′, σ⟩, hence the induction hypothesis immediately asserts the thesis. □

We are now ready to prove Theorem 4.36.

Proof.(Completeness Theorem 4.36) Assume there is a proof of t =_{A} t′. By Lemma 4.44 there is also a normal proof of t =_{A} t′, so by Theorem 4.45 N (e) = N (e′). □

5 Completeness of rational: groups

We now show how we can get a completeness theorem for groups similar to Theorem 4.36. We begin by observing that the theory developed above is not enough as is: if G is a group, a : G and v_{0}^{0} ][_{ρ} a, then v_{0}^{0} + v_{0}^{0} ][_{ρ} a + a, but N (v_{0}^{0} + v_{0}^{0}) = v_{0}^{0} × 2 + 0 which cannot be interpreted in G, so part (ii) of Lemma 4.26 fails to hold. Therefore we begin by extending the interpretation relation in a conservative way.

Definition 5.1 Let G be a group, n : ℤ and a : G. Then n · a is inductively defined as follows.

0 · a := 0  (20)
(n + 1) · a := n · a + a, for n ≥ 0  (21)
(n − 1) · a := n · a − a, for n ≤ 0  (22)

Proposition 5.2 Let R be a ring. Then, for all n : ℤ and a : R, n · a =_{R} \underline{n} × a is provable.

Proof. Straightforward induction. If n = 0 then n · a = 0 and \underline{0} = 0, so the equality reduces to 0 × a =_{R} 0, which is provable. Assume that n · a =_{R} \underline{n} × a for n ≥ 0; then (n + 1) · a = n · a + a =_{R} \underline{n}×a+a =_{R} (\underline{n}+1)×a = \underline{n + 1}×a. Similarly, if n ≤ 0 then (n − 1)·a = n·a−a =_{R} \underline{n}×a−a =_{R} (\underline{n} − 1) × a = \underline{n − 1} × a. □

Lemma 5.3 Let ρ be a substitution pair for a ring A. The interpretation relation satisfies the following rule:

e ][_{ρ} t_{1} ∧ n · t_{1} =_{A} t → e × n ][_{ρ} t

where n : ℤ.

Proof. By the previous proposition n · t_{1} =_{A} \underline{n} × t_{1} is provable, whence \underline{n} × t_{1} =_{A} t is provable by hypothesis, Set_{2} and Set_{3}. Furthermore, \underline{n} ][_{ρ} n by Set_{1} and (11). By hypothesis e ][_{ρ} t_{1}. Therefore, by (13), e × n ][_{ρ} t. □

Hence, this clause can be added to the inductive definition of the interpretation relation without changing it when defined over a ring or field but extending it in the case of groups. We also need the case k = 0 of (11). That is, we consider the interpretation relation as defined in Definition 2.29 extended with the two following clauses.

0 =_{G} t → 0 ][_{ρ} t  (23)
e ][_{ρ} t_{1} ∧ n · t_{1} =_{G} t → e × n ][_{ρ} t  (24)

Notice that conditions (16) and (17) in Lemma (2.30) can be proved from these clauses, so that they also hold for groups with this extended interpretation relation. This allows us to prove the following version of Lemma 2.32.

Lemma 5.4 Let e : E, t, t′ : G and ρ be a substitution pair for G such that e ][_{ρ} t and e ][_{ρ} t′. Then t =_{G} t′.

Proof. By induction on ][_{ρ} (Coq checked). □

We can now prove the following results, which are group analogues of those proved in Subsection 4.2.

Lemma 5.5 Let G be a group and ρ be a substitution pair for G. The auxiliary normalization functions satisfy the following properties.

(i) if m ][_{ρ} t then m ·_{Mℤ} i ][_{ρ} i · t;

(ii) if x × m ][_{ρ} t then m ·_{M𝕍} x ][_{ρ} t;

(iii) if m × m′ ][_{ρ} t or m′ × m ][_{ρ} t then m ·_{MM} m′ ][_{ρ} t;

(iv) if m ][_{ρ} t and m′ ][_{ρ} t′ then m +_{MM} m′ ][_{ρ} t + t′;

(v) if p ][_{ρ} t and m′ ][_{ρ} t′ then p +_{PM} m′ ][_{ρ} t + t′;

(vi) if p ][_{ρ} t and p′ ][_{ρ} t′ then p +_{PP} p′ ][_{ρ} t + t′;

(vii) if p × m′ ][_{ρ} t or m′ × p ][_{ρ} t then p ·_{PM} m′ ][_{ρ} t;

(viii) if p × p′ ][_{ρ} t then p ·_{PP} p′ ][_{ρ} t.

Proof. By induction (Coq checked). □

Some of the hypotheses in the previous lemma may seem a bit strange. The problem is, we cannot say as before that “if m ][_{ρ} t and m′ ][_{ρ} t′ then m ·_{MM} m′ ][_{ρ} t × t′” because in G there is no multiplication. Hence, we replace this by the equivalent (in a ring) form “if m × m′ ][_{ρ} t then m·_{MM} m′ ][_{ρ} t”. However, this is still not enough, since ·_{MM} may switch the order of its arguments; hence the disjunction in the actual lemma, which in fact says that one of the arguments to ·_{MM} is an integer.

Similar remarks hold for ·_{PM}. In the case of ·_{M𝕍} we already know that the second argument is a variable, so one of the clauses of the disjunction never holds and we can erase it. As for ·_{PP}, it will only be called by N when a product appears in the original expression, which is clearly impossible if this is the result of lifting a term in G; it is however needed in the proof of the following lemma.

Lemma 5.6 Let e : E and t : G. If e ][_{ρ} t then N (e) ][_{ρ} t.

Proof. By induction (Coq checked). Since products in expressions can now only be interpreted by means of (24), the stronger hypotheses in Lemma 5.5 are seen to be satisfied by analyzing the proof of e ][_{ρ} t. □

Corollary 5.7 Let t, t′ : G and define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). If N (e) = N (e′), then t =_{G} t′ can be proved from the group axioms and unfolding of the definition of −.

Proof. Let e and e′ be as defined above and suppose that N (e) = N (e′). By Lemma 3.9, both e ][_{ρ} t and e′ ][_{ρ} t′. By Proposition 5.6 also N (e) ][_{ρ} t and N (e′) ][_{ρ} t′. Since N (e) = N (e′), we have that N (e) ][_{ρ} t and N (e) ][_{ρ} t′, whence t =_{G} t′ by Lemma 5.4. □

Theorem 5.8 Let t, t′ : G be such that the equality t =_{G} t′ can be proved only from the group axioms and unfolding of the definition of −. Define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). Then N (e) = N (e′).

Proof. Immediate from Theorem 4.36, since the group axioms are a proper subset of the ring axioms. □

6 Partial completeness of rational: fields

We now try to extend the results in the previous sections to an arbitrary field structure A. We begin by extending the type of normal forms and the normalization function.

Definition 6.1 The set F of field expressions in normal form is the set {p/q|p, q ∈ P }.

Definition 6.2 +_{FF} is defined as follows.

+_{FF} : F × F → F
e_{1}/e_{2}, f_{1}/f_{2} ↦ ((e_{1} ·_{PP} f_{2}) +_{PP} (e_{2} ·_{PP} f_{1})) /(e_{2} ·_{PP} f_{2})

Proposition 6.3 +_{FF} satisfies the following properties:

(i) +_{FF} is well defined;

(ii) if p ][_{ρ} t and q ][_{ρ} t′, then p +_{FF} q ][_{ρ} t + t′.

Proof. Direct consequence of the definition of F and Propositions 4.20 and 4.24 (the second is Coq checked). □

Definition 6.4 ·_{FF} is defined as follows.

+_{FF} : F × F → F
e_{1}/e_{2}, f_{1}/f_{2} ↦ (e_{1} ·_{PP} f_{1})/(e_{2} ·_{PP} f_{2})

Proposition 6.5 ·_{FF} satisfies the following properties:

(i) ·_{FF} is well defined;

(ii) if p ][_{ρ} t and q ][_{ρ} t′, then p ·_{FF} q ][_{ρ} t × t′.

Proof. Direct consequence of the definition of F and Proposition 4.24 (the second is Coq checked).

□

Definition 6.6 /_{FF} is defined as follows.

/_{FF} : F × F → F
e_{1}/e_{2}, f_{1}/f_{2} ↦ (e_{1} ·_{PP} f_{2})/(e_{2} ·_{PP} f_{1})

Proposition 6.7 /_{FF} satisfies the following properties:

(i) /_{FF} is well defined;

(ii) if p ][_{ρ} t and q ][_{ρ} t′ ≠ 0, then p/_{FF}q ][_{ρ} t/t′.

Proof. Direct consequence of the definition of F and Propositions 4.20 and 4.24 (the second is Coq checked). □

Definition 6.8 The normalization function N_{F} is defined as follows.

N_{F} : E → P
i ↦ i
v_{i}^{0} ↦ (v_{i}^{0} × 1 + 0) /1
e + f ↦ N_{F} (e) +_{FF} N_{F} (f)
e × f ↦ N_{F} (e) ·_{FF} N_{F} (f)
e/f ↦ N_{F} (e)/_{FF}N_{F} (f)
v_{i}^{1}(e) ↦ (v_{i}^{1}(N_{F} (e)) × 1 + 0) /1

Proposition 6.9 N_{F} satisfies the following properties:

(i) N_{F} is well defined;

(ii) if e ][_{ρ} t then N_{F} (e) ][_{ρ} t.

Proof. As before, the first part is a straightforward induction, similar to the proof of Proposition 4.26.

The second property is proved by induction (Coq checked); notice that the hypothesis e ][_{ρ} t is essential to guarantee that N_{F} will not introduce divisions by zero (compare with the situation for groups). □

6.1 Correctness and completeness

Unfortunately, rational as described above does not work so well with this normalization function as before, as the following (simple) example shows.

Example 6.10 Let x : A be a variable such that x ≠ 0. Then x × 1/x =_{A} 1 is a special case of axiom F.

A simple calculation shows that

lift(x × 1/x, ∅) = ⟨v_{0}^{0} × 1/v_{0}^{0}, [v_{0}^{0} := x]⟩
lift(1, [v_{0}^{0} := x]) = ⟨1, [v_{0}^{0} := x]⟩

but N_{F} (v_{0}^{0} × 1/v_{0}^{0}) = (v^{0} × 1 + 0)/(v^{0} × 1 + 0), while N_{F} (1) = 1.

The problem lies in the algebraic structure of F with the operations above defined, and in trying to generalize the properties in Section 4.3. Although ⟨F, +_{FF}, 0/1, ·_{FF}, 1/1⟩ is a ring, it is not an integral domain: any expression of the form 0/e is an additive unit, and therefore F does not become a field when we add /_{FF} as a division operator.

The crux of the matter is that terms in F are not restricted to irreducible fractions (with the intuitive meaning of what “irreducible” should mean). Adding this restriction is also far from trivial: rewriting quotients of polynomials to irreducible fractions is known to be an extremely difficult problem, and implementing such an algorithm in N_{F} would make rational extremely slow.

Therefore, we will use a different approach. Going back to the example, it is easy to check that N_{F} (v_{0}^{0} × 1/v_{0}^{0} − 1) = 0/(v_{0}^{0} × 1 + 0). Therefore, we will use the following modified version of rational for fields: instead of comparing the normal form of the two expressions e and f, we compute the normal form of e − f and check that it has the form 0/e′. This is correct.

Corollary 6.11 Let t, t′ : A and define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). If N_{F} (e − e′) = 0/e′′, where e′′ is an arbitrary expression, then t =_{A} t′ can be proved from the field axioms and unfolding of the definitions of −, zring and nexp.

Proof. Let e and e′ be as defined above and suppose that N (e − e′) = 0/e′′ for some e′′. By Lemma 3.9, both e ][_{ρ} t and e′ ][_{ρ} t′. By Proposition 4.26 also N (e) ][_{ρ} t and N (e′) ][_{ρ} t′. Since N (e − e′) = N (e) +_{FF} N (e′) ·_{FF} (−1), Lemmas 6.3 and 6.5 together with (11) imply that N (e − e′) ][_{ρ} t + t′ × −1; but N (e − e′) = 0/e′′, hence 0/e′′ can be interpreted, and therefore 0/e′′ ][_{ρ} 0 by (14) and (11). By Lemma 2.32 it then follows that t + t′ × −1 =_{A} 0, from which the thesis follows. □

The only drawback of this approach is that the completeness proof does not go through. A proof analogous to that of Theorem 4.36, obtained by replacing “N (e) = N (e′)” with “N (e−e′) = 0/e′′” everywhere, fails on the induction step for Set_{4}, since the induction hypothesis will not be strong enough to prove an equivalent of Lemma 4.41. All other proofs can be adapted, though, thus yielding the following (partial) completeness result.

Theorem 6.12 Let t, t′ : A be such that the equality t =_{A} t′ can be proved only from the field axioms and unfolding of the definitions of −, zring and nexp in t and t′, without using Set_{4} except for − and ·^{n} (n closed). Define ⟨e, ρ⟩ = lift(t, ∅) and ⟨e′, σ⟩ = lift(t′, ρ). Then N (e − e′) has the form 0/e′′ for some expression e′′.

Proof. Similar to the proof of Theorem 4.36. □

To see that the extra hypothesis is really needed, consider f(x) =_{A} f(x/2 + x/2), which is clearly provable. Then

lift(f(x), ∅) = ⟨v_{0}^{1}(v_{0}^{0}), ⟨[v_{0}^{0} := x], [v_{0}^{1} := f]⟩⟩
lift(f(x/2 + x/2), ⟨[v_{0}^{0} := x], [v_{0}^{1} := f]⟩) = ⟨v_{0}^{1}(v_{0}^{0}/2 + v_{0}^{0}/2), ⟨[v_{0}^{0} := x], [v_{0}^{1} := f]⟩⟩

and N_{F} (v_{0}^{1}(v_{0}^{0}) − v_{0}^{1}(v_{0}^{0}/2 + v_{0}^{0}/2)) = (v_{0}^{1}((v_{0}^{0} × 1 + 0)/1) × 1 + v_{0}^{1}((v_{0}^{0} × 4 + 0)/4) × (−1) + 0)/1 ≠ 0.

In practice, though, the difference in strength between Theorem 4.36 and Theorem 6.12 is not very serious. In most situations axiom Set_{4} is not needed, and in several where it is used rational still works (this will be the case whenever the hypothesis of this axiom can be proved just from the ring axioms). In particular, rational still works on goals like f(x+x)/4+f(2x)/4 = f(x+x+0)/2, and this is usually enough. Throughout C-CoRN, less than five situations were found where this limitation of rational made an alternative proof necessary.

7 Remarks on the implementation

As mentioned in the Introduction, the theoretical treatment of rational we made considered a simplified version of the tactic. The actual implementation covers all the expressions considered in the type of setoids in C-CoRN, in particular binary functions and partial unary functions, the latter being implemented as functions of a setoid element and a proof term.

These extra cases pose no new difficulties. There is one new axiom Set′_{4}, stating a similar version of Set_{4} for partial functions. The type of expressions needs to be extended with two new constructors for variables representing these functions, and the interpretation and lift must be adapted accordingly. As a consequence several new cases need to be considered when proving results about the order in which terms are lifted, but these can be treated in a similar way to the like cases for variables in 𝕍_{1} (unlike variables in 𝕍_{0}, which behave differently). The completeness results for groups and rings still hold; as for fields, as would be expected, the hypothesis of Theorem 6.12 has to be strengthened since Set′_{4} and Set_{5} cannot be used either in the proof of t = t′.

8 Conclusions

In this paper we formally described rational and undertook a study of its behavior as a decision procedure. It was shown to be correct and complete for groups and rings, which is very useful information in interactive proof development, and correct and partially complete for fields, which is also very useful, as explained in Section 6.

Furthermore, we hope to use the completeness of rational to take the tactic a step further. By the completeness of the theory of fields we also know that for every equality t = t′ that cannot be proved from the axioms there is a field where t ≠ t′ holds. We hope to use the information provided by rational upon failure (namely, an expression in normal form that does not equal zero) to construct such a model within Coq, thus reflecting completeness within the system.

Although rational is designed for Coq, we conducted this study at a level of abstraction that should make it easy to develop similar (partially) complete tactics for other proof assistants based on type theory. It is also possible that rational can be adapted to other systems.

Acknowledgments

The authors wish to thank Henk Barendregt and Herman Geuvers for their helpful suggestions and support.

This work was partially supported by the European Project IST-2001-33562 MoWGLI and by FCT and FEDER under POCTI, namely through CLC project FibLog FEDER POCTI / 2001 / MAT / 37239.

References

[1] Stuart F. Allen, Robert L. Constable, Douglas J. Howe, and William Aitken. The Semantics of Reflected Proof. In Proceedings of the 5th Symposium on Logic in Computer Science, pages 95–197, Philadelphia, Pennsylvania, June 1990. IEEE, IEEE Computer Society Press.

[2] C. C. Chang and H. Jerome Keisler. Model Theory. North-Holland, 1990.

[3] The Coq Development Team. The Coq Proof Assistant Reference Manual, April 2004. Version 8.0.

[4] L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN: the Constructive Coq Repository at Nijmegen. In MKM 2004, LNCS. Springer Verlag, 2004. To appear.

[5] L. Cruz-Filipe and F. Wiedijk. Hierarchical Reflection. In Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, LNCS. Springer Verlag, 2004. To appear.

[6] H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg. The Algebraic Hierarchy of the FTA Project. Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, pages 271–286, 2002.

[7] H. Geuvers, F. Wiedijk, and J. Zwanenburg. Equational Reasoning via Partial Reflection. In M. Aagaard and J. Harrison, editors, Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, volume 1869 of LNCS, pages 162–178, Berlin, Heidelberg, New York, 2000. Springer Verlag.

A Proof of Equality (19)

Throughout this section, ξ is a (fixed) renaming of variables. We prove the following equality, valid for all p, q : P:

N ((p ⋆ q)^{ξ}) = N ((p ⋆_{PP} q)^{ξ}).

We will only deal with the case ⋆ = +, since the case ⋆ = × is similar. We prove this in a series of steps.

Lemma A.1 Let m : M and v_{i}^{0} : 𝕍_{0}. Then N ((m ·_{M𝕍} v_{i}^{0})^{ξ}) = N (m^{ξ}) ·_{PP} N (v_{i}^{0}^{ξ}).

Proof. By induction on m. If m ∈ ℤ, then trivially

N ((m ·_{M𝕍} v_{i}^{0})^{ξ}) = N ((v_{i}^{0} × m)^{ξ})
= N (v_{i}^{0}^{ξ} × m)
= N (v_{i}^{0}^{ξ}) ·_{PP} N (m)
= N (m) ·_{PP} N (v_{i}^{0}^{ξ})
= N (m × v_{i}^{0}^{ξ})
= N ((m × v_{i}^{0})^{ξ})

Suppose now that m = v_{j}^{0} × e. If i ≤ j, the previous proof still holds replacing m with m^{ξ} in the third through sixth expression; else the following shows the equality.

N (((v_{j}^{0} × e) ·_{M𝕍} v_{i}^{0})^{ξ}) = N ((v_{j}^{0} × (e ·_{M𝕍} v_{i}^{0}))^{ξ})
= N (v_{j}^{0}^{ξ}) ·_{PP} N ((e ·_{M𝕍} v_{i}^{0})^{ξ})
=^{IH} N (v_{j}^{0}^{ξ}) ·_{PP} (N (e^{ξ}) ·_{PP} N (v_{i}^{0}^{ξ}))
= (N (v_{j}^{0}^{ξ}) ·_{PP} N (e^{ξ})) ·_{PP} N (v_{i}^{0}^{ξ})
= N ((v_{j}^{0} × e)^{ξ}) ·_{PP} N (v_{i}^{0}^{ξ})

Finally, if m = v_{j}^{1}(p) × e then again the first argument holds. □

Lemma A.2 Let m : M, v_{i}^{1} : 𝕍_{1} and p : P. Then N ((m ·_{M𝕍} v_{i}^{1}(p))^{ξ}) = N (m^{ξ}) ·_{PP} N (v_{i}^{1}(p)^{ξ}).

Proof. Analogous to the previous. □

Lemma A.3 Let m_{1}, m_{2} : M be such that |m_{1}| = |m_{2}|. Then N ((m_{1} +_{MM} m_{2})^{ξ}) = N (m_{1}^{ξ}) +_{PP} N (m_{2}^{ξ}).

Proof. By induction on m_{1}.

If m_{1} = i ∈ ℤ, then also m_{2} = j ∈ ℤ because |m_{1}| = |m_{2}|. Then both sides of the equality reduce to i + j.

If m_{1} = v_{i}^{0} × e, then also m_{2} = v_{i}^{0} × e′, whence

N ((v_{i}^{0} × e +_{MM} v_{i}^{0} × e′)^{ξ}) = N (((e +_{MM} e′) ·_{M𝕍} v_{i}^{0})^{ξ})
=^{⋆} N ((e +_{MM} e′)^{ξ}) ·_{PP} N (v_{i}^{0}^{ξ})
=^{IH} (N (e^{ξ}) +_{PP} N (e′^{ξ})) ·_{PP} N (v_{i}^{0}^{ξ})
= N (v_{i}^{0}^{ξ}) ·_{PP} N (e^{ξ}) +_{PP} N (v_{i}^{0}^{ξ}) ·_{PP} N (e′^{ξ})
= N ((v_{i}^{0} × e)^{ξ}) +_{PP} N ((v_{i}^{0} × e′)^{ξ})

where ⋆ denotes application of Lemma A.1.

The case m_{1} = v_{i}^{1}(p) × e is analogous resorting to Lemma A.2. □

Lemma A.4 Let p : P and m : M. Then N ((p +_{PM} m)^{ξ}) = N (p^{ξ}) +_{PP} N (m^{ξ}).

Proof. By induction on p and m.

Suppose p = i ∈ ℤ. If m = j ∈ ℤ, then both expressions reduce to i + j; else N ((i +_{PM} m)^{ξ}) = N ((m + i)^{ξ}) = N (m^{ξ}) +_{PP} N (i^{ξ}) = N (i^{ξ}) +_{PP} N (m^{ξ}).

Suppose now that p = e_{1} + e_{2}. There are several cases to consider.

• if m = i ∈ ℤ or |e_{1}| <_{M} |m|, then

N (((e_{1} + e_{2}) +_{PM} m)^{ξ}) = N ((e_{1} + (e_{2} +_{PM} m))^{ξ})
= N (e_{1}^{ξ}) +_{PP} N ((e_{2} +_{PM} m)^{ξ})
=^{IH} N (e_{1}^{ξ}) +_{PP} (N (e_{2}^{ξ}) +_{PP} N (m^{ξ}))
= (N (e_{1}^{ξ}) +_{PP} N (e_{2}^{ξ})) +_{PP} N (m^{ξ})
= N ((e_{1} + e_{2})^{ξ}) +_{PP} N (m^{ξ})

• if |e_{1}| = |m|, then

N (((e_{1} + e_{2}) +_{PM} m)^{ξ}) = N ((e_{2} +_{PM} (e_{1} +_{MM} m))^{ξ})
=^{IH} N (e_{2}^{ξ}) +_{PP} N ((e_{1} +_{MM} m)^{ξ})
=^{⋆} N (e_{2}^{ξ}) +_{PP} (N (e_{1}^{ξ}) +_{PP} N (m^{ξ}))
= (N (e_{1}^{ξ}) +_{PP} N (e_{2}^{ξ})) +_{PP} N (m^{ξ})
= N ((e_{1} + e_{2})^{ξ}) +_{PP} N (m^{ξ})

where ⋆ denotes application of Lemma A.3.

• if |e_{1}| ≥_{M} |m|, then

N ((p +_{PM} m)^{ξ}) = N ((m + p)^{ξ})
= N (m^{ξ}) +_{PP} N (p^{ξ})
= N (p^{ξ}) +_{PP} N (m^{ξ})
□

Lemma A.5 Let p, q : P. Then N ((p +_{PP} q)^{ξ}) = N (p^{ξ}) +_{PP} N (q^{ξ}). Proof. By induction on p. If p = i ∈ ℤ then N ((i +_{PP} q)^{ξ}) = N ((q +_{PM} i)^{ξ}) = N (q^{ξ}) +_{PP} N (i^{ξ}) = N (i^{ξ}) +_{PP} N (q^{ξ}) by Lemma A.4.

Finally, if p = e_{1} + e_{2} then the following reasoning proves the desired equality.

N (((e_{1} + e_{2}) +_{PP} q)^{ξ}) = N (((e_{2} +_{PP} q) +_{PM} e_{1})^{ξ})
=^{⋆} N ((e_{2} +_{PP} q)^{ξ}) +_{PP} N (e_{1}^{ξ})
=^{IH} (N (e_{2}^{ξ}) +_{PP} N (q^{ξ})) +_{PP} N (e_{1}^{ξ})
= (N (e_{1}^{ξ}) +_{PP} N (e_{2}^{ξ})) +_{PP} N (q^{ξ})
= N ((e_{1} + e_{2})^{ξ}) +_{PP} N (q^{ξ})
□

Corollary A.6 Let p, q : P. Then N ((p +_{PP} q)^{ξ}) = N ((p + q)^{ξ}). Proof. N ((p + q)^{ξ}) = N (p^{ξ}) +_{PP} N (q^{ξ}), and by Lemma A.5 we are done. □