I’m trying to use Equations package to define a function over vectors in Coq. The minimum code that shows the problem that I will describe is available at the following gist:
My idea is to code a function that does a lookup on a “proof” that some type holds for all elements of a vector, which has a standard definition:
Inductive vec (A : Type) : nat -> Type :=
| VNil : vec A 0
| VCons : forall n, A -> vec A n -> vec A (S n).
Using the previous type, I had defined the following (also standard) lookup operation (using Equations):
Equations vlookup {A}{n}(i : fin n) (v : vec A n) : A :=
vlookup FZero (VCons x _) := x ;
vlookup (FSucc ix) (VCons _ xs) := vlookup ix xs.
Now, the trouble begins. I want to define the type of “proofs” that some property holds for all elements in a vector. The following inductive type does this job:
Inductive vforall {A : Type}(P : A -> Type) : forall n, vec A n -> Type :=
| VFNil : vforall P _ VNil
| VFCons : forall n x xs,
P x -> vforall P n xs -> vforall P (S n) (VCons x xs).
Finally, the function that I want to define is
Equations vforall_lookup
{n}
{A : Type}
{P : A -> Type}
{xs : vec A n}
(idx : fin n) :
vforall P xs -> P (vlookup idx xs) :=
vforall_lookup FZero (VFCons _ _ pf _) := pf ;
vforall_lookup (FSucc ix) (VFCons _ _ _ ps) := vforall_lookup ix ps.
At least to me, this definition make sense and it should type check. But, Equations had showed the following warning and left me with a proof obligation in which I had no idea on how to finish it.
The message presented after the definition of the previous function is:
Warning:
In environment
eos : end_of_section
fix_0 : forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n)
(idx : fin n) (v : vforall P xs),
vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)
A : Type
P : A -> Type
n0 : nat
x : A
xs0 : vec A n0
idx : fin n0
p : P x
v : vforall P xs0
Unable to unify "VFCons P n0 x xs0 p v" with "v".
The obligation left is
Obligation 1 of vforall_lookup_ind_fun:
(forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n)
(idx : fin n) (v : vforall P xs),
vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)).
Later, after looking at a similar definition in Agda standard library, I realised that the previous function definition is missing a case for the empty vector:
lookup : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} →
(i : Fin k) → All P xs → P (Vec.lookup i xs)
lookup () []
lookup zero (px ∷ pxs) = px
lookup (suc i) (px ∷ pxs) = lookup i pxs
My question is, how can I specify that, for the empty vector case, the right-hand side should be empty, i.e. a contradiction? The Equations manual shows an example for equality but I could adapt it to this case. Any idea on what am I doing wrong?