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

From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import ListUtils.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import KDomSet_alpha.
From Padec Require Import KDomSet_specification.
From Padec Require Import Tree_topology_ALT.
From Padec Require Import FoldRight.


Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Section KDom_Network.

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

  Class KDomSet_Assume :=
    mkKDom {
        G: relation Node;
        T: relation Node;
        T_compat: Proper pequiv T;
        T_dec: Decider T;

        Root: Node;
        Tree: is_tree (flip T) Root;
        Spanning: is_spanning_tree (flip T) G Root
      }.

  Context {Graph_assumption: KDomSet_Assume}.
  Existing Instance T_compat.

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

  Definition Input_matching
             (_children: Node -> list Channel): Prop :=
    Network_assumption Net _children.

  Global Instance Input_matching_compat:
    Proper ((equiv ==> equivlistA equiv) ==> equiv) Input_matching.

  Instance flip_T_compat: Proper pequiv (flip T).

  Lemma flip_T_dec: Decider (flip T).

  Instance is_root_flip_compat: Proper pequiv (is_root (flip T)).

  Lemma is_root_Root: is_root (flip T) Root.

  Lemma is_root_Root': forall p, p == Root <-> is_root (flip T) p.

End KDom_Network.

Section KDomSet_common.

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

  Context {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.
  Context {Graph_assumption: KDomSet_Assume}
          {Graph_network_assumption: Graph_Network_matching}.
  Existing Instance T_compat.

#[refine] Global Instance KDomSet_RO_assumption:
    Stable_Assumption (Algo := KDomSet_algo k)
                      (Net := Net)
    := {| Assume_RO :=
            (fun ro: Node -> KDomROState =>
               Input_matching (fun n: Node => _children (ro n))
            )|}.

  Section Range_of_alpha.

    Lemma new_alpha_0_2k:
      forall ca, 0 <= NewAlpha k ca <= 2*k.

  End Range_of_alpha.

  Section Children_Access.

    Variable (alpha: Node -> Z)
             (alpha_compat: Proper fequiv alpha).

    Definition lcA: Node -> list Z :=
      fun p: Node =>
        map alpha
            (filter (fun q => if T_dec p q then true else false) all_nodes).

    Lemma InA_Children:
      forall x p, InA equiv x (lcA p) <-> exists q, T p q /\ x = alpha q.
  End Children_Access.

  Instance lcA_compat: Proper (fequiv ==> equiv ==> equivlistA equiv) lcA.

  Definition kDominator (alpha: Node -> Z) (p: Node) :=
    alpha p = k \/ alpha p < k /\ p == Root.

  Global Instance kDominator_compat: Proper fequiv kDominator.

  Lemma kDominator_dec:
    forall alpha p, {kDominator alpha p} + {~kDominator alpha p}.

  Definition enabled_alpha alpha n: Prop :=
    alpha n <> NewAlpha k (lcA alpha n).

  Global Instance enabled_alpha_compat: Proper fequiv enabled_alpha.

  Section KDom_Graph.

    Definition is_kDom_edge (alpha: Node -> Z)
               (x y: Node): Prop :=
      match alpha y ?= k with
      | Lt => T x y
      | Eq => False
      | Gt => T y x /\ alpha x = alpha y - 1
      end.

    Global Instance is_kDom_edge_compat: Proper fequiv is_kDom_edge.

  End KDom_Graph.

End KDomSet_common.
Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.