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 ??????. 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 319 320
  {| 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.
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 332
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
333
  induction n as [|n IH]; intros [|x l] ?; 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.