finite.v 11.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
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 list.
4
5
6

Class Finite A `{ x y : A, Decision (x = y)} := {
  enum : list A;
7
  NoDup_enum : NoDup enum;
8
9
10
  elem_of_enum x : x  enum
}.
Arguments enum _ {_ _} : clear implicits.
11
Arguments NoDup_enum _ {_ _} : clear implicits.
12
13
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
14
15
  encode := λ x,
    Pos.of_nat $ S $ from_option 0 $ fst <$> list_find (x =) (enum A);
16
17
18
19
20
  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.
21
22
23
  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.
24
25
Qed.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
26
  list_find P (enum A) = decode_nat  fst.
27
28
29
30

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

Lemma card_0_inv P `{finA: Finite A} : card A = 0  A  P.
Proof.
66
  intros ? x. destruct finA as [[|??] ??]; simplify_eq.
67
68
69
70
  by destruct (not_elem_of_nil x).
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A  Inhabited A.
Proof.
71
  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
72
73
  constructor; exact x.
Qed.
74
75
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A  B)
  `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
76
Proof.
77
  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
78
Qed.
79
80
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  f <$> enum A  enum B.
81
Proof.
82
  intros. apply contains_Permutation_length_eq.
83
84
  - by rewrite fmap_length.
  - by apply finite_inj_contains.
85
Qed.
86
87
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  Surj (=) f.
88
89
Proof.
  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
90
  rewrite finite_inj_Permutation; auto using elem_of_enum.
91
92
Qed.

93
94
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A  card B   g : B  A, Surj (=) g.
95
96
97
98
99
100
101
Proof.
  intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
  exists (λ y : B, from_option x' (decode_nat (encode_nat y))).
  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.
102
103
Lemma finite_inj A `{Finite A} B `{Finite B} :
  card A  card B   f : A  B, Inj (=) (=) f.
104
105
Proof.
  split.
106
  - intros. destruct (decide (card A = 0)) as [HA|?].
107
    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
108
109
    destruct (finite_surj A B) as (g&?); auto with lia.
    destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
110
  - intros [f ?]. unfold card. rewrite <-(fmap_length f).
111
    by apply contains_length, (finite_inj_contains f).
112
113
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
114
  card A = card B   f : A  B, Inj (=) (=) f  Surj (=) f.
115
116
Proof.
  split.
117
  - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
118
    exists f; auto using (finite_inj_surj f).
119
  - intros (f&?&?). apply (anti_symm ()); apply finite_inj.
120
    + by exists f.
121
    + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
122
Qed.
123
124
125
126
127
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.
128
Proof.
129
130
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
131
132
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A  B)
133
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
134
135
Proof. apply finite_bijective. eauto. Qed.

136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
(** Decidability of quantification over finite types *)
Section forall_exists.
  Context `{Finite A} (P : A  Prop) `{ x, Decision (P x)}.

  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.

  Global Instance forall_dec: Decision ( x, P x).
  Proof.
   refine (cast_if (decide (Forall P (enum A))));
    abstract by rewrite <-Forall_finite.
  Defined.
  Global Instance exists_dec: Decision ( x, P x).
  Proof.
   refine (cast_if (decide (Exists P (enum A))));
    abstract by rewrite <-Exists_finite.
  Defined.
End forall_exists.

157
158
159
160
161
162
163
164
165
166
167
168
(** Instances *)
Section enc_finite.
  Context `{ x y : A, Decision (x = y)}.
  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',
169
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
170
171
172
173
174
175
176
177
178
179
180
181
    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.
182
  Context `{Finite A,  x y : B, Decision (x = y)} (f : A  B) (g : B  A).
183
  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
184
185

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
186
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
187
188
189
190
191
192
193
194
195
  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.
196
197
  - rewrite elem_of_list_fmap. by intros (?&?&?).
  - apply (NoDup_fmap_2 _); auto using NoDup_enum.
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
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.

220
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
221
222
223
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
  intros. apply NoDup_app; split_ands.
224
225
226
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
  - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
227
228
229
230
231
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
    eauto using @elem_of_enum.
Qed.
232
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
233
234
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

235
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
236
237
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
238
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
239
240
  { constructor. }
  apply NoDup_app; split_ands.
241
  - by apply (NoDup_fmap_2 _), NoDup_enum.
242
  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
243
244
245
    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
    { rewrite elem_of_nil. tauto. }
    rewrite elem_of_app, elem_of_list_fmap.
246
    intros [(?&?&?)|?]; simplify_eq.
247
248
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
249
  - done.
250
251
252
Qed.
Next Obligation.
  intros ?????? [x y]. induction (elem_of_enum x); simpl.
253
254
  - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
  - rewrite elem_of_app; eauto.
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
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.

Let list_enum {A} (l : list A) :  n, list { l : list A | length l = n } :=
  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.
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.
273
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
274
  apply NoDup_app; split_ands.
275
276
  - by apply (NoDup_fmap_2 _).
  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
277
    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
278
279
    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
280
    intros [([??]&?&?)|?]; simplify_eq/=; auto.
281
  - apply IH.
282
283
284
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
285
  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
286
287
288
  { 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 *.
289
  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
290
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
291
  - rewrite elem_of_app. eauto.
292
293
294
295
296
297
298
299
Qed.
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.