Theory Dijkstra_Impl

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

section ‹Implementation of Dijkstra's algorithm›

theory Dijkstra_Impl
  imports Indexed_PQueue_Impl "../Functional/Dijkstra"
begin

text ‹
  Imperative implementation of Dijkstra's shortest path algorithm. The
  algorithm is also verified by Nordhoff and Lammich in
  \<^cite>‹"Dijkstra_Shortest_Path-AFP"›.
›

datatype dijkstra_state = Dijkstra_State (est_a: "nat array") (heap_pq: "nat indexed_pqueue")
setup ‹add_simple_datatype "dijkstra_state"›

fun dstate :: "state ⇒ dijkstra_state ⇒ assn" where
  "dstate (State e M) (Dijkstra_State a pq) = a ↦⇩a e * idx_pqueue_map M (length e) pq"
setup ‹add_rewrite_ent_rule @{thm dstate.simps}›

subsection ‹Basic operations›

fun dstate_pq_init :: "graph ⇒ nat ⇒ nat indexed_pqueue Heap" where
  "dstate_pq_init G 0 = idx_pqueue_empty (size G)"
| "dstate_pq_init G (Suc k) = do {
    p ← dstate_pq_init G k;
    if k > 0 then update_idx_pqueue k (weight G 0 k) p
    else return p }"

lemma dstate_pq_init_to_fun [hoare_triple]:
  "k ≤ size G ⟹
   <emp>
   dstate_pq_init G k
   <idx_pqueue_map (map_constr (λi. i > 0) (λi. weight G 0 i) k) (size G)>⇩t"
@proof @induct k @qed
 
definition dstate_init :: "graph ⇒ dijkstra_state Heap" where
  "dstate_init G = do {
     a ← Array.of_list (list (λi. if i = 0 then 0 else weight G 0 i) (size G));
     pq ← dstate_pq_init G (size G);
     return (Dijkstra_State a pq)
   }"

lemma dstate_init_to_fun [hoare_triple]:
  "<emp>
   dstate_init G
   <dstate (dijkstra_start_state G)>⇩t" by auto2

fun dstate_update_est :: "graph ⇒ nat ⇒ nat ⇒ nat indexed_pqueue ⇒ nat array ⇒ nat array Heap" where
  "dstate_update_est G m 0 pq a = (return a)"
| "dstate_update_est G m (Suc k) pq a = do {
     b ← has_key_idx_pqueue k pq;
     if b then do {
       ek ← Array.nth a k;
       em ← Array.nth a m;
       a' ← dstate_update_est G m k pq a;
       a'' ← Array.upd k (min (em + weight G m k) ek) a';
       return a'' }
     else dstate_update_est G m k pq a }"

lemma dstate_update_est_ind [hoare_triple]:
  "k ≤ length e ⟹ m < length e ⟹
   <a ↦⇩a e * idx_pqueue_map M (length e) pq>
   dstate_update_est G m k pq a
   <λr. dstate (State (list_update_set_impl (λi. i ∈ keys_of M)
                      (λi. min (e ! m + weight G m i) (e ! i)) e k) M) (Dijkstra_State r pq)>⇩t"
@proof @induct k @qed

lemma dstate_update_est_to_fun [hoare_triple]:
  "<dstate (State e M) (Dijkstra_State a pq) * ↑(m < length e)>
   dstate_update_est G m (length e) pq a
   <λr. dstate (State (list_update_set (λi. i ∈ keys_of M)
               (λi. min (e ! m + weight G m i) (e ! i)) e) M) (Dijkstra_State r pq)>⇩t" by auto2

fun dstate_update_heap ::
  "graph ⇒ nat ⇒ nat ⇒ nat array ⇒ nat indexed_pqueue ⇒ nat indexed_pqueue Heap" where
  "dstate_update_heap G m 0 a pq = return pq"
| "dstate_update_heap G m (Suc k) a pq = do {
     b ← has_key_idx_pqueue k pq;
     if b then do {
       ek ← Array.nth a k;
       pq' ← dstate_update_heap G m k a pq;
       update_idx_pqueue k ek pq' }
     else dstate_update_heap G m k a pq }"

lemma dstate_update_heap_ind [hoare_triple]:
  "k ≤ length e ⟹ m < length e ⟹
   <a ↦⇩a e * idx_pqueue_map M (length e) pq>
   dstate_update_heap G m k a pq
   <λr. dstate (State e (map_update_all_impl (λi. e ! i) M k)) (Dijkstra_State a r)>⇩t"
@proof @induct k @qed

lemma dstate_update_heap_to_fun [hoare_triple]:
  "m < length e ⟹
   ∀i∈keys_of M. i < length e ⟹
   <dstate (State e M) (Dijkstra_State a pq)>
   dstate_update_heap G m (length e) a pq
   <λr. dstate (State e (map_update_all (λi. e ! i) M)) (Dijkstra_State a r)>⇩t" by auto2

fun dijkstra_extract_min :: "dijkstra_state ⇒ (nat × dijkstra_state) Heap" where
  "dijkstra_extract_min (Dijkstra_State a pq) = do {
     (x, pq') ← delete_min_idx_pqueue pq;
     return (fst x, Dijkstra_State a pq') }"
  
lemma dijkstra_extract_min_rule [hoare_triple]:
  "M ≠ empty_map ⟹
   <dstate (State e M) (Dijkstra_State a pq)>
   dijkstra_extract_min (Dijkstra_State a pq)
   <λ(m, r). dstate (State e (delete_map m M)) r * ↑(m < length e) * ↑(is_heap_min m M)>⇩t" by auto2

setup ‹del_prfstep_thm @{thm dstate.simps}›

subsection ‹Main operations›

fun dijkstra_step_impl :: "graph ⇒ dijkstra_state ⇒ dijkstra_state Heap" where
  "dijkstra_step_impl G (Dijkstra_State a pq) = do {
     (x, S') ← dijkstra_extract_min (Dijkstra_State a pq);
     a' ← dstate_update_est G x (size G) (heap_pq S') (est_a S');
     pq'' ← dstate_update_heap G x (size G) a' (heap_pq S');
     return (Dijkstra_State a' pq'') }"

lemma dijkstra_step_impl_to_fun [hoare_triple]:
  "heap S ≠ empty_map ⟹ inv G S ⟹
   <dstate S (Dijkstra_State a pq)>
   dijkstra_step_impl G (Dijkstra_State a pq)
   <λr. ∃⇩AS'. dstate S' r * ↑(is_dijkstra_step G S S')>⇩t" by auto2

lemma dijkstra_step_impl_correct [hoare_triple]:
  "heap S ≠ empty_map ⟹ inv G S ⟹
   <dstate S p>
   dijkstra_step_impl G p
   <λr. ∃⇩AS'. dstate S' r * ↑(inv G S') * ↑(card (unknown_set S') = card (unknown_set S) - 1)>⇩t" by auto2

fun dijkstra_loop :: "graph ⇒ nat ⇒ dijkstra_state ⇒ dijkstra_state Heap" where
  "dijkstra_loop G 0 p = (return p)"
| "dijkstra_loop G (Suc k) p = do {
    p' ← dijkstra_step_impl G p;
    p'' ← dijkstra_loop G k p';
    return p'' }"

lemma dijkstra_loop_correct [hoare_triple]:
  "<dstate S p * ↑(inv G S) * ↑(n ≤ card (unknown_set S))>
   dijkstra_loop G n p
   <λr. ∃⇩AS'. dstate S' r * ↑(inv G S') * ↑(card (unknown_set S') = card (unknown_set S) - n)>⇩t"
@proof @induct n arbitrary S p @qed

definition dijkstra :: "graph ⇒ dijkstra_state Heap" where
  "dijkstra G = do {
    p ← dstate_init G;
    dijkstra_loop G (size G - 1) p }"

text ‹Correctness of Dijkstra's algorithm.›
theorem dijkstra_correct [hoare_triple]:
  "size G > 0 ⟹
   <emp>
   dijkstra G
   <λr. ∃⇩AS. dstate S r * ↑(inv G S) * ↑(unknown_set S = {}) *
        ↑(∀i∈verts G. has_dist G 0 i ∧ est S ! i = dist G 0 i)>⇩t" by auto2

end