From 2acd88d6ed7516113bf62c0ad547b86925535b23 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 2 Mar 2025 17:13:50 -0500
Subject: [PATCH] Add is_substring

---
 src/Util/Strings/String.v | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/Util/Strings/String.v b/src/Util/Strings/String.v
index b5c4898ca8..ebffd319e8 100644
--- a/src/Util/Strings/String.v
+++ b/src/Util/Strings/String.v
@@ -412,3 +412,19 @@ Fixpoint strip_leading_newlines (s : list string) : list string
 
 Definition strip_trailing_newlines (s : list string) : list string
   := List.rev_append (strip_leading_newlines (List.rev_append s nil)) nil.
+
+(** [is_substring s1 s2] returns [true] if [s1] is a substring of [s2] *)
+Definition is_substring (s1 s2 : string) : bool :=
+  if (s1 =? "")%string
+  then true
+  else
+    match split s1 s2 with
+    | nil => false
+    | _ :: nil => false
+    | _ :: _ :: _ => true
+    end.
+
+Lemma is_substring_correct s1 s2 :
+  is_substring s1 s2 = true <-> exists n, substring n (String.length s1) s2 = s1.
+Proof.
+Abort.