Hierarchical Reflection

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

1 Department of Computer Science, University of Nijmegen 2 Center for Logic and Computation, Lisboa

                          {lcf,freek}@cs.kun.nl

Abstract. The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets interpreted in the domain of discourse. By allowing the interpretation function to be partial or even a relation one gets a more general method known as “partial reflection”. In this paper we show how one can take advantage of the partiality of the interpretation to uniformly define a family of tactics for equational reasoning that will work in different algebraic structures. These tactics then follow the hierarchy of those algebraic structures in a natural way.

1 Introduction

1.1 Problem

Computers have made formalization of mathematical proof practical. They help getting formalizations correct by verifying all the details, but they also make it easier to formalize mathematics by automatically generating parts of the proofs.

One way to automate proof is the technique called reflection. With reflection one describes the desired automation inside the logic of the theorem prover, by formalizing relevant meta-theory. Reflection is the common approach for proof automation in type theoretical systems like NuPRL and Coq. Another name for reflection is “the two-level approach”.

In Nijmegen we formalized the Fundamental Theorems of Algebra and Calculus in Coq, and then extended these formalizations into a structured library of mathematics named the C-CoRN library [3, 4]. For this library we defined a reflection tactic called Rational that automatically establishes equalities of rational expressions in a field by bringing both to the same side of the equal sign and then multiplying everything out. With this tactic, equalities like

\frac{1}{x} + \frac{1}{y} = \frac{x + y}{xy}

can be automatically proved without any human help.

The Rational tactic only works for expressions in a field, but using the same idea one can define analogous tactics for expressions in a ring or a group. The trivial way to define these is to duplicate the definition of the Rational tactic and modify it for these simpler algebraic structures by removing references to division or multiplication. This was actually done to implement a ring version of Rational.

However this is not efficient, as it means duplication of the full code of the tactic. In particular the normalization function that describes the simplification of expressions, which is quite complicated, has to be defined multiple times. But looking at the normalization function for field expressions, it is clear that it contains the normalization function for rings. In this paper we study a way to integrate these tactics for different algebraic structures.

1.2 Approach

In the C-CoRN library algebraic structures like fields, rings and groups are organized into an Algebraic Hierarchy. The definition of a field reuses the definition of a ring, and the definition of a ring reuses the definition of a group. This hierarchy means that theory about these structures is maximally reusable. Lemmas about groups are automatically also applicable to rings and fields, and lemmas about rings also apply to fields. In this paper we organize the equational tactics for fields, rings and groups in a similar hierarchical manner.

It turns out that expression simplification in a field can be directly applied to equational reasoning in rings and groups as well. This is quite surprising: the normal forms of expressions that get simplified in this theory will contain functions like multiplication and division, operations that do not make sense in a group.

1.3 Related Work

Rational is for the C-CoRN setoid framework what the standard Coq tactic Field is for Leibniz equality. Both tactics were developed at about the same time. Field is a generalization of the Coq Ring tactic, so with the Field and Ring tactics the duplication of effort that we try to eliminate is also present. Also the Ring tactic applies to rings as well as to semirings (to be able to use it with the natural numbers), so there is also this kind of duplication within the Ring tactic itself.

Reflection has also been widely used in the NuPRL system as described originally in [1]. More recently, [8] introduces other techniques that allow code reuse for tactics in MetaPRL, although the ideas therein are different from ours. Since the library of this system also includes an algebraic hierarchy built using subtyping (see [9]), it seems reasonable to expect that the work we describe could be easily adapted to that framework.

1.4 Contribution

We show that it is possible to have one unified mechanism for simplification of expressions in different algebraic structures like fields, rings and groups. We also show that it is not necessary to have different normalization functions for these expressions, but that it is possible to decide equalities on all levels with only one normalization function.

1.5 Outline

In Section 2 we summarize the methods of reflection and partial reflection. In Section 3 we describe in detail the normalization function of the Rational tactic. Section 4 is a small detour where we generalize the same method to add uninterpreted function symbols to the expressions that Rational understands. In Section 5 we show how to do reflection in an algebraic hierarchy in a hierarchical way. Finally in Section 6 we present a possibility to have even tighter integration in a hierarchical reflection tactic, which unfortunately turns out to require the so-called K axiom.

2 Reflection and Partial Reflection

In this section we will briefly summarize [7]. That paper describes a generalization of the technique of reflection there called partial reflection. One can give a general account of reflection in terms of decision procedures, but here we will only present the more specific method of reflection with a normalization function, which is used to do equational reasoning.

In the normal, “total”, kind of reflection one defines a type E of syntactic expressions for the domain A that one is reasoning about, together with an interpretation function

[[−]]_{ρ} : E → A

which assigns to a syntactic expression e an interpretation [[e]]_{ρ}. In this, ρ is a valuation that maps the variables in the syntactic expressions to values in 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 inside the type theory (this is not possible for A; so the reason for introducing the type E is to be able to define this N).

N : E → E

One now proves the correctness lemma that states that the normalization function conserves the interpretation.

[[e]]_{ρ} =_{A} [[N (e)]]_{ρ}

Then, to reason about the domain A that [[−]] maps to, one first a valuation ρ and syntactic expressions in E which map under [[−]]_{ρ} to the terms that one want to reason about, and after that one uses the lemma to do the equational reasoning.

For instance, suppose that one wants to prove a =_{A} b. One finds e, f and ρ with [[e]]_{ρ} = a and [[f]]_{ρ} = b. Now if N (e) = N (f) then we get a = [[e]]_{ρ} =_{A} [[N (e)]]_{ρ} = [[N (f)]]_{ρ} =_{A} [[f]]_{ρ} = b. (Clearly this uses the correctness lemma twice, see Figure 1.) Note that the operation of finding an expression in E that corresponds to a given expression in A (dotted arrows) is not definable in the type theory, and needs to be implemented outside of it. In a system like Coq it will be implemented in ML or in the tactic language L_{tac}.

[figure: e ∈ E; N; [[−]]_{ρ}; N (e) = N (f); [[−]]_{ρ}; [[−]]_{ρ}; f ∈ E; N; [[−]]_{ρ}; a ∈ A; =_{A}; b ∈ A]

Fig. 1. Proving equalities

Things get more interesting when the syntactic expressions in E contain partial operations, like division. In that case the interpretation [[e]]_{ρ} will not always be defined. To address this we generalized the method of reflection to partial reflection. The naive way to do this is to define a predicate

wf_{ρ} : E → Prop

that tells whether an expression is well-formed. Then the interpretation function takes another argument of type wf_{ρ}(e).

[[−]]_{ρ} : Π_{e:E}. wf_{ρ}(e) → F

The problem with this approach is that the definition of wf needs the interpretation function [[−]]. Therefore the inductive definition of wf and the recursive definition of [[−]] need to be given simultaneously. This is called an inductiverecursive definition. Inductive-recursive definitions are not supported by the Coq system, and for a good reason: induction-recursion makes a system significantly stronger. In set theory it corresponds to the existence of a Mahlo cardinal [5].

The solution from [7] for doing partial reflection without induction-recursion, is to replace the interpretation function with an inductively defined interpretation relation.

][_{ρ} ⊆ E × A

The relation [[e]]_{ρ} = a now becomes e ][_{ρ} a. It means that the syntactic expression e is interpreted under the valuation ρ by the object a. The lemmas that one then proves are the following.

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

The first lemma states that the interpretation relation is functional, and the second lemma is again the correctness of the normalization function. Note that it is not an equivalence but just an implication. This is the only direction that is needed. It is easy to see that in fact in our application the equivalence does not hold.^{3}

3 A simple example is e = 1/(1/0), which does not relate to any a. Its normal form is 0/1, which interprets to 0.

For each syntactic expression e that one constructs for an object a, one also needs to find an inhabitant of the statement e ][_{ρ} a. In [7] a type Ē_{ρ}(a) of proof loaded syntactic expressions is introduced to make this easier. These types correspond to the expressions that evaluate to a. They are mapped to the normal syntactic expressions by a forgetful function

|−| : Ē_{ρ}(a) → E

and they satisfy the property that for all ē in the type Ē_{ρ}(a)

|ē| ][_{ρ} a.

In this paper we will not further go into this, although everything that we do also works in the presence of these proof loaded syntactic expressions.

3 Normalization Function

We will now describe how we defined the normalization function for our main example of rational expressions. Here the type E of syntactic expressions is given by the following grammar.

E ::= ℤ | 𝕍 | E + E | E · E | E/E

In this ℤ are the integers, and 𝕍 is a countable set of variable names (in the Coq formalization we use a copy of the natural numbers for this). Variables will denoted by x, y, z, integers by i, j, k. The elements of this type E are just syntactic objects, so they are different kind of objects from the values of these expressions in specific fields. Note that in these expressions it is possible to divide by zero: 0/0 is one of the terms in this type.

Other algebraic operations are defined as an abbreviation from operations that occur in the type. For instance, subtraction is defined by

e − f ≡ e + (−1) · f

We now will describe how we define the normalization function N (e) that maps an element of E to a normal form. As an example, the normal form of \frac{1}{x−y} + \frac{1}{x+y} is

N (\frac{1}{x − y} + \frac{1}{x + y}) = \frac{x · 2 + 0}{x · x · 1 + y · y · (−1) + 0}.

This last expression is the “standard form” of the way one would normally write this term, which is

\frac{2x}{x^{2} − y^{2}} .

From this example it should be clear how the normalization function works: it multiplies everything out until there is just a quotient of two polynomials left. These polynomials are then in turn written in a “standard form”. The expressions in normal form are given by the following grammar.

F ::= P/P
P ::= M + P | ℤ
M ::= 𝕍 · M | ℤ

In this grammar F represents a fraction of two polynomials, P are the polynomials and M are the monomials. One should think of P as a “list of monomials” (where + is the “cons” and the integers take the place of the “nil”) and of M as a “list of variables” (where · is the “cons” and again the integers take the place of the “nil”).

On the one hand we want the normalization function to terminate, but on the other hand we want the set of normal forms to be as small as possible. We achieve this by requiring the polynomials and monomials to be sorted; furthermore, no two monomials in a polynomial can have exactly the same set of variables. Thus normal forms for polynomials will be unique.

For this we have an ordering of the variable names. So the “list” that is a monomial has to be sorted according to this order on 𝕍, and the “list” that is a polynomial also has to be sorted, according to the corresponding lexicographic ordering on the monomials. If an element of P or M is sorted like this, and monomials with the same set of variables have been collected together, we say it is in normal form.

Now to define N we have to “program” the multiplying out of E expressions together with the sorting of monomials and polynomials, and collecting factors and terms. This is done in a systematic way. Instead of first multiplying out the expressions and then sorting them to gather common terms, we systematically combine these two things.

We recursively define the following functions (using the Fixpoint operation of Coq).

− ·_{M ℤ} − : M × ℤ → M
− ·_{M 𝕍} − : M × 𝕍 → M
− ·_{MM} − : M × M → M
− +_{MM} − : M × M → M
− +_{PM} − : P × M → P
− +_{PP} − : P × P → P
− ·_{PM} − : P × M → P
− ·_{PP} − : P × P → P
− +_{FF} − : F × F → F
− ·_{FF} − : F × F → F
− /_{FF} − : F × F → F

(Actually, all these functions have all type

E × E → E

as we do not have separate types for F, P and M. However, the idea is that they only will be called with arguments that are of the appropriate shape and in normal form. In that case the functions will return the appropriate normal form. If the other case it will return any term that is equal to the sum or product of the arguments — generally we just use the sum or product of the arguments.)

For example, the multiplication function ·_{MM} looks like

e ·_{MM} f := \{ \begin{matrix}f ·_{M ℤ} i & if e = i ∈ ℤ \\ (e_{2} ·_{MM} f) ·_{MV} e_{1} & if e = e_{1} · e_{2} \\ e · f & otherwise \end{matrix}

and the addition function +_{PM} is^{4}

e +_{PM} f := \{ \begin{matrix}i +_{MM} j & if e = i ∈ ℤ, f = j ∈ ℤ \\ f + i & if e = i ∈ ℤ \\ e_{1} + (e_{2} +_{PM} i) & if e = e_{1} + e_{2}, f = i ∈ ℤ \\ e_{2} +_{PM} (e_{1} +_{MM} f) & if e = e_{1} + e_{2}, e_{1} = f \\ e_{1} + (e_{2} +_{PM} f) & if e = e_{1} + e_{2}, e_{1} <_{lex} f \\ f + e & if e = e_{1} + e_{2}, e_{1} >_{lex} f \\ e + f & otherwise \end{matrix}

where the lexicographic ordering <_{lex} is used to guarantee that the monomials in the result are ordered.

Finally we used these functions to recursively “program” the normalization function. For instance the case where the argument is a division is defined like

N (e/f) := N(e) /_{FF} N(f).

The base case (when e is a variable) looks like

N (v) := \frac{v · 1 + 0}{1}.

To prove that a = b, then, one builds the expression corresponding to a − b and checks that this normalizes to an expression of the form 0/e. (This turns out to be stronger than building expressions e and f interpreting to a and b and verifying that N (e) = N (f), since normal forms are in general not unique.)

4 Uninterpreted Function Symbols

When one starts working with the tactic defined as above, one quickly finds out that there are situations in which it fails because two terms which are easily seen to be equal generate two expressions whose difference fails to normalize to 0. A simple example arises is when function symbols are used; for example, trying to prove that

f(a + b) = f(b + a)

4 In the fourth case, the equality e_{1} = f is equality as lists, meaning that they might differ in the integer coefficient at the end.

will fail because f(a + b) will be syntactically represented as a variable x and f(b + a) as a (different) variable y, and the difference between these expressions normalizes to

\frac{x · 1 + y · (−1) + 0}{1},

which is not zero.

In this section we describe how the syntactic type E and the normalization function N can be extended to recognize and deal with function symbols. The actual implementation includes unary and binary total functions, as well as unary partial functions (these are binary functions whose second argument is a proof)^{5}. We will discuss the case for unary total functions in detail; binary and partial functions are treated in an analogous way.

Function symbols are treated much in the same way as variables; thus, we extend the type E of syntactic expressions with a new countable set of function variable names 𝕍_{1}, which is implemented (again) as the natural numbers. The index 1 stands for the arity of the function; the original set of variables is now denoted by 𝕍_{0}. Function variables will be denoted u, v.

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

Intuitively, the normalization function should also normalize the arguments of function variables. The grammar for normal forms becomes the following.

F ::= P/P
P ::= M + P | ℤ
M ::= 𝕍_{0} · M | 𝕍_{1}(F) · M | ℤ

But now a problem arises: the extra condition that both polynomials and monomials correspond to sorted lists requires ordering not only variables in 𝕍_{0}, but also expressions of the form 𝕍_{1}(F). The simplest way to do this is by defining an ordering on the whole set E of expressions.

This is achieved by ordering first the sets 𝕍_{0} and 𝕍_{1} themselves. Then, 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).

With this different ordering, the same normalization function as before can be used with only trivial changes. In particular, the definitions of the functions ·_{MM}

5 Other possibilities, such as ternary functions or binary partial functions, were not considered because this work was done in the setting of the C-CoRN library, where these are the types of functions which are used in practice.

and +_{PM} stay unchanged. Only at the very last step does one have to add a rule saying that

N (v(e)) := \frac{v(N (e)) · 1 + 0}{1}.

Notice the similarity with the rule for the normal form of variables.

The next step is to change the interpretation relation. Instead of the valuation ρ, we now need two valuations

ρ_{0} : 𝕍_{0} → A
ρ_{1} : 𝕍_{1} → (A → A)

and the inductive definition of the interpretation relation is extended with the expected constructor for interpreting expressions of the form v(e).

As before, one can again prove the two lemmas

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

Now, our original equality f(a + b) = f(b + a) can easily be solved: f(a + b) can now be more faithfully represented by the expression v(x + y), where ρ_{1}(v) = f, ρ_{0}(x) = a and ρ_{0}(y) = b; the syntactic representation of f(b + a) becomes v(y + x); and each of these normalizes to

\frac{v (\frac{x·1+y·1+0}{1}) · 1 + 0}{1},

so that their difference normalizes to 0 as was intended.

Adding binary functions simply requires a new sort 𝕍_{2} of binary function symbols and extend the type of expressions to allow for the like of v(e, f); the normalization function and the interpretation relation can easily be adapted, the latter requiring yet another valuation

ρ_{2} : 𝕍_{2} → (A × A → A).

Partial functions are added likewise, using a sort V_{1̸} for partial function symbols and a valuation

ρ_{1̸} : 𝕍_{1̸} → (A ↛ A).

As was already the case with division, one can write down expressions like v(e) even when ρ_{1̸}(v) is not defined at the interpretation of e; the definition of ][_{ρ_{0},ρ_{1},ρ_{1̸},ρ_{2}} ensures that only correctly applied partial functions will be interpreted.

5 Hierarchical Reflection

The normalization procedure described in Section 3 was used to define a tactic which would prove algebraic equalities in an arbitrary field in the context of the Algebraic Hierarchy of [6].

In this hierarchy, fields are formalized as rings with an extra operation (division) which satisfies some properties; rings, in turn, are themselves Abelian groups where a multiplication is defined also satisfying some axioms. The question then arises of whether it is possible to generalize this mechanism to the different structures of this Algebraic Hierarchy. This would mean having three “growing” types of syntactic expressions E_{G}, E_{R} and E_{F} (where the indices stand for groups, rings and fields respectively) together with interpretation relations^{6}.

\xymatrix{E_{F} \ar[r]^{][_{ρ}^{F}} & F : Field \ar[d] \\ E_{R} \ar[u]^{⊆} \ar[r]^{][_{ρ}^{R}} & R : Ring \ar[d] \\ E_{G} \ar[u]^{⊆} \ar[r]^{][_{ρ}^{G}} & G : Group}

However one can do better. The algorithm in the normalization function works outwards; it first pushes all the divisions to the outside, and then proceeds to normalize the resulting polynomials. In other words, it first deals with the field-specific part of the expression, and then proceeds working within a ring. This suggests that the same normalization function could be reused to define a decision procedure for equality of algebraic expressions within a ring, thus allowing E_{F} and E_{R} to be unified.

Better yet, looking at the functions operating on the polynomials one also quickly realizes that these will never introduce products of variables unless they are already implicitly in the expression (in other words, a new product expression can arise e.g. from distributing a sum over an existing product, but if the original expression contains no products then its normal form will not, either). So our previous picture can be simplified to this one.

[figure: E; ][_{ρ}^{F}; ][_{ρ}^{R}; ][_{ρ}^{G}; F : Field; R : Ring; G : Group]

6 For simplicity we focus on the setting where function symbols are absent; the more general situation is analogous.

The key idea is to use the partiality of the interpretation relation to be able to map E into a ring R or a group G. In the first case, expressions of the form e/f will not be interpreted; in the latter, neither these nor expressions of the form e · f relate to any element of the group.

There is one problem, however. Suppose x is a variable with ρ(x) = a; then a + a is represented by x + x, but

N (x + x) = \frac{x · 2 + 0}{1} ][_{ρ}^{G} a + a

does not hold.

In order to make sense of the normal forms defined earlier, one needs to interpret the special cases e/1 in groups and rings, as well as e·f with f = i ∈ ℤ in groups (assuming, of course, that e can be interpreted).

We summarize what each of the interpretation relations can interpret in the following table.

][_{ρ}^{G}  ][_{ρ}^{R}  ][_{ρ}^{F}
v ∈ 𝕍  yes  yes  yes
i ∈ ℤ  if i = 0  yes  yes
e + f  yes  yes  yes
e · f  if f ∈ ℤ  yes  yes
e/f  if f = 1  if f = 1  if f ≠ 0

In the last three cases the additional requirement that e and f can be interpreted is implicit.

Once again, one has to prove the lemmas

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

and analogous for ][_{ρ}^{R} and ][_{ρ}^{F}.

In these lemmas, one needs to use the knowledge that the auxiliary functions will only be applied to the “right” arguments to be able to finish the proofs. This is trickier to do for groups than for rings and fields. For example, while correctness of ·_{MM} w.r.t. ][_{ρ}^{F} is unproblematic, as it states that

e ][_{ρ}^{F} a ∧ f ][_{ρ}^{F} b ⇒ e ·_{MM} f ][_{ρ}^{F} a · b,

the analogue of this statement for ][_{ρ}^{G} cannot be written down, as a · b has no meaning in a group. However, by the definition of ][_{ρ}^{F}, this is equivalent to the following.

e · f ][_{ρ}^{F} a · b ⇒ e ·_{MM} f ][_{ρ}^{F} a · b

Now this second version does possess an analogue for ][_{ρ}^{G}, by replacing the expression a · b with a variable.

e · f ][_{ρ}^{G} c ⇒ e ·_{MM} f ][_{ρ}^{G} c.

This is still not provable, because ·_{MM} can swap the order of its arguments. The correct version is

e · f ][_{ρ}^{G} c ∨ f · e ][_{ρ}^{G} c ⇒ e ·_{MM} f ][_{ρ}^{G} c;

the condition of this statement reflects the fact that the normalization function will only require computing e ·_{MM} f whenever either e or f is an integer.

The implementation of the tactic for the hierarchical case now becomes slightly more sophisticated than the non-hierarchical one. When given a goal a =_{A} b it builds the syntactic representation of a and b as before; and then looks at the type of A to decide whether it corresponds to a group, a ring or a field. Using this information the tactic can then call the lemma stating correctness of N w.r.t. the appropriate interpretation relation.

Optimization

As was mentioned in Section 3, normal forms for polynomials are unique, contrarily to what happens with field expressions in general. This suggests that, when A is a group or a ring, the decision procedure for a =_{A} b can be simplified by building expressions e and f interpreting respectively to a and b and comparing their normal forms. Clearly, this is at most as time-consuming as the previous version, since computing N (e − f) requires first computing N (e) and N (f).

Also, since the normalization function was not defined at once, but resorting to the auxiliary functions earlier presented, it is possible to avoid using divisions altogether when working in rings and groups by defining directly N′ by e.g.

N′(e + f) = N′(e) +_{PP} N (f)′;

the base case now looks like

N′(v) = v · 1 + 0.

Notice that although we now have two different normalization functions we still avoid duplication of the code, since they are both defined in terms of the same auxiliary functions and these are where the real work is done.

6 Tighter Integration

In the previous section we managed to avoid having different syntactic expressions for the different kinds of algebraic structures. We unified the types of syntactic expressions into one type E.

However we still had different interpretation relations ][_{ρ}^{F}, ][_{ρ}^{R} and ][_{ρ}^{G}. We will now analyze the possibility of unifying those relations into one interpretation relation ][_{ρ}^{S}. This turns out to be possible, but when one tries to prove the relevant lemmas for it one runs into problems: to get the proofs finished one needs to assume an axiom (in the type theory of Coq).

Every field, ring or group has an underlying carrier. We will write Â for the carrier of an algebraic structure A. We now define an interpretation relation ][_{ρ}^{S} from the type of syntactic expressions E to an arbitrary set^{7} S, where that set is a parameter of the inductive definition. This inductive definition quantifies over different kinds of algebraic structures in the clauses for the different algebraic operations. For instance the inductive clause for addition quantifies over groups.

Π_{G:Group}Π_{e,f:E}Π_{a,b,c:Ĝ} (a +_{G} b =_{G} c) → (e ][Ĝ ; ρ a) → (f ][Ĝ ; ρ b) → (e + f ][Ĝ ; ρ c)

With this definition the diagram becomes the following.

[figure: E; ][_{ρ}^{S}; F : Field; R : Ring; G : Group; ˆ ·; S : Set]

This gives a nice unification of the interpretation relations. However when one tries to prove the relevant lemmas for it in Coq, the obvious way does not work. To prove e.g.

e ][_{ρ}^{S} a ∧ e ][_{ρ}^{S} b ⇒ a =_{A} b

one needs to use inversion with respect to the inductive definition of ][_{ρ}^{S} to get the possible ways that e ][_{ρ}^{S} a can be obtained; but the Inversion tactic of Coq then only produces an equality between dependent pairs where what one needs is equality between the second components of those pairs. In Coq this is not derivable without the so-called K axiom, which states uniqueness of equality proofs.

             (A:Set; x:A; p:(x=x))p==(refl_equal A x)

We did not want to assume an axiom to be able to have our tactic prove equalities in algebraic structures that are clearly provable without this axiom. For this reason we did not fully implement this more integrated version of hierarchical reflection.

7 In the formalization we actually have setoids instead of sets, but that does not make a difference.

7 Conclusion

7.1 Discussion

We have shown how the Rational tactic (first described in [7]), which is used to prove equalities of expressions in arbitrary fields, can be generalized in two distinct directions.

First, we showed in Section 4 how this tactic could be extended so that it would also look at the arguments of functions; the same mechanism can be applied not only to unary total functions, as explained, but also to binary (or nary) functions, as well as to partial functions as defined in the C-CoRN library [3].

In Section 5 we discussed how the same syntactic type E and normalization function N could be reused to define similar tactics that will prove equalities in arbitrary rings or commutative groups. The work here described has been successfully implemented in Coq, and is intensively used throughout the whole C-CoRN library.

Further extensions of this tactic are possible; in particular, the same approach easily yields a tactic that will work in commutative monoids (e.g. the natural numbers with addition). For simplicity, and since this adds nothing to this presentation, this situation was left out of this paper.

Extending the same mechanism to non-commutative structures was not considered. The normalization function intensively uses commutativity of both addition and multiplication, so it cannot be reused for structures that do not satisfy these; and the purpose of this work was to reuse as much of the code needed for Rational as possible.

The correctness of the normalization function w.r.t. the interpretation relation had to be proved three times, one for each type of structure. In Section 6 we showed one possible way of overcoming this, that unfortunately failed because proving correctness of the tactic would then require assuming an axiom which is not needed to prove the actual equalities that the tactic is meant to solve.

A different approach to the same problem would be to use the constructor subtyping of [2]. This would allow one to define e.g. the interpretation relation for rings ][_{ρ}^{R} by adding one constructor to that for groups ][_{ρ}^{G}; proving the relevant lemmas for the broader relation would then only require proving the new case in all the inductive proofs instead of duplicating the whole code.

Another advantage of this solution, when compared to the one explored in Section 6, would be that the tactic could be programmed and used for e.g. groups before rings and fields were even defined. It would also be more easily extended to other structures. Unfortunately, constructor subtyping for Coq is at the moment only a theoretical possibility which has not been implemented.

It would be interesting to know whether the approach from Section 6 can be made to work without needing the K axiom for the proofs of the correctness lemmas.

Acknowledgments. Support for the first author was provided by the Portuguese Fundação para a Ciência e Tecnologia, under grant SFRH / BD / 4926 / 2001, and by the FCT and FEDER via CLC.

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. Gilles Barthe and Femke van Raamsdonk. Constructor subtyping in the Calculus of Inductive Constructions. In Jerzy Tiuryn, editor, Proceedings 3rd Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS’2000, Berlin, Germany, 25 March – 2 Apr 2000, volume 1784, pages 17–34, Berlin, 2000. Springer-Verlag.

3. Constructive Coq Repository at Nijmegen. http://www.cs.kun.nl/fnds/ccorn.

4. L. Cruz-Filipe, H. Geuvers, and F. Wiedijk. C-CoRN: the Constructive Coq Repository at Nijmegen. to appear.

5. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1–47, 2003.

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.

8. Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Eli Barzilay, Yegor Bryukhov, Richard Eaton, Adam Granicz, Alexei Kopylov, Christoph Kreitz, Vladimir N. Krupski, Lori Lorigo, Stephan Schmitt, Carl Witty, and Xin Yu. MetaPRL — A modular logical environment. In David Basin and Burkhart Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), volume 2758 of LNCS, pages 287–303. Springer-Verlag, 2003.

9. Xin Yu, Aleksey Nogin, Alexei Kopylov, and Jason Hickey. Formalizing abstract algebra in type theory with dependent records. In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pages 13–27. Universität Freiburg,