add theorems for cycle detection to topological_sortTheory

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();