[COQ débutant] récursion polymorphe [Résolu]

[SpiceGuid]

Bonjour amis COQeurs au grand cœur,

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

Code OCaml 3.12 :

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 COQ 8.1 :

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.

[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.

[SpiceGuid]

J'ai terminé la traduction, y compris rectangle_to_list

[gasche]

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

[TropMDR]

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.

[TropMDR]

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 !!

[TropMDR]

Alors, tu en es où ?

[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é.

Envoyé par gasche

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

Envoyé par TropMDR

Alors, tu en es où ?

J'ai prouvé la terminaison

[TropMDR]

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 !

Envoyé par SpiceGuid

J'ai prouvé la terminaison

Tu as écrit la fonction donc :-D

[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.

[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" !