How to prove list split is valid?

Question

I am exercising. Here seems to be a trivial thing to do (simplified to show the problem is obviously in list splitting):

  infixr 4 _::_ _++_ _==_

  data _==_ {A : Set} : (x : A) -> (y : A) -> Set where
    refl : (x : A) -> x == x

  data List (A : Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  _++_ : forall {A} -> List A -> List A -> List A
  nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  data Permutation {A : Set} : List A -> List A -> Set where
    pnil : Permutation nil nil
    p::  : forall {xs} -> (x : A) -> 
                          (zs : List A) -> (y : A) -> (ys : List A) ->
                          x == y -> Permutation xs (zs ++ ys) ->
                          Permutation (x :: xs) (zs ++ (y :: ys))

  lemma-ripTop : forall {A} -> (xs : List A) ->
                               (y : A) -> (ys : List A) ->
                               Permutation xs (y :: ys) ->
                               Permutation xs (y :: ys)
  lemma-ripTop nil y ys ()
  lemma-ripTop (x :: xs) y ys (p:: .x zs y1 ys1 x==y1 ps) = 
                          p:: x zs y1 ys1 x==y1 ps

Long and short of it, I declare that one can define a Permutation of two lists, if they can provide a Permutation of smaller lists with a pair of equal elements x and y, and the insertion position of y being determined by zs and ys.

Then lemma-ripTop (was meant to do something completely different, but here it is just id on Permutation) needs to prove something given a Permutation for a list (y :: ys).

1. I cannot understand why Agda needs to see zs ++ (y1 :: ys1) == y :: ys (that's the error I get) - I thought this should be clear from the type declaration and the constructor? I.e. since Permutation xs (y :: ys) was given on input, then the split provided as witness in constructor p:: should have added up to y :: ys.

2. How to convince Agda that this split of the list is valid?

Error message:

zs ++ y1 :: ys1 != y :: ys of type List A
when checking that the pattern p:: .x zs y1 ys1 x==y1 ps has type
Permutation (x :: xs) (y :: ys)

Answer 1

Consider the following snippet (you may know this as the induction principle for the identity type/propositional equality):

J : {A : Set} (P : (x y : A) → x == y → Set)
  (f : ∀ x → P x x (refl x)) (x y : A) (p : x == y) → P x y p
J P f x y p = ?

When we pattern match on p and replace it with refl:

J P f x y (refl .x) = ?

Agda will shout that

x != y of type A
when checking that the pattern refl .x has type x == y

This is because x and y can no longer be arbitrary patterns: there's relation between these two that has been revealed by pattern matching on p. Namely, x and y must be the same thing. You have to write this instead:

J P f x .x (refl .x) = f x

Perhaps even better example is the parity view on natural numbers:

data Parity : ℕ → Set where
  even : ∀ k → Parity     (k * 2)
  odd  : ∀ k → Parity (1 + k * 2)

We can compute the parity of every natural number:

parity : ∀ n → Parity n
parity 0 = even 0
parity (suc n) with parity n
parity (suc     .(k * 2)) | even k = odd k
parity (suc .(1 + k * 2)) | odd  k = even (1 + k)

Notice that after pattern matching, n is no longer arbitrary - it must be either k * 2 (in case of even) or 1 + k * 2 (in case of odd).

---

Now, let's see where the problem with your code is. When you pattern match on the permutation parameter, y and ys become fixed - the pattern reveals their structure, much like in the cases above. So you actually have rewrite y and ys to express the fact that they are no longer arbitrary. But here's the problem: if you try to write down how should y and ys look, you'll realize you can't do that. y can either be the first element of zs or it can be y1, depending on zs.

lemma-ripTop (x :: xs) .z .(zs ++ y1 :: ys1)
    (p:: .x (z :: zs) y1 ys1 x==y1 ps) = ?

Pattern matching on zs unfortunately doesn't work. The whole (dotted) pattern should be z :: zs ++ y1 :: ys1, but here it's split in two separate patterns, which I guess is a no-no (cannot say if it's something that Agda cannot do or just doesn't do, sorry).

---

One option is to move everything into proofs, I'm not sure how helpful is it for your situation, but here you go.

Firstly, we will need to express existential quantification. Dependent pairs (sigma types) do exactly that; here's the definition from standard library:

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

So, for example, the statement "there exists a natural number n such that n * n == 4" would be represented as Σ ℕ λ n → n * n == 4 and a proof would be a pair of natural number and a proof that its square indeed is 4. In our case this would be (2 , refl 4).

The fact that we can split l into zs ++ ys will be represented by a proof that there exist r₁ and r₂, such that l == r₁ ++ r₂ and if the final permutation is k, then we require proof that k == r₁ ++ y :: r₂. Here's the whole thing:

data Permutation {A : Set} : (xs ys : List A) → Set a where
  nil : Permutation nil nil
  cons : (x y : A) (xs ys zs : List A)
    (p₁ : Σ _ λ r₁ → Σ _ λ r₂ → ys == r₁ ++ r₂)
    (p₂ : x == y)
    (p₃ : let (r₁ , r₂ , _) = p₁ in zs == r₁ ++ y :: r₂) →
    Permutation xs ys → Permutation (x :: xs) zs

This might or might not be pleasant to work with, but it stays faithful to your original implementation. If you are willing to use something different: you can express the fact that x is somewhere in xs using auxilary data type:

data insert_into_==_ {A : Set} (x : A) : List A → List A → Set where
  here  : ∀ {xs}           → insert x into xs == (x :: xs)
  there : ∀ {y} {xs} {xys} → insert x into xs == xys →
                             insert x into (y :: xs) == (y :: xys)

Permutation is then:

data Permutation {A : Set} : (xs ys : List A) → Set where
  nil : Permutation nil nil
  cons : ∀ {x xs ys xys} →
         insert x into xs == xys →
         Permutation xs ys →
         Permutation (x :: xs) xys