🍃 String.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Environment.V7.Proofs.Pervasives.
Require Import Coq.Strings.String.
Import Pervasives.Notations.

Module Int_length.

Strings whose length fits in an OCaml's [int]. This condition is required for all operations involving [length] or [nth] primitives.

  Definition t (s : string) : Prop :=
    String.length s = Z.of_nat (Strings.String.length s).
  #[global] Hint Unfold t : tezos_z.
End Int_length.

The [length] function outputs a *non-negative* valid integer.

Lemma length_is_non_negative s :
  Int_length.t s →
  Pervasives.Int.Valid.non_negative (String.length s).
Proof.
  intros H.
  split; [|unfold String.length]; lia.
Qed.

The [length] function is valid.

Lemma length_is_valid s :
  Int_length.t s →
  Pervasives.Int.Valid.t (String.length s).
Proof.
  intros H.
  split; [|unfold String.length]; lia.
Qed.

If the length is zero, then the string is empty.

Lemma length_zero_implies_empty s :
  Int_length.t s →
  String.length s = 0 →
  s = "".
Proof.
  intros H_valid H_length.
  rewrite H_valid in H_length.
  sauto lq: on rew: off.
Qed.

(* @TODO *)

Index of char in a string without it is the length of the string

Axiom index_opt_eq : ∀ {s1 s2 : string} {sep : ascii},
  String.contains s1 sep = false →
  String.index_opt (s1 ++ (String.String sep s2)) sep = Some (String.length s1).

The concatenation with empty string is itself

Lemma concat_with_empty {s1 : string} :
  s1 ++ "" = s1.
Proof.
  induction s1; sfirstorder.
Qed.

The substring of its own length from the beginning is itself

Lemma substring_of_s_l {s1 : string} :
  substring 0 (length s1) s1 = s1.
Proof.
  induction s1; sfirstorder.
Qed.

The substring of zero length from the beginning is empty string

Lemma substring_of_0_l {s1 : string} :
  substring 0 0 s1 = "".
Proof.
  sauto lq: on.
Qed.

The substring left identity

Lemma substring_l_eq : ∀ {s1 s2},
  String.sub (s1 ++ s2) 0 (String.length s1) = s1.
Proof.
  induction s1; cbn; intros s2; [apply substring_of_0_l|].
  unfold String.length.
Admitted.

(* @TODO *)

The substring right identity

Axiom substr_r_eq : ∀ {s1 s2cont} {sep : ascii},
  String.contains s1 sep = false →
  let s2 := String sep s2cont in
  let fullstr := s1 ++ s2 in
  let fulllen := String.length fullstr in
  let s1len_p1 := (String.length s1) +i 1 in
  let s2contlen := fulllen -i (String.length s1 +i 1) in
  String.sub fullstr s1len_p1 s2contlen = s2cont.

(* @TODO *)

The concatenation of two substrings identity

Axiom substr_concat_eq : ∀ s sep i,
  String.index_opt s sep = Some i →
  let len := String.length s in
  let s1 := String.sub s 0 i in
  let s2cont := String.sub s (i +i 1) (len -i (i +i 1))%Z in
  let s2 := String sep s2cont in
  s1 ++ s2 = s.

A substring with non-positive length is empty

Axiom sub_length_0_eq : ∀ s offset length,
  length ≤ 0 →
  String.sub s offset length = "".

The same as above but for Coq.Strings.String.

Axiom sub_length_0_eq' : ∀ s offset,
  Coq.Strings.String.substring offset 0 s = "".

The substring of an empty string is always empty

Lemma sub_empty_eq : ∀ offset length, String.sub "" offset length = "".
  destruct length; unfold String.sub; simpl in *;
  destruct (Z.to_nat _); try easy;
  destruct (Pos.to_nat _); easy.
Qed.

Axiom compare_eq_iff : ∀ (s s' : string),
  String.compare s s' = 0 → s = s'.
  (* TODO https://github.com/coq/coq/blob/master/theories/Strings/String.v#L102 *)
  (* induction s, s'; intuition; inversion H. *)

Lemma length_empty_string : String.length "" = 0.
Proof. reflexivity. Qed.

Lemma length_any_string_not_zero : ∀ s, String.length s ≥ 0.
Proof.
  intro s.
Admitted.

(* @TODO *)
Axiom string_sub_zero : ∀ s n, String.sub s n 0 = "".

(* @TODO *)
Axiom string_sub_length : ∀ s, String.sub s 0 (String.length s) = s.

Lemma op_caret_second_empty : ∀ s, op_caret s "" = s.
Proof.
  intro s; induction s as [| s ss IHs]; [| simpl; rewrite IHs];
    reflexivity.
Qed.

Lemma string_length_cons : ∀ a s,
      String.length (String.String a s) = ((String.length s) + 1)%Z.
Proof.
  (* intros a s; unfold String.length, CoqOfOCaml.String.length; simpl; lia. *)
Admitted.

Lemma string_length_empty : String.length "" = 0.
Proof.
  unfold String.length, CoqOfOCaml.String.length; reflexivity.
Qed.

(* @TODO *)
Axiom compare_string_sub : ∀ s1 s2, String.compare
      (String.sub (op_caret s1 s2) 0 (String.length s1))
      s1 =? 0 = true.

(* @TODO *)
Axiom string_compare_string_sub : ∀ s1 s2,
    String.compare (String.sub (op_caret s1 s2) 0
                   (String.length s1)) s1 =? 0 = true.

(* @TODO *)
Axiom sub_op_caret_cons_eq : ∀ a s1 s2,
    (String.sub (String.String a (op_caret s1 s2))
                (String.length (String.String a s1))
                (String.length s2)) =
    (String.sub (op_caret s1 s2) (String.length s1) (String.length s2)).

Lemma string_length_compat (d : string) :
  String.length d = Z.of_nat (Strings.String.length d).
Proof.
  induction d.
  - reflexivity.
  - unfold String.length.
    unfold CoqOfOCaml.String.length.
Admitted.

Lemma string_length_non_neg (d : string) :
  0 ≤ Z.of_int (String.length d).
Proof.
  induction d.
  - reflexivity.
  - unfold String.length.
    unfold of_int.
    unfold CoqOfOCaml.String.length.
Admitted.