From aa170a503f19bdcb8ba51a067c3c84591ee2f468 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Sun, 15 Dec 2024 14:28:49 +0000
Subject: [PATCH] Add some theorems about dropWhile

---
 src/list/src/listScript.sml      | 10 ++++++++++
 src/list/src/rich_listScript.sml | 22 +++++++++++++++++++++-
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/list/src/listScript.sml b/src/list/src/listScript.sml
index 84a465bb0d..e728fddbe0 100644
--- a/src/list/src/listScript.sml
+++ b/src/list/src/listScript.sml
@@ -4734,6 +4734,16 @@ val EL_LENGTH_dropWhile_REVERSE = Q.store_thm("EL_LENGTH_dropWhile_REVERSE",
    >> fs [NOT_EVERY, dropWhile_APPEND_EXISTS, arithmeticTheory.ADD1])
 end
 
+Theorem dropWhile_id:
+ (dropWhile P ls = ls) <=> NULL ls \/ ~P(HD ls)
+Proof
+  Cases_on`ls` \\ rw[dropWhile_def, NULL]
+  \\ disch_then(mp_tac o Q.AP_TERM`LENGTH`)
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`dropWhile P l`
+  \\ Q.SPECL_THEN[`P`,`l`]mp_tac LENGTH_dropWhile_LESS_EQ
+  \\ simp[]
+QED
+
 val IMP_EVERY_LUPDATE = store_thm("IMP_EVERY_LUPDATE",
   “!xs h i. P h /\ EVERY P xs ==> EVERY P (LUPDATE h i xs)”,
   Induct THEN fs [LUPDATE_def] THEN REPEAT STRIP_TAC
diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml
index 092d1e2cec..08638478e9 100644
--- a/src/list/src/rich_listScript.sml
+++ b/src/list/src/rich_listScript.sml
@@ -8,7 +8,7 @@ open HolKernel Parse boolLib BasicProvers;
 open numLib metisLib simpLib combinTheory arithmeticTheory prim_recTheory
      pred_setTheory listTheory pairTheory markerLib TotalDefn;
 
-local open listSimps pred_setSimps in end;
+local open listSimps pred_setSimps dep_rewrite in end;
 
 val FILTER_APPEND = FILTER_APPEND_DISTRIB
 val REVERSE = REVERSE_SNOC_DEF
@@ -3783,6 +3783,26 @@ Proof
 QED
 (* END more lemmas of IS_SUFFIX *)
 
+Theorem IS_SUFFIX_dropWhile:
+  IS_SUFFIX ls (dropWhile P ls)
+Proof
+  Induct_on`ls`
+  \\ rw[IS_SUFFIX_CONS]
+QED
+
+Theorem LENGTH_dropWhile_id:
+  (LENGTH (dropWhile P ls) = LENGTH ls) <=> (dropWhile P ls = ls)
+Proof
+  rw[EQ_IMP_THM]
+  \\ rw[dropWhile_id]
+  \\ Cases_on`ls` \\ fs[]
+  \\ strip_tac \\ fs[]
+  \\ `IS_SUFFIX t (dropWhile P t)` by simp[IS_SUFFIX_dropWhile]
+  \\ fs[IS_SUFFIX_APPEND]
+  \\ `LENGTH t = LENGTH l + LENGTH (dropWhile P t)` by metis_tac[LENGTH_APPEND]
+  \\ fs[]
+QED
+
 Theorem nub_GENLIST:
   nub (GENLIST f n) =
     MAP f (FILTER (\i. !j. (i < j) /\ (j < n) ==> f i <> f j) (COUNT_LIST n))