The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Le 28 mars 08 à 09:07, Michael Day a écrit :

> Hi,

Hi,

> I have defined a simple vector type and a function to get the first  
> element of non-empty vectors as follows:
>
> Inductive vec (A:Type) : nat -> Type :=
>   | Vnil : vec A 0
>   | Vcons : forall (a:A) (n:nat), vec A n -> vec A (S n).
>
> Definition get_first (A:Type) (n:nat) (v:vec A (S n)) (default:A) :  
> A :=
>   match v with
>   | Vnil => default    (* I want to delete this line *)
>   | Vcons a _ _ => a
>   end.
>
> Coq prevents me from calling get_first with an empty vector, so the  
> Vnil case will never be matched and the default value will never be  
> used. However, Coq does not permit me to omit this case:
>
> Error: Non exhaustive pattern-matching: no clause found for pattern  
> Vnil
>
> This is incredibly frustrating. Why does Coq think that "Vnil" is an  
> inhabitant of "vec (S n)"? After reading Conor McBride's papers on  
> Epigram I expect the system to understand that 0 <> S n :)
>
> The Vhead function in the Bvector module in the standard library  
> uses the inversion tactic instead, but that seems to generate a very  
> large and complicated definition for something that should be quite  
> simple.

The reason for this complicated term is that exhaustiveness of pattern- 
matching with dependent types is an NP-complete problem [1], hence we  
can find no effective procedure to always decide exhaustiveness that  
could be used during typing. There are different ways to go around this:

- Epigram and Agda(s) have a kind of "best effort" algorithm that  
tries to derive as much information as possible from the type of the  
matched term and the patterns using first-order unification.
This permits to get rid of most(all?) of the innaccessible branches.  
However, to justify this fairly complicated algorithm, you have to  
prove that it can be "compiled away" to the core type theory [2]. The  
resulting compiled term will have more or less the same form as the  
one generated by the Coq tactics, using the propositional equality to  
carry information on the objects and patterns.

- Coq does nothing about it (yet), but can almost be used as a core  
theory (assembly) to compile higher-level pattern matching to. It  
needs to be extended with an axiom such as Streicher's K to be really  
a good target. There is ongoing work on adding K and inversion of  
pattern-matching in the kernel.

- Program/Russell does the compilation in Coq. It generates the  
equalities during pattern-matching and uses the existing proof  
machinery to try to derive contradictions in inaccessible branches.
For example you may write:
<<
Require Import Coq.Program.Program.

Program Definition tail' (A:Type) (n:nat) (v:vec A (S n)) : vec A n :=
  match v with
  | Vnil => !
  | Vcons _ n' v' => v'
  end.
>>
This will generate two obligations, one to prove that (S n = 0 ->  
False) and another to prove that (S n = S n' -> n' = n). You still  
have to give the inaccesible branches but that's only an engineering  
issue (it prevents finding out you have forgottoen a pattern only when  
trying to prove the obligations). The resulting term is ugly and  
somewhat hard to work with.

Regarding the trick of pattern-matching on the index in the clause, it  
seems you can go a long way, as this is accepted by Coq:

Definition tail (A:Type) (n:nat) (v:vec A (S n)) (default:A) : vec A  
n :=
  match v in (vec _ m) return (match m with 0 => True | S n' => vec A  
n' end) with
  | Vnil => I    (* I want to delete this line *)
  | Vcons _ _ v' => v'
  end.

Also, False_rect is extracted to assert false, not a complicated  
computation :)
[1] N. Oury. Pattern matching coverage checking with dependent types  
using set approximations. In A. Stump and H. Xi, editors, PLPV, pages  
47–56. ACM, 2007.

[2] H. Goguen, C. McBride, and J. McKinna. Eliminating dependent  
pattern matching. In K. Futatsugi, J.-P. Jouannaud, and J. Meseguer,  
editors, Essays Dedicated to Joseph A. Goguen, volume 4060 of Lecture  
Notes in Computer Science, pages 521–540. Springer, 2006.

-- Matthieu Sozeau