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 WellfoundedUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Spanning_Tree.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_def_termination.
From Padec Require Import KClustering_hd_termination.
From Padec Require Import KClustering_correctness_alpha.

Open Scope Z_scope.
Set Implicit Arguments.

Section KClustering_Correctness.

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

  Existing Instance KC_Stable.
  Existing Instance OrdChans.

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

  Let k_pos := k_pos.

  Definition clusterHeadID (s: State): IdNode := (hd s).
  Definition clusterParent (s: State): option Channel := (parCl s).
  Definition kCluster (g: Env) (h: Node) (n: Node): Prop :=
    id (g h) == clusterHeadID (g n).
  Notation clusterHead g h := (kCluster g h h).
  Notation is_cluster_parent := (is_cluster_parent clusterParent).

  Instance clusterHeadID_compat: Proper fequiv clusterHeadID.

  Instance clusterParent_compat: Proper fequiv clusterParent.

  Instance kCluster_compat: Proper fequiv kCluster.

  Section With_Terminal.

    Variable (g: Env) (term: terminal g).

    Lemma state:
      forall n,
        alpha (g n) = NewAlpha (g n) (local_env g n) /\
        parCl (g n) == NewparCl (g n) (local_env g n) /\
        hd (g n) == NewHead (g n) (local_env g n).

    Variable (root: Node)
             (span: spanning_tree root (Par_part g))
             (sym: Symmetric_Network_assumption
                     Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n)))
             (uniqueID: forall n1 n2, id (g n1) == id (g n2) -> n1 == n2).

    Instance is_cluster_parent_compat: Proper fequiv is_cluster_parent.

    Lemma inclu:
      inclusion (is_cluster_parent g) (is_kDom_edge g).

    Lemma is_cluster_parent_wf:
      well_founded (is_cluster_parent g).

    Notation cluster_path := (cluster_path clusterParent g).
    Instance cluster_path_compat: Proper fequiv cluster_path.

    Notation cluster_path_ :=
      (agreed_cluster_path clusterHeadID clusterParent g).

    Instance cluster_path__compat: Proper fequiv cluster_path_.

    Lemma ok_length:
      forall p b e, cluster_path_ b p e -> Z_of_nat (length p ) <= k.

    Lemma same_hd:
      forall p b e, cluster_path b p e -> (hd (g b)) == (hd (g e)).

    Lemma chain_TC:
      forall (p: list Node), p <> nil ->
                             forall (x y: Node),
                               cluster_path x p y ->
                               transitive_closure (is_cluster_parent g) x y.

    Lemma minidminatall_not_none:
      forall p, alpha (g p) > k ->
                exists c pp, Some c == MinIDMinATall (g p) (local_env g p) /\
                             peer p c == Some pp.

    Lemma non_pcl_self_head:
      forall p, parCl (g p) == None -> id (g p) == hd (g p).

    Lemma diff_id_in_cluster_path:
      forall p b e, cluster_path b p e
                    -> p <> nil -> ~ (id (g b)) == (id (g e)).

    Lemma parCl_is_a_node:
      forall p c, parCl (g p) = Some c -> exists pp, (peer p c) == (Some pp).

    Lemma hd_id_same:
      forall n, (parCl (g n)) == None <-> (id (g n)) == (hd (g n)).

    Lemma pcl_not_none:
      forall p, kDominator g p = true <-> (parCl (g p)) == None.

    Lemma clusterHead_is_kDominator:
      forall (n: Node), kDominator g n = true <-> clusterHead g n.


    Definition get_cluster_parent (n: Node): option Node :=
      match (parCl (g n)) with
      | None => None
      | Some c => (peer n c)
      end.

    Instance get_cluster_parent_compat: Proper fequiv get_cluster_parent.
    Definition is_cp x y := (Some x) == (get_cluster_parent y).

    Lemma is_cp_equiv:
      forall x y, is_cp x y <-> (is_cluster_parent g) x y.

    Instance is_cp_compat: Proper fequiv is_cp.

    Lemma is_cp_wf: well_founded is_cp.

    Definition build_cluster_path (n: Node)
               (W: Acc is_cp n): list Node :=
      @Fix_F Node is_cp (fun _ => list Node)
             (fun (x : Node)
                  (f_rec : forall y : Node, is_cp y x -> list Node) =>
                (match get_cluster_parent x as x0
                       return (x0 == get_cluster_parent x -> list Node)
                 with
                 | Some px => fun heq => (f_rec px heq)
                 | None => fun _ => nil
                 end (Equivalence_Reflexive (get_cluster_parent x)))
                  ++ x::nil) n W.

    Definition build_cp (n: Node): list Node :=
      build_cluster_path (is_cp_wf n).

    Instance build_cp_compat: Proper (equiv ==> eqlistA equiv) build_cp.

    Lemma build_cp_is_cluster_path:
      forall n,
        match (build_cp n) with
        | nil => False
        | hd::tl => cluster_path hd tl n
        end.

    Lemma build_cp_head:
      forall n,
        match (build_cp n) with
        | nil => False
        | hd::_ => clusterHead g hd
        end.

    Lemma build_cp_head_id:
      forall b e,
        kCluster g b e ->
        match (build_cp e) with
        | nil => False
        | hdd::_ => hdd == b
        end.

    Lemma build_cluster_path_pr:
      forall b e, kCluster g b e ->
                   (exists p, cluster_path b p e) /\ clusterHead g b.

    Lemma clusterHeadID_OK_OK:
      clusterHeadID_OK kCluster id clusterHeadID g.

    Lemma cluster_path'_cluster_path:
      forall b p e, cluster_path b p e <-> cluster_path_ b p e.

    Lemma cluster_path_OK_OK:
      cluster_path_OK kCluster clusterHeadID clusterParent g.

    Lemma kCluster_partition_OK:
      partition_OK kCluster g.

    Lemma kClustering_ID_SPEC_OK:
      kClustering_ID_SPEC kCluster id clusterHeadID clusterParent g.

  End With_Terminal.

End KClustering_Correctness.

Close Scope Z_scope.
Unset Implicit Arguments.