Set.v 11.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
16 17 18
Require HighOrd.
Require map.Map.
Require map.Const.
19

MARCHE Claude's avatar
MARCHE Claude committed
20 21
Require Import ClassicalEpsilon.

22
Lemma predicate_extensionality:
23 24
  forall A (P Q : A -> bool),
    (forall x, P x = Q x) -> P = Q.
25
Admitted.
MARCHE Claude's avatar
MARCHE Claude committed
26

27
(* Why3 assumption *)
28
Definition set (a:Type) := a -> Init.Datatypes.bool.
MARCHE Claude's avatar
MARCHE Claude committed
29

MARCHE Claude's avatar
MARCHE Claude committed
30
Global Instance set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
31 32
Proof.
intros.
33
split.
34
exact (fun _ => false).
35 36
intros x y.
apply excluded_middle_informative.
37 38
Qed.

39
(* Why3 assumption *)
40 41 42
Definition mem {a:Type} {a_WT:WhyType a} (x:a) (s:a -> Init.Datatypes.bool) :
    Prop :=
  ((s x) = Init.Datatypes.true).
MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46

Hint Unfold mem.

(* Why3 assumption *)
47 48
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:a -> Init.Datatypes.bool)
    (s2:a -> Init.Datatypes.bool) : Prop :=
49
  forall (x:a), mem x s1 <-> mem x s2.
MARCHE Claude's avatar
MARCHE Claude committed
50 51 52 53

Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).

(* Why3 goal *)
54
Lemma extensionality {a:Type} {a_WT:WhyType a} :
55 56
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  infix_eqeq s1 s2 -> (s1 = s2).
57
Proof.
58
intros s1 s2 h1.
59 60 61 62 63 64 65 66 67 68
apply predicate_extensionality.
intros x.
generalize (h1 x).
unfold mem.
intros [h2 h3].
destruct (s1 x).
now rewrite h2.
destruct (s2 x).
now apply h3.
easy.
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71
Qed.

(* Why3 assumption *)
72 73
Definition subset {a:Type} {a_WT:WhyType a} (s1:a -> Init.Datatypes.bool)
    (s2:a -> Init.Datatypes.bool) : Prop :=
74
  forall (x:a), mem x s1 -> mem x s2.
MARCHE Claude's avatar
MARCHE Claude committed
75

76
(* Why3 goal *)
77
Lemma subset_refl {a:Type} {a_WT:WhyType a} :
78
  forall (s:a -> Init.Datatypes.bool), subset s s.
79
Proof.
80
now intros s x.
81 82
Qed.

MARCHE Claude's avatar
MARCHE Claude committed
83
(* Why3 goal *)
84
Lemma subset_trans {a:Type} {a_WT:WhyType a} :
85 86 87
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool)
    (s3:a -> Init.Datatypes.bool),
  subset s1 s2 -> subset s2 s3 -> subset s1 s3.
88
Proof.
89
intros s1 s2 s3 h1 h2 x H.
90
now apply h2, h1.
MARCHE Claude's avatar
MARCHE Claude committed
91 92 93
Qed.

(* Why3 assumption *)
94 95
Definition is_empty {a:Type} {a_WT:WhyType a} (s:a -> Init.Datatypes.bool) :
    Prop :=
96
  forall (x:a), ~ mem x s.
MARCHE Claude's avatar
MARCHE Claude committed
97 98

(* Why3 goal *)
99
Lemma is_empty_empty {a:Type} {a_WT:WhyType a} :
100
  is_empty (map.Const.const Init.Datatypes.false : a -> Init.Datatypes.bool).
101
Proof.
102
now intros x.
103 104
Qed.

MARCHE Claude's avatar
MARCHE Claude committed
105
(* Why3 goal *)
106 107 108
Lemma empty_is_empty {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), is_empty s ->
  (s = (map.Const.const Init.Datatypes.false : a -> Init.Datatypes.bool)).
109
Proof.
110 111 112 113 114 115
intros s h1.
apply predicate_extensionality.
unfold is_empty in h1; unfold Const.const.
unfold mem in h1.
intros x. generalize (h1 x).
destruct (s x); intuition.
MARCHE Claude's avatar
MARCHE Claude committed
116 117 118
Qed.

(* Why3 goal *)
119 120 121 122 123 124 125
Lemma mem_singleton {a:Type} {a_WT:WhyType a} :
  forall (x:a) (y:a),
  mem y
  (map.Map.set
   (map.Const.const Init.Datatypes.false : a -> Init.Datatypes.bool) x
   Init.Datatypes.true) ->
  (y = x).
126
Proof.
127 128 129 130
intros x y h1.
unfold mem, Map.set, Const.const in h1.
destruct (why_decidable_eq x y) as [->|H] ; intuition.
discriminate h1.
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133
Qed.

(* Why3 goal *)
134
Lemma add_remove {a:Type} {a_WT:WhyType a} :
135 136 137
  forall (x:a) (s:a -> Init.Datatypes.bool), mem x s ->
  ((map.Map.set (map.Map.set s x Init.Datatypes.false) x Init.Datatypes.true)
   = s).
138
Proof.
139
intros x s h1.
MARCHE Claude's avatar
MARCHE Claude committed
140
apply extensionality; intro y.
141 142
unfold mem, Map.set. unfold mem in h1.
destruct (why_decidable_eq x y) as [->|H] ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
143 144 145
Qed.

(* Why3 goal *)
146
Lemma remove_add {a:Type} {a_WT:WhyType a} :
147 148 149
  forall (x:a) (s:a -> Init.Datatypes.bool),
  ((map.Map.set (map.Map.set s x Init.Datatypes.true) x Init.Datatypes.false)
   = (map.Map.set s x Init.Datatypes.false)).
150
Proof.
151
intros x s.
MARCHE Claude's avatar
MARCHE Claude committed
152
apply extensionality; intro y.
153 154
unfold mem, Map.set.
destruct (why_decidable_eq x y) as [->|H] ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
155 156 157
Qed.

(* Why3 goal *)
158
Lemma subset_remove {a:Type} {a_WT:WhyType a} :
159 160
  forall (x:a) (s:a -> Init.Datatypes.bool),
  subset (map.Map.set s x Init.Datatypes.false) s.
161
Proof.
162
intros x s y.
163 164
unfold mem, Map.set.
destruct (why_decidable_eq x y) as [->|H] ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
165 166 167
Qed.

(* Why3 goal *)
168
Definition union {a:Type} {a_WT:WhyType a} :
169 170
  (a -> Init.Datatypes.bool) -> (a -> Init.Datatypes.bool) ->
  a -> Init.Datatypes.bool.
171
Proof.
172
intros s1 s2.
173
exact (fun x => orb (s1 x) (s2 x)).
MARCHE Claude's avatar
MARCHE Claude committed
174 175 176
Defined.

(* Why3 goal *)
177
Lemma union_def {a:Type} {a_WT:WhyType a} :
178
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool) (x:a),
179
  ((union s1 s2 x) = Init.Datatypes.true) <-> mem x s1 \/ mem x s2.
180
Proof.
181
intros s1 s2 x.
182
apply Bool.orb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
183 184 185
Qed.

(* Why3 goal *)
186
Lemma subset_union_1 {a:Type} {a_WT:WhyType a} :
187
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
188
  subset s1 (union s1 s2).
189
Proof.
190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
intros s1 s2.
unfold subset, union.
unfold mem.
intros x hx.
apply Bool.orb_true_iff. intuition.
Qed.

(* Why3 goal *)
Lemma subset_union_2 {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  subset s2 (union s1 s2).
Proof.
intros s1 s2.
unfold subset, union.
unfold mem.
intros x hx.
apply Bool.orb_true_iff. intuition.
207 208 209
Qed.

(* Why3 goal *)
210
Definition inter {a:Type} {a_WT:WhyType a} :
211 212
  (a -> Init.Datatypes.bool) -> (a -> Init.Datatypes.bool) ->
  a -> Init.Datatypes.bool.
213
Proof.
214
intros s1 s2.
215
exact (fun x => andb (s1 x) (s2 x)).
MARCHE Claude's avatar
MARCHE Claude committed
216 217 218
Defined.

(* Why3 goal *)
219
Lemma inter_def {a:Type} {a_WT:WhyType a} :
220
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool) (x:a),
221
  ((inter s1 s2 x) = Init.Datatypes.true) <-> mem x s1 /\ mem x s2.
222
Proof.
223
intros s1 s2 x.
224
apply Bool.andb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
225 226 227
Qed.

(* Why3 goal *)
228
Lemma subset_inter_1 {a:Type} {a_WT:WhyType a} :
229
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
230
  subset (inter s1 s2) s1.
231
Proof.
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248
intros s1 s2.
unfold subset, inter.
unfold mem.
intros x hx.
apply Bool.andb_true_iff in hx. intuition.
Qed.

(* Why3 goal *)
Lemma subset_inter_2 {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  subset (inter s1 s2) s2.
Proof.
intros s1 s2.
unfold subset, inter.
unfold mem.
intros x hx.
apply Bool.andb_true_iff in hx. intuition.
249 250 251
Qed.

(* Why3 goal *)
252
Definition diff {a:Type} {a_WT:WhyType a} :
253 254
  (a -> Init.Datatypes.bool) -> (a -> Init.Datatypes.bool) ->
  a -> Init.Datatypes.bool.
255
Proof.
256
intros s1 s2.
257
exact (fun x => andb (s1 x) (negb (s2 x))).
MARCHE Claude's avatar
MARCHE Claude committed
258 259 260
Defined.

(* Why3 goal *)
261
Lemma diff_def {a:Type} {a_WT:WhyType a} :
262
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool) (x:a),
263
  ((diff s1 s2 x) = Init.Datatypes.true) <-> mem x s1 /\ ~ mem x s2.
264
Proof.
265
intros s1 s2 x.
266 267 268 269 270 271
unfold mem, diff.
rewrite Bool.not_true_iff_false.
rewrite <- Bool.negb_true_iff.
apply Bool.andb_true_iff.
Qed.

MARCHE Claude's avatar
MARCHE Claude committed
272
(* Why3 goal *)
273
Lemma subset_diff {a:Type} {a_WT:WhyType a} :
274 275
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  subset (diff s1 s2) s1.
276
Proof.
277
intros s1 s2 x.
278 279
unfold mem.
rewrite diff_def. intuition.
MARCHE Claude's avatar
MARCHE Claude committed
280 281 282
Qed.

(* Why3 goal *)
283 284
Definition complement {a:Type} {a_WT:WhyType a} :
  (a -> Init.Datatypes.bool) -> a -> Init.Datatypes.bool.
285
Proof.
286
intros s.
287
exact (fun x => negb (s x)).
MARCHE Claude's avatar
MARCHE Claude committed
288 289 290
Defined.

(* Why3 goal *)
291
Lemma complement_def {a:Type} {a_WT:WhyType a} :
292
  forall (s:a -> Init.Datatypes.bool) (x:a),
293
  ((complement s x) = Init.Datatypes.true) <-> ~ mem x s.
294
Proof.
295
intros s x.
296
unfold mem, complement.
297 298
rewrite Bool.not_true_iff_false.
apply Bool.negb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
299 300 301
Qed.

(* Why3 goal *)
302
Definition pick {a:Type} {a_WT:WhyType a} : (a -> Init.Datatypes.bool) -> a.
303
Proof.
304
intros s.
305 306
assert (i: inhabited a) by (apply inhabits, why_inhabitant).
exact (epsilon i (fun x => mem x s)).
MARCHE Claude's avatar
MARCHE Claude committed
307 308 309
Defined.

(* Why3 goal *)
310 311
Lemma pick_def {a:Type} {a_WT:WhyType a} :
  forall (s:a -> Init.Datatypes.bool), ~ is_empty s -> mem (pick s) s.
312
Proof.
313
intros s h1.
314
unfold pick.
315 316
apply epsilon_spec.
now apply not_all_not_ex.
MARCHE Claude's avatar
MARCHE Claude committed
317
Qed.
318

319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387
(* Why3 assumption *)
Definition disjoint {a:Type} {a_WT:WhyType a} (s1:a -> Init.Datatypes.bool)
    (s2:a -> Init.Datatypes.bool) : Prop :=
  forall (x:a), ~ mem x s1 \/ ~ mem x s2.

(* Why3 goal *)
Lemma disjoint_inter_empty {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  disjoint s1 s2 <-> is_empty (inter s1 s2).
Proof.
intros s1 s2.
unfold disjoint, is_empty, inter.
unfold mem.
intuition.
destruct (H x); intuition.
apply H1.
rewrite Bool.andb_true_iff in H0. intuition.
apply H1.
rewrite Bool.andb_true_iff in H0. intuition.
generalize (H x).
rewrite Bool.andb_true_iff.
destruct (s1 x); destruct (s2 x); intuition.
Qed.

(* Why3 goal *)
Lemma disjoint_diff_eq {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  disjoint s1 s2 <-> ((diff s1 s2) = s1).
Proof.
intros s1 s2.
unfold disjoint, diff.
unfold mem.
intuition.
apply (extensionality _ s1). unfold infix_eqeq.
unfold mem.
intuition.
destruct (H x); intuition.
rewrite Bool.andb_true_iff in H0. intuition.
rewrite Bool.andb_true_iff in H0. intuition.
rewrite Bool.andb_true_iff.
intuition.
destruct (H x); intuition.
rewrite <- H.
rewrite Bool.andb_true_iff.
destruct (s2 x); intuition.
Qed.

(* Why3 goal *)
Lemma disjoint_diff_s2 {a:Type} {a_WT:WhyType a} :
  forall (s1:a -> Init.Datatypes.bool) (s2:a -> Init.Datatypes.bool),
  disjoint (diff s1 s2) s2.
Proof.
intros s1 s2.
unfold disjoint, diff.
unfold mem.
intros x.
rewrite Bool.andb_true_iff.
destruct (s2 x); intuition.
Qed.

(* Why3 goal *)
Definition map {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  (a -> b) -> (a -> Init.Datatypes.bool) -> b -> Init.Datatypes.bool.
Proof.
intros f s y.
set (P := fun (x:a) => mem x s /\ y = f x).
assert (inhabited a).
destruct a_WT.
exact (inhabits why_inhabitant).
388
set (x := epsilon H P).
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
destruct b_WT.
destruct (why_decidable_eq y (f x)).
exact (s x).
exact false.
Defined.

(* Why3 goal *)
Lemma map_def {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  forall (f:a -> b) (u:a -> Init.Datatypes.bool) (y:b),
  ((map f u y) = Init.Datatypes.true) <->
  (exists x:a, mem x u /\ (y = (f x))).
Proof.
intros f u y.
unfold map, mem.
destruct b_WT.
destruct a_WT.
set (P := fun (x:a) => u x = true /\ y = f x).
set (inh := (inhabits why_inhabitant0)).
generalize (epsilon_spec inh P).
set (x := epsilon inh P).
destruct (classic (exists x, P x)).
destruct (why_decidable_eq y (f x)).
intuition.
unfold P in H1. intuition.
intuition.
unfold P in H1. intuition.
destruct (why_decidable_eq y (f x)).
intuition.
exists x; unfold P; intuition.
intuition.
discriminate H1.
Qed.

(* Why3 goal *)
Lemma mem_map {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
  forall (f:a -> b) (u:a -> Init.Datatypes.bool), forall (x:a), mem x u ->
  mem (f x) (map f u).
Proof.
intros f u x h1.
generalize (map_def f u (f x)).
intuition.
apply H1.
exists x; intuition.
Qed.