Problème avec un dependent pattern matching

Comment aider Coq à se souvenir qu’ils font la même taille ?

a marqué ce sujet comme résolu.
Auteur du sujet

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.

Le gist fonctionne avec coq 8.6, sa première révision avec coq 8.5

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 !

Édité par lthms

I don’t like syntax highlighting.

+0 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte