Trouble in implementing dependently typed lookup in Coq using Equations

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
            {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:

  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?

Hi Rodrigo, you’re not doing anything wrong, it’s the Equations generation of the elimination principle that was having some trouble, but vforall_lookup is defined correctly. The bug is fixed in Equations’s master branch which will become the 1.2 release soon, in the meantime you can disable the generation of the elimination principle using the (noind) option: Equations(noind) vforall_lookup ....
There’s no need to give an empty pattern to rule out the empty case here, Equations can figure it out by itself.

1 Like

Hi Matthieu, thanks for your answer! It works fine now!