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

From Padec Require Import SetoidUtil.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.
From Padec Require Import OptionUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Count.
From Padec Require Import Graph_Diameter.
From Padec Require Import Tree_topology_ALT.
From Padec Require Import BFS_algo.

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

Section BFS_Network.

  Context {Chans: Channels}
          {Net: Network}.

  Class BFS_Assume :=
    mkBFS {
        G:relation Node;
        G_compat: Proper pequiv G;
        G_dec: Decider G;
        
        Bidir: forall x y, G x y -> G y x;
        Connected: is_connected G;
        
        Root: Node;

        Diam := compute_diameter'
                  all_nodes_prop G_compat G_dec Root (DA := Node_dec)
      }.

  Context {Graph_assumption: BFS_Assume}.

  Definition Graph_Network_matching: Prop :=
    forall x y, G x y <-> exists c, is_channel x c y.

  Definition Input_matching
             (_root: Node -> bool)
             (_neighbors: Node -> list Channel): Prop :=
    Network_assumption Net _neighbors /\
    (forall x, _root x = true <-> x == Root).

  Global Instance Input_matching_compat: Proper pequiv Input_matching.
  Class BFS_D := mkBFS_D { D: nat; HD: D >= Diam }.

  Context {D_Assumption: BFS_D}.

  #[refine] Global Instance BFS_RO_assumption: Stable_Assumption
                                       (Algo := BFS_algo D)
                                       (Net := Net)
    := {| Assume_RO :=
            (fun ro: Node -> BFSROState =>
               Input_matching
                 (fun n: Node => root (ro n))
                 (fun n: Node => neighbors (ro n))
            )|}.

  Notation dist := (dist G_compat G_dec Connected all_nodes_prop (DA := Node_dec)).
  Lemma D_dist:
    forall p q, dist p q <= D.

End BFS_Network.

Section BFS_common.

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

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

  Definition Input_Assume (g: Env): Prop :=
    Input_matching (fun n => (root (g n))) (fun n => neighbors (g n)).

  Global Instance Input_Assume_compat: Proper pequiv Input_Assume.

  Lemma Input_Assume_Stable:
    forall g' g, Step g' g -> Input_Assume g -> Input_Assume g'.

  Fixpoint Par_ (c: Channel) (p: Node) (l: list Channel): Node :=
    match l with
    | nil => p
    | cc :: ll => if Channel_dec c cc
                  then match peer p c with None => p | Some q => q end
                  else Par_ c p ll
    end.

  Definition Par' (s: BFSState) (p: Node): Node :=
    Par_ (par s) p (neighbors s).

  Definition Par (g: Env) (p: Node): Node := Par' (g p) p.

  Instance Par__compat: Proper pequiv Par_.

  Global Instance Par'_compat: Proper pequiv Par'.

  Global Instance Par_compat: Proper pequiv Par.

  Lemma Par__spec_chan:
    forall c p l, InA equiv c l -> InA equiv c (peers p) ->
                  is_channel p c (Par_ c p l).
  Lemma Par__chan_conv:
    forall c l p q,
      InA equiv c l -> peer p c == Some q -> Par_ c p l == q.

  Lemma Par__None:
    forall c p l, peer p c == None -> Par_ c p l == p.

  Lemma Par__spec:
    forall c p l, InA equiv c l -> InA equiv c (peers p) ->
                  G p (Par_ c p l).

  Lemma Par'_spec_chan:
    forall (s: BFSState) p (ass: equivlistA equiv (neighbors s) (peers p)),
      InA equiv (par s) (peers p) ->
      is_channel p (par s) (Par' s p).

  Lemma Par'_spec:
    forall (s: BFSState) p (ass: equivlistA equiv (neighbors s) (peers p)),
      InA equiv (par s) (peers p) -> G p (Par' s p).

  Lemma Par_spec_chan:
    forall g (ass: Input_Assume g) p,
      InA equiv (par (g p)) (peers p) -> is_channel p (par (g p)) (Par g p).

  Lemma Par_spec:
    forall g (ass: Input_Assume g) p,
      InA equiv (par (g p)) (peers p) -> G p (Par g p).

  Lemma Dist_p_spec:
    forall l, l <> nil ->
              InA equiv (Dist_p l) l /\
              forall a, InA equiv a l -> Dist_p l <= a.

  Lemma Dist_p_spec':
    forall l dd, l <> nil ->
                 dd = Dist_p l <->
                 InA equiv dd l /\
                 forall a, InA equiv a l -> dd <= a.

  Lemma Dist_p_alone:
    forall a l, Dist_p (a :: l) = a -> ~ InA equiv a l ->
                forall x, InA equiv x l -> x > a.

  Lemma Dist_p_cons:
    forall a l x, Dist_p (a :: l) = x -> a = x \/ InA equiv x l.

  Lemma Dist_p_conv:
    forall a l x, Dist_p (a :: l) = x -> InA equiv x l ->
                  l <> nil -> Dist_p l = x.

  Lemma Dist_p_ge:
    forall l a, l <> nil ->
                (forall x, InA equiv x l -> x >= a)
                -> Dist_p l >= a.

  Notation neigh g p := (neighbor_list (g p) (local_env g p)).

  Lemma RUN_unfold:
    forall (g: Env) (p: Node),
      RUN g p =
      (if root (g p)
       then simple_run_Root (g p)
       else
         if
           Nat.eq_dec (d (g p)) (Dist_p (D :: (map S (map snd (neigh g p)))))
         then
           if Nat.eq_dec (d (g p)) (Dist_p (map S (map snd (neigh g p))))
           then
             if
               Nat.eq_dec (d (g p))
                          (S match local_env g p (par (g p)) with
                             | Some s => d s | None => d (g p) end)
             then
               {| d := d (g p); par := par (g p); BFSROpart := g p |}
             else
               {| d := d (g p);
                  par := Par_dist (d (g p)) (par (g p)) (neigh g p);
                  BFSROpart := g p |}
           else
             {| d := d (g p); par := par (g p); BFSROpart := g p |}
         else
           {| d := Dist_p (D :: (map S (map snd (neigh g p))));
              par := par (g p); BFSROpart := g p |}).

  Lemma RUN_le_D: forall (g: Env) (p: Node), d (RUN g p) <= D.

  Lemma RUN_root:
    forall g: Env, Input_Assume g -> d (RUN g Root) = 0.

  Lemma neighbor_list_prop:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p c dd,
      InA equiv (c, dd) (neigh g p) <->
      exists q, is_channel p c q /\ dd = d (g q).

  Lemma neighbor_list_proj:
    forall s l (l_compat: Proper pequiv l)
           c n, InA equiv (c, n) (neighbor_list s l) ->
                InA equiv c (neighbors s).

  Lemma get_neigh: forall p r, ~ p == r -> exists q, G p q.

  Lemma has_neigh':
    forall p r, ~ p == r -> exists c q, is_channel p c q.

  Lemma technical_neigh:
    forall p q (g: Env), Proper pequiv g ->
                         Input_Assume g -> ~ p == q ->
                         map S (map snd (neigh g p)) <> nil.

  Definition Neigh p: list Node :=
    filter (fun q => if G_dec p q then true else false) all_nodes.

  Global Instance Neigh_compat: Proper pequiv Neigh.

  Lemma Neigh_spec (p: Node):
    forall q, InA equiv q (Neigh p) <-> G p q.
  Lemma Neigh_not_nil: forall p, ~ p == Root -> Neigh p <> nil.

  Definition dist_Neigh g p := (map (fun q => d (g q)) (Neigh p)).

  Lemma dist_Neigh_spec:
    forall g (pg: Proper pequiv g) p x,
      InA equiv x (dist_Neigh g p) <->
      exists q, G p q /\ d (g q) = x.
  Lemma Sdist_Neigh_spec:
    forall g (pg: Proper pequiv g) p x,
      InA equiv x (map S (dist_Neigh g p)) <->
      exists q, G p q /\ S (d (g q)) = x.

  Global Instance min_list_compat_equivlist:
    Proper (equivlistA equiv ==> eq) min_list.
  Global Instance Dist_p_compat_equivlist:
    Proper (equivlistA equiv ==> eq) Dist_p.

  Lemma Dist_p1:
    forall g (ass: Input_Assume g) (pg: Proper pequiv g) p,
      Dist_p (D :: map S (map snd (neigh g p))) =
      Dist_p (D :: map S (dist_Neigh g p)).

  Lemma Dist_p2:
    forall g (ass: Input_Assume g) (pg: Proper pequiv g) p,
      Dist_p (map S (map snd (neigh g p))) =
      Dist_p (map S (dist_Neigh g p)).

  Lemma technical_not_nil:
    forall g p, ~ p == Root -> map S (dist_Neigh g p) <> nil.

  Lemma DistOK:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p dd,
      ~ p == Root ->
      Dist_p (map S (dist_Neigh g p)) = dd ->
      (exists q, G p q /\ S (d (g q)) = dd) /\
      forall q, G p q -> S (d (g q)) >= dd.
  Lemma Dist_p_split:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p,
      ~ p == Root ->
      Dist_p (D :: map S (dist_Neigh g p)) = D /\
      (forall q, G p q -> S (d (g q)) > D)
      \/
      Dist_p (D :: map S (dist_Neigh g p)) = Dist_p (map S (dist_Neigh g p)).

  Lemma RUN_CD0:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p (hr: ~ p == Root),
      d (RUN g p) = Dist_p (D :: map S (dist_Neigh g p)).

  Lemma RUN_CD1:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p (hr: ~ p == Root),
      d (RUN g p) <> Dist_p (map S (dist_Neigh g p)) ->
      d (RUN g p) = D /\ forall q, G p q -> S (d (g q)) > D.

  Lemma RUN_CD2:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p (hr: ~ p == Root),
      d (RUN g p) = Dist_p (map S (dist_Neigh g p)) ->
      (exists q, G p q /\ S (d (g q)) = d (RUN g p)) /\
      forall q, G p q -> S (d (g q)) >= d (RUN g p).

  Lemma filter_cons:
    forall A (f: A -> bool) a l,
      filter f (a :: l) = if f a then a :: filter f l
                          else filter f l.

  Lemma Par_dist_prop:
    forall l pd dum,
      (exists c n, InA equiv (c, n) l /\ S n = pd) ->
      exists nn, InA equiv (Par_dist pd dum l, nn) l /\ S nn = pd.

  Lemma RUN_CP:
    forall (g: Env) (ass: Input_Assume g) (pg: Proper pequiv g)
           p, ~ p == Root ->
              d (g p) = Dist_p (D :: map S (dist_Neigh g p)) ->
              d (g p) = Dist_p (map S (dist_Neigh g p)) ->
              G p (Par' (RUN g p) p) /\
              d (g p) = S (d (g (Par' (RUN g p) p))).

  Lemma disabled_root:
    forall g: Env, Input_Assume g ->
                   enabled_b g Root = false <-> d (g Root) = 0.

  Lemma enabled_root:
    forall g: Env,
      Input_Assume g ->
      enabled_b g Root = true <-> d (g Root) <> 0.

  Lemma disabled_non_root':
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        enabled_b g p = false ->
        d (g p) = Dist_p (D :: (map S (dist_Neigh g p))) /\
        ( d (g p) = Dist_p (map S (dist_Neigh g p)) ->
          d (g p) = S (d (g (Par g p))) ).

  Lemma disabled_non_root_CP:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        enabled_b g p = false ->
        d (g p) = Dist_p (map S (dist_Neigh g p)) ->
        (d (g p) <= D /\ G p (Par g p) /\
         d (g p) = S (d (g (Par g p))) /\
         forall q, G p q -> d (g p) <= S (d (g q))).

  Lemma disabled_non_root:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        enabled_b g p = false ->
        (d (g p) = D /\ forall q, G p q -> S (d (g q)) > D)
        \/
        (d (g p) <= D /\ G p (Par g p) /\
         d (g p) = S (d (g (Par g p))) /\
         forall q, G p q -> d (g p) <= S (d (g q))).

  Lemma enabled_non_root':
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        enabled_b g p = true ->
        d (g p) <> Dist_p (D :: (map S (dist_Neigh g p)))
        \/
        ( d (g p) = Dist_p (map S (dist_Neigh g p)) /\
          d (g p) <> S (d (g (Par g p))) ).

  Lemma enabled_non_root:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        enabled_b g p = true ->
        ( InA equiv (d (g p)) (D :: map S (dist_Neigh g p))
          -> d (g p) > D \/ exists q, G p q /\ d (g p) > S (d (g q)) )
        \/
        ( d (g p) = Dist_p (map S (dist_Neigh g p))
          /\ d (g p) <> S (d (g (Par g p))) ).
  Lemma enabled_non_root_CD1:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        ~ InA equiv (d (g p)) (D :: map S (dist_Neigh g p))
        -> enabled_b g p = true.

  Lemma enabled_non_root_CD2:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        d (g p) > D \/ (exists q, G p q /\ d (g p) > S (d (g q)))
        -> enabled_b g p = true.

  Lemma enabled_non_root_CP:
    forall p, ~ p == Root -> forall g: Env,
        Input_Assume g -> Proper pequiv g ->
        d (g p) = Dist_p (map S (dist_Neigh g p))
        -> d (g p) <> S (d (g (Par g p)))
        -> enabled_b g p = true.

  Lemma step_Root:
    forall (g g': Env),
      Input_Assume g ->
      Step g' g -> has_moved_b g' g Root = true ->
      d (g' Root) = 0.

  Lemma step_CD0:
    forall (g g': Env) (ass: Input_Assume g) (st: Step g' g)
           p, ~ p == Root -> has_moved_b g' g p = true ->
              d (g' p) = Dist_p (D :: map S (dist_Neigh g p)).

  Lemma step_CD1:
    forall (g g': Env) (ass: Input_Assume g) (st: Step g' g)
           p, ~ p == Root -> has_moved_b g' g p = true ->
              d (g' p) <> Dist_p (map S (dist_Neigh g p)) ->
              d (g' p) = D /\
              forall q, G p q -> S (d (g q)) > D.

  Lemma step_CD2:
    forall (g g': Env) (ass: Input_Assume g) (st: Step g' g)
           p, ~ p == Root -> has_moved_b g' g p = true ->
              d (g' p) = Dist_p (map S (dist_Neigh g p)) ->
              (exists q, G p q /\ S (d (g q)) = d (g' p)) /\
              (forall q, G p q -> S (d (g q)) >= d (g' p)).

  Lemma step_CP:
    forall (g g': Env) (ass: Input_Assume g) (st: Step g' g)
           p, ~ p == Root -> has_moved_b g' g p = true ->
              d (g p) = Dist_p (D :: map S (dist_Neigh g p)) ->
              d (g p) = Dist_p (map S (dist_Neigh g p)) ->
              G p (Par g' p) /\
              d (g p) = S (d (g (Par g' p))).

  Definition Par_Rel (gg: Env): relation Node :=
    (fun n n' => if Node_dec n Root then False else
                   Par gg n == n').

  Global Instance Par_Rel_compat: Proper pequiv Par_Rel.

  Lemma Par_Rel_is_root: forall g, is_root (Par_Rel g) Root.

End BFS_common.

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