[Agda] Proof involving associativity of ++ of vectors

[Jean-Philippe Bernardy]

Hi,

Apparently I can solve your problem using (a generalization of) the
"with for rewrite"  pattern.
(page 47 in Ulf's thesis). The generalization is to pattern match on
all indices that need to be unified, including
the implicit ones.

Incidentally, it would be nice to extend the "rewrite" syntactic sugar
that was pushed recently to support
heterogeneous equality.

Cheers,
JP.

The code:

module Mu where

  open import Data.Vec
  open import Data.Nat
  open import Relation.Binary.HeterogeneousEquality

  postulate
    A : Set
    P : ∀ {m} -> Vec A m -> Set
    Q : ∀ {m} -> Vec A m -> Set
    red : ∀ {x m} -> {xs : Vec A m} -> P (x ∷ xs) -> P xs

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


  thm' : ∀ {m n} (xs : Vec A m) → (zs : Vec A n) →
           P xs → Q (zs ++ xs)
  thm' [] _ _ = {!...!}
  thm' {suc m} {n} (x ∷ xs) zs pxs with (n + suc m) | zs ++ x ∷ xs |
sym (eq1 zs x xs)
  thm' {suc m} {n} (_∷_  x xs) zs pxs | ._ | ._ | refl  = thm' xs (zs
++ [ x ]) (red pxs)


On Fri, Oct 16, 2009 at 3:38 PM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>