finite.v 15.2 KB
Newer Older
1
From stdpp Require Export countable vector.
2
Set Default Proof Using "Type".
3

4
Class Finite A `{EqDecision A} := {
5
  enum : list A;
Ralf Jung's avatar
Ralf Jung committed
6
  (* [NoDup] makes it easy to define the cardinality of the type. *)
7
  NoDup_enum : NoDup enum;
8
9
  elem_of_enum x : x  enum
}.
10
Hint Mode Finite ! - : typeclass_instances.
11
12
13
14
Arguments enum : clear implicits.
Arguments enum _ {_ _} : assert.
Arguments NoDup_enum : clear implicits.
Arguments NoDup_enum _ {_ _} : assert.
15
Definition card A `{Finite A} := length (enum A).
16
17

Program Definition finite_countable `{Finite A} : Countable A := {|
18
  encode := λ x,
19
    Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
20
21
  decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
22
Arguments Pos.of_nat : simpl never.
23
24
Next Obligation.
  intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
25
  destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
26
  rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
27
  destruct (list_find_Some (x =.) xs i y); naive_solver.
28
Qed.
29
30
Hint Immediate finite_countable : typeclass_instances.

31
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
32
  list_find P (enum A) = decode_nat  fst.
33

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

70
71
72
73
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
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  | inleft (x  _) => x | inright _ => _
75
76
77
78
79
80
81
82
  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].
83
84
  { by rewrite fin_to_nat_to_fin, decode_encode_nat in Hx; simplify_eq. }
  exfalso; by rewrite ->fin_to_nat_to_fin, decode_encode_nat in Hx.
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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.

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

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

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

  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.

184
185
  Context `{ x, Decision (P x)}.

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

198
199
(** Instances *)
Section enc_finite.
200
  Context `{EqDecision A}.
201
202
203
204
205
206
207
208
209
  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',
210
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
    apply lookup_seq in Hi' as  [-> ?]. apply lookup_seq in Hj' as [-> ?].
212
213
214
215
216
217
218
219
220
221
222
    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.
223
  Context `{Finite A, EqDecision B} (f : A  B) (g : B  A).
224
  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
225
226

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
227
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
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) :=
234
  {| enum := None :: (Some <$> enum A) |}.
235
236
Next Obligation.
  constructor.
237
238
  - rewrite elem_of_list_fmap. by intros (?&?&?).
  - apply (NoDup_fmap_2 _); auto using NoDup_enum.
239
240
241
242
243
244
245
246
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.

Ralf Jung's avatar
Ralf Jung committed
247
248
249
250
251
252
Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
Next Obligation. intros []. Qed.
Lemma Empty_set_card : card Empty_set = 0.
Proof. done. Qed.

253
254
255
256
257
258
259
260
261
262
263
264
265
266
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.

267
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
268
269
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
270
  intros. apply NoDup_app; split_and?.
271
272
273
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
  - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
274
275
276
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
277
    [left|right]; (eexists; split; [done|apply elem_of_enum]).
278
Qed.
279
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
280
281
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

282
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
283
  {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
284
Next Obligation.
285
  intros A ?????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
286
  { constructor. }
287
  apply NoDup_app; split_and?.
288
  - by apply (NoDup_fmap_2 _), NoDup_enum.
289
  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
290
291
292
    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
    { rewrite elem_of_nil. tauto. }
    rewrite elem_of_app, elem_of_list_fmap.
293
    intros [(?&?&?)|?]; simplify_eq.
294
295
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
296
  - done.
297
298
299
Qed.
Next Obligation.
  intros ?????? [x y]. induction (elem_of_enum x); simpl.
300
  - rewrite elem_of_app, !elem_of_list_fmap. eauto using elem_of_enum.
301
  - rewrite elem_of_app; eauto.
302
303
304
305
306
307
308
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
309
Definition list_enum {A} (l : list A) :  n, list { l : list A | length l = n } :=
310
311
312
  fix go n :=
  match n with
  | 0 => [[]eq_refl]
313
  | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
314
  end.
Ralf Jung's avatar
Ralf Jung committed
315

316
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
317
318
  {| enum := list_enum (enum A) n |}.
Next Obligation.
319
  intros A ?? n. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
320
  revert IH. generalize (list_enum (enum A) n). intros l Hl.
321
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
322
  apply NoDup_app; split_and?.
323
324
  - by apply (NoDup_fmap_2 _).
  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
325
    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
326
327
    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
328
    intros [([??]&?&?)|?]; simplify_eq/=; auto.
329
  - apply IH.
330
331
Qed.
Next Obligation.
332
333
  intros A ?? n [l Hl]. revert l Hl.
  induction n as [|n IH]; intros [|x l] Hl; simpl; simplify_eq.
334
335
336
  { 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 *.
337
  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
338
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
339
  - rewrite elem_of_app. eauto.
340
Qed.
Ralf Jung's avatar
Ralf Jung committed
341

342
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
343
344
345
346
347
348
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.
349
350

Fixpoint fin_enum (n : nat) : list (fin n) :=
351
  match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
352
353
354
355
356
357
358
359
360
361
362
363
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.
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399

Section sig_finite.
  Context {A} (P : A  Prop) `{ x, Decision (P x)}.

  Fixpoint list_filter_sig (l : list A) : list (sig P) :=
    match l with
    | [] => []
    | x :: l => match decide (P x) with
              | left H => x  H :: list_filter_sig l
              | _ => list_filter_sig l
              end
    end.
  Lemma list_filter_sig_filter (l : list A) :
    proj1_sig <$> list_filter_sig l = filter P l.
  Proof.
    induction l as [| a l IH]; [done |].
    simpl; rewrite filter_cons.
    destruct (decide _); csimpl; by rewrite IH.
  Qed.

  Context `{Finite A} `{ x, ProofIrrel (P x)}.

  Global Program Instance sig_finite : Finite (sig P) :=
    {| enum := list_filter_sig (enum A) |}.
  Next Obligation.
    eapply NoDup_fmap_1. rewrite list_filter_sig_filter.
    apply NoDup_filter, NoDup_enum.
  Qed.
  Next Obligation.
    intros p. apply (elem_of_list_fmap_2_inj proj1_sig).
    rewrite list_filter_sig_filter, elem_of_list_filter.
    split; [by destruct p | apply elem_of_enum].
  Qed.
  Lemma sig_card : card (sig P) = length (filter P (enum A)).
  Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
End sig_finite.