[COQ débutant] récursion polymorphe

Version imprimable

Bonjour amis COQeurs au grand cœur,

Au départ j'ai du code ocaml pour un conteneur multimap bijectif entre 2 types:

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
type ('a, 'b) rev_map =
  | Nil 
  | Node of ('b, 'a) rev_map * 'a * 'b * ('b, 'a) rev_map

let rec insert : 'a 'b . 'a -> 'b -> ('a, 'b) rev_map -> ('a, 'b) rev_map =
  fun x y -> function 
  | Nil -> Node(Nil,x,y,Nil) 
  | Node (l,u,v,r) ->
      if x < u then Node (insert y x l,u,v,r)
      else if y > v then Node (l,u,v,insert y x r)
      else Node (l,u,y,insert v x r)
  
let rec member : 'a 'b . 'a -> 'b -> ('a, 'b) rev_map -> bool =
  fun x y -> function 
  | Nil -> false
  | Node (l,u,v,r) ->
      (x = u && y = v) or member y x (if x < u then l else r)
    
let interleave f w  = function
  | Nil -> []
  | Node (l, u, v, r) ->
      f w l @ (if v = w then [u] else []) @ f w r
(* find all values with the given key, in sorted order *)
let rec find_all k = function
  | Nil -> []
  | Node (l, u, v, r) ->
    if k < u then interleave find_all k l
    else (if k = u then [v] else []) @ interleave find_all k r
(* find all values y with key x (even levels) *)
let find_all_y x t =
  find_all x t
(* find all keys x with value y (interleaved version, odd levels) *)
let find_all_x y t =
  interleave find_all y t

Comme j'ai la chance d'avoir éventuellement tout un week-end à perdre, j'ai décidé de passer en mode "COQ pour les nuls".
Ça donne ceci pour commencer en douceur (oui oui vous pouvez cracher dessus) :

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Variable   C : Set.  
Inductive  order : Set := Less | Equal | More.
Hypothesis compare : C -> C -> order.

Inductive rev_map (A B:Set) : Set :=
  | Nil:  rev_map A B
  | Node: rev_map B A -> A -> B -> rev_map B A -> rev_map A B.

Fixpoint insert x y t {struct t} :=
  match t with
  | Nil => Node Nil x y Nil
  | Node l u v r =>
      match compare x u with
      | Less => Node (insert y x l) u v r 
      | _ => match compare y v with
             | More => Node l u v (insert y x r)
             | _ => Node l u y (insert v x r)
             end
      end
  end.

Fixpoint member x y t {struct t} :=
  match t with
  | Nil => false
  | Node l u v r =>
      match compare x u, compare y v with
      | Equal,Equal => true
      | Less,_ => member y x l 
      | _,_    => member y x r 
      end
  end.

Ça n'était pas censé bien se passer du premier coup.
Et sans surprise, en effet ça se passe mal.
Soit ça ne passe pas du tout comme insert.
Soit ça passe mal comme member.

Code:

1
2
3
Coq < Check member.
member
     : C -> C -> rev_map C C -> bool

J'aurais préféré:

Code:

1
2
3
Coq < Check member.
member
     : A -> B -> rev_map A B -> bool

Bien évidemment j'ai un problème de syntaxe avec la récursion polymorphe.
Il y a éventuellement (certainement) d'autres incompréhensions de ma part, merci de prendre du temps pour m'expliquer lesquelles.

10/09/2011, 22h50
gasche

Ton erreur est de définir "Variable (C : Set)." puis "Hypothesis compare : C -> C -> order". Du coup C est une globale et tous les arguments passés à "compare" sont inférés de type C. Une imprudence supplémentaire est de te reposer autant sur l'inférence de types dans tes déclarations; avec un petit
Fixpoint insert A B x y (t : rev_map A B) := ...
tu aurais eu un rapport d'erreur assez explicite.

Bref, la solution est de retirer la constante C et de définir
Hypothesis compare : forall (C : Set), C -> C -> order.

PS: merci de redonner un peu de vie à ce forum.
11/09/2011, 17h46
SpiceGuid

Merci.

J'ai terminé la traduction, y compris rectangle_to_list :)
12/09/2011, 06h54
gasche

C'est bien, mais maintenant il faut prouver la correction :mur:
12/09/2011, 10h02
TropMDR

Citation:

Envoyé par gasche

Bref, la solution est de retirer la constante C et de définir
Hypothesis compare : forall (C : Set), C -> C -> order.

Euh, je crois que tu ne veux surtout pas faire ça ! La tu demandes l'existence d'une fonction de comparaison universelle. Le jour où tu vas vouloir ajouter le fait que c'est bien une fonction de comparaison (du genre compare a a = Equal, compare a b = Equal -> compare b a = equal, compare a b = Less -> compare b a = More (et l'opposé)), tu vas un peu en chier pour écrire une version polymorphe :) (et par "un peu en chier", je veux évidement dire que tu ne pourras pas l'écrire).

Il te faut une fonction de comparaison par type (A et B). Pour ça, il y a deux grande méthodes

La méthode camleuse: un foncteur
La méthode haskellienne: une typeclass

C'est une question de gout.

Allez tiens, une version imbitable pour le débutant, avec typeclasses et type dépendants (youhou)

Code:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Generalizable Variables A B.

Definition relation (A:Type) := A -> A -> Prop.

Inductive  order {A: Type} (LT: relation A) (a b: A) :=
| Less: LT a b -> order LT a b
| Equal: a = b -> order LT a b
| More: LT b a -> order LT a b.



Class Comparable (A: Type) :=
  { LT: relation A;
    compare: forall a b, order LT a b}.

Notation "a < b" := (LT a b).


Inductive rev_map (A B:Type) : Type :=
  | Nil:  rev_map A B
  | Node: rev_map B A -> A -> B -> rev_map B A -> rev_map A B.

Implicit Arguments Nil [[A] [B]].
Implicit Arguments Node [[A] [B]].


Fixpoint insert `{Comparable A} `{Comparable B} (a:A) (b:B) (t: rev_map A B): rev_map A B :=
  match t with
  | Nil => Node Nil a b Nil
  | Node l u v r =>
      match compare a u with
      | Less _ => Node (insert b a l) u v r
      | _ => match compare b v with
             | More _ => Node l u v (insert b a r)
             | _ => Node l u b (insert v a r)
             end
      end
  end.

Fixpoint member `{Comparable A} `{Comparable B} (a:A) (b:B) (t: rev_map A B): bool:=
  match t with
  | Nil => false
  | Node l u v r =>
      match compare a u, compare b v with
      | Equal _ ,Equal _=> true
      | Less _ ,_ => member b a l
      | _,_    => member b a r
      end
  end.

Après, je persiste à penser que pour débuter, http://www.cis.upenn.edu/~bcpierce/sf/ est l'idéal !!

17/09/2011, 17h16
TropMDR

Alors, tu en es où ?
17/09/2011, 19h44
SpiceGuid

Comme je l'ai dit, grâce à l'aide de gasche, j'ai pu terminer la traduction en COQ dans le délai que je m'étais fixé.

Citation:

Envoyé par gasche

C'est bien, mais maintenant il faut prouver la correction

Citation:

Envoyé par TropMDR

Alors, tu en es où ?

J'ai prouvé la terminaison :mrgreen:
17/09/2011, 19h51
TropMDR

Citation:

Envoyé par SpiceGuid

Comme je l'ai dit, grâce à l'aide de gasche, j'ai pu terminer la traduction en COQ dans le délai que je m'étais fixé.

Sauf que comme je disais plus haut, son conseil de rajouter

Code:

Hypothesis compare : forall (C : Set), C -> C -> order.

est mauvais puisque tu n'arriveras jamais à écrire une telle fonction !

Citation:

Envoyé par SpiceGuid

J'ai prouvé la terminaison :mrgreen:

Tu as écrit la fonction donc :-D
18/09/2011, 08h09
gasche

TropMDR : j'ai proposé cet axiome dans le but de modéliser l'opérateur de comparaison polymorphe de OCaml. C'est effectivement un mauvais conseil (... et un mauvais opérateur) si le but est de tout implémenter en Coq, mais ça me semble un choix raisonnable dans une optique de spécification partielle; j'ai interprété le choix de SpiceGuid de définir la fonction de comparaison en axiome comme une optique "je me prends pas la tête sur cet aspect de l'algorithme", et dans ce cadre le choix me semble justifié.

Je suis tout à fait d'accord sur le fait que ta version avec typeclasses est meilleure (en plus elle est tout à fait lisible). Cependant, je ne suis pas convaincu qu'elle permette intrinsèquement d'avoir plus d'assurance dans les bonnes propriétés de la version l'algorithme déjà codé en OCaml, comme j'ai l'impression que c'était le but ici.
18/09/2011, 11h10
TropMDR

Effectivement, si le but est de modéliser les fonctions de comparaison polymorphe de caml, cet axiome semble raisonnable, en l'extrayant proprement. J'étais resté dans une vision purement "coq" !