finite.v 13.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* 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.
110 111
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A  B)
  `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
Robbert Krebbers's avatar
Robbert Krebbers committed
112 113 114
Proof.
  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
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 118
Proof.
  intros. apply contains_Permutation_length_eq.
119 120
  - by rewrite fmap_length.
  - by apply finite_inj_contains.
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).
147
    by apply contains_length, (finite_inj_contains 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 184 185 186 187 188 189 190 191 192 193 194 195 196
  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.

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