Require Import Uint63.
Require Export PrimString.
Require Export PrimStringAxioms.

Require Import Coq.micromega.Lia.
Require Import Coq.micromega.ZifyUint63.
Require Import Coq.micromega.Zify.
Require Import Coq.Numbers.Cyclic.Int63.Ring63.
Require Import ZArith.

#[local] Open Scope Z_scope.
#[local] Open Scope list_scope.
#[local] Arguments to_Z _/ : simpl nomatch.

#[local] Instance Op_max_length : ZifyClasses.CstOp max_length :=
  { TCst := 16777211%Z ; TCstInj := eq_refl }.
Add Zify CstOp Op_max_length.

#[local] Ltac case_if :=
  lazymatch goal with
  | |- context C [if ?b then _ else _] => destruct b eqn:?
  | H : context C [if ?b then _ else _] |- _ => destruct b eqn:?
  end.

Lemma to_list_inj (s1 s2 : string) :
  to_list s1 = to_list s2 -> s1 = s2.

Lemma to_of_list (l : list char63) :
  List.Forall char63_valid l ->
  Z.of_nat (List.length l) <= to_Z max_length ->
  to_list (of_list l) = l.

Lemma get_spec_in_bounds (s : string) (i : int) :
  to_Z i < to_Z (length s) ->
  char63_valid (get s i) /\
  List.nth_error (to_list s) (to_nat i) = Some (get s i).

Lemma get_spec_not_in_bounds (s : string) (i : int) :
  to_Z (length s) <= to_Z i ->
  get s i = 0%uint63.

Lemma make_spec_valid_length (i : int) (c : char63) :
  to_Z i <= to_Z max_length ->
  to_list (make i c) = List.repeat (c land 255)%uint63 (to_nat i).

Lemma make_spec_invalid_length (i : int) (c : char63) :
  to_Z max_length < to_Z i ->
  to_list (make i c) = List.repeat (c land 255)%uint63 (to_nat max_length).

Lemma cat_spec_valid_length (s1 s2 : string) :
  to_Z (length s1) + to_Z (length s2) <= to_Z max_length ->
  to_list (cat s1 s2) = to_list s1 ++ to_list s2.

Lemma valid_length (s : string) :
  to_Z (length s) <= to_Z max_length.

Lemma length_spec_int (s : string) :
  length s = of_Z (Z.of_nat (List.length (to_list s))).

Lemma length_spec_Z (s : string) :
  to_Z (length s) = Z.of_nat (List.length (to_list s)).

Lemma make_length_spec (i : int) (c : char63) :
  to_Z i <= to_Z max_length ->
  length (make i c) = i.

Lemma sub_length_spec (s : string) (off len : int) :
  to_Z off <= to_Z (length s) ->
  to_Z len <= to_Z (length s) - to_Z off ->
  length (sub s off len) = len.

Lemma cat_length_spec (s1 s2 : string) :
  length (cat s1 s2) = Uint63.min max_length (length s1 + length s2)%uint63.

Lemma cat_length_spec_no_overflow (s1 s2 : string) :
  to_Z (length s1) + to_Z (length s2) <= to_Z max_length ->
  length (cat s1 s2) = (length s1 + length s2)%uint63.

Lemma get_char63_valid (s : string) (i : int) :
  char63_valid (get s i).

Lemma make_get_spec (i j : int) (c : char63) :
  to_Z j < to_Z max_length ->
  to_Z j < to_Z i ->
  get (make i c) j = (c land 255)%uint63.

Lemma make_get_spec_valid (i j : int) (c : char63) :
  to_Z j < to_Z max_length ->
  to_Z j < to_Z i ->
  char63_valid c ->
  get (make i c) j = c.

Lemma sub_get_spec (s : string) (off len i : int) :
  to_Z off + to_Z i < wB ->
  to_Z i < to_Z len ->
  get (sub s off len) i = get s (off + i).

Lemma cat_get_spec_l (s1 s2 : string) (i : int) :
  to_Z i < to_Z (length s1) ->
  get (cat s1 s2) i = get s1 i.

Lemma cat_get_spec_r (s1 s2 : string) (i : int) :
  to_Z (length s1) <= to_Z i ->
  to_Z i < to_Z max_length ->
  get (cat s1 s2) i = get s2 (i - length s1).

Lemma char63_compare_refl (c1 c2 : char63) :
  char63_compare c1 c2 = Eq <-> c1 = c2.

Lemma char63_compare_antisym (c1 c2 : char63) :
  char63_compare c2 c1 = CompOpp (char63_compare c1 c2).

Lemma char63_compare_trans (c1 c2 c3 : char63) (c : comparison) :
  char63_compare c1 c2 = c -> char63_compare c2 c3 = c -> char63_compare c1 c3 = c.

Lemma compare_refl (s : string) : compare s s = Eq.

Lemma compare_antisym (s1 s2 : string) :
  compare s2 s1 = CompOpp (compare s1 s2).

Lemma compare_trans (c : comparison) (s1 s2 s3 : string) :
  compare s1 s2 = c -> compare s2 s3 = c -> compare s1 s3 = c.

Lemma compare_eq_correct (s1 s2 : string) :
  compare s1 s2 = Eq -> s1 = s2.

Lemma string_eq_ext (s1 s2 : string) :
  (length s1 = length s2 /\
   forall i, to_Z i < to_Z (length s1) -> get s1 i = get s2 i) ->
  s1 = s2.

Lemma to_list_firstn_skipn_middle (s : string) (i : int) :
  to_Z i < to_Z (length s) ->
  to_list s = List.firstn (to_nat i) (to_list s) ++
                get s i :: List.skipn (to_nat (i + 1)) (to_list s).

Lemma compare_spec (s1 s2 : string) (c : comparison) :
  compare s1 s2 = c <->
  exists i,
    to_Z i <= to_Z (length s1) /\
    to_Z i <= to_Z (length s2) /\
    (forall j, to_Z j < to_Z i -> get s1 j = get s2 j) /\
    match (i =? length s1, i =? length s2)%uint63 with
    | (true , true ) => c = Eq
    | (true , false) => c = Lt
    | (false, true ) => c = Gt
    | (false, false) =>
        match Uint63.compare (get s1 i) (get s2 i) with
        | Eq => False
        | ci => c = ci
        end
    end.

Lemma compare_eq (s1 s2 : string) : compare s1 s2 = Eq <-> s1 = s2.

Lemma compare_lt_spec (s1 s2 : string) :
  compare s1 s2 = Lt <->
  exists i,
    to_Z i <= to_Z (length s1) /\
    to_Z i <= to_Z (length s2) /\
    (forall j, to_Z j < to_Z i -> get s1 j = get s2 j) /\
    ((i = length s1 /\ to_Z i < to_Z (length s2)) \/
     (to_Z i < to_Z (length s1) /\
      to_Z i < to_Z (length s2) /\
      char63_compare (get s1 i) (get s2 i) = Lt)).

Lemma make_0 (c : char63) : make 0 c = ""%pstring.

Lemma length_0_empty (s : string) : length s = 0%uint63 -> s = ""%pstring.

Lemma cat_empty_l (s : string) : cat ""%pstring s = s.

Lemma cat_empty_r (s : string) : cat s ""%pstring = s.

Lemma cat_assoc (s1 s2 s3 : string) :
  cat (cat s1 s2) s3 = cat s1 (cat s2 s3).

Lemma sub_full (s : string) : sub s 0 (length s) = s.

Lemma sub_len_0 (off : int) (s : string) :
  sub s off 0 = ""%pstring.

Lemma split_cat_sub (s : string) (len : int) :
  s = cat (sub s 0 len) (sub s len (length s - len)%uint63).

Lemma sub_sub (s : string) (off1 len1 off2 len2 : int) :
  to_Z off1 + to_Z off2 = to_Z (off1 + off2)%uint63 ->
  to_Z len2 <= to_Z len1 - to_Z off2 ->
  sub (sub s off1 len1) off2 len2 = sub s (off1 + off2)%uint63 len2.

Lemma of_list_length (l : list char63) :
  Z.of_nat (List.length l) <= to_Z max_length ->
  length (of_list l) = of_Z (Z.of_nat (List.length l)).

Lemma of_list_app (l1 l2 : list char63) :
  of_list (l1 ++ l2) = cat (of_list l1) (of_list l2).

Lemma to_list_cat (s1 s2 : string) :
  (to_Z (length s1) + to_Z (length s2) <= to_Z max_length)%Z ->
  to_list (cat s1 s2) = app (to_list s1) (to_list s2).

Require OrderedType.

Module OT <: OrderedType.OrderedType with Definition t := string.
  Definition t := string.

  Definition eq s1 s2 := compare s1 s2 = Eq.
  Definition lt s1 s2 := compare s1 s2 = Lt.

  Lemma eq_refl (s : t) : eq s s.

  Lemma eq_sym (s1 s2 : t) : eq s1 s2 -> eq s2 s1.

  Lemma eq_trans (s1 s2 s3 : t) : eq s1 s2 -> eq s2 s3 -> eq s1 s3.

  Lemma lt_trans (s1 s2 s3 : t) : lt s1 s2 -> lt s2 s3 -> lt s1 s3.

  Lemma lt_not_eq (s1 s2 : t) : lt s1 s2 -> not (eq s1 s2).

  #[program]
  Definition compare (s1 s2 : t) : OrderedType.Compare lt eq s1 s2 :=
    match compare s1 s2 with
    | Eq => OrderedType.EQ _
    | Lt => OrderedType.LT _
    | Gt => OrderedType.GT _
    end.

  Hint Immediate eq_sym : core.
  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core.

  Definition eq_dec (s1 s2 : t) : {eq s1 s2} + {~ eq s1 s2}.
End OT.