Merge pull request #1375 from HOL-Theorem-Prover/upstreaming

Add more theorems and constants
HOL-Theorem-Prover · Dec 18, 2024 · 5bbb8a2 · 5bbb8a2
2 parents f7fbb5e + 8274f79
commit 5bbb8a2
Show file tree

Hide file tree

Showing 8 changed files with 701 additions and 115 deletions.
diff --git a/src/boss/prove_base_assumsScript.sml b/src/boss/prove_base_assumsScript.sml
diff --git 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/numposrepScript.sml b/src/list/src/numposrepScript.sml
@@ -422,4 +422,88 @@ val l2n_11 = Q.store_thm("l2n_11",
         \\ NTAC 2 (POP_ASSUM SUBST1_TAC)
         \\ FULL_SIMP_TAC (srw_ss()) [l2n_APPEND]]);
 
+Theorem BITWISE_l2n_2:
+  LENGTH l1 = LENGTH l2 ==>
+  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
+  l2n 2 (MAP2 (\x y. bool_to_bit $ op (ODD x) (ODD y)) l1 l2)
+Proof
+  Q.ID_SPEC_TAC`l2`
+  \\ Induct_on`l1`
+  \\ simp[BITWISE_EVAL]
+  >- simp[BITWISE_def, l2n_def]
+  \\ Q.X_GEN_TAC`b`
+  \\ Cases \\ fs[BITWISE_EVAL]
+  \\ strip_tac
+  \\ fs[l2n_def]
+  \\ simp[SBIT_def, ODD_ADD, ODD_MULT, GSYM bool_to_bit_def]
+QED
+
+Theorem l2n_2_neg:
+  !ls.
+  EVERY ($> 2) ls ==>
+  l2n 2 (MAP (\x. 1 - x) ls) = 2 ** LENGTH ls - SUC (l2n 2 ls)
+Proof
+  Induct
+  \\ rw[l2n_def]
+  \\ fs[EXP, ADD1]
+  \\ simp[LEFT_SUB_DISTRIB, LEFT_ADD_DISTRIB, SUB_RIGHT_ADD]
+  \\ Q.SPECL_THEN[`ls`,`2`]mp_tac l2n_lt
+  \\ simp[]
+QED
+
+Theorem l2n_max:
+  0 < b ==>
+  !ls. (l2n b ls = b ** (LENGTH ls) - 1) <=>
+       (EVERY ((=) (b - 1) o flip $MOD b) ls)
+Proof
+  strip_tac
+  \\ Induct
+  \\ rw[l2n_def]
+  \\ rw[EXP]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b * l + a`
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`b ** n`
+  \\ fs[EQ_IMP_THM]
+  \\ conj_tac
+  >- (
+    strip_tac
+    \\ Cases_on`n=0` \\ fs[] >- (fs[Abbr`n`] \\ rw[])
+    \\ `0 < b * b ** n` by simp[]
+    \\ `a + b * l + 1 = b * b ** n` by simp[]
+    \\ `(b * b ** n) DIV b = b ** n` by simp[MULT_TO_DIV]
+    \\ `(b * l + (a + 1)) DIV b = b ** n` by fs[]
+    \\ `(b * l) MOD b = 0` by simp[]
+    \\ `(b * l + (a + 1)) DIV b = (b * l) DIV b + (a + 1) DIV b`
+    by ( irule ADD_DIV_RWT \\ simp[] )
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `(a + 1) DIV b = if a = b - 1 then 1 else 0`
+    by (
+      rw[]
+      \\ `a + 1 < b` suffices_by rw[DIV_EQ_0]
+      \\ simp[Abbr`a`]
+      \\ `h MOD b < b - 1` suffices_by simp[]
+      \\ `h MOD b < b` by simp[]
+      \\ fs[] )
+    \\ `b * l DIV b = l` by simp[MULT_TO_DIV]
+    \\ pop_assum SUBST_ALL_TAC
+    \\ pop_assum SUBST_ALL_TAC
+    \\ `l < b ** n` by ( map_every Q.UNABBREV_TAC[`l`,`n`]
+                         \\ irule l2n_lt \\ simp[] )
+    \\ Cases_on`a = b - 1` \\ fs[] )
+  \\ strip_tac
+  \\ rewrite_tac[LEFT_SUB_DISTRIB]
+  \\ Q.PAT_X_ASSUM`_ = a`(SUBST1_TAC o SYM)
+  \\ fs[SUB_LEFT_ADD] \\ rw[]
+  \\ Cases_on`n=0` \\ fs[]
+  \\ `b ** n <= b ** 0` by simp[]
+  \\ fs[EXP_BASE_LE_IFF]
+QED
+
+Theorem l2n_PAD_RIGHT_0[simp]:
+  0 < b ==> l2n b (PAD_RIGHT 0 h ls) = l2n b ls
+Proof
+  Induct_on`ls` \\ rw[l2n_def, PAD_RIGHT, l2n_eq_0, EVERY_GENLIST]
+  \\ fs[PAD_RIGHT, l2n_APPEND]
+  \\ fs[l2n_eq_0, EVERY_GENLIST]
+QED
+
 val _ = export_theory()
diff --git 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
@@ -3189,6 +3189,201 @@ Proof
   \\ Cases_on`q` \\ fs[ADD1]
 QED
 
+Theorem chunks_append_divides:
+  !n l1 l2.
+    0 < n /\ divides n (LENGTH l1) /\ ~NULL l1 /\ ~NULL l2 ==>
+    chunks n (l1 ++ l2) = chunks n l1 ++ chunks n l2
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[dividesTheory.divides_def, PULL_EXISTS]
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q=0` \\ fs[] \\ rfs[]
+  \\ IF_CASES_TAC
+  >- ( Cases_on`q` \\ fs[ADD1, LEFT_ADD_DISTRIB] \\ fs[LESS_OR_EQ] )
+  \\ simp[DROP_APPEND, TAKE_APPEND]
+  \\ Q.MATCH_GOALSUB_ABBREV_TAC`lhs = _`
+  \\ simp[Once chunks_def]
+  \\ Cases_on`q = 1` \\ fs[]
+  >- (
+    simp[Abbr`lhs`]
+    \\ fs[NOT_LESS_EQUAL]
+    \\ simp[DROP_LENGTH_TOO_LONG])
+  \\ simp[Abbr`lhs`]
+  \\ `n - n * q = 0` by simp[]
+  \\ simp[]
+  \\ first_x_assum irule
+  \\ simp[NULL_EQ]
+  \\ qexists_tac`q - 1`
+  \\ simp[]
+QED
+
+Theorem chunks_length[simp]:
+  chunks (LENGTH ls) ls = [ls]
+Proof
+  rw[Once chunks_def]
+QED
+
+Theorem chunks_not_nil[simp]:
+  !n ls. chunks n ls <> []
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def]
+QED
+
+Theorem LENGTH_chunks:
+  !n ls. 0 < n /\ ~NULL ls ==>
+    LENGTH (chunks n ls) =
+    LENGTH ls DIV n + (bool_to_bit $ ~divides n (LENGTH ls))
+Proof
+  HO_MATCH_MP_TAC chunks_ind
+  \\ rw[]
+  \\ rw[Once chunks_def, dividesTheory.DIV_EQUAL_0, bool_to_bit_def,
+        dividesTheory.divides_def]
+  \\ fs[LESS_OR_EQ, ADD1, NULL_EQ, bool_to_bit_def] \\ rfs[]
+  \\ rw[]
+  \\ fs[dividesTheory.divides_def, dividesTheory.SUB_DIV]
+  \\ rfs[]
+  >- (
+    Cases_on`LENGTH ls DIV n = 0` >- rfs[dividesTheory.DIV_EQUAL_0]
+    \\ simp[] )
+  >- (
+    Cases_on`q` \\ fs[MULT_SUC]
+    \\ Q.MATCH_ASMSUB_RENAME_TAC`n + n * p`
+    \\ first_x_assum(Q.SPEC_THEN`2 + p`mp_tac)
+    \\ simp[LEFT_ADD_DISTRIB] )
+  >- (
+    first_x_assum(Q.SPEC_THEN`PRE q`mp_tac)
+    \\ Cases_on`q` \\ fs[MULT_SUC] )
+  \\ Cases_on`q` \\ fs[MULT_SUC]
+  \\ simp[ADD_DIV_RWT]
+QED
+
+Theorem EL_chunks:
+  !k ls n.
+  n < LENGTH (chunks k ls) /\ 0 < k /\ ~NULL ls ==>
+  EL n (chunks k ls) = TAKE k (DROP (n * k) ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[NULL_EQ]
+  \\ Q.PAT_X_ASSUM`_ < LENGTH _ `mp_tac
+  \\ rw[Once chunks_def] \\ fs[]
+  \\ rw[Once chunks_def]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`EL m _`
+  \\ Cases_on`m` \\ fs[]
+  \\ pop_assum mp_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[LENGTH_chunks]
+  \\ simp[NULL_EQ]
+  \\ strip_tac
+  \\ dep_rewrite.DEP_REWRITE_TAC[DROP_DROP]
+  \\ simp[MULT_SUC]
+  \\ Q.MATCH_GOALSUB_RENAME_TAC`k + k * m <= _`
+  \\ `k * m <= LENGTH ls - k` suffices_by simp[]
+  \\ `m <= (LENGTH ls - k) DIV k` suffices_by simp[X_LE_DIV]
+  \\ fs[bool_to_bit_def]
+  \\ pop_assum mp_tac \\ rw[]
+QED
+
+Theorem chunks_MAP:
+  !n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM MAP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[MAP_TAKE]
+QED
+
+Theorem chunks_ZIP:
+  !n ls l2. LENGTH ls = LENGTH l2 ==>
+  chunks n (ZIP (ls, l2)) = MAP ZIP (ZIP (chunks n ls, chunks n l2))
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ rw[Once chunks_def]
+  >- ( rw[Once chunks_def] \\ rw[Once chunks_def] )
+  >- rw[Once chunks_def]
+  \\ fs[]
+  \\ simp[GSYM ZIP_DROP]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ CONV_TAC(PATH_CONV"rrrr"(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ simp[ZIP_TAKE]
+QED
+
+Theorem chunks_TAKE:
+  !n ls m. divides n m /\ 0 < m ==>
+    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)
+Proof
+  HO_MATCH_MP_TAC chunks_ind \\ rw[]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+  >- (
+    rw[Once chunks_def] \\ fs[LENGTH_TAKE_EQ]
+    \\ fs[dividesTheory.divides_def]
+    \\ BasicProvers.VAR_EQ_TAC
+    \\ Q.MATCH_GOALSUB_RENAME_TAC`n * m`
+    \\ fs[ZERO_LESS_MULT]
+    \\ `n <= n * m` by simp[LE_MULT_CANCEL_LBARE]
+    \\ dep_rewrite.DEP_REWRITE_TAC[TAKE_LENGTH_TOO_LONG]
+    \\ simp[MULT_DIV] )
+  >- fs[dividesTheory.divides_def]
+  \\ fs[]
+  \\ simp[Once chunks_def, LENGTH_TAKE_EQ]
+  \\ `n <= m` by (
+    rfs[dividesTheory.divides_def] \\ rw[]
+    \\ fs[ZERO_LESS_MULT] )
+  \\ IF_CASES_TAC
+  >- (
+    pop_assum mp_tac \\ rw[]
+    \\ `m = n` by fs[] \\ rw[] )
+  \\ fs[TAKE_TAKE, DROP_TAKE]
+  \\ first_x_assum(Q.SPEC_THEN`m - n`mp_tac)
+  \\ simp[]
+  \\ impl_keep_tac >- (
+    fs[dividesTheory.divides_def]
+    \\ qexists_tac`q - 1`
+    \\ simp[LEFT_SUB_DISTRIB] )
+  \\ rw[]
+  \\ `m DIV n <> 0` by fs[dividesTheory.DIV_EQUAL_0]
+  \\ Cases_on`m DIV n` \\ fs[TAKE_TAKE_MIN]
+  \\ `MIN n m = n` by fs[MIN_DEF] \\ rw[]
+  \\ simp[dividesTheory.SUB_DIV]
+QED
+
+Definition chunks_tr_aux_def:
+  chunks_tr_aux n ls acc =
+    if LENGTH ls <= SUC n then REVERSE $ ls :: acc
+    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls :: acc)
+Termination
+  WF_REL_TAC`measure $ LENGTH o FST o SND`
+  \\ rw[LENGTH_DROP]
+End
+
+Definition chunks_tr_def:
+  chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n - 1) ls []
+End
+
+Theorem chunks_tr_aux_thm:
+  !n ls acc.
+    chunks_tr_aux n ls acc =
+    REVERSE acc ++ chunks (SUC n) ls
+Proof
+  HO_MATCH_MP_TAC chunks_tr_aux_ind
+  \\ rw[]
+  \\ rw[Once chunks_tr_aux_def]
+  >- rw[Once chunks_def]
+  \\ CONV_TAC(RAND_CONV(SIMP_CONV(srw_ss())[Once chunks_def]))
+  \\ rw[]
+QED
+
+Theorem chunks_tr_thm:
+  chunks_tr = chunks
+Proof
+  simp[FUN_EQ_THM, chunks_tr_def]
+  \\ Cases \\ rw[chunks_tr_aux_thm]
+QED
+
 (*---------------------------------------------------------------------------*)
 (* Various lemmas from the CakeML project https://cakeml.org                 *)
 (*---------------------------------------------------------------------------*)
@@ -3588,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))