Skip to content

Commit

Permalink
Revert "Prove more theorems about chunks"
Browse files Browse the repository at this point in the history 
This reverts commit 46a8614.
  • Loading branch information
@xrchz
xrchz committed Dec 15, 2024
1 parent 46a8614 commit 7b8e323
Showing 1 changed file with 0 additions and 195 deletions.
195 changes: 0 additions & 195 deletions src/list/src/rich_listScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3189,201 +3189,6 @@ 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:
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 *)
(*---------------------------------------------------------------------------*)
Expand Down

0 comments on commit 7b8e323

Please sign in to comment.