Library atoms

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')

Obligation Tactic := idtac.

Program Definition string_ord_mixin : Preord.mixin_of string :=
  Preord.Mixin string string_ord _ _.

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 _ _.

atom is actually a partial order with respect to =.
Lemma atom_strong_eq : forall (x y:atom), x y -> x = y.

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.

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

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

Lemma perms_len : forall n s s',
  In s' (perms n s) -> String.length s' = n.

Lemma perms_neq_nil : forall n a s,
  perms n (String a s) = nil -> False.

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)

The set of all "choosable" atoms. We enumerate this set using an unfold.
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

  Lemma wf_idents_wf : well_founded idents_wf.

Opaque perms.
  Lemma idents_find_len_aux :
    exists n, exists a,
      idents_set n = a /\ idents_out a.

  Lemma idents_find : exists s,
    s idents_set /\
    String.length s = len.

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.

Section fresh.
  Variable atoms : finset atom.

  Program Definition fresh_idents :=
    esubset_dec atom (fun x => ~In x atoms) _ idents_set.

  Lemma fresh_idents_inhabited : einhabited fresh_idents.

  Definition fresh_atom := choose atom fresh_idents fresh_idents_inhabited.

  Lemma fresh_atom_is_fresh : fresh_atom atoms.
End fresh.

Lemma fresh_atom_is_fresh' (l1 l2:finset atom) :
  l1 l2 ->
  fresh_atom l2 l1.