(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* MACHINE *)

(* Common descriptions for all abstract machines *)

Require Import List.
Require Export fifo.
Require Export table. 
Require Export reduce. 
Require Export sigma2. 

Unset Standard Proposition Elimination Names.

Section MACHINE.

Parameter Site : Set. 
Parameter owner : Site.

 
Axiom eq_site_dec : eq_dec Site. 

Definition change_site (E : Set) := change_x0 Site E eq_site_dec.

Lemma that_site :
 forall (E : Set) (f : Site -> E) (s0 : Site) (x : E),
 change_site E f s0 x s0 = x.
Proof.
(* Goal: forall (E : Set) (f : forall _ : Site, E) (s0 : Site) (x : E), @eq E (change_site E f s0 x s0) x *)
 intros; unfold change_site in |- *; apply here.
Qed.

Lemma other_site :
 forall (E : Set) (f : Site -> E) (s0 s1 : Site) (x : E),
 s0 <> s1 -> change_site E f s0 x s1 = f s1.
Proof.
(* Goal: forall (E : Set) (f : forall _ : Site, E) (s0 s1 : Site) (x : E) (_ : not (@eq Site s0 s1)), @eq E (change_site E f s0 x s1) (f s1) *)
 intros; unfold change_site in |- *; apply elsewhere; trivial.
Qed.

(* les couples de sites correspondent aux files d'attente *)

Definition eq_queue_dec := eq_couple_dec Site Site eq_site_dec eq_site_dec.

Definition change_queue (Q : Set) := update2_table Site eq_site_dec Q.

Lemma that_queue :
 forall (E : Set) (f : Site -> Site -> E) (s0 s1 : Site) (x : E),
 change_queue E f s0 s1 x s0 s1 = x.
Proof.
 intros; unfold change_queue in |- *; unfold update2_table in |- *;
  apply here2.
Qed.

Lemma other_queue :
 forall (E : Set) (f : Site -> Site -> E) (s0 s1 s2 s3 : Site) (x : E),
 s2 <> s0 \/ s3 <> s1 -> change_queue E f s0 s1 x s2 s3 = f s2 s3.
Proof.
 intros; unfold change_queue in |- *; unfold update2_table in |- *;
(* Goal: @eq Message m d *)
(* Goal: forall _ : not (@eq Message m d), sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
  apply elsewhere2; trivial.
Qed.

(* l'ensemble des sites est fini, la liste des sites sert a parcourir
et \`a sommer sur l'ensemble des sites *)

Parameter LS : list Site.

Axiom finite_site : list_of_elements Site eq_site_dec LS.

Lemma in_s_LS : forall s : Site, In s LS.
Proof.
 intros; apply only_once_in with (eq_E_dec := eq_site_dec);
  exact (finite_site s).
Qed.


Variable Data : Set.

Definition Bag_of_Data := Site -> Site -> queue Data.

End MACHINE.




Section M_ACTION.

Variable Message : Set.
Let Bag_of_message := Bag_of_Data Message.

(* This is taken straight from Jean's file *)

Definition Post_message (m0 : Message) (b0 : Bag_of_message)
  (s0 s1 : Site) :=
  change_queue (queue Message) b0 s0 s1 (input Message m0 (b0 s0 s1)).

Definition Collect_message (b0 : Bag_of_message) (s0 s1 : Site) :=
  change_queue (queue Message) b0 s0 s1 (first_out Message (b0 s0 s1)).

Lemma post_here :
 forall (b0 : Bag_of_message) (m0 : Message) (s0 s1 : Site),
 Post_message m0 b0 s0 s1 s0 s1 = input Message m0 (b0 s0 s1).
Proof.
(* Goal: forall (b0 : Bag_of_message) (m0 : Message) (s0 s1 : Site), @eq (queue Message) (Post_message m0 b0 s0 s1 s0 s1) (input Message m0 (b0 s0 s1)) *)
 intros; unfold Post_message in |- *; apply that_queue.
Qed.

Lemma post_elsewhere :
 forall (b0 : Bag_of_message) (m0 : Message) (s0 s1 s2 s3 : Site),
 s0 <> s2 \/ s1 <> s3 -> Post_message m0 b0 s0 s1 s2 s3 = b0 s2 s3.
Proof.
(* Goal: forall (b0 : Bag_of_message) (m0 : Message) (s0 s1 s2 s3 : Site) (_ : or (not (@eq Site s0 s2)) (not (@eq Site s1 s3))), @eq (queue Message) (Post_message m0 b0 s0 s1 s2 s3) (b0 s2 s3) *)
 intros; unfold Post_message in |- *; apply other_queue; elim H; auto.
Qed.

Lemma collect_here :
 forall (b0 : Bag_of_message) (s0 s1 : Site),
 Collect_message b0 s0 s1 s0 s1 = first_out Message (b0 s0 s1).
Proof.
(* Goal: forall (b0 : Bag_of_message) (s0 s1 : Site), @eq (queue Message) (Collect_message b0 s0 s1 s0 s1) (first_out Message (b0 s0 s1)) *)
 intros; unfold Collect_message in |- *; apply that_queue.
Qed.

Lemma collect_elsewhere :
 forall (b0 : Bag_of_message) (s0 s1 s2 s3 : Site),
 s0 <> s2 \/ s1 <> s3 -> Collect_message b0 s0 s1 s2 s3 = b0 s2 s3.
Proof.
(* Goal: forall (b0 : Bag_of_message) (s0 s1 s2 s3 : Site) (_ : or (not (@eq Site s0 s2)) (not (@eq Site s1 s3))), @eq (queue Message) (Collect_message b0 s0 s1 s2 s3) (b0 s2 s3) *)
 intros; unfold Collect_message in |- *; apply other_queue; elim H; auto.
Qed.

End M_ACTION.


Section IN_Q_EFFECT.

Variable Message : Set.
Let Bag_of_message := Bag_of_Data Message.

(* consequence sur l'appartenance *)

Lemma in_post :
 forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site),
 m <> m' ->
 In_queue Message m (Post_message Message m' bom s1 s2 s3 s4) ->
 In_queue Message m (bom s3 s4).
Proof.

(* Goal: forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site) (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
 intros m m' bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro.
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
 decompose [and] a; rewrite H; rewrite H0.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
 rewrite post_here.
(* Goal: forall (_ : not (@eq Message m m')) (_ : In_queue Message m (input Message m' (bom s3 s4))), In_queue Message m (bom s3 s4) *)
(* Goal: forall (_ : not (@eq Message m m')) (_ : In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)), In_queue Message m (bom s3 s4) *)
 intros; apply in_q_input with (d' := m'); trivial.

(* Goal: forall (_ : not (@eq Message m m')) (_ : In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)), In_queue Message m (bom s3 s4) *)
 rewrite post_elsewhere; auto.
Qed.

Lemma not_in_post :
 forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site),
 m <> m' ->
 ~ In_queue Message m (bom s3 s4) ->
 ~ In_queue Message m (Post_message Message m' bom s1 s2 s3 s4).
Proof.
(* Goal: forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site) (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
  intros m m' bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro.
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
  decompose [and] a; rewrite H; rewrite H0.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite post_here.
(* Goal: forall (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (input Message m' (bom s3 s4))) *)
(* Goal: forall (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
  intros H1 H2.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int true)) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  simpl in |- *.
(* Goal: not (or (@eq Message m m') (In_queue Message m (bom s3 s4))) *)
(* Goal: forall (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
  intuition.
(* Goal: forall (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
  intros H H0.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite post_elsewhere.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
Qed.

Lemma not_in_collect :
 forall (m : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site),
 ~ In_queue Message m (bom s3 s4) ->
 ~ In_queue Message m (Collect_message Message bom s1 s2 s3 s4).
Proof.
(* Goal: forall (m : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site) (_ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4)), In_queue Message m (bom s3 s4) *)
  intros m bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro.
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
  decompose [and] a; rewrite H; rewrite H0.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite collect_here.
(* Goal: forall _ : not (In_queue Message m (bom s3 s4)), not (In_queue Message m (first_out Message (bom s3 s4))) *)
(* Goal: forall _ : not (In_queue Message m (bom s3 s4)), not (In_queue Message m (Collect_message Message bom s1 s2 s3 s4)) *)
  intro H1.
(* Goal: not (In_queue Message m (first_out Message (bom s3 s4))) *)
(* Goal: forall _ : not (In_queue Message m (bom s3 s4)), not (In_queue Message m (Collect_message Message bom s1 s2 s3 s4)) *)
  apply not_in_q_output.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
  
(* Goal: forall _ : not (In_queue Message m (bom s3 s4)), not (In_queue Message m (Collect_message Message bom s1 s2 s3 s4)) *)
  intros H1.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite collect_elsewhere.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
  
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
Qed.


Lemma in_collect :
 forall (m : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site),
 In_queue Message m (Collect_message Message bom s1 s2 s3 s4) ->
 In_queue Message m (bom s3 s4).
Proof.
(* Goal: forall (m : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site) (_ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4)), In_queue Message m (bom s3 s4) *)
 intros m bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro.
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
 decompose [and] a; rewrite H; rewrite H0.
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s3 s4 s3 s4), In_queue Message m (bom s3 s4) *)
(* Goal: forall _ : In_queue Message m (Collect_message Message bom s1 s2 s3 s4), In_queue Message m (bom s3 s4) *)
 rewrite collect_here; intros; apply in_q_output; trivial.

(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
 rewrite collect_elsewhere; auto.
Qed.

Hypothesis eq_message_dec : eq_dec Message.

Lemma in_queue_decidable :
 forall (m : Message) (q : queue Message),
 {In_queue Message m q} + {~ In_queue Message m q}.
Proof.
(* Goal: forall (m : Message) (q : queue Message), sumbool (In_queue Message m q) (not (In_queue Message m q)) *)
  simple induction q.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int true)) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  right; simpl in |- *.
(* Goal: not False *)
(* Goal: forall (d : Message) (q : queue Message) (_ : sumbool (In_queue Message m q) (not (In_queue Message m q))), sumbool (In_queue Message m (input Message d q)) (not (In_queue Message m (input Message d q))) *)
  simpl in |- *; red in |- *; trivial.
  
(* Goal: forall (d : Message) (q : queue Message) (_ : sumbool (In_queue Message m q) (not (In_queue Message m q))), sumbool (In_queue Message m (input Message d q)) (not (In_queue Message m (input Message d q))) *)
  intros d q0 H.
(* Goal: sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
  case (eq_message_dec m d).
(* Goal: forall _ : @eq Message m d, sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
(* Goal: forall _ : not (@eq Message m d), sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
  intro; left; left.
(* Goal: @eq Message m d *)
(* Goal: forall _ : not (@eq Message m d), sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
  trivial.
  
(* Goal: forall _ : not (@eq Message m d), sumbool (In_queue Message m (input Message d q0)) (not (In_queue Message m (input Message d q0))) *)
  intro; simpl in |- *; elim H.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  left; right; auto.
  
(* Goal: not (or (@eq Message m m') (In_queue Message m (bom s3 s4))) *)
(* Goal: forall (_ : not (@eq Message m m')) (_ : not (In_queue Message m (bom s3 s4))), not (In_queue Message m (Post_message Message m' bom s1 s2 s3 s4)) *)
  intro; right; intuition.
Qed.


End IN_Q_EFFECT.

Section REDUCE_EFFECT.

Variable Message : Set.
Let Bag_of_message := Bag_of_Data Message.


Variable f : Message -> Z.


Lemma reduce_post_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 reduce Message f (Post_message Message m b s1 s2 s1 s2) =
 (reduce Message f (b s1 s2) + f m)%Z.
Proof.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), @eq Z (reduce Message f (Post_message Message m b s1 s2 s1 s2)) (Z.add (reduce Message f (b s1 s2)) (f m)) *)
  intros m s1 s2 b.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite post_here.
(* Goal: @eq Z (reduce Message f (input Message m (b s1 s2))) (Z.add (reduce Message f (b s1 s2)) (f m)) *)
  apply reduce_append_nil1.
Qed.

Lemma reduce_collect_message :
 forall (m : Message) (s1 s2 : Site) (b : Bag_of_message),
 first Message (b s1 s2) = value Message m ->
 reduce Message f (Collect_message Message b s1 s2 s1 s2) =
 (reduce Message f (b s1 s2) - f m)%Z.
Proof.
(* Goal: forall (m : Message) (s1 s2 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s1 s2)) (Z.sub (reduce Message f (b s1 s2)) (f m)) *)
  intros m s1 s2 b H.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite collect_here.
(* Goal: @eq Z (reduce Message f (first_out Message (b s1 s2))) (Z.sub (reduce Message f (b s1 s2)) (f m)) *)
  apply reduce_first_out.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
Qed.

Lemma reduce_post_message_null :
 forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message),
 f m = 0%Z ->
 reduce Message f (Post_message Message m b s1 s2 s3 s4) =
 reduce Message f (b s3 s4).
Proof.
(* Goal: forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message) (_ : @eq Z (f m) Z0), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intros m s1 s2 s3 s4 b H.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  case (eq_queue_dec s1 s3 s2 s4).
(* Goal: forall _ : and (@eq Site s1 s3) (@eq Site s2 s4), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intros a.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  decompose [and] a.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite H0; rewrite H1.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite post_here.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int true)) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int (t s))) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  rewrite H.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intro o.
(* Goal: @eq Z (reduce Message f (Post_message Message m b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite post_elsewhere.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
Qed.

Lemma reduce_collect_message_null :
 forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message),
 first Message (b s1 s2) = value Message m ->
 f m = 0%Z ->
 reduce Message f (Collect_message Message b s1 s2 s3 s4) =
 reduce Message f (b s3 s4).
Proof.
(* Goal: forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message) (_ : @eq (exc Message) (first Message (b s1 s2)) (value Message m)) (_ : @eq Z (f m) Z0), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intros m s1 s2 s3 s4 b H H0.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  case (eq_queue_dec s1 s3 s2 s4).
(* Goal: forall _ : and (@eq Site s1 s3) (@eq Site s2 s4), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intros a.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  decompose [and] a.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite H1; rewrite H2.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s3 s4 s3 s4)) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite collect_here.
(* Goal: @eq Z (reduce Message f (first_out Message (b s3 s4))) (reduce Message f (b s3 s4)) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite reduce_first_out with (m := m).
(* Goal: @eq Z (Z.sub (reduce Message f (b s3 s4)) (f m)) (reduce Message f (b s3 s4)) *)
(* Goal: @eq (exc Message) (first Message (b s3 s4)) (value Message m) *)
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite H0.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  rewrite <- H1; rewrite <- H2; auto.
(* Goal: forall _ : or (not (@eq Site s1 s3)) (not (@eq Site s2 s4)), @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  intro o.
(* Goal: @eq Z (reduce Message f (Collect_message Message b s1 s2 s3 s4)) (reduce Message f (b s3 s4)) *)
  rewrite collect_elsewhere.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
Qed.




End REDUCE_EFFECT.


Section SIG_SEND.

Let Send_T := Site -> Z.

Definition sigma_send_table (t : Send_T) :=
  sigma_table Site LS Z (fun (s : Site) (x : Z) => x) t.

Definition Inc_send_table (t0 : Send_T) (s0 : Site) :=
  update_table Site eq_site_dec Z t0 s0 (t0 s0 + 1)%Z.  

Definition Dec_send_table (t0 : Send_T) (s0 : Site) :=
  update_table Site eq_site_dec Z t0 s0 (t0 s0 - 1)%Z.  

Let Date_T := Site -> nat.

Definition Set_date_table (d0 : Date_T) (s0 : Site) 
  (new_date : nat) := update_table Site eq_site_dec nat d0 s0 new_date.

End SIG_SEND.

Section SEND_EFFECT.

Let Send_T := Site -> Z.

Lemma sigma_inc_send_table :
 forall (t : Send_T) (s : Site),
 sigma_send_table (Inc_send_table t s) = (sigma_send_table t + 1)%Z.
Proof.
(* Goal: forall (t : Send_T) (s : Site), @eq Z (sigma_send_table (Dec_send_table t s)) (Z.sub (sigma_send_table t) (Zpos xH)) *)
  intros t s.
(* Goal: @eq Z (sigma_send_table (Inc_send_table t s)) (Z.add (sigma_send_table t) (Zpos xH)) *)
  unfold Inc_send_table in |- *.
(* Goal: @eq Z (sigma_send_table (update_table Site eq_site_dec Z t s (Z.sub (t s) (Zpos xH)))) (Z.sub (sigma_send_table t) (Zpos xH)) *)
  unfold sigma_send_table in |- *.
  rewrite
   (sigma_table_change Site eq_site_dec LS Z t s (t s + 1)%Z
      (fun (s : Site) (x : Z) => x)).
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.


Lemma sigma_dec_send_table :
 forall (t : Send_T) (s : Site),
 sigma_send_table (Dec_send_table t s) = (sigma_send_table t - 1)%Z.
Proof.
(* Goal: forall (t : Send_T) (s : Site), @eq Z (sigma_send_table (Dec_send_table t s)) (Z.sub (sigma_send_table t) (Zpos xH)) *)
  intros t s.
(* Goal: @eq Z (sigma_send_table (Dec_send_table t s)) (Z.sub (sigma_send_table t) (Zpos xH)) *)
  unfold Dec_send_table in |- *.
(* Goal: @eq Z (sigma_send_table (update_table Site eq_site_dec Z t s (Z.sub (t s) (Zpos xH)))) (Z.sub (sigma_send_table t) (Zpos xH)) *)
  unfold sigma_send_table in |- *.
  rewrite
   (sigma_table_change Site eq_site_dec LS Z t s (t s - 1)%Z
      (fun (s : Site) (x : Z) => x)).
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.

End SEND_EFFECT. 

Section SIG_RECV.


Let Recv_T := Site -> bool.

Definition sigma_receive_table (t : Recv_T) :=
  sigma_table Site LS bool (fun s : Site => Int) t.

Definition Set_rec_table (r0 : Recv_T) (s0 : Site) :=
  change_site bool r0 s0 true.

Definition Reset_rec_table (r0 : Recv_T) (s0 : Site) :=
  change_site bool r0 s0 false.


Lemma sigma_set_receive_table :
 forall (t : Recv_T) (s : Site),
 t s = false ->
 sigma_receive_table (Set_rec_table t s) = (sigma_receive_table t + 1)%Z.
Proof.
(* Goal: forall (t : Recv_T) (s : Site) (_ : @eq bool (t s) true), @eq Z (sigma_receive_table (Reset_rec_table t s)) (Z.sub (sigma_receive_table t) (Zpos xH)) *)
  intros t s H.
(* Goal: @eq Z (sigma_receive_table (Set_rec_table t s)) (Z.add (sigma_receive_table t) (Zpos xH)) *)
  unfold Set_rec_table in |- *.
(* Goal: @eq Z (sigma_receive_table (change_site bool t s false)) (Z.sub (sigma_receive_table t) (Zpos xH)) *)
  unfold sigma_receive_table in |- *.
(* Goal: @eq Z (sigma_table Site LS bool (fun _ : Site => Int) (change_site bool t s true)) (Z.add (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
  rewrite (sigma_table_change Site eq_site_dec LS bool t s true).
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int (t s))) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  rewrite H.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int true)) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.

                 

Lemma sigma_reset_receive_table :
 forall (t : Recv_T) (s : Site),
 t s = true ->
 sigma_receive_table (Reset_rec_table t s) = (sigma_receive_table t - 1)%Z.
Proof.
(* Goal: forall (t : Recv_T) (s : Site) (_ : @eq bool (t s) true), @eq Z (sigma_receive_table (Reset_rec_table t s)) (Z.sub (sigma_receive_table t) (Zpos xH)) *)
  intros t s H.
(* Goal: @eq Z (sigma_receive_table (Reset_rec_table t s)) (Z.sub (sigma_receive_table t) (Zpos xH)) *)
  unfold Reset_rec_table in |- *.
(* Goal: @eq Z (sigma_receive_table (change_site bool t s false)) (Z.sub (sigma_receive_table t) (Zpos xH)) *)
  unfold sigma_receive_table in |- *.
(* Goal: @eq Z (sigma_table Site LS bool (fun _ : Site => Int) (change_site bool t s false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
  rewrite (sigma_table_change Site eq_site_dec LS bool t s false).
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int (t s))) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  rewrite H.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Int true)) (Int false)) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) Z0) (Z.sub (sigma_table Site LS bool (fun _ : Site => Int) t) (Zpos xH)) *)
(* Goal: only_once Site eq_site_dec s LS *)
  omega.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.

                 
End SIG_RECV.





Section BUT_OWNER.

Variable Data : Set.
Let Table := Site -> Data.
Variable f : Site -> Data -> Z.


Definition sigma_table_but_owner (st : Table) :=
  sigma_but Site owner eq_site_dec LS (fun s : Site => f s (st s)).


Lemma sigma_sigma_but_owner :
 forall t : Table,
 sigma_table Site LS Data f t =
 (sigma_table_but_owner t + f owner (t owner))%Z.
Proof.
(* Goal: forall t : Table, @eq Z (sigma_table Site LS Data f t) (Z.add (sigma_table_but_owner t) (f owner (t owner))) *)
  intros t.
(* Goal: @eq Z (sigma_table Site LS Data f t) (Z.add (sigma_table_but_owner t) (f owner (t owner))) *)
  unfold sigma_table_but_owner in |- *.
(* Goal: @eq Z (sigma_table Site LS Data f t) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
  unfold sigma_table in |- *.
(* Goal: @eq Z (sigma Site LS (fun s : Site => f s (t s))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
  rewrite (sigma_sigma_but Site owner eq_site_dec).
(* Goal: @eq Z (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) (Z.add (sigma_but Site owner eq_site_dec LS (fun s : Site => f s (t s))) (f owner (t owner))) *)
(* Goal: only_once Site eq_site_dec owner LS *)
  auto.
(* Goal: only_once Site eq_site_dec owner LS *)
  apply finite_site.
Qed.

End BUT_OWNER.
