countable.v 11.9 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From Coq.QArith Require Import QArith_base Qcanon.
2
From stdpp Require Export list numbers list_numbers.
3
Set Default Proof Using "Type".
4
5
Local Open Scope positive.

6
Class Countable A `{EqDecision A} := {
7
8
9
10
  encode : A  positive;
  decode : positive  option A;
  decode_encode x : decode (encode x) = Some x
}.
11
Hint Mode Countable ! - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
Arguments encode : simpl never.
Arguments decode : simpl never.
14

15
Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
16
Proof.
17
  intros x y Hxy; apply (inj Some).
18
19
  by rewrite <-(decode_encode x), Hxy, decode_encode.
Qed.
20
21
22
23
24

Definition encode_nat `{Countable A} (x : A) : nat :=
  pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
  decode (Pos.of_nat (S i)).
25
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
26
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
27
Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
28
29
30
31
32
33
Proof.
  pose proof (Pos2Nat.is_pos (encode x)).
  unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
  by rewrite Pos2Nat.id, decode_encode.
Qed.

34
35
36
37
38
39
40
41
42
Definition encode_Z `{Countable A} (x : A) : Z :=
  Zpos (encode x).
Definition decode_Z `{Countable A} (i : Z) : option A :=
  match i with Zpos i => decode i | _ => None end.
Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
Proof. apply decode_encode. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
43
(** * Choice principles *)
44
Section choice.
45
  Context `{Countable A} (P : A  Prop).
46
47

  Inductive choose_step: relation positive :=
48
    | choose_step_None {p} : decode (A:=A) p = None  choose_step (Pos.succ p) p
49
    | choose_step_Some {p} {x : A} :
50
       decode p = Some x  ¬P x  choose_step (Pos.succ p) p.
51
52
53
54
55
  Lemma choose_step_acc : ( x, P x)  Acc choose_step 1%positive.
  Proof.
    intros [x Hx]. cut ( i p,
      i  encode x  1 + encode x = p + i  Acc choose_step p).
    { intros help. by apply (help (encode x)). }
56
    intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
57
58
59
60
61
62
    { constructor. intros j. assert (p = encode x) by lia; subst.
      inversion 1 as [? Hd|?? Hd]; subst;
        rewrite decode_encode in Hd; congruence. }
    constructor. intros j.
    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
  Qed.
63
64
65

  Context `{ x, Decision (P x)}.

66
67
68
69
  Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
    match Some_dec (decode i) with
    | inleft (xHx) =>
      match decide (P x) with
Robbert Krebbers's avatar
Robbert Krebbers committed
70
      | left _ => x | right H => choose_go (Acc_inv acc (choose_step_Some Hx H))
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
      end
    | inright H => choose_go (Acc_inv acc (choose_step_None H))
    end.
  Fixpoint choose_go_correct {i} (acc : Acc choose_step i) : P (choose_go acc).
  Proof. destruct acc; simpl. repeat case_match; auto. Qed.
  Fixpoint choose_go_pi {i} (acc1 acc2 : Acc choose_step i) :
    choose_go acc1 = choose_go acc2.
  Proof. destruct acc1, acc2; simpl; repeat case_match; auto. Qed.

  Definition choose (H:  x, P x) : A := choose_go (choose_step_acc H).
  Definition choose_correct (H:  x, P x) : P (choose H) := choose_go_correct _.
  Definition choose_pi (H1 H2 :  x, P x) :
    choose H1 = choose H2 := choose_go_pi _ _.
  Definition choice (HA :  x, P x) : { x | P x } := _choose_correct HA.
End choice.

87
Lemma surj_cancel `{Countable A} `{EqDecision B}
88
  (f : A  B) `{!Surj (=) f} : { g : B  A & Cancel (=) f g }.
89
Proof.
90
91
  exists (λ y, choose (λ x, f x = y) (surj f y)).
  intros y. by rewrite (choose_correct (λ x, f x = y) (surj f y)).
92
93
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
(** * Instances *)
95
(** ** Injection *)
96
Section inj_countable.
97
  Context `{Countable A, EqDecision B}.
98
99
  Context (f : B  A) (g : A  option B) (fg :  x, g (f x) = Some x).

100
  Program Instance inj_countable : Countable B :=
101
102
    {| encode y := encode (f y); decode p := x  decode p; g x |}.
  Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
103
End inj_countable.
104

105
106
107
108
109
110
111
112
Section inj_countable'.
  Context `{Countable A, EqDecision B}.
  Context (f : B  A) (g : A  B) (fg :  x, g (f x) = x).

  Program Instance inj_countable' : Countable B := inj_countable f (Some  g) _.
  Next Obligation. intros x. by f_equal/=. Qed.
End inj_countable'.

Ralf Jung's avatar
Ralf Jung committed
113
114
115
116
117
(** ** Empty *)
Program Instance Empty_set_countable : Countable Empty_set :=
  {| encode u := 1; decode p := None |}.
Next Obligation. by intros []. Qed.

118
119
120
121
122
123
124
125
126
127
128
129
(** ** Unit *)
Program Instance unit_countable : Countable unit :=
  {| encode u := 1; decode p := Some () |}.
Next Obligation. by intros []. Qed.

(** ** Bool *)
Program Instance bool_countable : Countable bool := {|
  encode b := if b then 1 else 2;
  decode p := Some match p return bool with 1 => true | _ => false end
|}.
Next Obligation. by intros []. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
130
(** ** Option *)
131
Program Instance option_countable `{Countable A} : Countable (option A) := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
  encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
  decode p := if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
134
135
136
137
138
139
|}.
Next Obligation.
  intros ??? [x|]; simpl; repeat case_decide; auto with lia.
  by rewrite Pos.pred_succ, decode_encode.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
140
(** ** Sums *)
141
142
143
144
145
146
147
148
149
150
151
Program Instance sum_countable `{Countable A} `{Countable B} :
  Countable (A + B)%type := {|
    encode xy :=
      match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
    decode p :=
      match p with
      | 1 => None | p~0 => inl <$> decode p | p~1 => inr <$> decode p
      end
  |}.
Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
152
(** ** Products *)
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
Fixpoint prod_encode_fst (p : positive) : positive :=
  match p with
  | 1 => 1
  | p~0 => (prod_encode_fst p)~0~0
  | p~1 => (prod_encode_fst p)~0~1
  end.
Fixpoint prod_encode_snd (p : positive) : positive :=
  match p with
  | 1 => 1~0
  | p~0 => (prod_encode_snd p)~0~0
  | p~1 => (prod_encode_snd p)~1~0
  end.
Fixpoint prod_encode (p q : positive) : positive :=
  match p, q with
  | 1, 1 => 1~1
  | p~0, 1 => (prod_encode_fst p)~1~0
  | p~1, 1 => (prod_encode_fst p)~1~1
  | 1, q~0 => (prod_encode_snd q)~0~1
  | 1, q~1 => (prod_encode_snd q)~1~1
  | p~0, q~0 => (prod_encode p q)~0~0
  | p~0, q~1 => (prod_encode p q)~1~0
  | p~1, q~0 => (prod_encode p q)~0~1
  | p~1, q~1 => (prod_encode p q)~1~1
  end.
Fixpoint prod_decode_fst (p : positive) : option positive :=
  match p with
  | p~0~0 => (~0) <$> prod_decode_fst p
  | p~0~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
  | p~1~0 => (~0) <$> prod_decode_fst p
  | p~1~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
  | 1~0 => None
  | 1~1 => Some 1
  | 1 => Some 1
  end.
Fixpoint prod_decode_snd (p : positive) : option positive :=
  match p with
  | p~0~0 => (~0) <$> prod_decode_snd p
  | p~0~1 => (~0) <$> prod_decode_snd p
  | p~1~0 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
  | p~1~1 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
  | 1~0 => Some 1
  | 1~1 => Some 1
  | 1 => None
  end.

Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
Proof.
  assert ( p, prod_decode_fst (prod_encode_fst p) = Some p).
201
  { intros p'. by induction p'; simplify_option_eq. }
202
  assert ( p, prod_decode_fst (prod_encode_snd p) = None).
203
204
  { intros p'. by induction p'; simplify_option_eq. }
  revert q. by induction p; intros [?|?|]; simplify_option_eq.
205
206
207
208
Qed.
Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
Proof.
  assert ( p, prod_decode_snd (prod_encode_snd p) = Some p).
209
  { intros p'. by induction p'; simplify_option_eq. }
210
  assert ( p, prod_decode_snd (prod_encode_fst p) = None).
211
212
  { intros p'. by induction p'; simplify_option_eq. }
  revert q. by induction p; intros [?|?|]; simplify_option_eq.
213
214
215
Qed.
Program Instance prod_countable `{Countable A} `{Countable B} :
  Countable (A * B)%type := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
216
    encode xy := prod_encode (encode (xy.1)) (encode (xy.2));
217
218
219
220
221
222
    decode p :=
     x  prod_decode_fst p = decode;
     y  prod_decode_snd p = decode; Some (x, y)
  |}.
Next Obligation.
  intros ?????? [x y]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
223
224
  rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
  by rewrite !decode_encode.
225
226
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
227
(** ** Lists *)
228
229
230
231
Global Program Instance list_countable `{Countable A} : Countable (list A) :=
  {| encode xs := positives_flatten (encode <$> xs);
     decode p := positives  positives_unflatten p;
                 mapM decode positives; |}.
232
Next Obligation.
233
234
235
236
237
  intros A EqA CA xs.
  simpl.
  rewrite positives_unflatten_flatten.
  simpl.
  apply (mapM_fmap_Some _ _ _ decode_encode).
238
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
242

(** ** Numbers *)
Instance pos_countable : Countable positive :=
  {| encode := id; decode := Some; decode_encode x := eq_refl |}.
243
244
245
246
247
Program Instance N_countable : Countable N := {|
  encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
  decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
|}.
Next Obligation.
248
249
  intros [|p]; simpl; [done|].
  by rewrite decide_False, Pos.pred_succ by (by destruct p).
250
251
Qed.
Program Instance Z_countable : Countable Z := {|
Robbert Krebbers's avatar
Robbert Krebbers committed
252
253
  encode x := match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
  decode p := Some match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
254
255
|}.
Next Obligation. by intros [|p|p]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
Program Instance nat_countable : Countable nat :=
  {| encode x := encode (N.of_nat x); decode p := N.to_nat <$> decode p |}.
258
Next Obligation.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
  by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
260
Qed.
Hai Dang's avatar
Hai Dang committed
261

262
263
264
265
266
267
Global Program Instance Qc_countable : Countable Qc :=
  inj_countable
    (λ p : Qc, let 'Qcmake (x # y) _ := p return _ in (x,y))
    (λ q : Z * positive, let '(x,y) := q return _ in Some (Q2Qc (x # y))) _.
Next Obligation.
  intros [[x y] Hcan]. f_equal. apply Qc_is_canon. simpl. by rewrite Hcan.
Hai Dang's avatar
Hai Dang committed
268
269
Qed.

270
271
272
273
274
275
276
Global Program Instance Qp_countable : Countable Qp :=
  inj_countable
    Qp_car
    (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
Next Obligation.
  intros [p Hp]. unfold mguard, option_guard; simpl.
  case_match; [|done]. f_equal. by apply Qp_eq.
Hai Dang's avatar
Hai Dang committed
277
Qed.
278
279

(** ** Generic trees *)
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
280
Local Close Scope positive.
281
282
283
284
285
286
287
288
289
290

Inductive gen_tree (T : Type) : Type :=
  | GenLeaf : T  gen_tree T
  | GenNode : nat  list (gen_tree T)  gen_tree T.
Arguments GenLeaf {_} _ : assert.
Arguments GenNode {_} _ _ : assert.

Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
Proof.
 refine (
291
  fix go t1 t2 := let _ : EqDecision _ := @go in
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
  match t1, t2 with
  | GenLeaf x1, GenLeaf x2 => cast_if (decide (x1 = x2))
  | GenNode n1 ts1, GenNode n2 ts2 =>
     cast_if_and (decide (n1 = n2)) (decide (ts1 = ts2))
  | _, _ => right _
  end); abstract congruence.
Defined.

Fixpoint gen_tree_to_list {T} (t : gen_tree T) : list (nat * nat + T) :=
  match t with
  | GenLeaf x => [inr x]
  | GenNode n ts => (ts = gen_tree_to_list) ++ [inl (length ts, n)]
  end.

Fixpoint gen_tree_of_list {T}
    (k : list (gen_tree T)) (l : list (nat * nat + T)) : option (gen_tree T) :=
  match l with
  | [] => head k
  | inr x :: l => gen_tree_of_list (GenLeaf x :: k) l
  | inl (len,n) :: l =>
     gen_tree_of_list (GenNode n (reverse (take len k)) :: drop len k) l
  end.

Lemma gen_tree_of_to_list {T} k l (t : gen_tree T) :
  gen_tree_of_list k (gen_tree_to_list t ++ l) = gen_tree_of_list (t :: k) l.
Proof.
318
  revert t k l; fix FIX 1; intros [|n ts] k l; simpl; auto.
319
320
321
  trans (gen_tree_of_list (reverse ts ++ k) ([inl (length ts, n)] ++ l)).
  - rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
    induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
322
    rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
323
324
325
326
327
328
329
330
331
332
  - simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
      by (by rewrite reverse_length).
Qed.

Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
  inj_countable gen_tree_to_list (gen_tree_of_list []) _.
Next Obligation.
  intros T ?? t.
  by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.