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
}.
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 $ from_option id 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 26 27
  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.
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 35 36

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.
37 38
  rewrite Nat2Pos.id by done; simpl.
  destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
39 40
  - 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.
41 42 43 44 45 46 47 48
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.
49 50 51
  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.
52 53 54 55 56
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.
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 61 62 63 64
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.
65
  intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
66
  rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
67
  exists y. by rewrite !Nat2Pos.id by done.
68 69
Qed.

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
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.

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, from_option id 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; auto using (finite_inj_surj f).
158
  - intros (f&?&?). apply (anti_symm ()); apply finite_inj.
159
    + by exists f.
160
    + destruct (surj_cancel f) as (g&?); eauto using 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/=.
211 212 213 214 215 216 217 218 219 220 221 222
    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.
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 234 235 236
  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.
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 247 248 249 250 251 252 253 254 255 256 257 258 259 260
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.

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

276
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
277 278
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
279
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
280
  { constructor. }
281
  apply NoDup_app; split_and?.
282
  - by apply (NoDup_fmap_2 _), NoDup_enum.
283
  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
284 285 286
    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
    { rewrite elem_of_nil. tauto. }
    rewrite elem_of_app, elem_of_list_fmap.
287
    intros [(?&?&?)|?]; simplify_eq.
288 289
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
290
  - done.
291 292 293
Qed.
Next Obligation.
  intros ?????? [x y]. induction (elem_of_enum x); simpl.
294 295
  - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
  - rewrite elem_of_app; eauto.
296 297 298 299 300 301 302
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
303
Definition list_enum {A} (l : list A) :  n, list { l : list A | length l = n } :=
304 305 306 307 308
  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
309

310 311 312 313 314
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.
315
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
316
  apply NoDup_app; split_and?.
317 318
  - by apply (NoDup_fmap_2 _).
  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
319
    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
320 321
    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
322
    intros [([??]&?&?)|?]; simplify_eq/=; auto.
323
  - apply IH.
324 325 326
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
327
  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
328 329 330
  { 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 *.
331
  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
332
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
333
  - rewrite elem_of_app. eauto.
334
Qed.
Ralf Jung's avatar
Ralf Jung committed
335

336 337 338 339 340 341 342
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.
343 344 345 346 347 348 349 350 351 352 353 354 355 356 357

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.