# Matching in Types in Coq

A few days ago, I ran into a fairly ugly problem involving matches in dependent
types. This post will walk through a simplified version of this problem,
demonstrating the different solution attempts I made along the way and
explaining why they do not work, until arriving at a somewhat satisfactory
solution. While this post doesn’t contain anything groundbreaking, it might
strengthen your understanding of the effects `matches`

have on types. I won’t go
over the basics of functional or dependently typed programming. However, a sound
intuition for the matter should be sufficient to understand this post.

The example we will use throughout this post is a simple language of arithmetic
expressions `arith`

made up of binary operators and constants. Instead of
explicitly choosing which constants and operators to include, we generalize the
type `arith`

over a class of signatures `Signature`

, which specifies types containing
the operator and constant symbols. Declaring it as a class instead of a regular structure
gives us the benefit Coq of attempting to automatically infer which `Signature`

we are
trying to use, saving us some typing. We also write a recursive function `eval`

that can
evaluate an expression, given functions describing how to treat the operators and constants.

```
Class Signature := B_S { ops : Type ; consts : Type }.
Section Arith.
Context {Sigma : Signature}.
Inductive arith : Type :=
| Op : ops -> arith -> arith -> arith
| C : consts -> arith.
Fixpoint eval (oint : ops -> nat -> nat -> nat) (cint : consts -> nat) e :=
match e with
| Op o e1 e2 => oint o (eval oint cint e1) (eval oint cint e2)
| C c => cint c
end.
End Arith.
```

Having set up the basic definitions, we can move on to the problematic bits. It can
often be useful to define functions that transform a given signature. For our example, we
will consider the function `sig_ext`

which extends a signature with one new constant symbol `inr I`

.

```
Definition sig_ext (Sigma : Signature) :=
match Sigma with
B_S ops consts => B_S ops (consts + True)
end.
```

Such a signature transformation calls for a matching function on expressions. Hence,
we define a function `lift_arith`

that lifts expressions in an expression `Sigma`

to
expressions in `sig_ext Sigma`

. Our first, naive attempt would probably look like this:

```
Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
match e with
| Op o e1 e2 => Op o (lift_arith e1) (lift_arith e2)
| C c => C (inl c)
end.
```

However, Coq will reject this definition with the following gripe:

```
The term "lift_arith Sigma e1" has type "@arith (sig_ext Sigma)"
while it is expected to have type "@arith Sigma".
```

The reason for this is fairly easy to figure out. Coq has inferred that `Op`

is the
constructor to `@arith Sigma`

, as it is applied `o : @ops Sigma`

. This can be fixed by
explicitly telling Coq which variant of `Op`

we want.

```
Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
match e with
| Op o e1 e2 => @Op (sig_ext Sigma) o (lift_arith e1) (lift_arith e2)
| C c => @C (sig_ext Sigma) (inl c)
end.
```

However, Coq is still not happy with this. This time, it tells us:

```
The term "o" has type "@ops Sigma" while it is expected to have type
"@ops (sig_ext Sigma)".
```

Now, what went wrong here? Clearly, looking at the definition of `sig_ext`

, we know
that `@ops Sigma = @ops (sig_ext Sigma)`

. However, the reason Coq can not infer this
is fairly simple. Unfolding `sig_ext Sigma`

, we arrive at

```
match Sigma with B_S ops consts => B_S ops (consts + True) end
```

Coq is unable reduce this `match`

(and hence can’t infer that `o : @ops (sig_ext Sigma)`

)
as it does not know the specific makeup of `Sigma`

. If this were a proof, we would have
to do a `destruct`

of `Sigma`

to get this `match`

to reduce. The Gallina equivalent of a
`destruct`

is a `match`

, hence we have to insert a `match`

on `Sigma`

into the function
`lift_arith`

. However, this turns out to be problematic. Naively inserting the `match`

like this will not work.

```
Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
match Sigma with
B_S os cs as Sig =>
match e with
| Op o e1 e2 => @Op (sig_ext Sig) o (lift_arith e1) (lift_arith e2)
| C c => @C (sig_ext Sigma) (inl c)
end
end.
```

Coq will complain with the following message (after a `Set Printing All`

):

```
Error:
In environment
e : @arith Sigma
o : @ops Sigma
(* ... *)
The term "o" has type "@ops Sigma" while it is expected to have type
"@ops (sig_ext Sig)".
```

As we can see, the types of `e`

and `o`

are unaffected by the `match`

(we might expect them
to be of type `@arith Sig`

and `@ops Sig`

, respectively). This seemingly strange behavior
is caused by the details of how `match`

works. Intuitively, we would expect all occurrences
of `Sigma`

to be replaced by `Sig`

. However, this is not really what it does. This
replacement is only performed in our “goal” (that is, the return type of the `match`

).
In this case, this is `@arith (sig_ext Sigma)`

which is transformed into `@arith (sig_ext Sig)`

.
As `e`

is not part of the goal, it remains unchanged.

This behavior might be surprising to readers familiar with proving in Coq, as
`destruct`

does also perform these replacements in your hypothesis. However, a
quick look at the proof generated (using `Show Proof`

) will reveal that
`destruct`

cleverly reverts all the relevant hypothesis before performing the
`match`

, thereby moving them into the goal. We can fix our example by copying
that trick. That is, we revert the expression `e`

before the `match`

and reintroduce
it afterwards.

```
Fixpoint lift_arith {Sigma : Signature} (e : @arith Sigma) : @arith (sig_ext Sigma) :=
(match Sigma with
B_S os cs as Sig => fun e' : @arith Sig =>
match e' with
| Op o e1 e2 => @Op (sig_ext Sig) o (lift_arith e1) (lift_arith e2)
| C c => @C (sig_ext Sig) (inl c)
end
end) e.
```

I hope this ordeal has improved or reinforced your intuition about the effects
on types `match`

es have in Coq, just as it did for me. While this definition
looks somewhat inelegant, it is the nicest solution to this problem that I know
of. If you know an even nicer solution, please do not hesitate to contact me
with it.