Skip to main content

🍃 String.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.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)).

Propositional equality and [equal] are equivalent on [String].
Lemma equal_is_valid : Compare.Equal.Valid.t (fun _True) String.equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros s1 s2 _ _.
  unfold String.equal. symmetry.
  apply Coq.Strings.String.eqb_eq.
Qed.