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

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.
From Padec Require Import KDomSet_specification_tree_topology.
From Padec Require Import Self_Stabilization.

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

Section KDomSet_Correctness.

  Context {Chans: Channels}
          {Net: Network}
          {DTN: Down_Tree_Network Net}
          {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Notation Tree := (DTN_topo (Net := Net)).
  Context {SPAN: is_spanning _ Tree}.

  Notation Algo := KDom_algo.
  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).

  Existing Instance KDom_Stable.
  Existing Instance KDom_RO_assumption.

  Notation alphas_ :=
    (fun (env: Env) n => alphas (children_states (env n) (local_env env n))).

  Notation new_alpha_ := (fun env n => new_alpha (alphas_ env n)).

  Section Final_kDomSet.

    Variable (env: Env)
             (env_compat: Proper pequiv env)
             (hassume: Assume env).

    Variable (final: forall (n: Node), enabled_b env n = false).

    Lemma same: forall (n: Node), alpha (env n) = new_alpha_ env n.

    Definition is_kDom_path := chain (is_kDom_edge env).

    Lemma tall_has_path_to_root:
      forall (n: Node) (i: nat),
        alpha (env n) = k + Z_of_nat i ->
        exists (r: Node),
          kDominator env r = true /\
          exists (p: list Node), (is_kDom_path r p n).

    Lemma tall_is_linked:
      forall (n: Node) (i: nat),
        alpha (env n) = k + Z_of_nat i ->
        (exists (r: Node),
          kDominator env r = true /\
          exists (p: list Node), (is_kDom_path r p n)).

    Lemma tall_is_kDominated:
      forall (n: Node) (i: nat),
        alpha (env n) = k + Z_of_nat i ->
        forall r p, is_kDom_path r p n -> (length p <= i)%nat.

    Lemma tall_k:
      forall (n: Node),
        _IsTall (alpha (env n)) = true ->
        exists (i: nat), alpha (env n) = k + Z.of_nat i.

    Lemma short_k:
      forall (n: Node),
        _IsShort (alpha (env n)) = true ->
        exists (i: nat), (Z.of_nat i < k)%Z /\
                         alpha (env n) = k - 1 - Z.of_nat i.

    Lemma alpha_monotonic_small:
      forall (n m: Node),
        isParent m n ->
        _IsShort (alpha (env n)) = true ->
        alpha (env m) >= alpha (env n) + 1.

    Lemma short_is_linked:
      forall (i: nat) (n: Node),
        alpha (env n) = k - Z.of_nat i ->
        (exists (r: Node),
           kDominator env r = true /\
           exists (p: list Node), (is_kDom_path r p n)).

    Lemma short_is_kDominated:
      forall (i: nat) (n: Node),
        alpha (env n) = k - Z.of_nat i ->
        forall r p, is_kDom_path r p n -> (length p <= i)%nat.

    Lemma any_is_linked:
      forall (n: Node), exists (r: Node),
        kDominator env r = true /\
        exists (p: list Node), (is_kDom_path r p n).

    Lemma any_is_kDominated:
      forall (n: Node),
      forall r p, is_kDom_path r p n -> Z.of_nat (length p) <= k.

    Definition IsInkDomSet (k: Z) (root: Node) (n: Node): Prop :=
      kDominator env root = true /\
      exists p, (is_kDom_path root p n) /\ (Z_of_nat (length p) <= k)%Z.

    Lemma any_is_in_kDom_set:
      forall (n: Node), exists (r: Node), IsInkDomSet k r n.

  End Final_kDomSet.

    Section Correctness.

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

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

    Lemma kDOM_partial_correctness:
      P_correctness KDom_RO_assumption (kDOM kDominator_ (k := k)).

  End Correctness.

End KDomSet_Correctness.

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