Coq Library
PADEC - Coq Library

Library Padec.Model.NatBuild

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Imports

From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Lt.
From Coq Require Import NArith.
From Coq Require Import Omega.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.

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

Build a network given as adjacency lists; nodes are numbers from

0 up to N
Connections are given as a list of lists of option ltk: - channel is rank of peers in peer list - reply_to: - find peer: if None return 0 else - find self in peer's peers: return index if found 0 if not found
Section make_net.

  Variable (matrix: list (list N)).
  Definition K := match length matrix with O => 1%N | n => N.of_nat n end.

  Lemma Kpos: (0<K)%N.

  Definition node_matrix :=
    map (map_filter (ltK_inj K)) matrix.

  Fixpoint channel_error n (l: list (ltK K)) i:=
    match l with
      nil => None
    | n'::q => if (N.eq_dec n (proj1_sig n')) then Some i
               else channel_error n q (S i)

  Lemma channel_error_prop: forall n l i,
      channel_error (proj1_sig n) (l: list (ltK K)) 0 == Some i ->
      nth_error l i == Some n.

  Definition row (n: N) :=
    nth (N.to_nat n) node_matrix nil.

  Definition peer_ (n: N) (c:nat) :=
    let l := row n in
    match nth_error l c with
      Some n' =>
      if (N.eq_dec n (proj1_sig n')) then None else
        match channel_error (proj1_sig n') l 0 with
          Some c' =>if (Nat.eq_dec c c') then Some n' else None
        | None => None end
    | None => None

  Lemma peer_prop: forall n c n',
    peer_ n c == Some n' ->
      nth_error (row n) c == Some n' /\
      channel_error (proj1_sig n') (row n) 0 == Some c /\
      ~ n == (proj1_sig n').

  Definition link_ (n: N) (n': N) :=
    if N.eq_dec n' n then None else channel_error n' (row n) 0.

  Definition peers_ n l :=
      (fun n' => if N.eq_dec (proj1_sig n') n then None else
                   channel_error (proj1_sig n') l 0) l.

  Definition reply_to_ n c:=
    match peer_ n c with
      None => 0
    | Some n' =>
      match channel_error n (row (proj1_sig n')) 0 with
        None => 0
      | Some c' => c'
      end end.

  Instance Chans: Channels := {| Channel := nat; Channel_dec := Nat.eq_dec |}.

  Program Definition Net: Network (Chans:=Chans) :=
      Node := ltK K;
      Node_dec := ltK_dec (K := K);
      all_nodes:=Kenum K;
      all_nodes_prop := ltK_in_Kenum (K := K)
End make_net.

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