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) :
Ça n'était pas censé bien se passer du premier coup.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.
Et sans surprise, en effet ça se passe mal.
Soit ça ne passe pas du tout comme insert.
Soit ça passe mal comme member.
J'aurais préféré:Code:
1
2
3 Coq < Check member. member : C -> C -> rev_map C C -> bool
Bien évidemment j'ai un problème de syntaxe avec la récursion polymorphe.Code:
1
2
3 Coq < Check member. member : A -> B -> rev_map A B -> bool
Il y a éventuellement (certainement) d'autres incompréhensions de ma part, merci de prendre du temps pour m'expliquer lesquelles.