[COQ] Débuter, arbres binaires de recherche

**dividee** · 13/12/2008, 00h28

edit
Je pense que ma fonction insert était sous-spécifiée et qu'il faudrait ajouter cette propriétée:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
Theorem insert_preserves_order :
forall t, tree_ordered t ->
forall n, not (member t n) -> tree_ordered (insert t n).

remarque: la condition not (member t n) est nécessaire parce que mon prédicat tree_ordered impose que tous les éléments soient distincts (j'ai pensé que ça ne pouvait que simplifier la tâche).

Oui; je n'ai pas eu ce problème car j'ai changé un peu la définition de insert pour que tous les éléments soient distincts. Voici les définitions que j'ai utilisées:

Code :

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
Require Import Arith.

Inductive tree : Set :=
  | Leaf: tree
  | Node: tree -> nat -> tree -> tree.

Fixpoint find (t:tree) (n:nat) {struct t} :=
  match t with
  | Leaf => false
  | Node l m r =>
      match nat_compare n m with
      | Lt => find l n
      | Gt => find r n
      | Eq => true
      end
  end.

Fixpoint insert (t:tree) (n:nat) {struct t} :=
  match t with
  | Leaf => Node Leaf n Leaf
  | Node l m r =>
      match nat_compare n m with
      | Lt => Node (insert l n) m r
      | Gt => Node l m (insert r n)
      | Eq => t
      end
  end.

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 -> a < 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 -> 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 -> 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).

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

**SpiceGuid** · 19/06/2009, 17h22

Merci dividee.

J'ai (re-)tenté et cette fois-ci j'arrive (presque) à quelque chose.

Mon (modeste) objectif :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
Theorem insert_is_inclusive :
forall t n, member (insert t n) n.

Mon début de tentative :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
Goal forall t n, member (insert t n) n.
  intros t n. induction t.
  simpl. apply root_member.
  simpl.

J'obtiens alors ceci :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
1 subgoal
  
  t1 : tree
  n0 : nat
  t2 : tree
  n : nat
  IHt1 : member (insert t1 n) n
  IHt2 : member (insert t2 n) n
  ============================
   member
     match nat_compare n n0 with
     | Eq => Node t1 n0 t2
     | Lt => Node (insert t1 n) n0 t2
     | Gt => Node t1 n0 (insert t2 n)
     end n

Encore une commande:

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

case (nat_compare n n0).

Et j'obtiens cela :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
3 subgoals
  
  t1 : tree
  n0 : nat
  t2 : tree
  n : nat
  IHt1 : member (insert t1 n) n
  IHt2 : member (insert t2 n) n
  ============================
   member (Node t1 n0 t2) n

subgoal 2 is:
  member (Node (insert t1 n) n0 t2) n
subgoal 3 is:
  member (Node t1 n0 (insert t2 n)) n

Mais là je ne comprends pas comment m'en sortir, je pense que mon problème c'est que je n'ai que la partie droite du match, toute la partie gauche a été oubliée. En fait je m'attendais à obtenir ce triple but :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
  n = n0 -> member (Node t1 n0 t2) n

subgoal 2 is:
  n < n0 -> member (Node (insert t1 n) n0 t2) n
subgoal 3 is:
  n > n0 -> member (Node t1 n0 (insert t2 n)) n

Dont j'aurais résolu le 1er par intros Heq; subst n0; apply root_member.
Mais sans la partie gauche du match je suis bel et bien coincé.

alex_pi · 20/06/2009, 01h21

Envoyé par SpiceGuid

J'ai (re-)tenté et cette fois-ci j'arrive (presque) à quelque chose.

Pour aider, peux tu nous donner tout le script de preuve d'un seul coup ?

**SpiceGuid** · 20/06/2009, 01h31

Code :

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
35
36
37
Require Import Arith.

Inductive tree : Set :=
  | Leaf: tree
  | Node: tree -> nat -> tree -> tree.

Fixpoint insert (t:tree) (n:nat) {struct t} :=
  match t with
  | Leaf => Node Leaf n Leaf
  | Node l m r =>
      match nat_compare n m with
      | Lt => Node (insert l n) m r
      | Gt => Node l m (insert r n)
      | Eq => t
      end
  end.

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

Theorem insert_is_inclusive :
forall t n, member (insert t n) n.
Proof.
  intros t n. induction t.
  simpl. apply root_member.
  simpl. case (nat_compare n n0).

J'ai honte de coincer au bout de seulement 3 lignes

alex_pi · 20/06/2009, 02h22

On est vendredi, il est un poil tard, donc je vais avoir du mal à vraiment donner une réponse

Toujours est-il que le problème est le suivant : quand tu fais un case sur "nat_compare", et que tu es dans le cas Eq, tu perds l'information que n = n0, ce qui ne te permet pas de faire une réécriture, et de conclure. Il doit forcément exister un lemme qui dit que quand "nat_compare" vaut Eq, les deux arguments sont égaux. Il faut donc utiliser ça, pour récupérer l'égalité et pouvoir avancer.

Si ça ne suffit pas, je regarderai demain, à tête plus reposé.

Bon courage !!

alex_pi · 20/06/2009, 02h24

c'est

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m.

alex_pi · 20/06/2009, 02h33

Bon, des vrais gens qui font du Coq hurlerais sans doute au scandale, mais ça devrais te débloquer :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
 remember (nat_compare n n0) as nc. destruct nc. 
  assert (n = n0). apply nat_compare_eq; auto. rewrite <- H.

**SpiceGuid** · 20/06/2009, 20h20

Comme j'avais lu A View From the Left, je me doutais bien que le filtrage devait me fournir les (in-)égalités nécessaires à l'application de root_member, left_member et right_member afin de terminer ma preuve.
Si j'ai commencé par aussi facile c'est justement pour que les obstacles soient essentiellement syntaxiques.

Passé ce remember, ce qui me barre la route ce sont certaines relations que j'ai du mal à utiliser de façon symétrique.

Par exemple Lt = nat_compare n n0 qui n'a pas le même type que nat_compare n n0 = Lt.
J'arrive à contourner avec assert (nat_compare n m = Lt). auto.
Mais ensuite je n'arrive pas à conclure n < n0 à l'aide de apply (nat_compare_lt n n0 H), le problème étant à nouveau que nat_compare n n0 = Lt <-> n < n0 n'a pas le même type que n < n0 <-> nat_compare n n0 = Lt.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
Check nat_compare_lt.
Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt.

alex_pi · 21/06/2009, 00h13

Tu peux appliquer une fonction dans ton contexte avec

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

apply f in H.

Et après tu as sym_eq et iff_sym dans la lib standard : http://coq.inria.fr/coq/distrib/curr...nit.Logic.html (oui, les conventions de nommages sont à chier

)

**SpiceGuid** · 21/06/2009, 16h18

Merci, maintenant ça se déroule tout seul.

Les membres utiles (applicables) d'une équivalence/conjonction sont extractibles à l'aide de proj1 et proj2.

alex_pi · 21/06/2009, 17h06

Envoyé par SpiceGuid

Les membres utiles (applicables) d'une équivalence/conjonction sont extractibles à l'aide de proj1 et proj2.

Note l'existence de destruct qui me parait plus intéressant que les projection puisse qu'il permet de récupérer les deux cotés en même temps

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
Theorem blah : forall A B : Prop, (A <-> B) -> (B <-> A).
Proof.
  intros A B Hequi.
  destruct Hequi as [H1 H2]. split; trivial.
Qed.

Tu peux même matcher en profondeur, ou dans le cas d'une disjonction, créer des nouveaux buts :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
Theorem blah2 : forall A B : Prop, A \/ B -> B \/ A.
Proof.
  intros A B Hor.
  destruct Hor as [HA | HB]; [right | left]; trivial.
Qed.

**SpiceGuid** · 14/02/2013, 00h19

Le même exercice que je n'ai toujours pas résolu

Ce que j'ai fait :

Code Coq :

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
Require Import Arith.

Inductive tree : Set :=
  | Leaf: tree
  | Node: tree -> nat -> tree -> tree.

Fixpoint insert t n :=
  match t with
  | Leaf => Node Leaf n Leaf
  | Node l m r =>
      match nat_compare n m with
      | Eq => t
      | Lt => Node (insert l n) m r
      | Gt => Node l m (insert r n)
      end
  end.

Inductive member : tree -> nat -> Prop :=
  | root_member :
      forall l n r,
      member (Node l n r) n
  | left_member :
      forall l m r n,
      member l n ->
      member (Node l m r) n 
  | right_member :
      forall l m r n,
      member r n ->
      member (Node l m r) n. 

Theorem insert_is_inclusive :
  forall t n, member (insert t n) n.
Proof.
  intros. induction t.
  simpl.
    apply root_member.
  simpl. remember (nat_compare n n0) as nc.
  destruct nc.
    symmetry in Heqnc.
    apply (nat_compare_eq n n0) in Heqnc.
    subst n0. apply root_member.
    symmetry in Heqnc.
    apply (proj2 (nat_compare_lt n n0)) in Heqnc.
    apply left_member. exact IHt1.
    symmetry in Heqnc.
    apply (proj2 (nat_compare_gt n n0)) in Heqnc.
    apply right_member. exact IHt2.
Qed.


Theorem insert_is_conservative :
  forall t m n, member t m -> member (insert t n) m.
Proof.
  intros. induction t.  
  simpl.
    apply left_member. exact H.
  remember (Node t1 n0 t2) as node.
  destruct H.
  simpl. destruct (nat_compare n n1).
    apply root_member.
    apply root_member.
    apply root_member.
  inversion Heqnode.
  rewrite H1 in H.
  simpl. destruct (nat_compare n n0).
    apply left_member. exact H.
    apply IHt1 in H. apply left_member. exact H.
    apply left_member. exact H.
  inversion Heqnode.
  rewrite H3 in H.
  simpl. destruct (nat_compare n n0).
    apply right_member. exact H.
    apply right_member. exact H.
    apply IHt2 in H. apply right_member. exact H.
Qed.
  
  
Fixpoint find t n :=
  match t with
  | Leaf => false
  | Node l m r =>
      match nat_compare n m with
      | Lt => find l n
      | Gt => find r n
      | Eq => true
      end
  end.

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 -> a < 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 -> 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 -> 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).

Ce que je voudrais faire :

Code Coq :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
Theorem find_iff_member :
forall t, tree_ordered t ->
forall n, find t n = true <-> member t n.
Admitted.

Theorem insert_preserves_order :
forall t, tree_ordered t ->
forall n, tree_ordered (insert t n).
Admitted.

**SpiceGuid** · 17/02/2013, 20h56

Quand j'ai montré ma première partie du code à un programmeur Java (titulaire d'une maîtrise de mathématiques pures) il a été très impressionné

Toutefois il a été déçu que je ne sois pas capable d'aller jusqu'au bout. À quoi ça sert une moitié de certification ? À rien

Dommage.

S'il vous plaît, si vous complétez mon code essayer d'utiliser les mêmes tactiques de base que j'ai déjà utilisées dans la première moitié du code. En effet, l'objectif n'est pas de pondre le code le plus concis mais de rédiger le tutoriel le plus lisible

Et donc qui utilise un ensemble minimal de tactiques plutôt que des astuces/tactiques de haut-niveau qu'il faudrait expliquer au lecteur dans un temps d'attention qui est toujours trop réduit.

**Ptival** · 18/02/2013, 00h09

SpiceGuid : Je vais essayer de voir ce que je peux faire. Ce qui est troublant, c'est que ta définition de tree_ordered n'est pas explicitement récursive, ce qui donne lieu à une drôle d'induction où l'on doit réapprendre que les sous-arbres sont bien triés, comme conséquence du fait qu'ils soient tree_less ou tree_more.

Ce seraient d'ailleurs deux lemmes intéressants avant de se lancer dans la première preuve, non ?

**SpiceGuid** · 18/02/2013, 15h33

gloire à vous les magiciens de la preuve qui venez de la planète Ω
Vivement la certification totale

Envoyé par Ptival

Ce seraient d'ailleurs deux lemmes intéressants avant de se lancer dans la première preuve, non ?

Si Adam Chlipala ne prouve pas que son arbre rouge-noir est totalement ordonné je ne veux même pas me donner la peine d'y songer.

Alors, messieurs les anglais tirez les premiers

**SpiceGuid** · 16/03/2013, 18h43

Envoyé par dividee

...
Pour prouver le premier (find_iff_member), j'ai préféré d'abord prouver quelques théorèmes plus simples (j'ai utilisé < au lieu de 'less' et 'nat_compare' au lieu de 'nat_less').

Code Coq :

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
Theorem tree_between_more:
  forall t a b,
  tree_between t a b -> tree_more t a.
Theorem tree_between_less:
  forall t a b,
  tree_between t a b -> tree_less t b.
Theorem tree_less_ordered:
  forall t n,
  tree_less t n -> tree_ordered t.
Theorem tree_more_ordered:
  forall t n,
  tree_more t n -> tree_ordered t.
Theorem member_more:
  forall t n a,
  member t n -> tree_more t a -> a < n.
Theorem member_less:
  forall t n a,
  member t n -> tree_less t a -> a > n.

Ensuite, j'ai prouvé l'implication dans les deux sens. Prouver l'équivalence directement est sans doute possible mais ne fait que repousser le travail dans des théorèmes annexes je pense.

Je peux poster les preuves si quelqu'un en veut, mais ça déborde pas de commentaires...

Oui je veux bien.

**dividee** · 17/03/2013, 02h55

Ça fait plus de quatre ans, mais par chance j'ai retrouvé le fichier

J'ai vérifié que ça passe toujours en Coq 8.4.

Code :

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
Require Import Arith.

Inductive tree : Set :=
  | Leaf: tree
  | Node: tree -> nat -> tree -> tree.

Fixpoint find (t:tree) (n:nat) {struct t} :=
  match t with
  | Leaf => false
  | Node l m r =>
      match nat_compare n m with
      | Lt => find l n
      | Gt => find r n
      | Eq => true
      end
  end.

Fixpoint insert (t:tree) (n:nat) {struct t} :=
  match t with
  | Leaf => Node Leaf n Leaf
  | Node l m r =>
      match nat_compare n m with
      | Lt => Node (insert l n) m r
      | Gt => Node l m (insert r n)
      | Eq => t
      end
  end.

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 -> a < 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 -> 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 -> 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).

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

Lemma tree_between_more:
  forall t a b,
    tree_between t a b -> tree_more t a.
Proof.
  induction t; intros a b tb.
    apply leaf_tree_more.
    inversion tb; subst; clear tb. apply node_tree_more.
      exact H2.
      destruct H5. exact H.
      exact (IHt2 n b H6).
Qed.

Lemma tree_between_less:
  forall t a b,
    tree_between t a b -> tree_less t b.
Proof.
  induction t; intros a b tb.
  apply leaf_tree_less.
  inversion tb; subst; clear tb. apply node_tree_less.
    exact (IHt1 a n H2).
    destruct H5. exact H0.
    exact H6.
Qed.

Lemma tree_less_ordered:
  forall t n,
  tree_less t n -> tree_ordered t.
Proof.
  intros. induction H.
    exact leaf_tree_ordered.
    apply node_tree_ordered.
      exact H.
      exact (tree_between_more r m b H1).
Qed.

Lemma tree_more_ordered:
  forall t n,
  tree_more t n -> tree_ordered t.
Proof.
  intros. induction H.
    exact leaf_tree_ordered.
    apply node_tree_ordered.
      exact (tree_between_less l a m H).
      exact H1.
Qed.

Lemma member_more:
  forall t n a,
  member t n -> tree_more t a -> a < n.
Proof.
  induction t; intros m a mem more.
    (* Leaf *)
    inversion mem.
    (* Node *)
    inversion more; subst; clear more.
    inversion mem; subst; clear mem.
      (* left_member *)
      apply tree_between_more in H2.
      exact (IHt1 m a H6 H2).
      (* right member *)
      apply gt_trans with (m := n).
        exact (IHt2 m n H6 H5).
        red. exact H4.
      (* root member *)
      exact H4.
Qed.

Lemma member_less:
  forall t n a,
  member t n -> tree_less t a -> a > n.
Proof.
  induction t; intros m a mem less.
  (* Leaf *)
  inversion mem.
  (* Node *)
  inversion less; subst; clear less.
  inversion mem; subst; clear mem.
    (* left_member *)
    apply gt_trans with (m := n).
      red. assumption.
      exact (IHt1 m n H6 H2).
    (* right_member *)
    apply tree_between_less in H5.
    exact (IHt2 m a H6 H5).
    (* root_member *)
    red. assumption.
Qed.


Theorem find_iff_member :
  forall t, tree_ordered t ->
  forall n, find t n = true <-> member t n.
Proof.
  intros t ord n.
  split; intro H.
    (* -> *)
    induction t.
      (* Leaf *)
      inversion H.
      (* Node *)
      inversion ord; subst; clear ord.
      simpl in H. remember (nat_compare n n0) as n_n0.
      symmetry in Heqn_n0. destruct n_n0.
        (* n = n0 *)
        apply nat_compare_eq in Heqn_n0. subst.
        apply root_member.
        (* n < n0 *)
        apply left_member. apply tree_less_ordered in H2.
        exact (IHt1 H2 H).
        (* n > n0 *)
        apply right_member. apply tree_more_ordered in H4.
        exact (IHt2 H4 H).
    (* <- *)
    induction t.
      (* Leaf *)
      inversion H.
      (* Node *)
      inversion ord; subst; clear ord.
      simpl. remember (nat_compare n n0) as n_n0.
      symmetry in Heqn_n0. destruct n_n0.
        (* n=m *)
        reflexivity.
        (* n<m *)
        apply tree_less_ordered in H2.
        inversion H; subst; clear H.
          (* left_member *)
          exact (IHt1 H2 H6).
          (* right_member *)
          apply nat_compare_lt in Heqn_n0.
          apply (member_more t2 n n0 H6) in H4.
          apply lt_asym in H4. contradiction.
          (* root_member *)
          apply nat_compare_lt in Heqn_n0.
          contradict Heqn_n0. apply lt_irrefl.
        (* n>m *)
        apply tree_more_ordered in H4.
        inversion H; subst; clear H.
          (* left_member *)
          apply nat_compare_gt in Heqn_n0.
          apply (member_less t1 n n0 H6) in H2.
          apply gt_asym in H2. contradiction.
          (* right_member *)
          exact (IHt2 H4 H6).
          (* root_member *)
          apply nat_compare_gt in Heqn_n0.
          contradict Heqn_n0. apply lt_irrefl.
Qed.

Theorem insert_conservative :
  forall t m n, member t m -> member (insert t n) m.
Proof.
  intros t m n mem.
  induction t.
    (* Leaf *)
    inversion mem.
    (* Node *)
    simpl. destruct (nat_compare n n0).
      (* n = n0 *)
      assumption.
      (* n < n0 *)
      inversion mem; subst; clear mem.
        (* left_member *)
        apply left_member. apply IHt1. assumption.
        (* right_member *)
        apply right_member. assumption.
        (* root_member *)
        apply root_member.
      (* n > n0 *)
      inversion mem; subst; clear mem.
        (* left_member *)
        apply left_member. assumption.
        (* right_member *)
        apply right_member. apply IHt2. assumption.
        (* root_member *)
        apply root_member.
Qed.

Theorem insert_inclusive :
  forall t n, member (insert t n) n.
Proof.
  intros t n. induction t.
    (* Leaf *)
    simpl. apply root_member.
    (* Node *)
    simpl. remember (nat_compare n n0) as n_n0. destruct n_n0.
      (* n = n0 *)
      symmetry in Heqn_n0.
      apply nat_compare_eq in Heqn_n0. subst.
      apply root_member.
      (* n < n0 *)
      apply left_member. assumption.
      (* n > n0 *)
      apply right_member. assumption.
Qed.

**SpiceGuid** · 17/03/2013, 16h53

à toi dividee

. Les autres, s'il-vous-plaît, n'oubliez pas de le

.
Comme quoi il suffisait de ~~dépasser la honte de l'abandon~~ d'avoir le courage de demander

Tantôt j'en tirerai un article (que developpez.net pourra gabariser).

**dividee** · 20/03/2013, 00h07

Et pour le dernier (insert_preserves_order):

Code :

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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
Lemma insert_preserves_between:
  forall t a b n, tree_between t a b -> a < n < b -> tree_between (insert t n) a b.
Proof.
  induction t; intros; simpl.
  repeat constructor; tauto.
  inversion H; subst; clear H.
  remember (nat_compare n0 n) as cmp. symmetry in Heqcmp.
  destruct cmp; constructor; auto.
    apply nat_compare_lt in Heqcmp. apply IHt1; tauto.
    apply nat_compare_gt in Heqcmp. apply IHt2; tauto.
Qed.

Lemma insert_preserves_less:
  forall t n m, tree_less t n -> m < n -> tree_less (insert t m) n.
Proof.
  induction t; intros.
  repeat constructor. assumption.
  inversion H; subst; clear H.
  simpl. remember (nat_compare m n) as cmp. symmetry in Heqcmp.
  destruct cmp; constructor; auto.
    apply IHt1.
      assumption.
      apply nat_compare_lt. assumption.
    apply nat_compare_gt in Heqcmp.
    apply insert_preserves_between; tauto.
Qed.

Lemma insert_preserves_more:
  forall t n m, tree_more t n -> m > n -> tree_more (insert t m) n.
Proof.
  induction t; intros.
  repeat constructor. assumption.
  inversion H; subst; clear H.
  simpl. remember (nat_compare m n) as cmp. symmetry in Heqcmp.
  destruct cmp; constructor; auto.
    apply nat_compare_lt in Heqcmp.
      apply insert_preserves_between; tauto.
    apply IHt2.
      assumption.
      apply nat_compare_gt. assumption.
Qed.


Theorem insert_preserves_order :
  forall t, tree_ordered t ->
  forall n, tree_ordered (insert t n).
Proof.
  induction t; intros.
  (* Leaf *)
  simpl. repeat constructor.
  (* Node *)
  simpl. remember (nat_compare n0 n) as cmp. symmetry in Heqcmp.
  destruct cmp.
    assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_lt in Heqcmp. apply insert_preserves_less; assumption.
    inversion H; subst; clear H. constructor; auto.
      apply nat_compare_gt in Heqcmp. apply insert_preserves_more; assumption.
Qed.

Il y a un peu plus d'automation mais tu devrais pouvoir le refaire à ton façon à partir de là...

Tes définitions de tree_between, tree_less et tree_more imposent des contraintes assez fortes sur l'arbre (plus fortes que nécessaire pour définir tree_ordered), ce qui complique les preuves.

Je pense que ce serait un peu plus simple avec par exemple ces définitions-ci:

Code :

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
Inductive tree_less : tree -> nat -> Prop :=
  | leaf_tree_less :
      forall b, tree_less Leaf b
  | node_tree_less :
      forall l m r b,
      tree_less l b -> tree_less r b -> m < b ->
      tree_less (Node l m r) b.

Inductive tree_more : tree -> nat -> Prop :=
  | leaf_tree_more :
      forall a, tree_more Leaf a
  | node_tree_more :
      forall l m r a,
      tree_more l a -> tree_more r a -> m > a ->
      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_ordered l -> tree_ordered r ->
      tree_less l m -> tree_more r m ->
      tree_ordered (Node l m r).