Discussion :

[dividee]

À première vue je ne peux pas m'empêcher de trouver arbitraire / bizarre d'avoir à la fois tree_less Leaf n et tree_more Leaf n
D'un autre côté il y des Leaf aussi bien à gauche qu'à droite des Node donc ça paraît cohérent.

Moi je trouve cela assez naturel. tree_less t n dit que toutes les valeurs de l'arbre t sont inférieures à n. S'il n'y a pas de valeurs dans l'arbre, c'est vacuously true (je sais pas comment ça se traduit en français). Même chose pour tree_more.

D'ailleurs, ça me fait penser, il doit y avoir encore mieux que mes définitions ci-dessus; ça peut être tout simplement:

Code :

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

1
2
3
4
5
Definition tree_less (t : tree) (n : nat) :=
  forall m, member t m -> m < n.

Definition tree_more (t : tree) (n : nat) :=
  forall m, member t m -> m > n.

Je vais essayer de refaire quelques preuves avec ça, voir si ça fonctionne...

[dividee]

Bon, en fait, ça simplifie certaines preuves mais ça en complique d'autres.
C'est plus simple de garder les définitions récursives mais de prouver ces équivalences:

Code :

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

1
2
3
4
Theorem tree_more_lower_bound:
  forall t n, tree_more t n <-> forall m, member t m -> m > n.
Theorem tree_less_upper_bound:
  forall t n, tree_less t n <-> forall m, member t m -> m < n.

Comme ça, on a le meilleur des deux mondes.

Le code complet:

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

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


Theorem tree_more_lower_bound: 
  forall t n, tree_more t n <-> forall m, member t m -> m > n.
Proof.
  split.
  (* -> *)
  intros Hmore m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hmore; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Theorem tree_less_upper_bound:
  forall t n, tree_less t n <-> forall m, member t m -> m < n.
Proof.
  split.
  (* -> *)
  intros Hless m Hm. induction t.
  inversion Hm.
  inversion Hm; inversion Hless; subst; auto.
  (* <- *)
  intros H. induction t.
    constructor.
    constructor.
      apply IHt1. intros m Hm. apply H. apply left_member. assumption.
      apply IHt2. intros m Hm. apply H. apply right_member. assumption.
      apply H. apply root_member.
Qed.

Lemma member_left:
  forall l m r n, tree_ordered (Node l m r) -> member (Node l m r) n -> n < m -> member l n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    assumption.
    apply tree_more_lower_bound with (m:=n) in H5.
      contradict H5. apply gt_asym. assumption.
      assumption.
    contradict Hlt. apply lt_irrefl.
Qed.

Lemma member_right:
  forall l m r n, tree_ordered (Node l m r) -> member (Node l m r) n -> n > m -> member r n.
Proof.
  intros l m r n Hord Hmem Hlt.
  inversion Hord; subst; clear Hord.
  inversion Hmem; subst; clear Hmem.
    apply tree_less_upper_bound with (m:=n) in H4.
      contradict H4. apply lt_asym. assumption. assumption.
    assumption.
    contradict Hlt. apply lt_irrefl.
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_clear ord.
      simpl in H. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n = n0 *)
        apply nat_compare_eq in Heqcmp. subst.
        apply root_member.
        (* n < n0 *)
        apply left_member. apply IHt1.
          assumption. assumption.
        (* n > n0 *)
        apply right_member. apply IHt2.
          assumption. assumption.
    (* <- *)
    induction t.
      (* Leaf *)
      inversion H.
      (* Node *)
      simpl. remember (nat_compare n n0) as cmp.
      symmetry in Heqcmp. destruct cmp.
        (* n=m *)
        reflexivity.
        (* n<m *)
        apply IHt1.
          inversion ord. assumption.
          apply nat_compare_lt in Heqcmp.
            apply member_left with (n:=n) in ord.
              assumption. assumption. assumption.
        (* n>m *)
        apply IHt2.
          inversion ord. assumption.
          apply nat_compare_gt in Heqcmp.
            apply member_right with (n:=n) in ord.
              assumption. assumption. assumption.
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; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
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; inversion H; subst; clear H.
  repeat constructor. assumption.
  simpl. destruct (nat_compare m n); constructor; auto.
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.

Globalement, je trouve quand-même cela plus simple qu'avec les définitions d'origine.

[SpiceGuid]

pour ce proof-engineering

Ça me fait plusieurs alternatives pour mon tutoriel, la concision importe, mais c'est surtout la lisibilité et l'accessibilité qui comptent, vu que je souhaite baisser au plus bas la barrière d'entrée.

Elle est vieille cette idée de tutoriel.

Elle est redevenue d'actualité lors d'un échange IRC avec le programmeur de Scrambled Nations :

moi: j'ai envahi avec plus de troupes que mon adversaire et pourtant c'est lui qui a capturé le territoire neutre
lui: c'est celui qui envahit avec le plus de troupe qui doit capturer un territoire neutre. mais j'avais écrit < au lieu de > , c'est corrigé maintenant. toi qui dis qu'avec un typage plus fort on signale plus d'erreurs à la compilation, j'aimerais bien savoir quel système de typage pourrait faire la différence entre < et >
moi: ocaml ne peut pas. mais coq peut le faire.
lui: je suis curieux de voir comment

Donc ce tutoriel aurait deux objectifs :
certifier une structure de données.
montrer que < et > sont tout à fait discriminables, pourvu qu'on ait à disposition un système de typage suffisamment expressif.