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

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import P_Q_Termination.
From Padec Require Import Count.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import KDomSet_specification.
From Padec Require Import KDomSet_common.
From Padec Require Import KDomSet_alpha.
From Padec Require Import KDomSet_correctness.
From Padec Require Import KDomSet_termination.
From Padec Require Import KDomSet_count.
From Padec Require Import Graph_Diameter.
From Padec Require Import Tree_topology_ALT.
From Padec Require Import ZUtils.

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

Section KDomSet_Specification_Proved.

  Context {Chans: Channels}
          {Net: Network}
          {KDP: KDomSet_parameters}
          {Graph_assumption: KDomSet_Assume}
          {Graph_network_assumption: Graph_Network_matching}.
  Let k_pos := k_pos.

  Existing Instance T_compat.
  Notation Algo := (KDomSet_algo k).
  Notation Env := (Env (Net := Net) (Algo := Algo)).

  Notation alpha_part := (fun (g: Env) n => alpha (g n)).
  Instance alpha_part_compat: Proper fequiv alpha_part.

  Lemma newAlpha_link:
    forall (g: Env) n,
      Assume g -> Proper pequiv g ->
      NewAlpha k (alpha_list (g n) (local_env g n)) =
      NewAlpha k (lcA (fun n0 => alpha (g n0)) n).

  Section Correctness.

    Lemma final:
      forall (g: Env),
        Assume g -> terminal g ->
        forall n: Node, ~ enabled_alpha (alpha_part g) n.

    Lemma final_alt:
      forall (g: Env),
        Assume g -> terminal g ->
        forall n: Node, alpha (g n) = NewAlpha k (lcA (alpha_part g) n).

    Definition kDominator_ (g: Env) (n: Node): Prop :=
      kDominator (alpha_part g) n.

    Theorem kdom_set_at_terminal:
      forall (g: Env),
        Assume g -> terminal g -> (kDOM kDominator_ g).

    Lemma kDOM_partial_correctness:
      P_correctness KDomSet_RO_assumption (kDOM kDominator_).

  End Correctness.

  Section Termination.

    Theorem k_dom_set_terminates:
      forall (g: Env), Assume g -> Acc Step g.

    Lemma kDOM_termination: termination KDomSet_RO_assumption.

  End Termination.

  Section Silent_Self_Stabilization.

    Theorem kdom_silent_self_stabilization:
      silence KDomSet_RO_assumption unfair_daemon /\
      self_stabilization KDomSet_RO_assumption
                         unfair_daemon (only_one (kDOM kDominator_)).

  End Silent_Self_Stabilization.

  Section Counting.

    Definition Dominators (g: Env) := { n: Node | kDominator_ g n }.

    Theorem counting:
      forall (g: Env),
        Assume g -> terminal g ->
        exists N D: nat,
          Num_Card Same Node N /\ Num_Card Same (Dominators g) D /\
          (N - 1 >= S (Z.to_nat k) * (D - 1))%nat.
  End Counting.

End KDomSet_Specification_Proved.

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