Qcert.Basic.Util.RFresh

Section RFresh.



  Section finder.
    Context {A:Type}.
    Context (incr:A→A).
    Context (f:A→bool).

    Fixpoint find_bounded (bound:nat) (init:A)
      := match bound with
           | O ⇒ None
           | S n ⇒
             if f init
             then Some init
             else find_bounded n (incr init)
         end.

    Lemma find_bounded_correct bound init y :
      find_bounded bound init = Some y →
      f y = true.

  End finder.

  Lemma find_bounded_S_ge f bound init y :
    find_bounded S f bound init = Some y →
    y ≥ init.

  Lemma find_bounded_S_seq f bound init :
    find_bounded S f bound init = find f (seq init bound).


  Lemma incl_NoDup_sublist_perm {A} {dec:EqDec A eq} {l1 l2:list A} :
    NoDup l1 →
    incl l1 l2 →
    ∃ l1', Permutation l1 l1' ∧ sublist l1' l2.

    Lemma incl_NoDup_length_le {A} {dec:EqDec A eq} {l1 l2:list A} :
    NoDup l1 →
    incl l1 l2 →
    length l1 ≤ length l2.

  Lemma find_fresh_from {A:Type} {dec:EqDec A eq} (bad l:list A) :
    length l > length bad →
    NoDup l →
    {y | find (fun x : A ⇒ if in_dec equiv_dec x bad then false else true) l = Some y}.

  Lemma find_over_map {A B} f (g:A→B) (l:list A) :
    find f (map g l) = lift g (find (fun x ⇒ f (g x)) l).

  Lemma seq_ge init bound :
    ∀ x, In x (seq init bound) → x ≥ init.

  Lemma seq_NoDup init bound :
    NoDup (seq init bound).

  Lemma find_bounded_S_nin_finds' {A:Type} f {dec:EqDec A eq} (dom:list A)
        (bound:nat) (pf:bound > length dom)
        (inj:∀ x y, f x = f y → x = y) :
        {y:A | lift f (find_bounded S
                 (fun x ⇒
                    if in_dec equiv_dec (f x) dom
                    then false else true)
                 bound 0) = Some y}.

  Definition find_bounded_S_nin_finds {A:Type} f {dec:EqDec A eq} (dom:list A)
        (bound:nat) (pf:bound > length dom)
        (inj:∀ x y, f x = f y → x = y) :
        {y:A | lift f (find_bounded S
                 (fun x ⇒
                    if in_dec equiv_dec (f x) dom
                    then false else true)
                 bound 0) = Some y}.

  Lemma compose_inj {A B C} (f:B→C) (g:A→B) :
    (∀ x y, f x = f y → x = y) →
    (∀ x y, g x = g y → x = y) →
    (∀ x y, f (g x) = f (g y) → x = y).

  Definition find_fresh_inj_f {A:Type} {dec:EqDec A eq} f (inj:∀ x y, f x = f y → x = y) (dom:list A) : A
    := proj1_sig (find_bounded_S_nin_finds f dom (S (length dom)) (gt_Sn_n _) inj).

  Lemma find_fresh_inj_f_fresh {A:Type} {dec:EqDec A eq} f (inj:∀ x y, f x = f y → x = y) (dom:list A) :
    ¬ In (find_fresh_inj_f f inj dom) dom.

  Definition find_fresh_string (dom:list string)
    := find_fresh_inj_f
         nat_to_string16
         nat_to_string16_inj
         dom.

  Lemma find_fresh_string_is_fresh (dom:list string) :
    ¬ In (find_fresh_string dom) dom.

  Lemma append_eq_inv1 x y z : append x y = append x z → y = z.

  Lemma prefix_refl y : prefix y y = true.

  Lemma substring_append_cancel x y :
    substring (String.length x) (String.length y) (append x y) = y.

  Lemma string_length_append x y :
    String.length (append x y) = String.length x + String.length y.

  Lemma prefix_nil post : prefix ""%string post = true.

  Lemma prefix_app pre post : prefix pre (append pre post) = true.

  Lemma prefix_break {pre x} :
    prefix pre x = true →
    {y | x = append pre y}.


  Lemma substring_split s n m l :
    append (substring s n l) (substring (s+n) m l) = substring s (n+m) l.

  Lemma substring_all l :
    substring 0 (String.length l) l = l.

  Lemma substring_bounded s n l :
    substring s n l = substring s (min n (String.length l - s)) l.

  Lemma substring_le_prefix s n m l :
    n ≤ m →
    prefix (substring s n l) (substring s m l) = true.

  Lemma substring_prefix n l :
    prefix (substring 0 n l) l = true.

  Lemma in_of_append pre y l :
      In (append pre y) l ↔
      In y (map
              (fun x ⇒ substring (String.length pre) (String.length x - String.length pre) x)
              (filter (prefix pre) l)).

  Definition fresh_var (pre:string) (dom:list string) :=
    let problems:=filter (prefix pre) dom in
    let problemEnds:=
        map (fun x ⇒ substring (String.length pre) (String.length x - String.length pre) x) problems in
    append pre (find_fresh_string problemEnds).

  Lemma fresh_var_fresh pre (dom:list string) :
    ¬ In (fresh_var pre dom) dom.

  Lemma fresh_var_fresh1 x1 pre dom :
    x1 ≠ fresh_var pre (x1::dom).

  Lemma fresh_var_fresh2 x1 x2 pre dom :
    x2 ≠ fresh_var pre (x1::x2::dom).

   Lemma fresh_var_fresh3 x1 x2 x3 pre dom :
    x3 ≠ fresh_var pre (x1::x2::x3::dom).

  Lemma fresh_var_fresh4 x1 x2 x3 x4 pre dom :
    x4 ≠ fresh_var pre (x1::x2::x3::x4::dom).

  Definition fresh_var2 pre1 pre2 (dom:list string) :=
    let fresh_var1 := fresh_var pre1 dom in
    (fresh_var1, fresh_var pre2 (fresh_var1::dom)).

  Lemma fresh_var2_distinct pre1 pre2 dom :
    (fst (fresh_var2 pre1 pre2 dom)) ≠
    (snd (fresh_var2 pre1 pre2 dom)).

  Definition get_var_base (sep:string) (var:string)
    := match index 0 (string_reverse sep) (string_reverse var) with
         | Some n ⇒ substring 0 (String.length var - (S n)) var
         | None ⇒ var
       end.

  Lemma get_var_base_pre sep var :
    prefix (get_var_base sep var) var = true.

  Definition fresh_var_from sep (oldvar:string) (dom:list string) : string
    := if in_dec string_dec oldvar dom
       then fresh_var (append (get_var_base sep oldvar) sep) dom
       else oldvar.

  Lemma fresh_var_from_fresh sep oldvar (dom:list string) :
    ¬ In (fresh_var_from sep oldvar dom) dom.

  Lemma append_ass s1 s2 s3 : ((s1 ++ s2) ++ s3 = s1 ++ s2 ++ s3)%string.


End RFresh.