Pattern match on specialised constructors

问题:

I've been banging my head against a problem for a few days, but my Agda skills are not very strong.

I am trying to write a function over an indexed data type which is defined only at a particular index. This is only possible for certain specialisations of the data constructors. I can't figure out how to define such a function. I've tried to reduce my problem to a smaller example.

The setup involves lists of natural numbers, with a type for witnessing members of the list, and a function for deleting list members.

open import Data.Nat
open import Relation.Binary.Core

data List : Set where
   nil : List
   _::_ : (x : ℕ) -> (xs : List) -> List

-- membership within a list
data _∈_ (x : ℕ) : List -> Set where 
   here : forall {xs} -> x ∈ (x :: xs)
   there : forall {xs y} -> (mem : x ∈ xs) -> x ∈ (y :: xs) 

-- delete
_\\_ : forall {x} (xs : List) -> (mem : x ∈ xs) -> List
_\\_ nil ()
_\\_ (_ :: xs) here = xs
_\\_ (_ :: nil) (there ()) 
_\\_ (x :: xs) (there p) = x :: (xs \\ p)

Just a quick check that removing the head element of a singleton list is the empty list:

check : forall {x} -> nil ≡ ((x :: nil) \\ here)
check = refl

Now I have some wrapper data type that is indexed by lists

-- Our test data type
data Foo : List -> Set where
  test : Foo nil
  test2 : forall {x} (xs : List) -> (mem : x ∈ xs) -> Foo (xs \\ mem)

The test2 constructor takes a list and a membership value and indexes the data type by the result of deleting the element from the list.

Now the bit where I am stuck is I want a function of the following signature:

foo : Foo nil -> ℕ
foo = {!!} 

i.e., taking a Foo value with its index specialised to nil. This is fine for the test case

foo test = 0

The second case is tricky. I initially imagined something like:

foo : Foo nil -> ℕ
foo test = 0 
foo (test2 .(_ :: nil) .here) = 1

But Agda complains that xs \\ mem != nil of type List when checking that the pattern test2 .(_ :: nil) .here has type Foo nil. So I tried using a with-clause:

foo : Foo nil -> ℕ
foo test = 0
foo (test2 xs m) with xs \\ m 
... | nil = 1
... | ()

This yields the same error. I have experimented with various permutations, but alas I can't quite figure out how to use the information that n \\ m = nil back in the pattern. I've tried various other kinds of predicates but can't quite figure out how to tell Agda what it needs to know. Would very much appreciate some help! Thanks.

---

Additional: I wrote a proof in Agda that given any xs : List and m : x \in xs that (xs \\ m = nil) implies that xs = x :: nil and m = here, which seems like it could be useful to give to the type checker, but I'm not sure how to do this. I had to introduce a pointwise equality on pi types that respects the dependency which complicates matters:

data PiEq {A : Set} {B : A -> Set} : (a : A) -> (b : A) -> (c : B a) -> (d : B b) -> Set where
   pirefl : forall {x : A} {y : B x} -> PiEq {A} {B} x x y y 

check' : forall {x xs m} {eq : xs \\ m ≡ nil} -> (PiEq {List} {\xs -> x ∈ xs} xs (x :: nil) m here)
check' {xs = nil} {()} 
-- The only case that works
check' {xs = ._ :: nil} {here} = pirefl
-- Everything else is refuted
check' {xs = ._ :: (_ :: xs)} {here} {()}
check' {xs = ._ :: nil} {there ()}
check' {xs = ._} {there here} {()}
check' {xs = ._} {there (there m)} {()} 

回答1:

With the way you set up your data type, you cannot really pattern match on values with non-trivial index in any meaningful way. The problem is of course that Agda cannot (in general) solve the unification of xs \\ mem and nil.

The way pattern matching is set up, you cannot really provide any proof to help the unification algorithm. However, you can ensure that the pattern matching works by leaving the index unrestricted and using another parameter with a proof that describes the actual restriction. This way, you can do a pattern match and then use the proof to eliminate impossible cases.

So, instead of having only foo, we'll have another function (say foo-helper) with extra parameter:

foo-helper : ∀ {xs} → xs ≡ nil → Foo xs → ℕ
foo-helper  p  test = 0
foo-helper  p  (test2 ys mem) with ys \\ mem
foo-helper  p  (test2 _ _) | nil = 1
foo-helper  () (test2 _ _) | _ :: _

You can then recover the original function by simply providing a proof that nil ≡ nil:

foo : Foo nil → ℕ
foo = foo refl

---

If you anticipate doing this kind of pattern matching often, it might be beneficial to instead change the definition of the data type:

data Foo′ : List → Set where
  test′ : Foo′ nil
  test2′ : ∀ {x} xs ys → (mem : x ∈ xs) → ys ≡ xs \\ mem → Foo′ ys

This way, you can always pattern match because you do not have complicated indices and still eliminate any impossible cases thanks to the included proof. If we want to write foo with this definition, we do not even need a helper function:

foo′ : Foo′ nil → ℕ
foo′ test′ = 0
foo′ (test2′ xs .nil mem _) with xs \\ mem
foo′ (test2′ _ ._ _ _ ) | nil = 1
foo′ (test2′ _ ._ _ ()) | _ :: _

---

And to show that these two data types are (logically) equivalent:

to : ∀ {xs} → Foo xs → Foo′ xs
to test = test′
to (test2 xs mem) = test2′ xs (xs \\ mem) mem refl

from : ∀ {xs} → Foo′ xs → Foo xs
from test′ = test
from (test2′ xs .(xs \\ mem) mem refl) = test2 xs mem

回答2:

Why not define foo by

foo : Foo nil -> ℕ
foo _ = 0

?

Note: Using the current development version of Agda (https://github.com/agda/agda/commit/06fe137dc7d7464b7f8f746d969250bbd5011489) I got the error

I'm not sure if there should be a case for the constructor test2,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  xs \\ mem ≟ nil
when checking the definition of foo

when I write

foo test = 0