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.
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.