finite.v 13.8 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
(* This file is distributed under the terms of the BSD license. *)
3
From stdpp Require Export countable vector.
4
Set Default Proof Using "Type".
5

6
Class Finite A `{EqDecision A} := {
7
  enum : list A;
8
  NoDup_enum : NoDup enum;
9
10
  elem_of_enum x : x  enum
}.
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
Arguments enum _ _ _ : clear implicits.
Arguments enum _ {_ _}.
Arguments NoDup_enum _ _ _ : clear implicits.
Arguments NoDup_enum _ {_ _}.
15
16
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
17
  encode := λ x,
18
    Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
19
20
21
22
23
  decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
Arguments Pos.of_nat _ : simpl never.
Next Obligation.
  intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
24
25
26
  destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto.
  rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
  destruct (list_find_Some (x =) xs i y); naive_solver.
27
28
Qed.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
29
  list_find P (enum A) = decode_nat  fst.
30
31
32
33

Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
Proof.
  destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
34
35
  rewrite Nat2Pos.id by done; simpl.
  destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
36
37
  - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
  - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
38
39
40
41
42
43
44
45
Qed.
Lemma encode_decode A `{finA: Finite A} i :
  i < card A   x, decode_nat i = Some x  encode_nat x = i.
Proof.
  destruct finA as [xs Hxs HA].
  unfold encode_nat, decode_nat, encode, decode, card; simpl.
  intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx].
  exists x. rewrite !Nat2Pos.id by done; simpl.
46
47
48
  destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto.
  destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
  rewrite Hj; csimpl; eauto using NoDup_lookup.
49
50
51
52
53
Qed.
Lemma find_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
  find P = Some x  P x.
Proof.
  destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
54
  intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=.
55
  rewrite !Nat2Pos.id in Hx by done.
56
  destruct (list_find_Some P xs i y); naive_solver.
57
58
59
60
61
Qed.
Lemma find_is_Some `{finA: Finite A} P `{ x, Decision (P x)} x :
  P x   y, find P = Some y  P y.
Proof.
  destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
62
  intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
63
  rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
64
  exists y. by rewrite !Nat2Pos.id by done.
65
66
Qed.

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
Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
  Fin.of_nat_lt (encode_lt_card x).
Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
  match Some_dec (decode_nat i) return _ with
  | inleft (exist x _) => x | inright _ => _
  end.
Next Obligation.
  intros A ?? i ?; exfalso.
  destruct (encode_decode A i); naive_solver auto using fin_to_nat_lt.
Qed.
Lemma decode_encode_fin `{Finite A} (x : A) : decode_fin (encode_fin x) = x.
Proof.
  unfold decode_fin, encode_fin. destruct (Some_dec _) as [[x' Hx]|Hx].
  { by rewrite fin_to_of_nat, decode_encode_nat in Hx; simplify_eq. }
  exfalso; by rewrite ->fin_to_of_nat, decode_encode_nat in Hx.
Qed.

Lemma fin_choice {n} {B : fin n  Type} (P :  i, B i  Prop) :
  ( i,  y, P i y)   f,  i, P i (f i).
Proof.
  induction n as [|n IH]; intros Hex.
  { exists (fin_0_inv _); intros i; inv_fin i. }
  destruct (IH _ _ (λ i, Hex (FS i))) as [f Hf], (Hex 0%fin) as [y Hy].
  exists (fin_S_inv _ y f); intros i; by inv_fin i.
Qed.
Lemma finite_choice `{Finite A} {B : A  Type} (P :  x, B x  Prop) :
  ( x,  y, P x y)   f,  x, P x (f x).
Proof.
  intros Hex. destruct (fin_choice _ (λ i, Hex (decode_fin i))) as [f ?].
  exists (λ x, eq_rect _ _ (f(encode_fin x)) _ (decode_encode_fin x)); intros x.
  destruct (decode_encode_fin x); simpl; auto.
Qed.

100
101
Lemma card_0_inv P `{finA: Finite A} : card A = 0  A  P.
Proof.
102
  intros ? x. destruct finA as [[|??] ??]; simplify_eq.
103
104
105
106
  by destruct (not_elem_of_nil x).
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A  Inhabited A.
Proof.
107
  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
108
109
  constructor; exact x.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A  B)
  `{!Inj (=) (=) f} : f <$> enum A + enum B.
112
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
114
Qed.
115
116
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  f <$> enum A  enum B.
117
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
  intros. apply submseteq_Permutation_length_eq.
119
  - by rewrite fmap_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
  - by apply finite_inj_submseteq.
121
Qed.
122
123
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  Surj (=) f.
124
125
Proof.
  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
126
  rewrite finite_inj_Permutation; auto using elem_of_enum.
127
128
Qed.

129
130
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A  card B   g : B  A, Surj (=) g.
131
132
Proof.
  intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
133
  exists (λ y : B, from_option id x' (decode_nat (encode_nat y))).
134
135
136
137
  intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
  { pose proof (encode_lt_card x); lia. }
  exists y. by rewrite Hy2, decode_encode_nat.
Qed.
138
139
Lemma finite_inj A `{Finite A} B `{Finite B} :
  card A  card B   f : A  B, Inj (=) (=) f.
140
141
Proof.
  split.
142
  - intros. destruct (decide (card A = 0)) as [HA|?].
143
    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
144
145
    destruct (finite_surj A B) as (g&?); auto with lia.
    destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
146
  - intros [f ?]. unfold card. rewrite <-(fmap_length f).
Robbert Krebbers's avatar
Robbert Krebbers committed
147
    by apply submseteq_length, (finite_inj_submseteq f).
148
149
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
150
  card A = card B   f : A  B, Inj (=) (=) f  Surj (=) f.
151
152
Proof.
  split.
153
  - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
154
    exists f; auto using (finite_inj_surj f).
155
  - intros (f&?&?). apply (anti_symm ()); apply finite_inj.
156
    + by exists f.
157
    + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
158
Qed.
159
160
161
162
163
Lemma inj_card `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A  card B.
Proof. apply finite_inj. eauto. Qed.
Lemma surj_card `{Finite A} `{Finite B} (f : A  B)
  `{!Surj (=) f} : card B  card A.
164
Proof.
165
166
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
167
168
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A  B)
169
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
170
171
Proof. apply finite_bijective. eauto. Qed.

172
173
(** Decidability of quantification over finite types *)
Section forall_exists.
174
  Context `{Finite A} (P : A  Prop).
175
176
177
178
179
180

  Lemma Forall_finite : Forall P (enum A)  ( x, P x).
  Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed.
  Lemma Exists_finite : Exists P (enum A)  ( x, P x).
  Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed.

181
182
  Context `{ x, Decision (P x)}.

183
  Global Instance forall_dec: Decision ( x, P x).
184
  Proof using Type*.
185
186
187
188
   refine (cast_if (decide (Forall P (enum A))));
    abstract by rewrite <-Forall_finite.
  Defined.
  Global Instance exists_dec: Decision ( x, P x).
189
  Proof using Type*.
190
191
192
193
194
   refine (cast_if (decide (Exists P (enum A))));
    abstract by rewrite <-Exists_finite.
  Defined.
End forall_exists.

195
196
(** Instances *)
Section enc_finite.
197
  Context `{EqDecision A}.
198
199
200
201
202
203
204
205
206
  Context (to_nat : A  nat) (of_nat : nat  A) (c : nat).
  Context (of_to_nat :  x, of_nat (to_nat x) = x).
  Context (to_nat_c :  x, to_nat x < c).
  Context (to_of_nat :  i, i < c  to_nat (of_nat i) = i).

  Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
  Next Obligation.
    apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
    destruct (seq _ _ !! i) as [i'|] eqn:Hi',
207
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
208
209
210
211
212
213
214
215
216
217
218
219
    destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
    rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
  Qed.
  Next Obligation.
    intros x. rewrite elem_of_list_fmap. exists (to_nat x).
    split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
  Qed.
  Lemma enc_finite_card : card A = c.
  Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
End enc_finite.

Section bijective_finite.
220
  Context `{Finite A, EqDecision B} (f : A  B) (g : B  A).
221
  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
222
223

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
224
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
225
226
227
228
229
230
231
232
233
  Next Obligation.
    intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
  Qed.
End bijective_finite.

Program Instance option_finite `{Finite A} : Finite (option A) :=
  {| enum := None :: Some <$> enum A |}.
Next Obligation.
  constructor.
234
235
  - rewrite elem_of_list_fmap. by intros (?&?&?).
  - apply (NoDup_fmap_2 _); auto using NoDup_enum.
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
Qed.
Next Obligation.
  intros ??? [x|]; [right|left]; auto.
  apply elem_of_list_fmap. eauto using elem_of_enum.
Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.

Program Instance unit_finite : Finite () := {| enum := [tt] |}.
Next Obligation. apply NoDup_singleton. Qed.
Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
Lemma unit_card : card unit = 1.
Proof. done. Qed.

Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Next Obligation.
  constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton.
Qed.
Next Obligation. intros [|]. left. right; left. Qed.
Lemma bool_card : card bool = 2.
Proof. done. Qed.

258
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
259
260
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
261
  intros. apply NoDup_app; split_and?.
262
263
264
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
  - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
265
266
267
268
269
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
    eauto using @elem_of_enum.
Qed.
270
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
271
272
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

273
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
274
275
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
276
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
277
  { constructor. }
278
  apply NoDup_app; split_and?.
279
  - by apply (NoDup_fmap_2 _), NoDup_enum.
280
  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
281
282
283
    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
    { rewrite elem_of_nil. tauto. }
    rewrite elem_of_app, elem_of_list_fmap.
284
    intros [(?&?&?)|?]; simplify_eq.
285
286
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
287
  - done.
288
289
290
Qed.
Next Obligation.
  intros ?????? [x y]. induction (elem_of_enum x); simpl.
291
292
  - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
  - rewrite elem_of_app; eauto.
293
294
295
296
297
298
299
Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
  unfold card; simpl. induction (enum A); simpl; auto.
  rewrite app_length, fmap_length. auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
300
Definition list_enum {A} (l : list A) :  n, list { l : list A | length l = n } :=
301
302
303
304
305
  fix go n :=
  match n with
  | 0 => [[]eq_refl]
  | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
  end.
Ralf Jung's avatar
Ralf Jung committed
306

307
308
309
310
311
Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
  {| enum := list_enum (enum A) n |}.
Next Obligation.
  intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
  revert IH. generalize (list_enum (enum A) n). intros l Hl.
312
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
313
  apply NoDup_app; split_and?.
314
315
  - by apply (NoDup_fmap_2 _).
  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
316
    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
317
318
    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
319
    intros [([??]&?&?)|?]; simplify_eq/=; auto.
320
  - apply IH.
321
322
323
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
324
  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
325
326
327
  { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
  revert IH. generalize (list_enum (enum A) n). intros k Hk.
  induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
328
  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
329
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
330
  - rewrite elem_of_app. eauto.
331
Qed.
Ralf Jung's avatar
Ralf Jung committed
332

333
334
335
336
337
338
339
Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
Proof.
  unfold card; simpl. induction n as [|n IH]; simpl; auto.
  rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
  induction (enum A) as [|x xs IH]; intros l; simpl; auto.
  by rewrite app_length, fmap_length, IH.
Qed.
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354

Fixpoint fin_enum (n : nat) : list (fin n) :=
  match n with 0 => [] | S n => 0%fin :: FS <$> fin_enum n end.
Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation.
  intros n. induction n; simpl; constructor.
  - rewrite elem_of_list_fmap. by intros (?&?&?).
  - by apply (NoDup_fmap _).
Qed.
Next Obligation.
  intros n i. induction i as [|n i IH]; simpl;
    rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
Qed.
Lemma fin_card n : card (fin n) = n.
Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.