collections.v 9.05 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
Require Export base orders.

Section collection.
  Context `{Collection A B}.

  Lemma elem_of_empty_iff x : x    False.
  Proof. split. apply elem_of_empty. easy. Qed.

  Lemma elem_of_union_l x X Y : x  X  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.
  Lemma elem_of_union_r x X Y : x  Y  x  X  Y.
  Proof. intros. apply elem_of_union. auto. Qed.

  Global Instance collection_subseteq: SubsetEq B := λ X Y,  x, x  X  x  Y.
  Global Instance: BoundedJoinSemiLattice B.
  Proof. firstorder. Qed.
  Global Instance: MeetSemiLattice B.
  Proof. firstorder. Qed.

  Lemma elem_of_subseteq X Y : X  Y   x, x  X  x  Y.
  Proof. easy. Qed.
  Lemma elem_of_equiv X Y : X  Y   x, x  X  x  Y.
  Proof. firstorder. Qed.
24
25
  Lemma elem_of_equiv_alt X Y :
    X  Y  ( x, x  X  x  Y)  ( x, x  Y  x  X).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
  Proof. firstorder. Qed.

  Global Instance: Proper ((=) ==> () ==> iff) ().
  Proof. intros ???. subst. firstorder. Qed.

31
32
33
34
35
  Lemma empty_ne_singleton x :    {[ x ]}.
  Proof.
    intros [_ E]. destruct (elem_of_empty x).
    apply E. now apply elem_of_singleton.
  Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
36
37
38
39
40
End collection.

Section cmap.
  Context `{Collection A C}.

41
42
  Lemma elem_of_map_1 (f : A  A) (X : C) (x : A) :
    x  X  f x  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  Proof. intros. apply (elem_of_map _). eauto. Qed.
44
45
  Lemma elem_of_map_1_alt (f : A  A) (X : C) (x : A) y :
    x  X  y = f x  y  map f X.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Proof. intros. apply (elem_of_map _). eauto. Qed.
47
48
  Lemma elem_of_map_2 (f : A  A) (X : C) (x : A) :
    x  map f X   y, x = f y  y  X.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
50
51
  Proof. intros. now apply (elem_of_map _). Qed.
End cmap.

52
53
Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x  X } :=
  exist ( X) (fresh X) (is_fresh X).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
57
58
59
60
61
62

Lemma elem_of_fresh_iff `{FreshSpec A C} (X : C) : fresh X  X  False.
Proof. split. apply is_fresh. easy. Qed.

Ltac split_elem_ofs := repeat
  match goal with
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_subseteq in H
  | H : context [ _  _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
  | H : context [ _   ] |- _ => setoid_rewrite elem_of_empty_iff in H
63
  | H : context [ _  {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
69
70
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_union in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_intersection in H
  | H : context [ _  _  _ ] |- _ => setoid_rewrite elem_of_difference in H
  | H : context [ _  map _ _ ] |- _ => setoid_rewrite elem_of_map in H
  | |- context [ _  _ ] => setoid_rewrite elem_of_subseteq
  | |- context [ _  _ ] => setoid_rewrite elem_of_equiv_alt
  | |- context [ _   ] => setoid_rewrite elem_of_empty_iff
71
  | |- context [ _  {[ _ ]} ] => setoid_rewrite elem_of_singleton
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_union
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_intersection
  | |- context [ _  _  _ ] => setoid_rewrite elem_of_difference
  | |- context [ _  map _ _ ] => setoid_rewrite elem_of_map
  end.

Ltac destruct_elem_ofs := repeat
  match goal with
  | H : context [ @elem_of (_ * _) _ _ ?x _ ] |- _ => is_var x; destruct x
  | H : context [ @elem_of (_ + _) _ _ ?x _] |- _ => is_var x; destruct x
  end.

Tactic Notation "simplify_elem_of" tactic(t) :=
  intros; (* due to bug #2790 *)
  simpl in *;
  split_elem_ofs;
  destruct_elem_ofs;
  intuition (simplify_eqs; t).
Tactic Notation "simplify_elem_of" := simplify_elem_of auto.

Ltac naive_firstorder t :=
  match goal with
  (* intros *)
  | |-  _, _ => intro; naive_firstorder t
  (* destructs without information loss *)
  | H : False |- _ => destruct H
  | H : ?X, Hneg : ¬?X|- _ => now destruct Hneg
  | H : _  _ |- _ => destruct H; naive_firstorder t
  | H :  _, _  |- _ => destruct H; naive_firstorder t
  (* simplification *)
  | |- _ => progress (simplify_eqs; simpl in *); naive_firstorder t
  (* constructs *)
  | |- _  _ => split; naive_firstorder t
  (* solve *)
  | |- _ => solve [t]
  (* dirty destructs *)
108
109
110
111
112
113
  | H : context [  _, _ ] |- _ =>
    edestruct H; clear H;naive_firstorder t || clear H; naive_firstorder t
  | H : context [ _  _ ] |- _ => 
    destruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
  | H : context [ _  _ ] |- _ =>
    edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  (* dirty constructs *)
  | |-  x, _ => eexists; naive_firstorder t
  | |- _  _ => left; naive_firstorder t || right; naive_firstorder t
  | H : _  False |- _ => destruct H; naive_firstorder t
  end.
Tactic Notation "naive_firstorder" tactic(t) :=
  unfold iff, not in *; 
  naive_firstorder t.

Tactic Notation "esimplify_elem_of" tactic(t) := 
  (simplify_elem_of t); 
  try naive_firstorder t.
Tactic Notation "esimplify_elem_of" := esimplify_elem_of (eauto 5).

Section no_dup.
  Context `{Collection A B} (R : relation A) `{!Equivalence R}.

  Definition elem_of_upto (x : A) (X : B) :=  y, y  X  R x y.
  Definition no_dup (X : B) :=  x y, x  X  y  X  R x y  x = y.

  Global Instance: Proper (() ==> iff) (elem_of_upto x).
  Proof. firstorder. Qed.
  Global Instance: Proper (R ==> () ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
139
140
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
142
143
144
145
146
147
148
  Qed.
  Global Instance: Proper (() ==> iff) no_dup.
  Proof. firstorder. Qed.

  Lemma elem_of_upto_elem_of x X : x  X  elem_of_upto x X.
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
  Lemma elem_of_upto_empty x : ¬elem_of_upto x .
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
149
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]}  R x y.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.

152
153
  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
157
158
159
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X   y, y  X  ¬R x y.
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.

  Lemma no_dup_empty: no_dup .
  Proof. unfold no_dup. simplify_elem_of. Qed.
160
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({[ x ]}  X).
Robbert Krebbers's avatar
Robbert Krebbers committed
161
  Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
162
163
164
165
166
  Lemma no_dup_inv_add x X : x  X  no_dup ({[ x ]}  X)  ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
    rewrite (Hnodup x y) in Hin; simplify_elem_of.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
169
170
171
172
173
174
175
176
177
178
179
180
  Lemma no_dup_inv_union_l X Y : no_dup (X  Y)  no_dup X.
  Proof. unfold no_dup. simplify_elem_of. Qed.
  Lemma no_dup_inv_union_r X Y : no_dup (X  Y)  no_dup Y.
  Proof. unfold no_dup. simplify_elem_of. Qed.
End no_dup.

Section quantifiers.
  Context `{Collection A B} (P : A  Prop).

  Definition cforall X :=  x, x  X  P x.
  Definition cexists X :=  x, x  X  P x.

  Lemma cforall_empty : cforall .
  Proof. unfold cforall. simplify_elem_of. Qed.
181
  Lemma cforall_singleton x : cforall {[ x ]}  P x.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
185
186
187
188
189
190
191
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union X Y : cforall X  cforall Y  cforall (X  Y).
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union_inv_1 X Y : cforall (X  Y)  cforall X.
  Proof. unfold cforall. simplify_elem_of. Qed.
  Lemma cforall_union_inv_2 X Y : cforall (X  Y)  cforall Y.
  Proof. unfold cforall. simplify_elem_of. Qed.

  Lemma cexists_empty : ¬cexists .
  Proof. unfold cexists. esimplify_elem_of. Qed.
192
  Lemma cexists_singleton x : cexists {[ x ]}  P x.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
197
198
199
200
201
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_1 X Y : cexists X  cexists (X  Y).
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_2 X Y : cexists Y  cexists (X  Y).
  Proof. unfold cexists. esimplify_elem_of. Qed.
  Lemma cexists_union_inv X Y : cexists (X  Y)  cexists X  cexists Y.
  Proof. unfold cexists. esimplify_elem_of. Qed.
End quantifiers.

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
Section more_quantifiers.
  Context `{Collection A B}.
  
  Lemma cforall_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cforall P X  cforall Q X.
  Proof. firstorder. Qed.
  Lemma cexists_weak (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
    cexists P X  cexists Q X.
  Proof. firstorder. Qed.
End more_quantifiers.

Section fresh.
  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .

  Fixpoint fresh_list (n : nat) (X : C) : list A :=
    match n with
    | 0 => []
    | S n => let x := fresh X in x :: fresh_list n ({[ x ]}  X)
    end.

  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X)  x  X.
  Proof.
    revert X. induction n; simpl.
    * easy.
    * intros X [?| Hin]. subst.
      + apply is_fresh.
      + apply IHn in Hin. simplify_elem_of.
  Qed.

  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
  Proof.
    revert X.
    induction n; simpl; constructor; auto.
    intros Hin. apply fresh_list_is_fresh in Hin.
    simplify_elem_of.
  Qed.
End fresh.