From 80f11ba0778b02662e0eedd9b5ae46a4e9def108 Mon Sep 17 00:00:00 2001 From: Gordon Date: Wed, 14 Feb 2024 14:19:34 +1100 Subject: [PATCH] add theorems for cycle detection to topological_sortTheory --- .../algorithms/topological_sortScript.sml | 358 ++++++++++++++++++ 1 file changed, 358 insertions(+) diff --git a/examples/algorithms/topological_sortScript.sml b/examples/algorithms/topological_sortScript.sml index adc6651f41..451a51ef31 100644 --- a/examples/algorithms/topological_sortScript.sml +++ b/examples/algorithms/topological_sortScript.sml @@ -109,6 +109,12 @@ Proof EVAL_TAC QED +Definition has_cycle_def: + has_cycle graph = + ((EXISTS (λl. 1 < LENGTH l) $ top_sort_any graph) ∨ + EXISTS (λ(v,l). MEM v l) graph) +End + (******************** Proofs ********************) @@ -397,6 +403,63 @@ Proof gvs[GSYM trans_clos_correct, ALL_DISTINCT_APPEND] >> metis_tac[] QED +Theorem top_sort_aux_same_partition: + ∀ns reach acc xs. + MEM xs (top_sort_aux ns reach acc) ⇒ + ∀x y nexts. + (∀n m. TC (λa b. needs a b reach) n m ⇒ + needs n m reach) ∧ + (∀as x y. MEM as acc ∧ x ≠ y ∧ + MEM x as ∧ MEM y as ⇒ needs x y reach) ∧ + x ≠ y ∧ + MEM x xs ∧ MEM y xs ⇒ needs x y reach +Proof + ho_match_mp_tac top_sort_aux_ind >> + rpt strip_tac + >- (fs[Once $ top_sort_aux_def] >> metis_tac[]) >> + qpat_x_assum `MEM _ (top_sort_aux _ _ _)` $ + assume_tac o SRULE[Once $ top_sort_aux_def,LET_THM] >> + qmatch_asmsub_abbrev_tac `MEM _ (_ ps)` >> + PairCases_on `ps` >> + fs[] >> + last_x_assum $ drule_then irule >> + rw[] + >- ( + drule partition_thm >> + simp[] >> + rpt strip_tac >> + qpat_x_assum `set _ ∪ set _ ∪ set _ = set _` $ + assume_tac o GSYM >> + Cases_on `x' = n` + >- (fs[] >> metis_tac[]) >> + Cases_on `y' = n` + >- (fs[] >> metis_tac[]) >> + `MEM x' ns ∧ MEM y' ns` by fs[] >> + qpat_x_assum `set _ = _ ∪ _` $ assume_tac o GSYM >> + fs[] >> + qpat_x_assum `!n m. TC _ _ _ ⇒ needs _ _ reach` $ + irule >> + irule $ cj 2 TC_RULES >> + qexists `n` >> + irule_at (Pos hd) $ cj 1 TC_RULES >> + irule_at (Pos $ el 2) $ cj 1 TC_RULES >> + simp[] + ) >> + metis_tac[] +QED + +(* Every pair of elements in the same partition +* is connected *) +Theorem top_sort_same_partition: + MEM xs (top_sort graph) ∧ x ≠ y ∧ + MEM x xs ∧ MEM y xs ⇒ + needs x y (trans_clos $ fromAList graph) +Proof + rw[top_sort_def] >> + drule top_sort_aux_same_partition >> + simp[trans_clos_TC_closed] +QED + Theorem to_nums_correct: !xs b res. to_nums b xs = res /\ @@ -413,6 +476,18 @@ Proof rw[EL_ALL_DISTINCT_EL_EQ] QED +Triviality ALL_DISTINCT_FLAT: + ∀l. ALL_DISTINCT (FLAT l) ⇔ + (∀l0. MEM l0 l ⇒ ALL_DISTINCT l0) ∧ + (∀i j. i < j ∧ j < LENGTH l ⇒ + ∀e. MEM e (EL i l) ⇒ ¬MEM e (EL j l)) +Proof + Induct >> + dsimp[ALL_DISTINCT_APPEND,MEM_FLAT, + arithmeticTheory.LT_SUC] >> + metis_tac[MEM_EL] +QED + Triviality ALOOKUP_MAPi_ID: !l k. ALOOKUP (MAPi (\i n. (i,n)) l) k = if k < LENGTH l then SOME (EL k l) else NONE @@ -604,5 +679,288 @@ Proof gvs[ALL_DISTINCT_APPEND] >> metis_tac[] QED +Triviality MEM_MEM_top_sort: + ALL_DISTINCT (MAP FST l) ∧ + MEM xs $ top_sort l ∧ + MEM n xs ⇒ + MEM n (MAP FST l) +Proof + strip_tac >> + drule_all $ SRULE[]top_sort_correct >> + strip_tac >> + pop_assum kall_tac >> + fs[EXTENSION] >> + metis_tac[MEM_FLAT] +QED + +Triviality ALL_DISTINCT_enc_graph: + ALL_DISTINCT + (MAPi + ($o FST o + (λi (n,ns). (i,to_nums (MAPi (λi n. (n,i)) (MAP FST graph)) ns))) + graph) +Proof + simp[indexedListsTheory.MAPi_GENLIST] >> + rw[ALL_DISTINCT_GENLIST] >> + ntac 2 (pairarg_tac >> fs[]) +QED + +Triviality RTC_ALOOKUP_enc_graph_IMP_depends_on: + ALL_DISTINCT (MAP FST graph) ⇒ + ∀n n'. RTC (λx y. + ∃aSetx. + ALOOKUP + (MAPi + (λi (n,ns). + (i,to_nums (MAPi (λi n. (n,i)) (MAP FST graph)) ns)) + graph) x = SOME aSetx ∧ + lookup y aSetx = SOME ()) n n' ⇒ + depends_on graph (EL n (MAP FST graph)) (EL n' (MAP FST graph)) +Proof + strip_tac >> + ho_match_mp_tac RTC_ind >> + rw[depends_on_def] >> + irule $ cj 2 RTC_RULES >> + first_x_assum $ irule_at (Pos last) >> + assume_tac ALL_DISTINCT_enc_graph >> + fs[GSYM MEM_ALOOKUP,indexedListsTheory.MEM_MAPi] >> + pairarg_tac >> + gvs[quantHeuristicsTheory.PAIR_EQ_EXPAND,EL_MAP] >> + qexists `SND (EL i graph)` >> + simp[PAIR,EL_MEM] >> + fs[GSYM domain_lookup_num_set] >> + `ALL_DISTINCT (MAP FST (MAPi (\i n.(n,i)) (MAP FST graph)))` by ( + simp[indexedListsTheory.MAP_MAPi, + indexedListsTheory.MAPi_GENLIST] >> + rw[ALL_DISTINCT_GENLIST] >> + metis_tac[EL_ALL_DISTINCT_EL_EQ,LENGTH_MAP]) >> + drule_then assume_tac (GSYM MEM_ALOOKUP) >> + drule_then assume_tac $ SRULE[]to_nums_correct >> + gvs[indexedListsTheory.MEM_MAPi,EL_MEM] +QED + +Theorem top_sort_any_same_partition: + ALL_DISTINCT (MAP FST graph) ∧ + MEM xs (top_sort_any graph) ∧ + MEM x xs ∧ MEM y xs ⇒ + depends_on graph x y +Proof + rpt strip_tac >> + Cases_on `x = y` + >- simp[depends_on_def] >> + fs[top_sort_any_def] >> + Cases_on `NULL graph` >> + gvs[MEM_MAP,MEM_FLAT] >> + `n ≠ n'` by (spose_not_then assume_tac >> gvs[]) >> + qpat_x_assum `option_CASE _ _ _ ≠ _` kall_tac >> + qmatch_asmsub_abbrev_tac `MEM _ (top_sort enc_graph)` >> + `ALL_DISTINCT (MAP FST enc_graph)` + by ( + rw[Abbr`enc_graph`,ALL_DISTINCT_GENLIST, + indexedListsTheory.MAPi_GENLIST] >> + ntac 2 (pairarg_tac >> fs[])) >> + `∀x. MEM x (MAP FST enc_graph) ⇒ x < LENGTH graph` + by ( + rw[Abbr`enc_graph`] >> + gvs[indexedListsTheory.MEM_MAPi] >> + pairarg_tac >> simp[]) >> + `MEM n (MAP FST enc_graph) ∧ MEM n' (MAP FST enc_graph)` + by metis_tac[MEM_MEM_top_sort] >> + drule_all_then strip_assume_tac top_sort_same_partition >> + `is_reachable (fromAList enc_graph) n n'` + by simp[GSYM trans_clos_correct] >> + fs[is_reachable_def,lambdify is_adjacent_def, + lookup_fromAList,ALOOKUP_MAPi_ID_f] >> + metis_tac[RTC_ALOOKUP_enc_graph_IMP_depends_on] +QED + +(* similar to depends_on, but we use TC instead of RTC *) +Definition TC_depends_on_def: + TC_depends_on alist ⇔ + TC (λa b. + ∃deps. + ALOOKUP alist a = SOME deps ∧ MEM b deps ∧ + MEM b (MAP FST alist)) +End + +Triviality TC_REFL_CASES_lem: + ∀x z. TC R x z ⇒ x = z ⇒ + (R x z ∨ (∃y. x ≠ y ∧ TC R x y ∧ TC R y z)) +Proof + ho_match_mp_tac TC_STRONG_INDUCT >> + rw[] >> + Cases_on `x = x'` >> + metis_tac[] +QED + +(* A cycle is either a self loop or +* there exists another node that is reachable from x and +* x is reachable from that node *) +Theorem TC_REFL_CASES: + TC R x x ⇔ (R x x ∨ (∃y. x ≠ y ∧ TC R x y ∧ TC R y x)) +Proof + iff_tac + >- metis_tac[TC_REFL_CASES_lem] >> + metis_tac[TC_RULES] +QED + +Triviality depends_on_IMP_MEM: + ∀x y. depends_on graph x y ⇒ x ≠ y ⇒ MEM y (MAP FST graph) +Proof + simp[depends_on_def] >> + ho_match_mp_tac RTC_ind >> + rw[] >> + Cases_on `y = x'` >> + simp[] +QED + +Theorem has_cycle_correct: + ALL_DISTINCT (MAP FST graph) ⇒ + (has_cycle graph ⇔ ∃x. TC_depends_on graph x x) +Proof + strip_tac >> + drule_then (assume_tac o GSYM) MEM_ALOOKUP >> + rw[EQ_IMP_THM,TC_depends_on_def,has_cycle_def, + EXISTS_MEM,LAMBDA_PROD,GSYM PEXISTS_THM] + >- ( + `∃x y. MEM x l ∧ MEM y l ∧ x ≠ y` + by ( + qexistsl [`EL 0 l`,`EL 1 l`] >> + simp[EL_MEM] >> + drule_then assume_tac $ + cj 1 $ SRULE[] top_sort_any_correct >> + `ALL_DISTINCT l` by fs[ALL_DISTINCT_FLAT] >> + (drule_then $ drule_then strip_assume_tac) $ + iffLR EL_ALL_DISTINCT_EL_EQ >> + pop_assum $ qspec_then `0` (assume_tac o SRULE[]) >> + fs[] + ) >> + `depends_on graph x y ∧ depends_on graph y x` by + metis_tac[top_sort_any_same_partition] >> + gvs[depends_on_def,RTC_CASES_TC] >> + qexists `x` >> + irule $ cj 2 TC_RULES >> + metis_tac[] + ) + >- ( + qexists `p1` >> + irule $ cj 1 TC_RULES >> + simp[] >> + first_assum $ irule_at Any >> + simp[MEM_MAP] >> + first_assum $ irule_at Any >> + simp[] + ) >> + fs[TC_REFL_CASES] + >- ( + disj2_tac >> + metis_tac[] + ) >> + disj1_tac >> + `depends_on graph y x` + by simp[RTC_CASES_TC,depends_on_def] >> + `depends_on graph x y` + by simp[RTC_CASES_TC,depends_on_def] >> + rpt $ qpat_x_assum `TC _ _ _` kall_tac >> + drule_then strip_assume_tac $ + SRULE[]top_sort_any_correct >> + fs[EXTENSION] >> + `MEM x (MAP FST graph)` by metis_tac[depends_on_IMP_MEM] >> + qpat_x_assum `∀x. MEM _ _ ⇔ MEM _ _` $ assume_tac o GSYM >> + fs[MEM_FLAT] >> + `∃xss zss. top_sort_any graph = xss ++ [l] ++ zss` + by metis_tac[MEM_SING_APPEND] >> + first_x_assum (drule_then $ drule_then drule) >> + disch_then assume_tac >> + `MEM y l` by fs[] >> + qpat_x_assum `_ ∧ (depends_on _ _ _ ⇒ _)` kall_tac >> + first_assum $ irule_at (Pos hd) >> + irule arithmeticTheory.LESS_LESS_EQ_TRANS >> + irule_at (Pos last) CARD_LIST_TO_SET >> + irule arithmeticTheory.LESS_LESS_EQ_TRANS >> + qexists `CARD {x;y}` >> + irule_at (Pos last) CARD_SUBSET >> + simp[] +QED + +(* Similar to TC_depends_on, but we do not require +* MEM b (MAP FST alist) *) +Definition TC_depends_on_weak_def: + TC_depends_on_weak alist ⇔ + TC (λa b. + ∃deps. + ALOOKUP alist a = SOME deps ∧ MEM b deps) +End + +Theorem TC_depends_on_weak_IMP_MEM: + ∀x y. TC_depends_on_weak graph x y ⇒ + MEM x (MAP FST graph) +Proof + PURE_REWRITE_TAC[TC_depends_on_weak_def] >> + ho_match_mp_tac TC_INDUCT >> + rw[]>> + drule ALOOKUP_MEM >> + rw[MEM_MAP] >> + first_assum $ irule_at (Pos last) >> + simp[] +QED + +Triviality TC_depends_on_weak_IMP_TC_depends_on: + ∀x y. TC_depends_on_weak graph x y ⇒ + MEM y (MAP FST graph) ⇒ + TC_depends_on graph x y +Proof + PURE_REWRITE_TAC[TC_depends_on_weak_def] >> + ho_match_mp_tac TC_STRONG_INDUCT_RIGHT1 >> + rw[TC_depends_on_def] + >- ( + irule $ cj 1 TC_RULES >> + simp[] + ) >> + irule TC_RIGHT1_I >> + last_x_assum $ irule_at (Pos last) >> + conj_tac + >- ( + simp[MEM_MAP] >> + drule_then (irule_at (Pos last)) ALOOKUP_MEM >> + simp[] + ) >> + simp[] +QED + +(* TC_depends_on_weak implies TC_depends_on +* if the last element is also in MAP FST graph *) +Theorem TC_depends_on_TC_depends_on_weak_thm: + ∀x y. TC_depends_on graph x y = + (TC_depends_on_weak graph x y ∧ MEM y (MAP FST graph)) +Proof + simp[EQ_IMP_THM,TC_depends_on_weak_IMP_TC_depends_on] >> + simp[TC_depends_on_weak_def,TC_depends_on_def] >> + simp[IMP_CONJ_THM,FORALL_AND_THM] >> + conj_tac + >- ( + rpt strip_tac >> + drule_at_then (Pos last) irule TC_MONOTONE >> + rw[] >> + metis_tac[] + ) >> + ho_match_mp_tac TC_INDUCT_RIGHT1 >> + rw[] +QED + +Theorem TC_depends_on_weak_cycle_thm: + TC_depends_on_weak graph x x = TC_depends_on graph x x +Proof + simp[TC_depends_on_TC_depends_on_weak_thm,EQ_IMP_THM] >> + metis_tac[TC_depends_on_weak_IMP_MEM] +QED + +Theorem has_cycle_correct2: + ALL_DISTINCT (MAP FST graph) ⇒ + (has_cycle graph ⇔ ∃x. TC_depends_on_weak graph x x) +Proof + simp[TC_depends_on_weak_cycle_thm] >> + metis_tac[has_cycle_correct] +QED val _ = export_theory();