Problème avec un dependent pattern matching

Bonjour à tous !

Il y a un petit moment déjà, j’avais écrit un article sur le typage fort de Coq. Ayant depuis pris un peu de bouteille, je me suis dis que j’allais faire une nouvelle version un peu plus poussée en utilisant notamment le Program des dernières versions de Coq, comme on me l’avait conseillé à l’époque.

J’ai presque réussi à faire tout ce que je voulais et le code complet peut être trouvé dans le gist suivant.

En gros, je reprends l’exemple mille fois cité des vecteurs normés, mais j’essaie d’aller plus loin que les exemples que je peux trouver sur Internet en ce qui concerne le type de retour des fonctions.

J’arrive à faire des choses plutôt cools (de mon point de vue), pour des fonctions comme take, drop, etc. :

1
2
3
4
5
6
7
8

(* un exemple au hasard *)
Program Fixpoint drop
        {A:   Type}
        {n:   nat}
        (v:  vector A n)
        (b:   nat)
        (Hbound: b <= n)
  : { v': vector A (n - b) | forall i, i < n - b -> nth v' i = nth v (b + i) }

Avec extract, j’arrive à peu près à tirer parti de la composition de ces fonctions, c’est encore mieux !

Par contre, pour une fonction de type zip, je bloque… je suis obligé de passer par une définition via des tactics, ce qui donne une extraction dégueulasse !

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

(* TODO: do not rely on tactics for this *)
Program Fixpoint zip
        {A B C: Type}
        {n:     nat}
        (v:     vector A n)
        (v':    vector B n)
        (f:     A -> B -> C)
  : { v'': vector C n | forall i, nth v'' i = option_app (option_map f (nth v i)) (nth v' i) } := _.
Next Obligation.
  dependent induction v; dependent induction v'.
  + remember (IHv v' f) as v''.
    inversion v''.
    refine (exist _ (vcons (f a a0) x) _).
    intros i.
    induction i.
    * cbv.
      reflexivity.
    * simpl.
      apply (H i).
  + refine (exist _ vnil _).
    cbv.
    reflexivity.
Qed.

À l’origine, l’implémentation promettait pourtant d’être simple, quelque chose du genre :

1
2
3
4

match v, v' with
| vcons a v, vcons b v' => vcons (f a b) (zip v v' f)
| _, _ => vnil
end.

Mais ça ne marche pas du tout ! Avec Program, je tombe sur une erreur très étrange qui parle de @eq. Sans Program, coq oublie que v et v’ ont la même taille…

Des idées ? Moi, je sèche complètement.

Merci d’avance !