(* 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                                                     *)


Require Export DistributedReferenceCounting.machine2.machine.
Require Export DistributedReferenceCounting.machine2.cardinal.
Require Export DistributedReferenceCounting.machine2.comm.

Unset Standard Proposition Elimination Names.

Section ALTERNATE.

Inductive D_queue : queue Message -> Prop :=
  | D_empty : D_queue (empty Message)
  | D_dec : forall qm : queue Message, D_queue (input Message dec qm).

Inductive alternate : queue Message -> Prop :=
  | alt_null : alternate (empty Message)
  | alt_single_inc :
      forall s0 : Site,
      alternate (input Message (inc_dec s0) (empty Message))
  | alt_any_alt :
      forall (qm : queue Message) (m : Message),
      (forall s : Site, m <> inc_dec s) ->
      alternate qm -> alternate (input Message m qm)
  | alt_inc_dec :
      forall (qm : queue Message) (s0 : Site),
      alternate qm ->
      alternate (input Message (inc_dec s0) (input Message dec qm)).

Lemma not_D_queue :
 forall (q0 : queue Message) (m : Message),
 m <> dec -> ~ D_queue (input Message m q0).
Proof.
(* Goal: forall (q0 : queue Message) (m : Message) (_ : not (@eq Message m dec)), not (D_queue (input Message m q0)) *)
  intros; red in |- *; intro.
(* Goal: False *)
  inversion H0.
(* Goal: False *)
  elim H; auto.
Qed.
	
Lemma D_first_out :
 forall q0 : queue Message, D_queue q0 -> D_queue (first_out Message q0).
Proof.
(* Goal: forall (q0 : queue Message) (_ : alternate q0), alternate (first_out Message q0) *)
 intros; elim H; simpl in |- *.
(* Goal: D_queue (empty Message) *)
(* Goal: forall (m : Message) (q : queue Message), D_queue (input Message dec (first_out Message (input Message m q))) *)
 apply D_empty.

(* Goal: forall qm : queue Message, D_queue match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end *)
 simple destruct qm.
(* Goal: D_queue (empty Message) *)
(* Goal: forall (m : Message) (q : queue Message), D_queue (input Message dec (first_out Message (input Message m q))) *)
 apply D_empty.

(* Goal: forall (m : Message) (q : queue Message), D_queue (input Message dec (first_out Message (input Message m q))) *)
 intros; apply D_dec.
Qed.
	
Lemma alt_first_out :
 forall q0 : queue Message, alternate q0 -> alternate (first_out Message q0).
Proof.
(* Goal: forall (q0 : queue Message) (_ : alternate q0), alternate (first_out Message q0) *)
 intros; elim H; simpl in |- *.
(* Goal: alternate (empty Message) *)
(* Goal: alternate (input Message m (first_out Message (input Message d q))) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 apply alt_null.

(* Goal: alternate (empty Message) *)
(* Goal: alternate (input Message m (first_out Message (input Message d q))) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 intro; apply alt_null.
 
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 simple induction qm; intros.
(* Goal: alternate (empty Message) *)
(* Goal: alternate (input Message m (first_out Message (input Message d q))) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 apply alt_null.

(* Goal: alternate (input Message m (first_out Message (input Message d q))) *)
(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 apply alt_any_alt; trivial.

(* Goal: forall (qm : queue Message) (s0 : Site) (_ : alternate qm) (_ : alternate (first_out Message qm)), alternate (input Message (inc_dec s0) match qm with | @empty _ => empty Message | @input _ d q => input Message dec (first_out Message qm) end) *)
 simple induction qm; intros.
(* Goal: alternate (input Message (inc_dec s1) (empty Message)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (empty Message))) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
 apply alt_single_inc.

(* Goal: alternate (input Message (inc_dec s0) (input Message dec (first_out Message (input Message d q)))) *)
 apply alt_inc_dec; trivial.
Qed.


End ALTERNATE.

Section MESS_ALT.

(* consequence sur la structure alternee *)

Variable b0 : Bag_of_Data Message.

Variable s0 : Site.

Lemma D_collect :
 forall s1 s2 : Site,
 D_queue (b0 s0 owner) -> D_queue (Collect_message Message b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (_ : alternate (b0 s0 owner)), alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 intros; case (eq_queue_dec s1 s0 s2 owner); intro.
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 decompose [and] a; rewrite H0; rewrite H1.
(* Goal: D_queue (Collect_message Message b0 s0 owner s0 owner) *)
(* Goal: D_queue (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_here; apply D_first_out; trivial.

(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_elsewhere; auto.
Qed.

Lemma D_post_elsewhere :
 forall (s1 s2 : Site) (m : Message),
 s1 <> s0 \/ s2 <> owner ->
 D_queue (b0 s0 owner) -> D_queue (Post_message Message m b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (m : Message) (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : alternate (b0 s0 owner)), alternate (Post_message Message m b0 s1 s2 s0 owner) *)
 intros; rewrite post_elsewhere; trivial.
Qed.

Lemma D_post_dec : D_queue (Post_message Message dec b0 s0 owner s0 owner).
Proof.
(* Goal: D_queue (Post_message Message dec b0 s0 owner s0 owner) *)
 intros; rewrite post_here; apply D_dec; trivial.
Qed.

Lemma alt_collect :
 forall s1 s2 : Site,
 alternate (b0 s0 owner) ->
 alternate (Collect_message Message b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (_ : alternate (b0 s0 owner)), alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 intros; case (eq_queue_dec s1 s0 s2 owner); intro.
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 decompose [and] a; rewrite H0; rewrite H1.
(* Goal: alternate (Collect_message Message b0 s0 owner s0 owner) *)
(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_here; apply alt_first_out; trivial.

(* Goal: alternate (Collect_message Message b0 s1 s2 s0 owner) *)
 rewrite collect_elsewhere; auto.
Qed.

Lemma alt_post_elsewhere :
 forall (s1 s2 : Site) (m : Message),
 s1 <> s0 \/ s2 <> owner ->
 alternate (b0 s0 owner) ->
 alternate (Post_message Message m b0 s1 s2 s0 owner).
Proof.
(* Goal: forall (s1 s2 : Site) (m : Message) (_ : or (not (@eq Site s1 s0)) (not (@eq Site s2 owner))) (_ : alternate (b0 s0 owner)), alternate (Post_message Message m b0 s1 s2 s0 owner) *)
 intros; rewrite post_elsewhere; trivial.
Qed.

Lemma alt_post_any :
 forall m : Message,
 (forall s : Site, m <> inc_dec s) ->
 alternate (b0 s0 owner) ->
 alternate (Post_message Message m b0 s0 owner s0 owner).
Proof.
(* Goal: forall (m : Message) (_ : forall s : Site, not (@eq Message m (inc_dec s))) (_ : alternate (b0 s0 owner)), alternate (Post_message Message m b0 s0 owner s0 owner) *)
 intros; rewrite post_here; apply alt_any_alt; auto.
Qed.

Lemma alt_post_inc :
 forall s1 : Site,
 alternate (b0 s0 owner) ->
 b0 s0 owner = empty Message \/
 last Message (b0 s0 owner) = value Message dec ->
 alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner).
Proof.
(* Goal: forall (s1 : Site) (_ : alternate (b0 s0 owner)) (_ : or (@eq (queue Message) (b0 s0 owner) (empty Message)) (@eq (exc Message) (last Message (b0 s0 owner)) (value Message dec))), alternate (Post_message Message (inc_dec s1) b0 s0 owner s0 owner) *)
   intros s1 H; rewrite post_here; inversion H; simpl in |- *; intros.
(* Goal: alternate (input Message (inc_dec s1) (empty Message)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (empty Message))) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  apply alt_single_inc.
  
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (empty Message))) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  decompose [or] H0; discriminate H2.
  
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  elim H3.
(* Goal: forall _ : @eq (exc Message) (value Message m) (value Message dec), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  intro.
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: forall _ : @eq (exc Message) (value Message m) (value Message dec), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  discriminate.
  
(* Goal: forall _ : @eq (exc Message) (value Message m) (value Message dec), alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  intro.
(* Goal: alternate (input Message (inc_dec s1) (input Message m qm)) *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  replace m with dec.
(* Goal: alternate (input Message (inc_dec s1) (input Message dec qm)) *)
(* Goal: @eq Message dec m *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  apply alt_inc_dec.
(* Goal: @eq Message dec dec *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  auto.
  
(* Goal: @eq Message dec m *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  inversion H4.
(* Goal: @eq Message dec dec *)
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  auto.
  
(* Goal: alternate (input Message (inc_dec s1) (input Message (inc_dec s2) (input Message dec qm))) *)
  decompose [or] H2; discriminate H3.
Qed.

End MESS_ALT.
