Matching patterns for specialized designers

Question

I hit my head several times on a problem, but my Agda skills are not very strong.

I am trying to write a function on an indexed data type that is defined only for a specific index. This is only possible for certain specializations of data constructors. I cannot figure out how to define such a function. I tried to reduce the problem to a smaller example.

The setting includes lists of natural numbers with a type for viewing list members and a function for deleting list items.

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 quickly check that deleting the title element of a singleton list is an empty list:

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

Now I have some type of wrapper data 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 constructor test2 accepts a list and a membership value and indexes the data type as a result of removing an item from the list.

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

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

ie, taking the value Foo with its index specialized for nil . This is normal for the test case.

 foo test = 0 

The second case is complicated. 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 with -clause:

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

This gives the same error. I experimented with various permutations, but, alas, I can’t figure out how to use the information that n \\ m = nil returns to the template. I tried various other predicates, but I can’t figure out how to tell Agda what he needs to know. Would love some help! Thanks.

---

Optional : I wrote a proof in Agda that yielded some xs : List and m : x \in xs that ( xs \\ m = nil ) implies xs = x :: nil and m = here , which seems to be It is useful to give a type controller, but I'm not sure how to do this. I had to introduce pointwise equality by type pi, which takes into account the dependency, which complicates the questions:

 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} xxyy 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)} {()} 

Answer 1

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

The pattern matching method is set, you cannot provide any evidence to help the unification algorithm. However, you can make sure that the pattern matching works by leaving the index unbounded and using another parameter with a proof that describes the actual constraint. This way you can perform pattern matching and then use the proof to rule out impossible cases.

So, instead of having only foo , we will have another function (say foo-helper ) with an additional 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 restore the original function by simply providing proof that nil ≡ nil :

 foo : Foo nil → ℕ foo = foo refl 

---

If you prefer to often run such an image, it may be useful to change the definition of the data type instead:

 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 match the pattern because you have no complex indexes and still exclude any impossible cases thanks to the included proof. If we want to write foo with this definition, we don’t 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 

Answer 2

Why not define foo on

 foo : Foo nil -> ℕ foo _ = 0 

?

Note. Using the current version of Agda development ( https://github.com/agda/agda/commit/06fe137dc7d7464b7f8f746d969250bbd5011489 ), I got an 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