Theory Dijkstra

(*
  File: Dijkstra.thy
  Author: Bohua Zhan
*)

section ‹Dijkstra's algorithm for shortest paths›

theory Dijkstra
  imports Mapping_Str Arrays_Ex
begin

text ‹
  Verification of Dijkstra's algorithm: function part.

  The algorithm is also verified by Nordhoff and Lammich in
  \<^cite>‹"Dijkstra_Shortest_Path-AFP"›.
›

subsection ‹Graphs›

datatype graph = Graph "nat list list"

fun size :: "graph ⇒ nat" where
  "size (Graph G) = length G"

fun weight :: "graph ⇒ nat ⇒ nat ⇒ nat" where
  "weight (Graph G) m n = (G ! m) ! n"

fun valid_graph :: "graph ⇒ bool" where
  "valid_graph (Graph G) ⟷ (∀i<length G. length (G ! i) = length G)"
setup ‹add_rewrite_rule @{thm valid_graph.simps}›

subsection ‹Paths on graphs›

text ‹The set of vertices less than n.›
definition verts :: "graph ⇒ nat set" where
  "verts G = {i. i < size G}"

lemma verts_mem [rewrite]: "i ∈ verts G ⟷ i < size G" by (simp add: verts_def)
lemma card_verts [rewrite]: "card (verts G) = size G" using verts_def by auto
lemma finite_verts [forward]: "finite (verts G)" using verts_def by auto

definition is_path :: "graph ⇒ nat list ⇒ bool" where [rewrite]:
  "is_path G p ⟷ p ≠ [] ∧ set p ⊆ verts G"

lemma is_path_to_in_verts [forward]: "is_path G p ⟹ hd p ∈ verts G ∧ last p ∈ verts G"
@proof @have "last p ∈ set p" @qed

definition joinable :: "graph ⇒ nat list ⇒ nat list ⇒ bool" where [rewrite]:
  "joinable G p q ⟷ (is_path G p ∧ is_path G q ∧ last p = hd q)"

definition path_join :: "graph ⇒ nat list ⇒ nat list ⇒ nat list" where [rewrite]:
  "path_join G p q = p @ tl q"
setup ‹register_wellform_data ("path_join G p q", ["joinable G p q"])›
setup ‹add_prfstep_check_req ("path_join G p q", "joinable G p q")›

lemma path_join_is_path:
  "joinable G p q ⟹ is_path G (path_join G p q)"
@proof @have "q = hd q # tl q" @qed
setup ‹add_forward_prfstep_cond @{thm path_join_is_path} [with_term "path_join ?G ?p ?q"]›

fun path_weight :: "graph ⇒ nat list ⇒ nat" where
  "path_weight G [] = 0"
| "path_weight G (x # xs) = (if xs = [] then 0 else weight G x (hd xs) + path_weight G xs)"
setup ‹fold add_rewrite_rule @{thms path_weight.simps}›

lemma path_weight_singleton [rewrite]: "path_weight G [x] = 0" by auto2
lemma path_weight_doubleton [rewrite]: "path_weight G [m, n] = weight G m n" by auto2

lemma path_weight_sum [rewrite]:
  "joinable G p q ⟹ path_weight G (path_join G p q) = path_weight G p + path_weight G q"
@proof @induct p @qed

fun path_set :: "graph ⇒ nat ⇒ nat ⇒ nat list set" where
  "path_set G m n = {p. is_path G p ∧ hd p = m ∧ last p = n}"

lemma path_set_mem [rewrite]:
  "p ∈ path_set G m n ⟷ is_path G p ∧ hd p = m ∧ last p = n" by simp

lemma path_join_set: "joinable G p q ⟹ path_join G p q ∈ path_set G (hd p) (last q)"
@proof @have "q = hd q # tl q" @case "tl q = []" @qed
setup ‹add_forward_prfstep_cond @{thm path_join_set} [with_term "path_join ?G ?p ?q"]›

subsection ‹Shortest paths›

definition is_shortest_path :: "graph ⇒ nat ⇒ nat ⇒ nat list ⇒ bool" where [rewrite]:
  "is_shortest_path G m n p ⟷
     (p ∈ path_set G m n ∧ (∀p'∈path_set G m n. path_weight G p' ≥ path_weight G p))"

lemma is_shortest_pathD1 [forward]:
  "is_shortest_path G m n p ⟹ p ∈ path_set G m n" by auto2

lemma is_shortest_pathD2 [forward]:
  "is_shortest_path G m n p ⟹ p' ∈ path_set G m n ⟹ path_weight G p' ≥ path_weight G p" by auto2
setup ‹del_prfstep_thm_eqforward @{thm is_shortest_path_def}›

definition has_dist :: "graph ⇒ nat ⇒ nat ⇒ bool" where [rewrite]:
  "has_dist G m n ⟷ (∃p. is_shortest_path G m n p)"

lemma has_distI [forward]: "is_shortest_path G m n p ⟹ has_dist G m n" by auto2
lemma has_distD [resolve]: "has_dist G m n ⟹ ∃p. is_shortest_path G m n p" by auto2
lemma has_dist_to_in_verts [forward]: "has_dist G u v ⟹ u ∈ verts G ∧ v ∈ verts G" by auto2
setup ‹del_prfstep_thm @{thm has_dist_def}›

definition dist :: "graph ⇒ nat ⇒ nat ⇒ nat" where [rewrite]:
  "dist G m n = path_weight G (SOME p. is_shortest_path G m n p)"
setup ‹register_wellform_data ("dist G m n", ["has_dist G m n"])›

lemma dist_eq [rewrite]:
  "is_shortest_path G m n p ⟹ dist G m n = path_weight G p" by auto2

lemma distD [forward]:
  "has_dist G m n ⟹ p ∈ path_set G m n ⟹ path_weight G p ≥ dist G m n" by auto2
setup ‹del_prfstep_thm @{thm dist_def}›

lemma shortest_init [resolve]: "n ∈ verts G ⟹ is_shortest_path G n n [n]" by auto2

subsection ‹Interior points›

text ‹List of interior points›
definition int_pts :: "nat list ⇒ nat set" where [rewrite]:
  "int_pts p = set (butlast p)"

lemma int_pts_singleton [rewrite]: "int_pts [x] = {}" by auto2
lemma int_pts_doubleton [rewrite]: "int_pts [x, y] = {x}" by auto2

definition path_set_on :: "graph ⇒ nat ⇒ nat ⇒ nat set ⇒ nat list set" where
  "path_set_on G m n V = {p. p ∈ path_set G m n ∧ int_pts p ⊆ V}"

lemma path_set_on_mem [rewrite]:
  "p ∈ path_set_on G m n V ⟷ p ∈ path_set G m n ∧ int_pts p ⊆ V" by (simp add: path_set_on_def)

text ‹Version of shortest path on a set of points›
definition is_shortest_path_on :: "graph ⇒ nat ⇒ nat ⇒ nat list ⇒ nat set ⇒ bool" where [rewrite]:
  "is_shortest_path_on G m n p V ⟷
    (p ∈ path_set_on G m n V ∧ (∀p'∈path_set_on G m n V. path_weight G p' ≥ path_weight G p))"

lemma is_shortest_path_onD1 [forward]:
  "is_shortest_path_on G m n p V ⟹ p ∈ path_set_on G m n V" by auto2

lemma is_shortest_path_onD2 [forward]:
  "is_shortest_path_on G m n p V ⟹ p' ∈ path_set_on G m n V ⟹ path_weight G p' ≥ path_weight G p" by auto2
setup ‹del_prfstep_thm_eqforward @{thm is_shortest_path_on_def}›

definition has_dist_on :: "graph ⇒ nat ⇒ nat ⇒ nat set ⇒ bool" where [rewrite]:
  "has_dist_on G m n V ⟷ (∃p. is_shortest_path_on G m n p V)"

lemma has_dist_onI [forward]: "is_shortest_path_on G m n p V ⟹ has_dist_on G m n V" by auto2
lemma has_dist_onD [resolve]: "has_dist_on G m n V ⟹ ∃p. is_shortest_path_on G m n p V" by auto2
setup ‹del_prfstep_thm @{thm has_dist_on_def}›

definition dist_on :: "graph ⇒ nat ⇒ nat ⇒ nat set ⇒ nat" where [rewrite]:
  "dist_on G m n V = path_weight G (SOME p. is_shortest_path_on G m n p V)"
setup ‹register_wellform_data ("dist_on G m n V", ["has_dist_on G m n V"])›

lemma dist_on_eq [rewrite]:
  "is_shortest_path_on G m n p V ⟹ dist_on G m n V = path_weight G p" by auto2

lemma dist_onD [forward]:
  "has_dist_on G m n V ⟹ p ∈ path_set_on G m n V ⟹ path_weight G p ≥ dist_on G m n V" by auto2
setup ‹del_prfstep_thm @{thm dist_on_def}›

subsection ‹Two splitting lemmas›

lemma path_split1 [backward]: "is_path G p ⟹ hd p ∈ V ⟹ last p ∉ V ⟹
  ∃p1 p2. joinable G p1 p2 ∧ p = path_join G p1 p2 ∧ int_pts p1 ⊆ V ∧ hd p2 ∉ V"
@proof @induct p @with
  @subgoal "p = a # p'"
    @let "p = a # p'"
    @case "p' = []"
    @case "hd p' ∉ V" @with @have "p = path_join G [a, hd p'] p'" @end
    @obtain p1 p2 where "joinable G p1 p2" "p' = path_join G p1 p2" "int_pts p1 ⊆ V" "hd p2 ∉ V"
    @have "p = path_join G (a # p1) p2"
  @endgoal @end
@qed

lemma path_split2 [backward]: "is_path G p ⟹ hd p ≠ last p ⟹
  ∃q n. joinable G q [n, last p] ∧ p = path_join G q [n, last p]"
@proof
  @have "p = butlast p @ [last p]"
  @have "butlast p ≠ []"
  @let "n = last (butlast p)"
  @have "p = path_join G (butlast p) [n, last p]"
@qed

subsection ‹Deriving has\_dist and has\_dist\_on›

definition known_dists :: "graph ⇒ nat set ⇒ bool" where [rewrite]:
  "known_dists G V ⟷ (V ⊆ verts G ∧ 0 ∈ V ∧
      (∀i∈verts G. has_dist_on G 0 i V) ∧
      (∀i∈V. has_dist G 0 i ∧ dist G 0 i = dist_on G 0 i V))"

lemma derive_dist [backward2]:
  "known_dists G V ⟹
   m ∈ verts G - V ⟹
   ∀i∈verts G - V. dist_on G 0 i V ≥ dist_on G 0 m V ⟹
   has_dist G 0 m ∧ dist G 0 m = dist_on G 0 m V"
@proof
  @obtain p where "is_shortest_path_on G 0 m p V"
  @have "is_shortest_path G 0 m p" @with
    @have "p ∈ path_set G 0 m"
    @have "∀p'∈path_set G 0 m. path_weight G p' ≥ path_weight G p" @with
      @obtain p1 p2 where "joinable G p1 p2" "p' = path_join G p1 p2"
                          "int_pts p1 ⊆ V" "hd p2 ∉ V"
      @let "x = last p1"
      @have "dist_on G 0 x V ≥ dist_on G 0 m V"
      @have "p1 ∈ path_set_on G 0 x V"
      @have "path_weight G p1 ≥ dist_on G 0 x V"
      @have "path_weight G p' ≥ dist_on G 0 m V + path_weight G p2"
    @end
  @end
@qed

lemma join_def' [resolve]: "joinable G p q ⟹ path_join G p q = butlast p @ q"
@proof
  @have "p = butlast p @ [last p]"
  @have "path_join G p q = butlast p @ [last p] @ tl q"
@qed

lemma int_pts_join [rewrite]:
  "joinable G p q ⟹ int_pts (path_join G p q) = int_pts p ∪ int_pts q"
@proof @have "path_join G p q = butlast p @ q" @qed

lemma dist_on_triangle_ineq [backward]:
  "has_dist_on G k m V ⟹ has_dist_on G k n V ⟹ V ⊆ verts G ⟹ n ∈ verts G ⟹ m ∈ V ⟹
   dist_on G k m V + weight G m n ≥ dist_on G k n V"
@proof
  @obtain p where "is_shortest_path_on G k m p V"
  @let "pq = path_join G p [m, n]"
  @have "V ∪ {m} = V"
  @have "pq ∈ path_set_on G k n V"
@qed

lemma derive_dist_on [backward2]:
  "known_dists G V ⟹
   m ∈ verts G - V ⟹
   ∀i∈verts G - V. dist_on G 0 i V ≥ dist_on G 0 m V ⟹
   V' = V ∪ {m} ⟹
   n ∈ verts G - V' ⟹
   has_dist_on G 0 n V' ∧ dist_on G 0 n V' = min (dist_on G 0 n V) (dist_on G 0 m V + weight G m n)"
@proof
  @have "has_dist G 0 m ∧ dist G 0 m = dist_on G 0 m V"
  @let "M = min (dist_on G 0 n V) (dist_on G 0 m V + weight G m n)"
  @have "∀p∈path_set_on G 0 n V'. path_weight G p ≥ M" @with
    @obtain q n' where "joinable G q [n', n]" "p = path_join G q [n', n]"
    @have "q ∈ path_set G 0 n'"
    @have "n' ∈ V'"
    @case "n' ∈ V" @with
      @have "dist_on G 0 n' V = dist G 0 n'"
      @have "path_weight G q ≥ dist_on G 0 n' V"
      @have "path_weight G p ≥ dist_on G 0 n' V + weight G n' n"
      @have "dist_on G 0 n' V + weight G n' n ≥ dist_on G 0 n V"
    @end
    @have "n' = m"
    @have "path_weight G q ≥ dist G 0 m"
    @have "path_weight G p ≥ dist G 0 m + weight G m n"
  @end
  @case "dist_on G 0 m V + weight G m n ≥ dist_on G 0 n V" @with
    @obtain p where "is_shortest_path_on G 0 n p V"
    @have "is_shortest_path_on G 0 n p V'" @with
      @have "p ∈ path_set_on G 0 n V'" @with @have "V ⊆ V'" @end
    @end
  @end
  @have "M = dist_on G 0 m V + weight G m n"
  @obtain pm where "is_shortest_path_on G 0 m pm V"
  @have "path_weight G pm = dist G 0 m"
  @let "p = path_join G pm [m, n]"
  @have "joinable G pm [m, n]"
  @have "path_weight G p = path_weight G pm + weight G m n"
  @have "is_shortest_path_on G 0 n p V'"
@qed

subsection ‹Invariant for the Dijkstra's algorithm›

text ‹The state consists of an array maintaining the best estimates,
  and a heap containing estimates for the unknown vertices.›
datatype state = State (est: "nat list") (heap: "(nat, nat) map")
setup ‹add_simple_datatype "state"›

definition unknown_set :: "state ⇒ nat set" where [rewrite]:
  "unknown_set S = keys_of (heap S)"

definition known_set :: "state ⇒ nat set" where [rewrite]:
  "known_set S = {..<length (est S)} - unknown_set S"

text ‹Invariant: for every vertex, the estimate is at least the shortest distance.
  Furthermore, for the known vertices the estimate is exact.›
definition inv :: "graph ⇒ state ⇒ bool" where [rewrite]:
  "inv G S ⟷ (let V = known_set S; W = unknown_set S; M = heap S in
      (length (est S) = size G ∧ known_dists G V ∧
      keys_of M ⊆ verts G ∧
      (∀i∈W. M⟨i⟩ = Some (est S ! i)) ∧
      (∀i∈V. est S ! i = dist G 0 i) ∧
      (∀i∈verts G. est S ! i = dist_on G 0 i V)))"

lemma invE1 [forward]: "inv G S ⟹ length (est S) = size G ∧ known_dists G (known_set S) ∧ unknown_set S ⊆ verts G" by auto2
lemma invE2 [forward]: "inv G S ⟹ i ∈ known_set S ⟹ est S ! i = dist G 0 i" by auto2
lemma invE3 [forward]: "inv G S ⟹ i ∈ verts G ⟹ est S ! i = dist_on G 0 i (known_set S)" by auto2
lemma invE4 [rewrite]: "inv G S ⟹ i ∈ unknown_set S ⟹ (heap S)⟨i⟩ = Some (est S ! i)" by auto2
setup ‹del_prfstep_thm_str "@eqforward" @{thm inv_def}›

lemma inv_unknown_set [rewrite]:
  "inv G S ⟹ unknown_set S = verts G - known_set S" by auto2

lemma dijkstra_end_inv [forward]:
  "inv G S ⟹ unknown_set S = {} ⟹ ∀i∈verts G. has_dist G 0 i ∧ est S ! i = dist G 0 i" by auto2

subsection ‹Starting state›

definition dijkstra_start_state :: "graph ⇒ state" where [rewrite]:
  "dijkstra_start_state G =
     State (list (λi. if i = 0 then 0 else weight G 0 i) (size G))
           (map_constr (λi. i > 0) (λi. weight G 0 i) (size G))"
setup ‹register_wellform_data ("dijkstra_start_state G", ["size G > 0"])›

lemma dijkstra_start_known_set [rewrite]:
  "size G > 0 ⟹ known_set (dijkstra_start_state G) = {0}" by auto2
    
lemma dijkstra_start_unknown_set [rewrite]:
  "size G > 0 ⟹ unknown_set (dijkstra_start_state G) = verts G - {0}" by auto2

lemma card_start_state [rewrite]:
  "size G > 0 ⟹ card (unknown_set (dijkstra_start_state G)) = size G - 1"
@proof @have "0 ∈ verts G" @qed

text ‹Starting start of Dijkstra's algorithm satisfies the invariant.›
theorem dijkstra_start_inv [backward]:
  "size G > 0 ⟹ inv G (dijkstra_start_state G)"
@proof
  @let "V = {0::nat}"
  @have "has_dist G 0 0 ∧ dist G 0 0 = 0" @with
    @have "is_shortest_path G 0 0 [0]" @end
  @have "has_dist_on G 0 0 V ∧ dist_on G 0 0 V = 0" @with
    @have "is_shortest_path_on G 0 0 [0] V" @end
  @have "V ⊆ verts G ∧ 0 ∈ V"
  @have (@rule) "∀i∈verts G. i ≠ 0 ⟶ has_dist_on G 0 i V ∧ dist_on G 0 i V = weight G 0 i" @with
    @let "p = [0, i]"
    @have "is_shortest_path_on G 0 i p V" @with
      @have "p ∈ path_set_on G 0 i V"
      @have "∀p'∈path_set_on G 0 i V. path_weight G p' ≥ weight G 0 i" @with
        @obtain q n where "joinable G q [n, last p']" "p' = path_join G q [n, last p']"
        @have "n ∈ V" @have "n = 0"
        @have "path_weight G p' = path_weight G q + weight G 0 i"
      @end
    @end
  @end
@qed

subsection ‹Step of Dijkstra's algorithm›

fun dijkstra_step :: "graph ⇒ nat ⇒ state ⇒ state" where
  "dijkstra_step G m (State e M) =
    (let M' = delete_map m M;
         e' = list_update_set (λi. i ∈ keys_of M') (λi. min (e ! m + weight G m i) (e ! i)) e;
         M'' = map_update_all (λi. e' ! i) M'
     in State e' M'')"
setup ‹add_rewrite_rule @{thm dijkstra_step.simps}›
setup ‹register_wellform_data ("dijkstra_step G m S", ["inv G S", "m ∈ unknown_set S"])›

lemma has_dist_on_larger [backward1]:
  "has_dist G m n ⟹ has_dist_on G m n V ⟹ dist_on G m n V = dist G m n ⟹
   has_dist_on G m n (V ∪ {x}) ∧ dist_on G m n (V ∪ {x}) = dist G m n"
@proof
  @obtain p where "is_shortest_path_on G m n p V"
  @let "V' = V ∪ {x}"
  @have "p ∈ path_set_on G m n V'" @with @have "V ⊆ V'" @end
  @have "is_shortest_path_on G m n p V'"
@qed

lemma dijkstra_step_unknown_set [rewrite]:
  "inv G S ⟹ m ∈ unknown_set S ⟹ unknown_set (dijkstra_step G m S) = unknown_set S - {m}" by auto2

lemma dijkstra_step_known_set [rewrite]:
  "inv G S ⟹ m ∈ unknown_set S ⟹ known_set (dijkstra_step G m S) = known_set S ∪ {m}" by auto2

text ‹One step of Dijkstra's algorithm preserves the invariant.›
theorem dijkstra_step_preserves_inv [backward]:
  "inv G S ⟹ is_heap_min m (heap S) ⟹ inv G (dijkstra_step G m S)"
@proof
  @let "V = known_set S" "V' = V ∪ {m}"
  @have (@rule) "∀i∈V. has_dist G 0 i ∧ has_dist_on G 0 i V' ∧ dist_on G 0 i V' = dist G 0 i"
  @have "has_dist G 0 m ∧ dist G 0 m = dist_on G 0 m V"
  @have "has_dist_on G 0 m V' ∧ dist_on G 0 m V' = dist G 0 m"
  @have (@rule) "∀i∈verts G - V'. has_dist_on G 0 i V' ∧ dist_on G 0 i V' = min (dist_on G 0 i V) (dist_on G 0 m V + weight G m i)"
  @let "S' = dijkstra_step G m S"
  @have "known_dists G V'"
  @have "∀i∈V'. est S' ! i = dist G 0 i"
  @have "∀i∈verts G. est S' ! i = dist_on G 0 i V'" @with @case "i ∈ V'" @end
@qed

definition is_dijkstra_step :: "graph ⇒ state ⇒ state ⇒ bool" where [rewrite]:
  "is_dijkstra_step G S S' ⟷ (∃m. is_heap_min m (heap S) ∧ S' = dijkstra_step G m S)"

lemma is_dijkstra_stepI [backward2]:
  "is_heap_min m (heap S) ⟹ dijkstra_step G m S = S' ⟹ is_dijkstra_step G S S'" by auto2

lemma is_dijkstra_stepD1 [forward]:
  "inv G S ⟹ is_dijkstra_step G S S' ⟹ inv G S'" by auto2

lemma is_dijkstra_stepD2 [forward]:
  "inv G S ⟹ is_dijkstra_step G S S' ⟹ card (unknown_set S') = card (unknown_set S) - 1" by auto2
setup ‹del_prfstep_thm @{thm is_dijkstra_step_def}›

end