Proof that under casual broadcast deliverable condition, merge and tick are equivalent.

VectorClock.v

Require Import Coq.Init.Nat.
Require Import Coq.Arith.PeanoNat.

(*
   A vector clock [vclock] is a total map from index to clock and is represented
   as a function from natural numbers to natural numbers. For index not in the
   map, the defualt clock is 0.
 *)
Definition vclock : Type := nat -> nat.

Definition empty_vc : vclock := fun _ => 0.

Definition update_vc (vc : vclock) (idx : nat) (clock : nat) : vclock :=
  fun idx' => if idx' =? idx
              then clock
              else vc idx.

Definition get_vc (vc : vclock) (idx : nat) : nat :=
  vc idx.

(*
   [merge] combines two vector clocks into a new one. For each index, the new
   vector clock maps it to the maximum of two vector clocks.
 *)
Definition merge (vc1 vc2 : vclock) : vclock :=
  fun idx => let clock1 := vc1 idx in
             let clock2 := vc2 idx in
             max clock1 clock2.

Theorem merge_rule : forall (vc1 vc2 : vclock) (n : nat),
    get_vc (merge vc1 vc2) n = max (get_vc vc1 n) (get_vc vc2 n).
Proof. intros. unfold merge. unfold get_vc. reflexivity. Qed.

(*
   [tick] increments the clock indexed by [idx] by 1. For each index, the new
   vector clock maps it to the original clock + 1 if the index equals [idx], to
   the original clock otherwise.
 *)
Definition tick (idx : nat) (vc : vclock) : vclock :=
  fun idx' => let clock := vc idx' in
              if idx' =? idx
              then clock + 1
              else clock.

Theorem tick_rule : forall (idx : nat) (vc : vclock) (n : nat),
    get_vc (tick idx vc) n = if n =? idx
                             then (get_vc vc n) + 1
                             else (get_vc vc n).
Proof. intros. unfold tick. unfold get_vc. reflexivity. Qed.

(*
   Two vector clocks are equal if they map each index to the same clock.
 *)
Definition eq_vc (vc1 vc2 : vclock) : Prop :=
  forall (n : nat), get_vc vc1 n = get_vc vc2 n.

(*
   The deliverable condition in casual broadcast. For process with vector clock
   [vcp]. A message with vector clock [vcm] sent from process with index [idx]
   is deliverable if and only if

      forall k : 0..n { VC(m)[k] == VC(p)[k] + 1    if k == idx
                      { VC(m)[k] <= VC(p)[k]        otherwise
 *)
Definition deliverable (idx : nat) (vcp vcm : vclock) : Prop :=
  forall (n : nat), if n =? idx
                    then get_vc vcm n = (get_vc vcp n) + 1
                    else get_vc vcm n <= get_vc vcp n.

(*
   If deliverable condition holds, the two new vector clocks produced by merging
   and ticking the process's local clock in sender's postion are equal.
 *)
Theorem eq_merge_tick_if_deliverable : forall (idx : nat) (vcp vcm : vclock),
    deliverable idx vcp vcm -> eq_vc (merge vcp vcm) (tick idx vcp).
Proof.
  intros. unfold eq_vc. intros.
  rewrite merge_rule. rewrite tick_rule.
  unfold deliverable in H. specialize H with (n := n).
  destruct (n =? idx).
  - rewrite <- H. apply max_r. rewrite H. rewrite Nat.add_1_r.
    apply le_S. apply le_n.
  - apply max_l. apply H.
Qed.