Posted on July 1, 2017 by Calvin Beck

Tags: coq, theorem proving, proofs, dependent types, pattern matching

# Induction

Working with dependent types in Coq has been causing me a number of headaches — which I have found somewhat surprising coming from Agda / Idris.

I believe part of this is syntactic, and that Agda for instance kind of has you working with terms in a dependently typed language in the raw, unlike Coq which often has you using tactics, which are a bit of a step away from what’s actually going on. But the other part seems to be that Agda includes this so called “axiom K” by default, and Coq does not.

## What is axiom K?

## Dependent pattern matching in Coq. The “convoy” pattern.

## Dealing with absurd cases.

In Agda you might use the absurd pattern to deal with branches of a program which should never be executed due to a condition which will never hold. I.e., if the condition to enter the branch is true, then that condition implies False.

```
hd {X} (xs : list X) (length xs > 0) : X
```

For instance, in the case of a `hd`

function, which takes the first element of the list, you might have an argument that’s a proof that the length of the list is greater than 0. But, you still have to provide a case to the match on the list for when it’s empty.

Well, that’s okay. Because in Coq we can use an empty pattern match on False. So you might think you can do something like this:

```
Require Import List.
Lemma length_nil_not_gt_0 :
forall {X}, @length X nil > 0 -> False.
Proof.
intros X H. inversion H.
Qed.
Definition hd {X} (xs : list X) (pf : length xs > 0) : X :=
match xs with
| nil => match length_nil_not_gt_0 pf with end
| h :: t => h
end.
```

But this doesn’t quite work.

```
Error:
In environment
X : Type
xs : list X
pf : length xs > 0
The term "pf" has type "length xs > 0" while it is expected to have type
"length nil > 0".
```

For some reason Coq seems to not be recognizing that in this branch `xs = nil`

, and so it’s not replacing `xs`

with `nil`

when it’s typechecking.

So, how can we get around this? What seems to be happening is that `pf`

is getting tied to the type `length xs > 0`

at the beginning, at the very top level.

The way to get around this is to make `hd`

actually return a function, which takes a proof as an argument. This lets the `pf`

have a different type in each branch.

```
Require Import List.
Lemma length_nil_not_gt_0 :
forall {X}, @length X nil > 0 -> False.
Proof.
intros X H. inversion H.
Qed.
Definition hd {X} (xs : list X) : (length xs > 0) -> X :=
match xs with
| nil => fun pf => match length_nil_not_gt_0 pf with end
| h :: t => fun _ => h
end.
```