Added proof for substr_l_eq

Added the proof along with helper lemma for substr_l_eq

OK cool for the proofs! Here is a proof suggestion using our practices:

(** The substring left identity *)
Lemma conc {s1 : string} :
  s1 ++ "" = s1.
Proof.
  induction s1; sfirstorder.
Qed.

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

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

Lemma substr_l_eq {s1 s2} :
  String.sub (s1 ++ s2) 0 (String.length s1) = s1.
Proof.
  induction s1; simpl.
  { apply zerozero. }
  { unfold String.sub, String.length, CoqOfOCaml.String.length in *.
    rewrite Nat2Z.id in *; simpl in *.
    sfirstorder.
  }
Qed.

Notes:

• sfirstorder and sauto are obtained from running the tactic best https://coqhammer.github.io/
• We separate sub-goals with { ... }
• We put the parameters of the lemma on the left of the : so that there are less intros to do.

Also, I added you to the project's members so that you can open a merge request without doing a fork and use the CI system.

(you can re-open your merge request then)

Merged as !568 (merged)

closed