Binding variables to terms involving later variables

Question

Consider the following pseudocode in a hypothetical proof assistant:

def f (n : ℕ) : P n
  := match n with
     | zero -> ?0
     | suc k -> ?1
     end

Under what seems to me to be the most natural approach to parsing this code, the variable n scopes over the rest of the definition after it appears, while the variable k scopes over its branch ?1. Since k is encountered later, it will be added to the context later, and so the context of the branch ?1 will then be something like

n : ℕ
k : ℕ

Except, in that branch the match variable n is supposed to be specialized to suc k. That certainly has to happen in the type: in that branch we have to give a term of type P (suc k). But it's hard to imagine forbidding the user from explicitly writing n inside that branch either; from the user's perspective that would amount to removing variables from the context, which is weird and unintuitive. So to allow the user to write n but ensure that it's equal to suc k, it seems that the context of the branch ?1 must be something like

n : ℕ := suc k
k : ℕ

Allowing some of the variables in a context to come with definitions (i.e. to be "let-bound") is fairly standard. But here we have a variable that occurs earlier in the context being let-bound to equal a term in which appears a variable that occurs later in the context. Mathematically, this is impossible under the usual inductive definition of contexts according to which we can extend a context with a variable belonging to a type in that context and possibly having a value in that context:

$$ \frac{\Gamma \vdash A\,\mathsf{type}}{(\Gamma, x:A)\,\mathsf{ctx}}\hspace{1cm} \frac{\Gamma \vdash A\,\mathsf{type}\quad \Gamma \vdash a:A}{(\Gamma, x:A := a)\,\mathsf{ctx}}$$

In an NbE-style implementation that separates De-Bruijn-index "terms" from De-Bruijn-level "values", and uses values for the types and values in a context, it is technically possible for a variable to have a value incorporating later variables. For example, one approach is for every (index) variable in a context to have a "value" which might be just "itself"; then our weird context would be

index1 : ℕ := suc level1
index0 : ℕ := level1

But this seems fraught with peril. In particular, when typechecking the branch, how do we define the transformation that takes the initial context such as n : ℕ, adds a variable to it, and then binds the existing variable n to a term involving the new later variable? In particular, there could be other variables in the initial context whose types and values involve n -- in its incarnation as a level variable in that context -- and which will need to be specialized to the new value of n, and part of the point of NbE is to avoid ever having to substitute for a level variable.

What is the best way to deal with this issue? How do existing proof assistants do it?

Edited to add: I don't think the solution can be quite as simple as just adding the new variable(s) in place of the match variable n or right before it. If the datatype is indexed, then the indices also have to be specialized depending on the branch, and so the new variables have to appear before all the indices (assuming they are all variables, as in the simplest sort of pattern-match on an indexed datatype without fancy unification). But there might be parameters on which the type of the new variables depend but which originally appear after these index variables in the context. For instance, consider:

data Vec (A : Type) : ℕ → Type
  nil : Vec A 0
  cons : (n : ℕ) → A → Vec A n → Vec A (suc n)

f (n : ℕ) (A : Type) (v : Vec A n) : P n A v
  := match v with
     | nil -> ?0
     | cons k a w -> ?1
     end

Now in the branch ?1, not only must we have v := cons k a w, we must specialize the index n := suc k. Thus, if we are simply inserting the new variables (k : ℕ) (a : A) (w : Vec A k) somewhere in the context (n : ℕ) (A : Type) (v : Vec A n), we have to insert them at the beginning so that the value n := suc k can depend on the variable k appearing before it:

k : ℕ
a : A
w : Vec A k
n : ℕ := suc k
A : Type
v : Vec A n := cons k a w

But now the variable a has a type A that depends on the parameter variable A that appears after it! So it seems that some more complicated shuffling or permuting of contexts is required, or else to represent contexts in some more nonlinear DAG-like way in the first place.

It sounds like maybe Agda is the only extant proof assistant that does anything like this, so I guess this is a question mostly about the implementation of Agda.

Answer 1

Great question Mike!

Since Thierry Coquand's talk at the 1991 TYPES meeting in Edinburgh, and reading Martin Löf's "Mathematics of infinity" paper, and various things by Thierry subsequently, I think the 'right' (mathematical!) way to understand these 'let-bindings' (which I think is not the right way to see them, at least on a first cut) is via context morphisms, together with a suitable notion, for pattern matching, of when a collection of context morphisms 'covers' another context (in the Grothendieck topology/crible sense).

From this point of view, the contexts in which each RHS of the evolving case tree are well typed are distinct (they just look as though they 'share' bindings), but they are all suitably correlated by the morphisms between them which furnish the 'let'-like instantiations. The 'evolving' nature of the pattern analysis also fits well with contexts-and-morphisms as a mathematically satisfactory account of 'stages of knowledge' along more traditional Brouwerian/sheaf-theoretic lines.

Whether or not any of our implementations actually realises this conceptual analysis is another matter.

Answer 2

Coq (and probably Lean too):

The answer for (vanilla) Coq is simple: it does not. Nothing is done to n to remember its relation to the pattern in the branch. The only way to keep a relation is to channel it through P. The usual technique is what has been called the convoy pattern by Chlipala, which adds an extra equality in P to recover that missing relation. In practice, this is what the fancier tools (Program, Equations) give you.

So with a little bit of work, you get a propositional equality. This is fairly generic, but also somewhat weak compared to a definitional equality in context (be it as a definitional equality, as in Andromeda, or a defined variable, as you suggest). The advantage is that it is relatively simple (and thus can be automated), and elaborates back to the "simple" pattern-matching. And as Andrej remarks, it works equally well if n is not a variable.

Agda:

Agda does something smarter, the only source I know of is Jesper Cockx's talk at Types '23 (here, around 7:30). Basically, when case-splitting on x you insert the variables corresponding to the pattern in the context at the place where x was. In the rules given in the talk, you then simply erase x, and apply the relevant substitution to the rest of the context and motive. If you have definitions in contexts, then you could insert the new variables just before x, and make x a definition (this is really a different way to represent the substitution).

The main drawback is that this only works if the case-split is on a variable. And you cannot just get around by doing something like let x := t in match x …, because your variable need to not to have a body in the context, which you would get with a let-bound one. But given the pseudo-syntax you are giving, you might be content with this.

Slightly out of topic, but having only pattern matching on variables has the other advantage that it is easier to figure out what the motive of the pattern-matching (your P) is, because the unification problem ?P t = … is much nicer to solve when t is in fact a variable.