From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import SetoidClass.

From Padec Require Import SetoidUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import BoolSet.
From Padec Require Import All_In.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Exec.
From Padec Require Import Fairness.
From Padec Require Import Rounds.
From Padec Require Import BFS_algo.
From Padec Require Import BFS_common.
From Padec Require Import Graph_Diameter.
From Padec Require Import BFS_specification.
From Padec Require Import BFS_correctness.
From Padec Require Import Tree_topology_ALT.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Section BFS_rounds.

  Context {Chans: Channels}
          {Net: Network}
          {Graph_assumption: BFS_Assume}
          {Graph_network_assumption: Graph_Network_matching}
          {D_Assumption: BFS_D}.
  Existing Instance G_compat.
  Existing Instance BFS_RO_assumption.

  Notation Algo := (BFS_algo D).
  Notation Env := (Env (Net := Net) (Algo := Algo)).
  Notation terminal := (terminal (Net := Net) (Algo := Algo)).
  Notation Exec := (Exec (Net := Net) (Algo := Algo)).

  Notation dist := (dist G_compat G_dec Connected all_nodes_prop (DA := Node_dec)).
  Notation dist_neighbors :=
    (dist_neighbors G_compat G_dec Connected all_nodes_prop
                    Bidir Root (DA := Node_dec)).
  Notation dist_neighbor_ex :=
    (dist_neighbor_ex G_compat G_dec Connected all_nodes_prop
                      (DA := Node_dec)).
  Lemma diam_dist: forall p q, dist p q <= Diam.
  Lemma dist_nil': forall p q, dist p q = 0 <-> p == q.

  Notation NodeSet := (BoolSet (A:=Node)).
  Notation eqNodeSet := (eqBoolSet (eqA := (equiv (A:=Node)))).
  Notation leNodeSet := (leBoolSet (eqA := (equiv (A:=Node)))).

  Definition CD1 := (fun (k: nat) (p: Node) (g: Env) =>
                       (dist p Root < k -> d (g p) = dist p Root)).
  Definition CD2 := (fun (k: nat) (p: Node) (g: Env) =>
                       (dist p Root >= k -> d (g p) >= k)).

  Definition CD :=
    (fun (k: nat) (p: Node) (g: Env) => CD1 k p g /\ CD2 k p g).

  Definition check_dist (k: nat) (g: Env): Prop :=
    forall p, CD k p g.

  Instance CD1_compat: Proper pequiv CD1.

  Instance CD2_compat: Proper pequiv CD2.

  Instance CD_compat: Proper pequiv CD.

  Instance check_dist_compat: Proper pequiv check_dist.

  Lemma CD1_dec: forall k p g, {CD1 k p g} + {~ CD1 k p g}.

  Lemma CD2_dec: forall k p g, {CD2 k p g} + {~ CD2 k p g}.

  Lemma CD_dec: forall k p g, {CD k p g} + {~ CD k p g}.

  Lemma check_dist_dec:
    forall k g,
      Proper pequiv g ->
      { check_dist k g } + { ~check_dist k g }.

  Lemma check_dist_clas:
    forall k g,
      Proper pequiv g ->
      check_dist k g \/ ~check_dist k g .

  Lemma check_dist_incr:
    forall k g, check_dist k g ->
                forall k', k' <= k -> check_dist k' g.

  Lemma check_dist_0: forall g, check_dist 0 g.

  Lemma check_dist_Diam:
    forall g, check_dist (S Diam) g <->
              forall p, d (g p) = dist p Root.

  Lemma check_dist_ge_Diam:
    forall g, check_dist (S Diam) g ->
              forall k, S Diam <= k -> check_dist k g.

  Lemma CD1_step:
    forall g' g, Assume g -> Step g' g ->
                 forall k p,
                   (forall q, G p q -> CD k q g) ->
                   CD1 (S k) p g -> CD1 (S k) p g'.

  Lemma CD2_step:
    forall g' g, Assume g -> Step g' g ->
                 forall k p,
                   (forall q, G p q -> CD k q g) ->
                   CD2 (S k) p g -> CD2 (S k) p g'.

  Lemma CD_step:
    forall g' g, Assume g -> Step g' g ->
                 forall k p,
                   (forall q, G p q -> CD k q g) ->
                   CD (S k) p g -> CD (S k) p g'.

  Lemma check_dist_step:
    forall g' g, Assume g -> Step g' g ->
                 forall k, check_dist k g -> check_dist k g'.

  Lemma CD1_exec_Always:
    forall e, Assume (s_hd e) -> is_exec e ->
              forall k p,
                check_dist k (s_hd e) ->
                CD1 (S k) p (s_hd e) ->
                Always (fun c => CD1 (S k) p (s_hd c)) e.
  Lemma CD2_exec_Always:
    forall e, Assume (s_hd e) -> is_exec e ->
              forall k p,
                check_dist k (s_hd e) ->
                CD2 (S k) p (s_hd e) ->
                Always (fun c => CD2 (S k) p (s_hd c)) e.
  Lemma check_dist_exec_Always:
    forall e, Assume (s_hd e) -> is_exec e ->
              forall k, check_dist k (s_hd e) ->
                        Always (fun c => check_dist k (s_hd c)) e.
  Lemma check_dist_terminal:
    forall g, Proper pequiv g -> terminal g ->
              Assume g ->
              forall k, check_dist k g.


  Lemma Root_remains_0:
    forall e, is_exec e -> Assume (s_hd e) ->
              d (s_hd e Root) = 0 ->
              Always (fun c => d (s_hd c Root) = 0) e.

  Lemma Root_act_neut:
    forall g (e: Exec),
      Assume g -> Step (s_hd e) g ->
      act_neut_b (s_cons g e) Root = true->
      d (s_hd e Root) = 0.
  Lemma BFS_round_base_case_1a:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)),
      at_most_rounds (Always
                         (fun c: Exec => d (s_hd c Root) = 0)) 1 e.
  Lemma non_Root_positive:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall p, ~ p == Root -> d (s_hd e p) > 0 ->
                Always (fun c => d (s_hd c p) >= 1) e.
  Lemma non_Root_d0_enabled:
    forall (g: Env) p,
      Proper pequiv g -> Assume g -> ~ p == Root ->
      d (g p) = 0 -> enabled_b g p = true.

  Lemma non_Root_act:
    forall g (e: Exec) p,
      Assume g -> Step (s_hd e) g ->
      ~ p == Root -> ACT_b p (s_cons g e) = true->
      d (s_hd e p) = Dist_p (D :: map S (dist_Neigh g p)).

  Lemma non_Root_neut:
    forall g (e: Exec) p,
      Assume g -> Step (s_hd e) g ->
      ~ p == Root -> NEUT_b p (s_cons g e) = true->
      d (s_hd e p) = Dist_p (D :: map S (dist_Neigh (s_hd e) p)).

  Lemma non_Root_act_neut_ge1:
    forall g (e: Exec) p,
      Assume g -> Step (s_hd e) g ->
      ~ p == Root -> act_neut_b (s_cons g e) p = true->
      d (s_hd e p) >= 1.

  Lemma BFS_round_base_case_1b:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)),
    forall p,
      ~ p == Root ->
      at_most_rounds (Always (fun c: Exec => d (s_hd c p) >= 1)) 1 e.
  Lemma BFS_round_base_case_1:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)),
      at_most_rounds (Always (fun c => check_dist 1 (s_hd c))) 1 e.


  Lemma node_remains_k:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall k p,
        k >= 1 -> check_dist k (s_hd e) ->
        dist p Root = k -> d (s_hd e p) = k ->
        Always (fun c => d (s_hd c p) = k) e.

  Lemma not_k_enabled:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall k p, k >= 1 -> check_dist k (s_hd e) ->
                  dist p Root = k -> d (s_hd e p) <> k ->
                  enabled_b (s_hd e) p = true.

  Lemma act_neut_k_aux:
    forall g p, Proper pequiv g ->
                ~ p == Root ->
                check_dist (dist p Root) g ->
                dist p Root = Dist_p (D :: map S (dist_Neigh g p)).

  Lemma act_neut_k:
    forall g e p, Assume g -> Step (s_hd e) g ->
                  ~ p == Root ->
                  check_dist (dist p Root) g ->
                  act_neut_b (s_cons g e) p = true ->
                  d (s_hd e p) = dist p Root.

  Lemma BFS_round_induction_case_ka:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)) k,
      k >= 1 ->
      check_dist k (s_hd e) ->
      forall p, dist p Root < S k ->
                at_most_rounds
                  (Always (fun c: Exec => d (s_hd c p) = dist p Root)) 1 e.

  Lemma node_remains_ge_Sk:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall k p, k >= 1 -> check_dist k (s_hd e) ->
                  dist p Root >= S k -> d (s_hd e p) >= S k ->
                  Always (fun c => d (s_hd c p) >= S k) e.

  Lemma lt_Sk_enabled:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall k p, k >= 1 -> check_dist k (s_hd e) ->
                  dist p Root >= S k -> d (s_hd e p) < S k ->
                  enabled_b (s_hd e) p = true.

  Lemma act_neut_ge_Sk_aux:
    forall g k p, Proper pequiv g ->
                  dist p Root >= S k ->
                  check_dist k g ->
                  Dist_p (D :: map S (dist_Neigh g p)) >= S k.

  Lemma act_neut_ge_Sk:
    forall g e k p, Assume g -> Step (s_hd e) g ->
                    dist p Root >= S k ->
                    check_dist k g ->
                    act_neut_b (s_cons g e) p = true ->
                    d (s_hd e p) >= S k.
  Lemma BFS_round_induction_case_kb:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)) k,
      k >= 1 ->
      check_dist k (s_hd e) ->
      forall p, dist p Root >= S k ->
                at_most_rounds (Always (fun c => CD2 (S k) p (s_hd c))) 1 e.
  Lemma BFS_round_induction_case_k:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)) k,
      k >= 1 ->
      check_dist k (s_hd e) ->
      at_most_rounds (Always (fun c => check_dist (S k) (s_hd c))) 1 e.

  Lemma not_check_dist_en:
    forall k g, Assume g -> Proper pequiv g ->
                ~ check_dist k g -> ~ terminal g.

  Lemma BFS_round_ind_ccl:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      at_most_rounds
        (fun c: Exec => forall p, d (s_hd c p) = dist p Root) (Diam + 1) e.

  Theorem BFS_rounds_CD:
    Round_complexity (fun e => is_exec e /\ Assume (s_hd e))
                     (fun e =>
                        forall p, d (s_hd e p) = dist p Root
                     )
                     (Diam + 1).

  Lemma check_dist_Diam_disabled_CD:
    forall g, Proper pequiv g -> Assume g ->
              check_dist (S Diam) g ->
              forall p,
                ~ p == Root ->
                d (g p) = Dist_p (map S (dist_Neigh g p)).

  Lemma check_dist_Diam_disabled_CD':
    forall g, Proper pequiv g -> Assume g ->
              check_dist (S Diam) g ->
              forall p,
                ~ p == Root ->
                d (g p) = Dist_p (D :: map S (dist_Neigh g p)).

  Lemma check_dist_Diam_d_unchanged:
    forall g, Proper pequiv g -> Assume g ->
              check_dist (S Diam) g ->
              forall p, d (g p) = d (RUN g p).

  Lemma check_dist_Diam_d_unchanged':
    forall g' g, Step g' g -> Assume g ->
                 check_dist (S Diam) g ->
                 forall p, d (g p) = d (g' p).

  Lemma disabled_non_Root:
    forall g,
      Proper pequiv g -> Assume g ->
      forall p,
        ~ p == Root ->
        d (g p) <= D ->
        G p (Par g p) ->
        d (g p) = S (d (g (Par g p))) ->
        (forall q : Node, G p q -> d (g p) <= S (d (g q)))
        -> enabled_b g p = false.

  Lemma check_dist_Diam_Par_OK:
    forall g p, Assume g -> Proper pequiv g -> ~ p == Root ->
                check_dist (S Diam) g ->
                d (g p) = S (d (g (Par' (RUN g p) p))) /\
                G p (Par' (RUN g p) p).

  Lemma check_dist_Diam_step_disabled:
    forall g e p, Assume g -> Step (s_hd e) g ->
                  check_dist (S Diam) g ->
                  (enabled_b g p = false \/
                   act_neut_b (s_cons g e) p = true) ->
                  enabled_b (s_hd e) p = false.
  Lemma node_remains_disabled:
    forall e,
      is_exec e -> Assume (s_hd e) ->
      forall p, check_dist (S Diam) (s_hd e) ->
                enabled_b (s_hd e) p = false ->
                Always (fun c => enabled_b (s_hd c) p = false) e.

  Lemma last_round_action_CP:
    forall e (ise: is_exec e) (ass: Assume (s_hd e)),
      (forall p, d ((s_hd e) p) = dist p Root) ->
      at_most_rounds (fun c => terminal (s_hd c)) 1 e.
  Lemma Par_Rel_dec:
    forall g, forall x y, {Par_Rel g x y} + {~ Par_Rel g x y}.

  Lemma G_channel_dec:
    forall p q,
      {exists c, is_channel p c q} +
      {~ (exists c, is_channel p c q)}.

  Lemma BFS_rounds_terminal:
    Round_complexity (fun e => is_exec e /\ Assume (s_hd e))
                     (fun e => terminal (s_hd e))
                     (Diam + 2).

  Theorem BFS_rounds:
    Round_complexity (fun e => is_exec e /\ Assume (s_hd e))
                     (fun e =>
                        (BFS_Spanning_Tree_spec (Net := Net))
                          Root Par_Rel (s_hd e))
                     (Diam + 2).
End BFS_rounds.

Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.