I'm trying to understand dependent types and dependent match in Coq, I have the code below, at the bottom I have the add_pair function, the idea is that I want to receive a (dependent) list with exactly two elements and return the sum of the two elements in the list. Since the size of the list is encoded in the type, I should be able to define it as a total function, but I got an error saying that the match is not exaustive
Here is the code
Module IList.
Section Lists.
(* o tipo generico dos elementos da lista *)
Variable A : Set.
(* data type da lista, recebe um nat que é
o tamanho da lista *)
Inductive t : nat -> Set :=
| nil : t 0 (* lista vazia, n = 0 *)
| cons : forall (n : nat), A -> t n -> t (S n). (* cons de uma lista
n = n + 1 *)
(* concatena duas listas, n = n1 + n2 *)
Fixpoint concat n1 (ls1 : t n1) n2 (ls2 : t n2) : t (n1 + n2) :=
match ls1 in (t n1) return (t (n1 + n2)) with
| nil => ls2
| cons x ls1' => cons x (concat ls1' ls2)
end.
(* computar o tamanho da lista é O(1) *)
Definition length n (l : t n) : nat := n.
End Lists.
Arguments nil {_}.
(* Isso aqui serve pra introduzir notações pra gente poder
falar [1;2;3] em vez de (cons 1 (cons 2 (cons 3 nil))) *)
Module Notations.
Notation "a :: b" := (cons a b) (right associativity, at level 60) : list_scope.
Notation "[ ]" := nil : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.
Open Scope list_scope.
End Notations.
Import Notations.
(* Error: Non exhaustive pattern-matching: no clause found for pattern [_] *)
Definition add_pair (l : t nat 2) : nat :=
match l in (t _ 2) return nat with
| (cons x (cons y nil)) => x + y
end.
End IList.
Indeed, it is true that the match you provided is exhaustive, but the pattern-matching algorithm of Coq is limited, and not able to detect it. The issue, I think, is that it compiles a nested pattern-matching such as yours (you have two imbricated cons) down to a successions of elementary pattern-matching (which have patterns of depth at most one). But in the cons branch of the outer match, the information that the index should be 1 is lost if you do not record it explicitly with an equality – something the current algorithm is not smart enough to do.
As a possible solution that avoids fiddling with impossible branches, equalities, and the like, I propose the following:
Definition head {A n} (l : t A (S n)) : A :=
match l with
| cons x _ => x
end.
Definition tail {A n} (l : t A (S n)) : t A n :=
match l with
| cons _ l' => l'
end.
Definition add_pair (l : t nat 2) : nat :=
head l + (head (tail l)).
For the record, a solution that does fiddle with the impossible branches and records the information of the index using equalities (there’s probably a nicer version):
Definition add_pair (l : t nat 2) : nat :=
match l in (t _ m) return (m = 2) -> nat with
| [] => fun e => ltac:(lia)
| x :: l' => fun e =>
match l' in (t _ m') return (m' = 1) -> nat with
| [] => fun e' => ltac:(lia)
| x' :: l'' => fun e' =>
match l'' in (t _ m'') return (m'' = 0) -> nat with
| [] => fun _ => x + x'
| _ => fun e'' => ltac:(lia)
end ltac:(lia)
end ltac:(lia)
end eq_refl.
The interesting part is the use of explicit equalities to record the value of the index (these are used by the lia tactic to discard impossible branches).