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 : Sélectionner tout - Visualiser dans une fenêtre à part
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 : Sélectionner tout - Visualiser dans une fenêtre à part
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 : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
Coq < Check member.
member
     : C -> C -> rev_map C C -> bool
J'aurais préféré:
Code : Sélectionner tout - Visualiser dans une fenêtre à part
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.