From Stdlib Require Import Uint63.
From Stdlib Require Export PrimString.
From Stdlib Require Export PrimStringAxioms.

From Stdlib.micromega Require Import Lia.
From Stdlib.micromega Require Import ZifyUint63.
From Stdlib.micromega Require Import Zify.
Require Import Stdlib.Numbers.Cyclic.Int63.Ring63.
From Stdlib 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).

From Stdlib 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.