From 3f6e78258b82149b95ab354e180b95cd094ec4e7 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sun, 3 Dec 2023 23:44:11 +0000 Subject: [PATCH] Add various theorems (#1168) * Add toSortedAList_fromList - thanks to Yong Kiam * Add size_map thms * Add more sptree theorems * Add fromList_fromAList * Add a couple more sptree thms --- src/finite_maps/sptreeScript.sml | 196 ++++++++++++++++++++--- src/list/src/rich_listScript.sml | 10 ++ src/num/extra_theories/logrootScript.sml | 6 + src/num/theories/arithmeticScript.sml | 18 +++ src/sort/sortingScript.sml | 15 ++ 5 files changed, 224 insertions(+), 21 deletions(-) diff --git a/src/finite_maps/sptreeScript.sml b/src/finite_maps/sptreeScript.sml index 55c4733159..72af3b91c6 100644 --- a/src/finite_maps/sptreeScript.sml +++ b/src/finite_maps/sptreeScript.sml @@ -620,6 +620,27 @@ val domain_fromList = store_thm( qmatch_assum_rename_tac `nn < SUC (LENGTH l)` >> Cases_on `nn` >> fs[] >> metis_tac[ADD1]); +val size_domain = Q.store_thm("size_domain", + `!t. size t = CARD (domain t)`, + Induct_on `t` + >- rw[size_def, domain_def] + >- rw[size_def, domain_def] + >> rw[CARD_UNION_EQN, CARD_INJ_IMAGE] + >- + (`IMAGE (\n. 2 * n + 2) (domain t) INTER + IMAGE (\n. 2 * n + 1) (domain t') = {}` + by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] + >> Cases_on `ODD x` + >> fs[ODD_EXISTS, ADD1, oddevenlemma]) + >> simp[]) >> + `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\ + (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t))) + INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})` + by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] + >> Cases_on `ODD x` + >> fs[ODD_EXISTS, ADD1, oddevenlemma]) + >> simp[]); + val ODD_IMP_NOT_ODD = prove( ``!k. ODD k ==> ~(ODD (k-1))``, Cases >> fs [ODD]); @@ -948,6 +969,18 @@ val ALL_DISTINCT_MAP_FST_toAList = store_thm("ALL_DISTINCT_MAP_FST_toAList", simp[MEM_MAP,PULL_EXISTS,pairTheory.EXISTS_PROD] >> metis_tac[ODD_EVEN,lemmas] ) +Theorem LENGTH_toAList[simp]: + LENGTH (toAList t) = size t +Proof + `LENGTH (toAList t) = LENGTH (MAP FST (toAList t))` by simp[]>> + pop_assum SUBST_ALL_TAC>> + DEP_REWRITE_TAC[GSYM ALL_DISTINCT_CARD_LIST_TO_SET]>> + simp[ALL_DISTINCT_MAP_FST_toAList,size_domain]>> + AP_TERM_TAC>> + rw[pred_setTheory.EXTENSION]>> + simp[MEM_MAP,pairTheory.EXISTS_PROD,MEM_toAList,domain_lookup] +QED + val _ = remove_ovl_mapping "lrnext" {Name = "lrnext", Thy = "sptree"} val foldi_FOLDR_toAList_lemma = prove( @@ -1658,27 +1691,6 @@ val mapi_Alist = Q.store_thm( simp[spt_eq_thm, wf_mapi, wf_fromAList, lookup_fromAList] >> srw_tac[boolSimps.ETA_ss][lookup_mapi, ALOOKUP_MAP_lemma, ALOOKUP_toAList]); -val size_domain = Q.store_thm("size_domain", - `!t. size t = CARD (domain t)`, - Induct_on `t` - >- rw[size_def, domain_def] - >- rw[size_def, domain_def] - >> rw[CARD_UNION_EQN, CARD_INJ_IMAGE] - >- - (`IMAGE (\n. 2 * n + 2) (domain t) INTER - IMAGE (\n. 2 * n + 1) (domain t') = {}` - by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] - >> Cases_on `ODD x` - >> fs[ODD_EXISTS, ADD1, oddevenlemma]) - >> simp[]) >> - `(({0} INTER IMAGE (\n. 2 * n + 2) (domain t)) = {}) /\ - (({0} UNION (IMAGE (\n. 2 * n + 2) (domain t))) - INTER (IMAGE (\n. 2 * n + 1) (domain t')) = {})` - by (rw[GSYM DISJOINT_DEF, IN_DISJOINT] - >> Cases_on `ODD x` - >> fs[ODD_EXISTS, ADD1, oddevenlemma]) - >> simp[]); - val num_set_domain_eq = Q.store_thm("num_set_domain_eq", `!t1 t2:unit spt. wf t1 /\ wf t2 ==> @@ -1692,6 +1704,25 @@ val union_num_set_sym = Q.store_thm ("union_num_set_sym", `!(t1:unit spt) t2. union t1 t2 = union t2 t1`, Induct >> fs[union_def] >> rw[] >> CASE_TAC >> fs[union_def]); +Theorem union_disjoint_sym: + !t1 t2. + wf t1 /\ wf t2 /\ DISJOINT (domain t1) (domain t2) ==> + union t1 t2 = union t2 t1 +Proof + Induct + >- rw[] + >- ( + rw[union_def] + \\ CASE_TAC \\ rw[union_def] + \\ fs[] ) + \\ rw[wf_def] \\ fs[] + \\ rw[Once union_def] + \\ CASE_TAC \\ rw[Once union_def, SimpRHS] \\ fs[] + \\ first_x_assum irule \\ fs[wf_def] + \\ gs[pred_setTheory.DISJOINT_IMAGE] + \\ simp[pred_setTheory.DISJOINT_SYM] +QED + Theorem difference_sub: (difference a b = LN) ==> (domain a SUBSET domain b) Proof @@ -1880,6 +1911,19 @@ Theorem wf_LN[simp]: wf LN Proof rw[wf_def] QED +Theorem wf_fromList[simp]: + wf (fromList ls) +Proof + rw[fromList_def] + \\ qmatch_goalsub_abbrev_tac`FOLDL f (0,LN) ls` + \\ qho_match_abbrev_tac`P (FOLDL f (0,LN) ls)` + \\ `FOLDL f (0,LN) ls = FOLDL f (0,LN) ls /\ P (FOLDL f (0,LN) ls)` + suffices_by rw[] + \\ irule rich_listTheory.FOLDL_CONG_invariant + \\ simp[Abbr`P`, Abbr`f`, pairTheory.FORALL_PROD] + \\ rw[wf_insert] +QED + val splem1 = Q.prove(` a <> 0 ==> (a-1) DIV 2 < a`, simp[DIV_LT_X]); @@ -2003,6 +2047,18 @@ Proof Induct_on `xs` \\ fs [list_size_def] QED +Theorem size_map[simp]: + size (map f t) = size t +Proof + rw[size_domain] +QED + +Theorem size_mapi[simp]: + size (mapi f t) = size t +Proof + rw[size_domain] +QED + val spt_size_def = definition "spt_size_def"; Theorem SUM_MAP_same_LE: @@ -2344,6 +2400,104 @@ Proof \\ simp [SORTED_toSortedAList, relationTheory.irreflexive_def] QED +Theorem toSortedAList_fromList: + toSortedAList (fromList ls) = ZIP (COUNT_LIST (LENGTH ls),ls) +Proof + mp_tac (sortingTheory.SORTED_ALL_DISTINCT_LIST_TO_SET_EQ + |> INST_TYPE [alpha |-> ``:num # 'a``] + |> Q.SPEC`(\x y. FST x < FST y)`)>> + impl_keep_tac >- + fs[relationTheory.transitive_def,relationTheory.antisymmetric_def]>> + disch_then match_mp_tac>> + CONJ_ASM1_TAC + >- ( + match_mp_tac sortingTheory.SORTED_weaken>> + irule_at Any (SORTED_toSortedAList |> SIMP_RULE std_ss [sortingTheory.sorted_map])>> + simp[])>> + CONJ_ASM1_TAC + >- ( + match_mp_tac sortingTheory.SORTED_FST_ZIP>> + simp[rich_listTheory.LENGTH_COUNT_LIST,sortingTheory.sorted_lt_count_list])>> + rw[] + >- ( + irule sortingTheory.SORTED_ALL_DISTINCT>> + first_x_assum (irule_at Any)>> + first_x_assum (irule_at Any)>> + simp[relationTheory.irreflexive_def]) + >- ( + irule sortingTheory.SORTED_ALL_DISTINCT>> + first_x_assum (irule_at Any)>> + first_x_assum (irule_at Any)>> + simp[relationTheory.irreflexive_def]) + >- ( + rw[pred_setTheory.EXTENSION]>> + Cases_on`x`>> + DEP_REWRITE_TAC[MEM_ZIP]>> + simp[rich_listTheory.LENGTH_COUNT_LIST,MEM_toSortedAList,lookup_fromList]>> + metis_tac[rich_listTheory.EL_COUNT_LIST]) +QED + +Theorem fromList_fromAList: + !l. fromList l = fromAList (ZIP (COUNT_LIST (LENGTH l), l)) +Proof + ho_match_mp_tac SNOC_INDUCT + \\ conj_tac >- rw[fromList_def, fromAList_def, + rich_listTheory.COUNT_LIST_def] + \\ rw[fromList_def, rich_listTheory.COUNT_LIST_def] + \\ rw[FOLDL_SNOC, pairTheory.UNCURRY] + \\ rw[GSYM rich_listTheory.COUNT_LIST_def] + \\ rw[rich_listTheory.COUNT_LIST_SNOC, + rich_listTheory.ZIP_SNOC, + rich_listTheory.LENGTH_COUNT_LIST] + \\ rw[SNOC_APPEND, fromAList_append] + \\ DEP_ONCE_REWRITE_TAC[union_disjoint_sym] + \\ simp[union_insert_LN] + \\ simp[wf_fromAList, wf_insert, domain_fromAList, + MAP_ZIP, rich_listTheory.LENGTH_COUNT_LIST, + rich_listTheory.MEM_COUNT_LIST] + \\ AP_THM_TAC \\ AP_THM_TAC + \\ AP_TERM_TAC + \\ qmatch_goalsub_abbrev_tac`FOLDL f e l` + \\ `!l e. FST (FOLDL f e l) = FST e + LENGTH l` suffices_by simp[Abbr`e`] + \\ Induct \\ rw[Abbr`f`, pairTheory.UNCURRY] +QED + +Theorem ALL_DISTINCT_MAP_FST_toSortedAList: + ALL_DISTINCT (MAP FST (toSortedAList t)) +Proof + irule sortingTheory.SORTED_ALL_DISTINCT>> + irule_at Any (SORTED_toSortedAList)>> + simp[relationTheory.irreflexive_def] +QED + +Theorem LENGTH_toSortedAList[simp]: + LENGTH (toSortedAList t) = size t +Proof + `LENGTH (toSortedAList t) = + LENGTH (MAP FST (toSortedAList t))` by simp[]>> + pop_assum SUBST_ALL_TAC>> + DEP_REWRITE_TAC[GSYM ALL_DISTINCT_CARD_LIST_TO_SET]>> + simp[ALL_DISTINCT_MAP_FST_toSortedAList,size_domain]>> + AP_TERM_TAC>> + rw[pred_setTheory.EXTENSION]>> + simp[MEM_MAP,pairTheory.EXISTS_PROD,MEM_toSortedAList,domain_lookup] +QED + +Theorem set_MAP_FST_toAList_domain: + set (MAP FST (toAList t)) = domain t +Proof + rw[EXTENSION] + \\ `(ALOOKUP (toAList t) x <> NONE) <=> x IN domain t` + suffices_by metis_tac[ALOOKUP_NONE] + \\ simp[ALOOKUP_toAList, lookup_NONE_domain] +QED + +Theorem size_fromList[simp]: + size (fromList ls) = LENGTH ls +Proof + rw[size_domain, domain_fromList] +QED + val _ = let open sptreepp in diff --git a/src/list/src/rich_listScript.sml b/src/list/src/rich_listScript.sml index 629e8c09de..5f7918a910 100644 --- a/src/list/src/rich_listScript.sml +++ b/src/list/src/rich_listScript.sml @@ -345,6 +345,16 @@ val MAP_FOLDL = Q.store_thm ("MAP_FOLDL", THEN GEN_TAC THEN REFL_TAC); +Theorem FOLDL_CONG_invariant: + !P f1 f2 l e. + P e /\ + (!x a. MEM x l /\ P a ==> f1 a x = f2 a x /\ P (f2 a x)) + ==> + FOLDL f1 e l = FOLDL f2 e l /\ P (FOLDL f2 e l) +Proof + ntac 3 gen_tac \\ Induct \\ rw[] +QED + val FILTER_FOLDR = Q.store_thm ("FILTER_FOLDR", `!P l. FILTER P l = FOLDR (\x l'. if P x then CONS x l' else l') [] l`, BasicProvers.Induct_on `l` diff --git a/src/num/extra_theories/logrootScript.sml b/src/num/extra_theories/logrootScript.sml index 2fa6910acb..f2f5063f32 100644 --- a/src/num/extra_theories/logrootScript.sml +++ b/src/num/extra_theories/logrootScript.sml @@ -171,6 +171,12 @@ val LOG_UNIQUE = Q.store_thm("LOG_UNIQUE", THEN METIS_TAC [exp_lemma5, DECIDE ``a < b <=> SUC a <= b``, LESS_EQ_TRANS, NOT_LESS, LOG, EXP]); +val LOG_POW = Q.store_thm("LOG_POW", + `!b n. 1n < b ==> (LOG b (b ** n) = n)`, + REPEAT STRIP_TAC + THEN irule LOG_UNIQUE + THEN SRW_TAC [ARITH_ss] [EXP]); + val LOG_ADD1 = Q.store_thm("LOG_ADD1", `!n a b. 0n < n /\ 1n < a /\ 0 < b ==> (LOG a (a ** SUC n * b) = SUC (LOG a (a ** n * b)))`, diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml index 0d01d1de2b..db55f734c1 100644 --- a/src/num/theories/arithmeticScript.sml +++ b/src/num/theories/arithmeticScript.sml @@ -3785,6 +3785,24 @@ val FUNPOW_1 = store_thm ("FUNPOW_1", REWRITE_TAC [FUNPOW, ONE]); val _ = export_rewrites ["FUNPOW_1"] +Theorem FUNPOW_CONG: + !n x f g. + (!m. m < n ==> f (FUNPOW f m x) = g (FUNPOW f m x)) + ==> + FUNPOW f n x = FUNPOW g n x +Proof + INDUCT_TAC \\ SRW_TAC[][FUNPOW_SUC] + THEN METIS_TAC[LESS_SUC, LESS_SUC_REFL] +QED + +Theorem FUNPOW_invariant: + !m x. + P x /\ (!x. P x ==> P (f x)) ==> + P (FUNPOW f m x) +Proof + Induct \\ SRW_TAC[][FUNPOW_SUC] +QED + val NRC_0 = save_thm ("NRC_0", CONJUNCT1 NRC); val _ = export_rewrites ["NRC_0"] diff --git a/src/sort/sortingScript.sml b/src/sort/sortingScript.sml index 5e85f7c391..2281e9ec88 100644 --- a/src/sort/sortingScript.sml +++ b/src/sort/sortingScript.sml @@ -1857,4 +1857,19 @@ Proof \\ simp[QSORT_SORTED] QED +Theorem SORTED_FST_ZIP: + !R ls rs. + SORTED R ls /\ LENGTH ls = LENGTH rs ==> + SORTED (\x y. R (FST x) (FST y)) (ZIP (ls,rs)) +Proof + ho_match_mp_tac SORTED_IND>>rw[] + >- (Cases_on`rs`>>fs[])>> + `?a b rss. rs = a::b::rss` by + (Cases_on`rs` \\ fs[] \\ + metis_tac[list_CASES,LENGTH_NIL,SUC_NOT]) >> + fs[]>> + first_x_assum(qspec_then`b::rss` mp_tac)>> + simp[] +QED + val _ = export_theory();