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 Coq Require Import Inclusion.
From Coq Require Import RelationPairs.

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 Spanning_Tree.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_def_termination.
From Padec Require Import KClustering_alpha_termination.
From Padec Require Import P_Q_Termination.

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

Section KClustering_Pcl_Termination.

  Context {Chans: Channels} {Net: Symmetric_Network}
          {KCP: KClustering_parameters} {KCT: KC_algo_tools}.

  Existing Instance KC_Stable.

  Notation Env := (Env (Algo := KC_algo)).

  Let k_pos := k_pos.

  Variable (root: Node).

  Definition pcl_potential (sg: sig (Pspanning_tree root)) (n: Node): nat :=
    if pcl_enabled_bb (proj1_sig sg) n then 1%nat else 0%nat.

  Global Instance pcl_potential_compat: Proper fequiv pcl_potential.

  Section With_Pcl_Step.

    Variable (g g': Env)
             (pg: Proper pequiv g) (pg': Proper pequiv g')
             (step: Step g' g)
             (pcl_step: pcl_step_b g' g = true)
             (span_tree: spanning_tree root (Par_part g) /\
                         Symmetric_Network_assumption
                           Net (fun n => KCpeers (g n))
                           (fun n => KCreverse (g n)))
             (span_tree': spanning_tree root (Par_part g') /\
                          Symmetric_Network_assumption
                            Net (fun n => KCpeers (g' n))
                            (fun n => KCreverse (g' n))).

    Lemma pcl_no_alpha_enabled_when_move:
      forall n, has_moved_b g' g n = true -> alpha_enabled_bb g n = false.

    Lemma exists_pcl_move:
      exists n, has_moved_b g' g n = true /\ pcl_enabled_bb g n = true.

    Lemma pcl_alpha_unchanged:
      forall n, alpha (g n) = alpha (g' n).

    Lemma pcl_NewParCl_unchanged_:
      (forall n, alpha (g n) = alpha (g' n)) ->
      forall n,
        NewparCl (g n) (local_env g n) == NewparCl (g' n) (local_env g' n).

    Lemma pcl_NewParCl_unchanged:
      forall n,
        NewparCl (g n) (local_env g n) == NewparCl (g' n) (local_env g' n).

    Lemma alpha_enabled_unchanged_pcl:
      forall n, alpha_enabled_bb g n = alpha_enabled_bb g' n.

    Lemma pcl_becomes_disabled:
      forall n, pcl_enabled_bb g n = true
                -> has_moved_b g' g n = true
                -> pcl_enabled_bb g' n = false.

    Lemma pcl_no_move:
      forall n, pcl_enabled_bb g n = false -> parCl (g' n) == parCl (g n).

    Lemma pcl_stays_disabled:
      forall n, pcl_enabled_bb g n = false -> pcl_enabled_bb g' n = false.

  End With_Pcl_Step.

  Section Pcl_Termination_Criteria.

    Variable (sg sg': sig (Pspanning_tree root))
             (step: Pcl_SafeStep sg' sg).

    Lemma Pcl_step_b: pcl_step_b (proj1_sig sg') (proj1_sig sg) = true.
    Lemma Pcl_step: Step (proj1_sig sg') (proj1_sig sg).

    Lemma global_pcl_criterium:
      exists n, pcl_potential sg n <> pcl_potential sg' n.

    Lemma local_pcl_criterium:
      forall n,
        (pcl_potential sg n) <> (pcl_potential sg' n) ->
        gt (pcl_potential sg n) (pcl_potential sg' n).

  End Pcl_Termination_Criteria.

  Section Pcl_Termination.

    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation Pot_pcl := (Pot pcl_potential).

    Lemma pcl_safe_inclusion:
      inclusion (Pcl_SafeStep (root := root)) (ltM @@ Pot_pcl).

  End Pcl_Termination.

End KClustering_Pcl_Termination.

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