Strategies for representing proofs of equality

Question

I am interested in strategies for representing proof terms inside the kernel of a proof assistant, specifically proofs of equality.

What are the different strategies that are available for representing proofs of equality inside the kernel of a proof assistant?

My question is motivated by learning about nth_rewrite in Lean for use in the natural numbers game, which made me realize I don't actually know what rewrite-like tactics are doing under the hood in the kernel of a "prototypical" proof assistant.

Note that this question is deliberately agnostic about whether my underlying logic is constructive or classical, but I just assume that we have the deduction theorem so I can paraphrase away uses of non-modus-ponens-like inference rules. My question is also agnostic about whether I have equality types or a separate notion of an equality judgment that is not part of the type hierarchy (I don't know the technical merits of one choice vs the other (or if any serious proof assistants have equality judgments that are not types)).

I think that rules like modus ponens $\frac{A \to B \;\; \text{and} \;\; A}{B}$ and universal instantiation $\frac{\forall x : S \mathop. \varphi(x) \;\;\text{and}\;\; \text{$t$ is a term of sort $S$}}{\varphi(t)}$ can be represented internally as something kind of like a function application.

Other inference rules like $\frac{A \land B}{A}$ can be represented as axioms $A \land B \to A$ and modus ponens.

However, I have no idea how one would represent proofs of equalities like $s = t$.

For example, suppose I knew $s = t$ and I wanted to prove that $s * s = s * t$.

I know that $s * s = s * s$ holds by reflexivity, so I probably need something like $\text{refl}(\alpha) : \alpha = \alpha$ for all $\alpha$.

Cool, I have my proof, $\text{refl}{s * s} : s * s = s * s$.

However, I now need to change that into $s * s = s * t$. If I naively apply $s * t$ as a rewrite, I will end up with $t * t = t * t$ or something, I need to control which part of $s * s$ gets rewritten.

In Coq, as a user, I would use setoid_rewrite or similar to achieve this and to target just the site that I'm interested in.

Inside a kernel, I can imagine having $\text{nthRewrite}(\beta, 47, \alpha : s = t)$ as a proof of $\beta = \beta[s :=^ {47} t]$ where $[s :=^ {47} t]$ denotes replacing the $47$th occurrence of $s$ with $t$ in $\beta$. My number could also just indicate which position in the wff to replace according to some numbering scheme instead of counting unification sites.

I think that such a primitive term would actually suffice for any possible rewrite that I might want to represent, but it would be horrifically inconvenient to "reindex" the rewrites if I want to normalize proof terms.

I cloud also imagine using something similar to the Leibniz inference rule in equational logic, but I don't know how the details would work out.

Answer 1

Actually, your proposed scheme for $\mathrm{nthRewrite}$ is quite close to a version of Leibniz's equality (the wikipedia page you linked is a bit strange, I find this one clearer). This is the usual way propositional equality can be used in proof assistants – there are variations, but they mostly agree on this part.

The rule is often called transport, and it says the following: assume that

• $P$ is a proposition with (at least) one free variable $x$
• we can show $P[x := s]$ for some $s$
• we can show $s = t$

then we deduce $P[x := t]$. In a dependent type theory, we would have a rule like the following (equality is indexed by the type of the objects it relates): $$ \frac{ \vdash e : s =_{A} t \quad x : A \vdash P : \mathrm{Prop} \quad \vdash p : P[x := s] }{ \vdash \mathrm{transp}(e,x.P,p) : P[x := t] } $$ This is a neat primitive, both very general and well-behaved, so we like it!

Now, back to your question: what does $\mathrm{nthRewrite}$ do? The point is that, in general, when you are faced with a goal $P[x := t]$, you need to identify what $P$ is. There are in general multiple possibilities, and Lean can't guess by itself which exactly is the one you intend! For instance if the goal is $t + 0 = k + m + t$, there are four different $P$, depending on which occurrences of $t$ you select (none, the first one, the second one, or both).

What $\mathrm{nthRewrite}$ does is roughly as follows:

• take in a proof of $s = t$ and an integer $n$
• find the $n$-th occurrence of $s$ in the current goal $G$
• build $P$ that replaces that $n$-th occurrence of $s$ with a variable $x$ (thus, $G$ is $P[x := s]$)
• use transport along the proof of equality with that $P$ to turn the goal into a new goal $P[x := t]$, which amounts to $G$ but where the $n$-th occurrence of $s$ has been replaced with $t$

In short, $\mathrm{nthRewrite}$ is a handy way of letting Lean figure out exactly the $P$ and transport you are after. But the latter is a more general and simpler primitive (for instance, it does not depend on the textual order in which things are represented, which is a recipe for disaster!), and so this is typically what kernels implement.

A last subtle but important note: in dependent type theory, the action of "abstracting over a subterm" is not always a valid operation! That is, if we take a goal $G$ and build some $P$ such that $P[x := s]$ is $G$, it is not guaranteed that $P$ is always well-formed. This can only happen in relatively complicated cases which involve type dependency, but can be a real source of headaches and cryptic errors – in Coq, they are usually phrased as Error: cannot abstract over …