collections.v 8.17 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
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
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.
  Lemma elem_of_equiv_alt X Y : X  Y  ( x, x  X  x  Y)  ( x, x  Y  x  X).
  Proof. firstorder. Qed.

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

  Lemma empty_ne_singleton x :    {{ x }}.
  Proof. intros [_ E]. destruct (elem_of_empty x). apply E. now apply elem_of_singleton. Qed. 
End collection.

Section cmap.
  Context `{Collection A C}.

  Lemma elem_of_map_1 (f : A  A) (X : C) (x : A) : x  X  f x  map f X.
  Proof. intros. apply (elem_of_map _). eauto. Qed.
  Lemma elem_of_map_1_alt (f : A  A) (X : C) (x : A) y : x  X  y = f x  y  map f X.
  Proof. intros. apply (elem_of_map _). eauto. Qed.
  Lemma elem_of_map_2 (f : A  A) (X : C) (x : A) : x  map f X   y, x = f y  y  X.
  Proof. intros. now apply (elem_of_map _). Qed.
End cmap.

Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x  X } := exist ( X) (fresh X) (is_fresh X).

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
  | H : context [ _  {{ _ }} ] |- _ => setoid_rewrite elem_of_singleton in H
  | 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
  | |- context [ _  {{ _ }} ] => setoid_rewrite elem_of_singleton
  | |- 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 *)
  | H : context [  _, _ ] |- _ => edestruct 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
  | H : context [ _  _ ] |- _ => edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
  (* 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.
     rewrite <-E1, <-E2; intuition.
    rewrite E1, E2; intuition.
  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.
  Lemma elem_of_upto_singleton x y : elem_of_upto x {{ y }}  R x y.
  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.

  Lemma elem_of_upto_union X Y x : elem_of_upto x (X  Y)  elem_of_upto x X  elem_of_upto x Y.
  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.
  Lemma no_dup_add x X : ¬elem_of_upto x X  no_dup X  no_dup ({{ x }}  X).
  Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
  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.
  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.
  Lemma cforall_singleton x : cforall {{ x }}  P x.
  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.
  Lemma cexists_singleton x : cexists {{ x }}  P x.
  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.

Lemma cforall_weak `{Collection A B} (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
  cforall P X  cforall Q X.
Proof. firstorder. Qed.
Lemma cexists_weak `{Collection A B} (P Q : A  Prop) (Hweak :  x, P x  Q x) X :
  cexists P X  cexists Q X.
Proof. firstorder. Qed.