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