[Agda] Proof involving associativity of ++ of vectors

[Shin-Cheng Mu]

Hi,

I have encountered this proof pattern a number of times, but
cannot figure out how to do the proof in Agda.

The property I want to prove is something like:

    thm : ∀ xs → P xs → Q xs

for vectors xs. Proving by induction, P (x ∷ xs) can be
reduced to P xs, but Q (x ∷ xs) and R (x ∷ xs) are just
themselves. So we try to prove a more general theorem:

    thm' : ∀ xs zs → P xs → Q (zs ++ xs)

The inductive case, if done by hand, would be something like:

        P (x : xs)
    =>  P xs
    =>    { induction (thm' xs (zs ++ [ x ])) }
        Q ((zs ++ [ x ]) ++ xs)
    ==  Q (zs ++ x ∷ xs)

Proving the theorem in Agda, I'd ideally like to do something
like:

    thm' : ∀ {m n} (xs : Vec A m) → (zs : Vec A n) →
             P xs → Q (zs ++ xs)
    thm' [] ... = ...
    thm' (x ∷ xs) zs pxs = thm' xs (zs ++ [ x ]) pxs

But apparently it does not type check, for the call to thm' has
type Q (zs ++ [ x ] ++ xs) while we need Q (zs ++ x ∷ xs),
and the result type is wrong for the same reason.

So it seems that I need to perform a type cast:

    thm (x ∷ xs) zs pxs qzsxs =
        subst (λ ws → Q ws) eq1 (thm xs (zs ++ [ x ]) pxs)   -- (*)

assuming that I can prove

   eq1 : ∀ {a m n} (xs : Vec a m) (x : a) (ys : Vec a n) →
                    (xs ++ [ x ]) ++ ys ≅ xs ++ (x ∷ ys)

But I am not even allowed to do this type cast -- Agda complains
about the type of ws in (*). Indeed, when we look at the type
of subst:

   subst : ∀ {a} (Q : a → Set) → ∀ {x y} → x ≅ y → Q x  
→ Q y

We notice that, in Q (zs ++ [ x ] ++ xs) and Q (zs ++ x ∷ xs),
Q is applied to arguments of different types, so we don't know
how to instantiate a in the type of subst.

I will probably have to resort to implement the type casting
Q ((xs ++ [ x ]) ++ ys) → Q (xs ++ (x ∷ ys)) for the special
case of Q (which I have not tried -- hope I won't run into the
same problem in a different level). But is there a better way
to do this kind of proof?

In one desperate attempt I tried to define

   rev : ∀ {a m n} → Vec₁ a m → Vec₁ a n → Vec₁ a (m + n)
   rev [] ys = ys
   rev (x ∷ xs) ys = rev xs (x ∷ ys)     -- (**)

(we also need a subst in (**)) and tried to prove

   thm'' : ∀ {m n} (xs : Vec A m) → (zs : Vec A n) →
             P xs → Q (rev zs xs)

hoping rev would make it easer to show that Q (rev (z ∷ zs) xs)
equals Q (rev zs (z ∷ xs)). However, rev (z ∷ zs) xs and
rev zs (z ∷ xs) still have different types and it seems that I
still need some complicated type casting so I gave up there.

Thanks!

sincerely,
Shin