[COQ] Débuter, arbres binaires de recherche
Premières impressions.
Pour un système qui est déjà en version 8, je m'attendais à trouver plus d'exemples et de tutoriels.
Là j'ai l'impression de quelque chose de confidentiel avec quelques tutoriels qui paraissent insipides sur le plan algorithmique.
Par exemple la librairie standard et les contributions sont loin de couvrir toutes les structures arborescentes.
Pourtant le système a l'air mature, à mon avis c'est surtout une question de (manque de) popularité, à partir du moment où l'utilisateur accepte sa condition de "pionnier" il n'est pas censé avoir besoin d'encouragements.
Premiers essais
Je ne sais pas si on peut parler d'essai puisque je n'ai fais que recoder ce que je connais déjà.
Par exemple la recherche et l'insertion dans un arbre binaire ne m'ont pas posé de difficultés, hormis le fait que < est de type nat → nat → Prop et non de type nat → nat → bool ce qui m'a ralenti un certain moment.
Propriétés
Code : Sélectionner tout - Visualiser dans une fenêtre à part
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
28Inductive tree : Set := | Leaf | Node: tree -> nat -> tree -> tree. (* je dois vraiment coder nat_less moi-même ? *) Fixpoint nat_less (a b : nat) {struct a} := match a,b with | O,S n => true | m,O => false | S m,S n => nat_less m n end. Fixpoint find (t:tree) (n:nat) {struct t} := match t with | Leaf => false | Node l m r => if nat_less n m then find l n else if nat_less m n then find r n else true end. Fixpoint insert (t:tree) (n:nat) {struct t} := match t with | Leaf => Node Leaf n Leaf | Node l m r => if nat_less n m then Node (insert l n) m r else Node l m (insert r n) end.
J'ai pensé que dans un second temps il serait bon d'avoir quelques propriétés intéressantes sur les arbres binaires de recherche.
Notamment tree_ordered, la propriété caractéristique:
Et member, pour exprimer que mon TAD est un conteneur :
Code : Sélectionner tout - Visualiser dans une fenêtre à part
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
34Definition less a b := nat_less a b = true. Inductive tree_between : tree -> nat -> nat -> Prop := | leaf_tree_between : forall a b, tree_between Leaf a b | node_tree_between : forall l m r, forall a b, tree_between l a m -> less a m -> less m b -> tree_between r m b -> tree_between (Node l m r) a b with tree_less : tree -> nat -> Prop := | leaf_tree_less : forall b, tree_less Leaf b | node_tree_less : forall l m r, forall b, tree_less l m -> less m b -> tree_between r m b -> tree_less (Node l m r) b with tree_more : tree -> nat -> Prop := | leaf_tree_more : forall a, tree_more Leaf a | node_tree_more : forall l m r, forall a, tree_between l a m -> less a m -> tree_more r m -> tree_more (Node l m r) a. Inductive tree_ordered : tree -> Prop := | leaf_tree_ordered : tree_ordered Leaf | node_tree_ordered : forall l m r, tree_less l m -> tree_more r m -> tree_ordered (Node l m r).
Bien sûr, je n'en suis pas arrivé là sans m'inspirer du code existant, d'où un certain doute :
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3
4
5
6
7
8
9
10
11
12Inductive member : tree -> nat -> Prop := | left_member : forall m n l r, member l n -> member (Node l m r) n | right_member : forall m n l r, member r n -> member (Node l m r) n | root_member : forall l n r, member (Node l n r) n.
- pourquoi le code existant ressemble si peu au mien ?
- est-ce que j'ai suivi une bonne approche ?
- est-ce que je n'aurais pas du commencer par les tutoriels rébarbatifs ?
Théorèmes
Mon idée c'était d'en arriver au point où je suis en mesure d'exprimer les théorèmes qui valident mes opérations :
Démarche
Code : Sélectionner tout - Visualiser dans une fenêtre à part
2
3
4
5
6
7
8
9
10
11
D'un certain point de vue je n'ai pas progressé puisque je retrouve la difficulté que j'avais différé jusqu'ici.
Est-ce qu'au moins j'ai pris un bon départ ?
Si oui, est-ce que les preuves sont à ma portée ou est-ce que je dois d'abord me faire la main sur des exemples plus abordables ?
Pour l'équivalence find_iff_member, je peux la prouver directement ou bien je dois prouver l'implication dans les deux sens ?
Répondre avec citation
Envoyé par alex_pi
)
).
je préfère comme ça.
avec un guide comme toi je n'ai plus d'excuse pour ne pas progresser.
Partager