Coq Library
Tools

#### Global imports

From Coq Require Import Arith.
From Coq Require Import NArith.
From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Morphisms.
From Coq Require Import List.
From Coq Require Import Omega.

#### Local imports

Open Scope signature_scope.
Open Scope nat_scope.
Set Implicit Arguments.

Section Decr_Generic_Net.

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

# (Very Simple) Example

The state of the nodes are natural numbers.
This algorithm does not use neighborhood: At each step, the node decreases its state.

Program Instance Decr: Algorithm :=
{|
State_setoid := Setoid_nat;
State_dec := eq_nat_dec;
run := fun n _ => pred n;

|}.

End Decr_Generic_Net.

Section Decr.

Nodes are also natural numbers, labeled from 0 to K-1.
Context {Chans:Channels}.

Variable K: N.

The network is made of K nodes, with no edge.
Program Instance NetK: Network:=
{| Node_dec := ltK_dec (K := K);
peer := fun _ _ => None;
link := fun _ _ => None;
all_nodes := Kenum K
|}.

Configurations
Notation env := (@Env _ NetK Decr).

Terminal Configuration to reach
Definition target (g: env ) := forall n , g n = 0.

target is indeed a terminal configuration, i.e. no more valid step can be executed from it.
Theorem final: forall e, target e <-> terminal e.

Potential is defined as the sum of the states on all nodes.
Definition potential g :=
List.fold_right plus 0 (List.map g (@all_nodes _ NetK)).

Any valid step decreases the global potential
Theorem potential_decreases:
forall (g g': env), Step g' g -> potential g' < potential g.

Steps of this algorithm on this network are well founded
Lemma WF_decr: well_founded (@Step _ NetK Decr).

Program Instance Null_Assumption: Stable_Assumption (Algo:= Decr) :=
{|
getRO:= fun _ => tt;
Assume_RO:= fun _ => True;
|}.

Lemma SS_decr:
self_stabilization Null_Assumption unfair_daemon
(fun e => target (Stream.s_hd e)).

End Decr.

Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.