A Coq library for domain theory (http://rwd.rdockins.name/domains/)

root / atoms.v

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
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
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
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
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
(* Copyright (c) 2014, Robert Dockins *)

Require Import Ascii.
Require Export String.
Open Scope string_scope.

Require Import Setoid.
Require Import NArith.
Require Import Arith.
Require Import Omega.
Require Import List.

Require Import basics.
Require Import categories.
Require Import preord.
Require Import sets.
Require Import finsets.
Require Import esets.

(**  * Atoms for nominal types

     Atoms are concretely represented by ASCII strings.
     Here we provide some operations on atoms, including an
     operation for choosing fresh atoms.
  *)

(**  ASCII characters are ordered by inheriting their numerical order.
  *)
Definition char_ord (x y:ascii) := N.le (N_of_ascii x) (N_of_ascii y).

(**  Strings are ordered lexicographically.
  *)
Fixpoint string_ord (x y:string) :=
  match x, y with
  | "", _ => True
  | String a x', "" => False
  | String a x', String b y' =>
       (a <> b /\ char_ord a b) \/
       (a = b /\ string_ord x' y')
  end.

Obligation Tactic := idtac.

Program Definition string_ord_mixin : Preord.mixin_of string :=
  Preord.Mixin string string_ord _ _.
Next Obligation.
  induction x; simpl; auto.
Qed.
Next Obligation.
  induction x; simpl; auto.
  induction y; simpl; intuition.
  destruct z; auto.
  intuition subst.
  left. 
  unfold char_ord in *.
  split; auto.
  intro. subst a.
  apply H.
  rewrite <- (ascii_N_embedding a1).
  rewrite <- (ascii_N_embedding a0).
  f_equal.
  apply N.le_antisymm; auto.
  eapply N.le_trans; eauto.
  auto.
  destruct z. elim H0.
  subst a0.
  intuition subst; auto.
  right; split; eauto.
Qed.

(**  [atom] is the preorder of strings with their
     lexicographic order.  We use these for object-level
     variables.
  *)
Canonical Structure atom : Preord.type :=
  Preord.Pack string string_ord_mixin.

(**   The order on [atom] is decidable.
  *)
Program Definition atom_dec : ord_dec atom := OrdDec _ _.
Next Obligation.
  induction x; simpl; intros.
  left. exact I.
  destruct y.
  right. intro. apply H.
  case_eq (N_of_ascii a ?= N_of_ascii a0)%N.
  intros.
  destruct (IHx y).
  left. red. simpl.
  right. split; auto.
  rewrite <- (ascii_N_embedding a).
  rewrite <- (ascii_N_embedding a0).
  replace (N_of_ascii a) with (N_of_ascii a0); auto.
  symmetry.
  apply N.compare_eq. auto.
  right.
  intro. red in H0. simpl in H0.
  intuition.
  apply H0.
  rewrite <- (ascii_N_embedding a).
  rewrite <- (ascii_N_embedding a0).
  replace (N_of_ascii a) with (N_of_ascii a0); auto.
  symmetry.
  apply N.compare_eq. auto.
  intro.
  left. red; simpl.
  left.
  split. intro.
  subst a0.
  generalize (N.compare_ge_iff (N_of_ascii a) (N_of_ascii a)).
  intros. destruct H0. apply H1. apply N.le_refl. auto.
  red. red. rewrite H. discriminate.
  intro. right. intro.
  red in H0. simpl in H0.
  destruct H0.
  destruct H0. hnf in H1.
  apply H1; auto.
  destruct H0. subst a0.
  generalize (N.compare_le_iff (N_of_ascii a) (N_of_ascii a)).
  rewrite H. intros.
  destruct H0. apply H2; auto.
  apply N.le_refl.
Defined.

(**  [atom] is actually a partial order with respect to [=].
  *)
Lemma atom_strong_eq : forall (x y:atom), x ≈ y -> x = y.
Proof.
  induction x.
  induction y; simpl; intros; auto.
  destruct H. elim H0.
  induction y; simpl; intros; auto.
  destruct H. elim H.
  destruct H.  
  destruct H. destruct H0.
  destruct H; destruct H0.
  elim H.
  rewrite <- (ascii_N_embedding a).
  rewrite <- (ascii_N_embedding a0).
  f_equal.
  apply N.le_antisymm; auto.
  destruct H; destruct H0.
  elim H; auto.
  destruct H0.
  destruct H; destruct H0.
  elim H0; auto.
  destruct H; destruct H0.
  subst a0.
  f_equal. apply IHx.
  split; auto.
Qed.


Section unfold.
  Variables X A:Type.
  Variable step : X -> X * A.
  
  Definition unfold_stream (seed:X) (n:N) : A :=
       N.peano_rect (fun _ => X -> A)
                    (fun x => snd (step x))
                    (fun _ r x => r (fst (step x)))
                    n seed.

  Variable invariant : X -> Prop.
  Variable wf_rel : X -> X -> Prop.
  Variable out_prop : A -> Prop.

  Hypothesis wf : well_founded wf_rel.

  Hypothesis ind_step : forall x,
    invariant x -> let (x',a) := step x in
      (invariant x' /\ wf_rel x' x) \/ out_prop a.
      
  Lemma unfold_find : forall x,
    invariant x ->
    exists n a, unfold_stream x n = a /\ out_prop a.
  Proof.
    induction x using (well_founded_induction wf); intros.
    generalize (ind_step x H0).
    case_eq (step x); intros x' a ?.
    intros [[??]|?].
    destruct (H x') as [n [a' [??]]]; auto.
    exists (N.succ n). exists a'.
    split; auto.
    unfold unfold_stream; rewrite N.peano_rect_succ.
    rewrite H1. simpl. auto.
    exists N.zero. exists a.
    compute.
    rewrite H1; split; simpl; auto.   
  Defined.

End unfold.

(**  When choosing fresh atoms, these are the only characters
     that will be used.
  *)
Definition allowable_chars := "abcdefghijklmnopqrstuvwxyz".


Fixpoint adjoin_char (s:string) (ls:list string) :=
  match s with
  | "" => nil
  | String a s' => map (fun q => String a q) ls ++ 
                   adjoin_char s' ls
  end.

Fixpoint perms (n:nat) (s:string) : list string :=
  match n with
  | 0 => ""::nil
  | S n' => adjoin_char s (perms n' s)
  end.

Lemma perms_len : forall n s s',
  In s' (perms n s) -> String.length s' = n.
Proof.
  induction n; simpl; intuition subst; auto.
  revert H. generalize s at 1.
  induction s0; simpl; intros. elim H.
  apply in_app_or in H. destruct H.
  generalize (IHn s). revert H.
  generalize (perms n s).
  induction l; simpl; intuition.
  subst s'. simpl. f_equal.
  apply H0; auto.
  apply IHs0; auto.
Qed.

Lemma perms_neq_nil : forall n a s,
  perms n (String a s) = nil -> False.
Proof.
  induction n; simpl; intros.
  discriminate.
  apply (IHn a s).
  destruct (perms n (String a s)); auto.
  simpl in H. discriminate.
Qed.

Definition idents_step (x:nat * list string) :
  (nat * list string * option string) :=
  match x with
  | (n, s::l) => (n, l, Some s)
  | (n, nil)  => (S n, perms (S n) allowable_chars, None)
  end.

(**  The set of all "choosable" atoms.  We enumerate
     this set using an unfold.
  *)
Definition idents_set : eset atom :=
  unfold_stream (nat*list string) (option string) idents_step (0, nil).

(**  The [idents_set] contains at least on string of a given
     (nonzero) length.  This will be used to show that we can
     always choose a fresh atom distinct from any finite set of atoms.
  *)
Section idents_length.
  Variable len:nat.
  Hypothesis len0 : 0 < len. 

  Definition idents_inv (x:nat * list string) :=
    fst x < len \/ 
    (fst x = len /\ 
      snd x <> nil /\
      forall s, In s (snd x) -> String.length s = len).

  Definition idents_wf (x' x:nat * list string) :=
    (fst x < fst x' <= len) \/ 
    (fst x = fst x' /\ length (snd x') < length (snd x)).

  Definition idents_out (a:option string) :=
    match a with
    | None => False
    | Some s => String.length s = len
    end.

  Lemma wf_idents_wf : well_founded idents_wf.
  Proof.
    red. intros [x l].
    destruct (le_gt_dec x len) as [H|H].
    set (z := len - x).
    assert (x = len - z).
    subst z. 
    omega.
    clearbody z. revert x l H H0.
    induction z using (well_founded_induction lt_wf).
    intro x. 
    induction l using 
      (well_founded_induction (well_founded_ltof _ (@List.length string))); intros.
    constructor; intros.
    destruct y; simpl in *.
    destruct H3; simpl in *.
    apply H with (len - n); omega.
    destruct H3. subst n.
    apply H0; auto.
    induction l using 
      (well_founded_induction (well_founded_ltof _ (@List.length string))); intros.
    constructor; intros.
    destruct H1. simpl in *.
    elimtype False. omega.
    simpl in *. destruct H1.
    destruct y; simpl in *.  
    subst n. apply H0.
    auto.
  Defined.

Opaque perms.
  Lemma idents_find_len_aux :
    exists n, exists a,
      idents_set n = a /\ idents_out a.
  Proof.
    apply unfold_find with idents_inv idents_wf.
    apply wf_idents_wf.
    unfold idents_inv. unfold idents_step.
    intros [n l]. simpl.
    intros. destruct H.
    destruct l; simpl.
    left.
    split.
    destruct (eq_nat_dec (S n) len).
    right. split; auto.
    split.
    red. apply perms_neq_nil.
    rewrite e.
    apply perms_len.
    left. omega.
    red. simpl.
    left. omega.
    left. split; auto.
    red. simpl.
    right. split; auto.
    destruct H as [?[??]]. subst n.
    destruct l. elim H0. auto.
    simpl. right.
    apply H1. simpl; auto.
    hnf. simpl.
    auto.
  Defined.

  Lemma idents_find : exists s,
    s ∈ idents_set /\
    String.length s = len.
  Proof.
    destruct idents_find_len_aux as [n [a [??]]].
    hnf in H0. destruct a. 2: elim H0.
    exists c. split; auto.
    exists n. rewrite H. auto.
  Defined.

End idents_length.

Definition max_len
  := fold_right (fun x y => max (String.length x) y) 0.

Lemma max_len_le (xs:finset atom) (x:atom) :
  x ∈ xs ->
  String.length x <= max_len xs.
Proof.
  induction xs; simpl; intros.
  apply nil_elem in H. elim H.
  apply cons_elem in H. destruct H.
  apply atom_strong_eq in H. subst x.
  apply Max.le_max_l.
  apply le_trans with (max_len xs); auto.
  apply Max.le_max_r.
Qed.  

Section fresh.
  Variable atoms : finset atom.

  Program Definition fresh_idents :=
    esubset_dec atom (fun x => ~In x atoms) _ idents_set.
  Next Obligation.
    intro.
    destruct (In_dec string_dec x atoms); auto.
  Defined.

  Lemma fresh_idents_inhabited : einhabited fresh_idents.
  Proof.    
    apply member_inhabited.
    destruct (idents_find (S (max_len atoms))) as [s [??]].
    red. auto with arith.
    exists s. unfold fresh_idents.
    destruct H as [n ?].
    exists n. simpl.
    unfold esubset_dec.
    destruct (idents_set n).
    2: elim H.
    unfold fresh_idents_obligation_1.
    destruct (in_dec string_dec c atoms).
    assert (String.length s <= max_len atoms).
    apply max_len_le. exists c. split; auto.
    rewrite H0 in H1.
    omega.
    auto.
  Defined.

  Definition fresh_atom := choose atom fresh_idents fresh_idents_inhabited.

  Lemma fresh_atom_is_fresh : fresh_atom ∉ atoms.
  Proof.
    red; intro.
    unfold fresh_atom in H.
    unfold choose in H.
    destruct (find_inhabitant atom fresh_idents fresh_idents_inhabited)
      as [a [b [??]]].
    simpl in *.
    unfold fresh_idents in e.
    unfold esubset_dec in e.
    destruct (idents_set b). 2: discriminate.
    destruct (fresh_idents_obligation_1 c).
    apply n.
    inversion e. subst a.
    destruct H as [q [??]].
    apply atom_strong_eq in H0. subst q. auto.
    discriminate.
  Qed.
End fresh.

Lemma fresh_atom_is_fresh' (l1 l2:finset atom) :
  l1 ⊆ l2 ->
  fresh_atom l2 ∉ l1.
Proof.
  repeat intro.
  apply H in H0.
  apply (fresh_atom_is_fresh l2); auto.
Qed.