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

6
Class Finite A `{EqDecision A} := {
Robbert Krebbers's avatar
Robbert Krebbers committed
7
8
9
10
  enum : list A;
  NoDup_enum : NoDup enum;
  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 _ {_ _}.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
  encode := λ x,
18
    Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
  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.
  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.
Qed.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
  list_find P (enum A) = decode_nat  fst.

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.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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.
  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.
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/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
58
59
60
61
62
  rewrite !Nat2Pos.id in Hx by done.
  destruct (list_find_Some P xs i y); naive_solver.
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.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
  exists y. by rewrite !Nat2Pos.id by done.
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
Lemma card_0_inv P `{finA: Finite A} : card A = 0  A  P.
Proof.
102
  intros ? x. destruct finA as [[|??] ??]; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
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|].
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
  intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
Qed.
122
123
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  Surj (=) f.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
128
Qed.

129
130
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A  card B   g : B  A, Surj (=) g.
Robbert Krebbers's avatar
Robbert Krebbers committed
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))).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
Proof.
  split.
142
  - intros. destruct (decide (card A = 0)) as [HA|?].
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
148
149
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
150
  card A = card B   f : A  B, Inj (=) (=) f  Surj (=) f.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
    + by exists f.
157
    + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof.
165
166
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
Robbert Krebbers's avatar
Robbert Krebbers committed
167
168
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A  B)
169
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
Robbert Krebbers's avatar
Robbert Krebbers committed
170
171
172
173
Proof. apply finite_bijective. eauto. Qed.

(** Decidability of quantification over finite types *)
Section forall_exists.
174
  Context `{Finite A} (P : A  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
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)}.

Robbert Krebbers's avatar
Robbert Krebbers committed
183
  Global Instance forall_dec: Decision ( x, P x).
184
  Proof using Type*.
Robbert Krebbers's avatar
Robbert Krebbers committed
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*.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
192
193
194
195
196
   refine (cast_if (decide (Exists P (enum A))));
    abstract by rewrite <-Exists_finite.
  Defined.
End forall_exists.

(** Instances *)
Section enc_finite.
197
  Context `{EqDecision A}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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/=.
Robbert Krebbers's avatar
Robbert Krebbers committed
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}.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
225
226
227
228
229
230
231
232
233

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
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.

Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
  {| 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
265
266
267
268
269
270
271
272
273
274
275
276
277
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
    eauto using @elem_of_enum.
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
  { 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
286
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
287
  - done.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 } :=
Robbert Krebbers's avatar
Robbert Krebbers committed
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

Robbert Krebbers's avatar
Robbert Krebbers committed
307
308
309
310
311
312
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.
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
323
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
324
  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
Robbert Krebbers's avatar
Robbert Krebbers committed
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'.
Robbert Krebbers's avatar
Robbert Krebbers committed
329
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
330
  - rewrite elem_of_app. eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
Qed.
Ralf Jung's avatar
Ralf Jung committed
332

Robbert Krebbers's avatar
Robbert Krebbers committed
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.