Set.v 6.6 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
MARCHE Claude's avatar
MARCHE Claude committed
4
(*  Copyright 2010-2017   --   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 28
(* Why3 assumption *)
Definition set (a:Type) := (a -> 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 40 41
(* Why3 assumption *)
Definition mem {a:Type} {a_WT:WhyType a} (x:a) (s:(a -> bool)): Prop := ((s
  x) = true).
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45

Hint Unfold mem.

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

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

(* Why3 goal *)
52 53
Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a ->
  bool)) (s2:(a -> bool)), (infix_eqeq s1 s2) -> (s1 = s2).
54
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
55
intros a a_WT s1 s2 h1.
56 57 58 59 60 61 62 63 64 65
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
66 67 68
Qed.

(* Why3 assumption *)
69 70
Definition subset {a:Type} {a_WT:WhyType a} (s1:(a -> bool)) (s2:(a ->
  bool)): Prop := forall (x:a), (mem x s1) -> (mem x s2).
MARCHE Claude's avatar
MARCHE Claude committed
71

72
(* Why3 goal *)
73
Lemma subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)),
74
  (subset s s).
75 76
Proof.
now intros a a_WT s x.
77 78
Qed.

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

(* Why3 assumption *)
89
Definition is_empty {a:Type} {a_WT:WhyType a} (s:(a -> bool)): Prop :=
MARCHE Claude's avatar
MARCHE Claude committed
90 91 92
  forall (x:a), ~ (mem x s).

(* Why3 goal *)
93 94
Lemma mem_empty : forall {a:Type} {a_WT:WhyType a}, (is_empty
  (map.Const.const false: (a -> bool))).
95 96
Proof.
now intros a a_WT x.
MARCHE Claude's avatar
MARCHE Claude committed
97 98
Qed.

99
(* Why3 goal *)
100 101 102
Lemma add_spec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
  bool)), forall (y:a), (mem y (map.Map.set s x true)) <-> ((y = x) \/ (mem y
  s)).
103
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
104
intros a a_WT x y s.
105 106
unfold Map.set, mem.
destruct why_decidable_eq ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
107 108 109
Qed.

(* Why3 goal *)
110 111 112
Lemma remove_spec : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
  bool)), forall (y:a), (mem y (map.Map.set s x false)) <-> ((~ (y = x)) /\
  (mem y s)).
113
Proof.
114 115 116
intros a a_WT x s y.
unfold Map.set, mem.
destruct why_decidable_eq ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
117 118 119
Qed.

(* Why3 goal *)
120 121
Lemma add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
  bool)), (mem x s) -> ((map.Map.set (map.Map.set s x false) x true) = s).
122
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
123 124
intros a a_WT x s h1.
apply extensionality; intro y.
125 126
rewrite add_spec.
rewrite remove_spec.
127
destruct (why_decidable_eq y x) as [->|H] ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
128 129 130
Qed.

(* Why3 goal *)
131 132 133
Lemma remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
  bool)), ((map.Map.set (map.Map.set s x true) x false) = (map.Map.set s x
  false)).
134
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
135 136
intros a a_WT x s.
apply extensionality; intro y.
137 138 139
rewrite remove_spec.
rewrite remove_spec.
rewrite add_spec.
140
destruct (why_decidable_eq y x) as [->|H] ; intuition.
MARCHE Claude's avatar
MARCHE Claude committed
141 142 143
Qed.

(* Why3 goal *)
144 145
Lemma subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(a ->
  bool)), (subset (map.Map.set s x false) s).
146 147
Proof.
intros a a_WT x s y.
148
rewrite remove_spec.
149
now intros [_ H].
MARCHE Claude's avatar
MARCHE Claude committed
150 151 152
Qed.

(* Why3 goal *)
153 154 155
Definition union: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a ->
  bool) -> (a -> bool).
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
156
intros a a_WT s1 s2.
157
exact (fun x => orb (s1 x) (s2 x)).
MARCHE Claude's avatar
MARCHE Claude committed
158 159 160
Defined.

(* Why3 goal *)
161 162 163
Lemma union_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
  (s2:(a -> bool)), forall (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/
  (mem x s2)).
164
Proof.
165 166
intros a a_WT s1 s2 x.
apply Bool.orb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
167 168 169
Qed.

(* Why3 goal *)
170 171 172
Definition inter: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a ->
  bool) -> (a -> bool).
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
173
intros a a_WT s1 s2.
174
exact (fun x => andb (s1 x) (s2 x)).
MARCHE Claude's avatar
MARCHE Claude committed
175 176 177
Defined.

(* Why3 goal *)
178 179 180
Lemma inter_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
  (s2:(a -> bool)), forall (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\
  (mem x s2)).
181
Proof.
182 183
intros a a_WT s1 s2 x.
apply Bool.andb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
184 185 186
Qed.

(* Why3 goal *)
187 188 189
Definition diff: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a ->
  bool) -> (a -> bool).
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
190
intros a a_WT s1 s2.
191
exact (fun x => andb (s1 x) (negb (s2 x))).
MARCHE Claude's avatar
MARCHE Claude committed
192 193 194
Defined.

(* Why3 goal *)
195 196 197
Lemma diff_spec : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
  (s2:(a -> bool)), forall (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\
  ~ (mem x s2)).
198
Proof.
199 200 201 202 203
intros a a_WT s1 s2 x.
unfold mem, diff.
rewrite Bool.not_true_iff_false.
rewrite <- Bool.negb_true_iff.
apply Bool.andb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
204 205 206
Qed.

(* Why3 goal *)
207 208
Lemma subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(a -> bool))
  (s2:(a -> bool)), (subset (diff s1 s2) s1).
209 210
Proof.
intros a a_WT s1 s2 x.
211
rewrite diff_spec.
212
now intros [H _].
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215
Qed.

(* Why3 goal *)
216 217 218
Definition complement: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> (a ->
  bool).
Proof.
MARCHE Claude's avatar
MARCHE Claude committed
219
intros a a_WT s.
220
exact (fun x => negb (s x)).
MARCHE Claude's avatar
MARCHE Claude committed
221 222 223
Defined.

(* Why3 goal *)
224 225
Lemma complement_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(a ->
  bool)), forall (x:a), (((complement s) x) = true) <-> ~ ((s x) = true).
226
Proof.
227 228 229 230
intros a a_WT s x.
unfold complement.
rewrite Bool.not_true_iff_false.
apply Bool.negb_true_iff.
MARCHE Claude's avatar
MARCHE Claude committed
231 232 233
Qed.

(* Why3 goal *)
234 235 236 237 238
Definition choose: forall {a:Type} {a_WT:WhyType a}, (a -> bool) -> a.
Proof.
intros a a_WT s.
assert (i: inhabited a) by (apply inhabits, why_inhabitant).
exact (epsilon i (fun x => mem x s)).
MARCHE Claude's avatar
MARCHE Claude committed
239 240 241
Defined.

(* Why3 goal *)
242 243
Lemma choose_spec : forall {a:Type} {a_WT:WhyType a}, forall (s:(a -> bool)),
  (~ (is_empty s)) -> (mem (choose s) s).
244
Proof.
245 246 247 248
intros a a_WT s h1.
unfold choose.
apply epsilon_spec.
now apply not_all_not_ex.
MARCHE Claude's avatar
MARCHE Claude committed
249
Qed.
250