Support cycle detection in topological_sortTheory

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

621 stars 140 forks source link

Support cycle detection in topological_sortTheory #1197

Closed Gordon-Sau closed 7 months ago

Gordon-Sau commented 7 months ago

add has_cycle which checks if there are cycles in the graph
prove that any pair of elements in a partition of the output of the top_sort is connected.
add predicats TC_depends_on (a TC version of depends_on) and TC_depends_on_weak (which removes the MEM b (MAP FST graph) condition from TC_depends_on)
prove the correctness of has_cycle (has_cycle_correct and has_cycle_correct2)

Gordon-Sau commented 7 months ago

I am going to add some theorems related to strongly connected components to make it more reusable. The definition of SCC is SCC E x y = RTC E x y /\ RTC E y x.

mn200 commented 7 months ago

Thanks for this. The SCC notion feels like it could be moved to relationTheory, but that can be done later.