Require Export ZArith List Bool.
Open Scope Z_scope.

Inductive aexpr : Type :=
  avar : Z -> aexpr
| aint : Z -> aexpr
| aplus : aexpr -> aexpr -> aexpr.

Inductive bexpr : Type :=
| blt : aexpr -> aexpr -> bexpr
| bor : bexpr -> bexpr -> bexpr
| band : bexpr -> bexpr -> bexpr
| beq : aexpr -> aexpr -> bexpr.

Inductive instr : Type :=
  skip 
| assign (v:Z) (e:aexpr)
| sequence (i1 i2:instr)
| while (b:bexpr) (i:instr)
| par (i1 i2:instr).

Delimit Scope instr_scope with i.
Bind Scope instr_scope with instr.
Arguments Scope sequence [Z_scope instr_scope].
Arguments Scope while [_ instr_scope].

Infix "++" := sequence : instr_scope.
Infix "||" := par : instr_scope.


Inductive a_eval : list(Z*Z) -> aexpr -> Z -> Prop :=
  ae_int : forall r n, a_eval r (aint n) n
| ae_var1 : forall r x v, a_eval ((x,v)::r) (avar x) v
| ae_var2 : forall r x y v v' , x <> y -> a_eval r (avar x) v' ->
              a_eval ((y,v)::r) (avar x) v'
| ae_plus : forall r e1 e2 v1 v2,
              a_eval r e1 v1 -> a_eval r e2 v2 ->
              a_eval r (aplus e1 e2) (v1 + v2).

Theorem ex1 : a_eval ((1,2)::nil)(aplus (avar 1)(aint 4)) 6.
Proof (ae_plus ((1,2)::nil) (avar 1) (aint 4) 2 4
        (ae_var1 nil  1 2) (ae_int ((1,2)::nil) 4)).

Hint Resolve ae_int ae_var1 ae_var2 ae_plus.

Inductive b_eval : list(Z*Z) -> bexpr -> bool -> Prop :=
| be_lt1 : forall r e1 e2 v1 v2,
            a_eval r e1 v1 -> a_eval r e2 v2 ->
            v1 < v2 -> b_eval r (blt e1 e2) true
| be_lt2 : forall r e1 e2 v1 v2,
            a_eval r e1 v1 -> a_eval r e2 v2 ->
            v2 <= v1 -> b_eval r (blt e1 e2) false
| be_or1 : forall r e1 e2,
           b_eval r e1 false -> b_eval r e2 false ->
           b_eval r (bor e1 e2) false
| be_or2 : forall r e1 e2,
           b_eval r e1 true -> b_eval r (bor e1 e2) true
| be_or3 : forall r e1 e2 v,
           b_eval r e1 v -> b_eval r e2 true ->
           b_eval r (bor e1 e2) true
| be_and1 : forall r e1 e2,
           b_eval r e1 true -> b_eval r e2 true ->
           b_eval r (band e1 e2) true
| be_and2 : forall r e1 e2,
           b_eval r e1 false -> b_eval r (band e1 e2) false
| be_and3 : forall r e1 e2 v,
           b_eval r e1 v -> b_eval r e2 false ->
           b_eval r (band e1 e2) false
| be_eq1 : forall r e1 e2 v,
           a_eval r e1 v -> a_eval r e2 v ->
           b_eval r (beq e1 e2) true
| be_eq2 : forall r e1 e2 v1 v2,
           a_eval r e1 v1 -> a_eval r e2 v2 -> v1 <> v2 ->
           b_eval r (beq e1 e2) false.

Inductive s_update : list(Z*Z)->Z->Z->list(Z*Z)->Prop :=
| s_up1 : forall r x v v', s_update ((x,v)::r) x v' ((x,v')::r)
| s_up2 : forall r r' x y v v', s_update r x v' r' ->
            x <> y -> s_update ((y,v)::r) x v' ((y,v)::r').


Inductive sos_step : list(Z*Z)->instr->instr->list(Z*Z)->Prop :=
  SOS1 : forall r r' x e v,
   a_eval r e v -> s_update r x v r' ->
   sos_step r (assign x e) skip r'
| SOS2 : forall r i2, sos_step r (sequence skip i2) i2 r
| SOS3 : forall r r' i1 i1' i2,
               sos_step r i1 i1' r' ->
               sos_step r (sequence i1 i2)(sequence i1' i2) r'
| SOS4 :
     forall r b i, b_eval r b true ->
       sos_step r (while b i) (sequence i (while b i)) r
| SOS5 :
     forall r b i, b_eval r b false ->
       sos_step r (while b i) skip r
| SOSP1 : forall r i2, sos_step r (par skip i2) i2 r
| SOSP2 : forall r i1, sos_step r (par i1 skip) i1 r
| SOSP3 : forall r r' i1 i1' i2,
               sos_step r i1 i1' r' ->
               sos_step r (par i1 i2)(par i1' i2) r'
| SOSP4 : forall r r' i1 i2 i2',
               sos_step r i2 i2' r' ->
               sos_step r (par i1 i2)(par i1 i2') r'.

Inductive sos_star : list(Z*Z)->instr->instr->list(Z*Z)->Prop :=
  SOS6 : forall r i, sos_star r i i r
| SOS7 : forall r r' r'' i i' i'',
             sos_step r i i' r' -> sos_star r' i' i'' r'' ->
             sos_star r i i'' r''.         

Hint Resolve SOS1 SOS2 SOS3 SOS5 SOS4 SOS6 SOS7 SOSP1 SOSP2 SOSP3 SOSP4.

Section Protected_variables.

Fixpoint val r v : option Z :=
 match r with
 | nil => None
 | (a,n)::r' => if Z_eq_dec a v then Some n else val r' v
 end.

Fixpoint preserve i v : Prop :=
  match i with
    (i1++i2)%i => preserve i1 v /\ preserve i2 v
  | while _ i => preserve i v
  | assign x _ => if Z_eq_dec x v then False else True
  | skip => True
  | (i1||i2)%i => preserve i1 v /\ preserve i2 v
  end.

Lemma s_update_eq : forall r x v r', s_update r x v r' -> val r' x = Some v.
induction 1.
 simpl; case (Z_eq_dec x x);[ | intros abs; case abs]; reflexivity.
simpl; case (Z_eq_dec y x);[ intros; case H0 | ];solve[auto].
Qed.

Lemma s_update_diff : forall r x v r', s_update r x v r' -> forall y, x <> y ->
  val r y = val r' y.
intros r x v r' H; induction H.
 simpl; intros y.
 case (Z_eq_dec x y);[intros a a';case a';assumption |reflexivity].
simpl; intros y' xny'.
 case (Z_eq_dec y y');[reflexivity | solve[auto]].
Qed.

Lemma preserve_step :
  forall i v, preserve i v -> forall r i' r', sos_step r i i' r' ->
    preserve i' v.
intros i v ip r i' r' H; induction H; 
 try (simpl in ip |- *; try destruct ip; solve[auto]).
Qed.

Lemma preserve_star :
  forall i v, preserve i v -> forall r i' r', sos_star r i i' r' ->
    preserve i' v.
intros i v ip r i' r' H; induction H.
 assumption.
apply IHsos_star; eapply preserve_step; eauto.
Qed.

Lemma preserve_sem' :
  forall i v,  preserve i v ->
  forall r i' r', sos_step r i i' r' -> val r v = val r' v.
intros i v ip r i' r' H; induction H;
    try (simpl in ip; try destruct ip; solve[auto]).
simpl in ip.
destruct (Z_eq_dec x v) as [_ | xnv];[solve[case ip] | ].
apply s_update_diff with (1:= H0); assumption.
Qed.

Lemma preserve_sem :
  forall i v, preserve i v ->
  forall r i' r', sos_star r i i' r' -> val r v = val r' v.
intros i v ip r i' r' H; induction H.
 reflexivity.
rewrite <- IHsos_star.
 apply preserve_sem' with i i'; assumption.
eapply preserve_step; eauto.
Qed.

Fixpoint preserve_all i l :=
  match l with
    nil => True
  | a::tl => preserve i a /\ preserve_all i tl
  end.

Lemma preserve_all_star : 
  forall i l, preserve_all i l -> forall r i' r', sos_star r i i' r' ->
    preserve_all i' l.
intros i l; induction l; intros pil r i' r' st.
 solve[auto].
simpl in pil |- *; destruct pil; split;[eapply preserve_star; eauto | eauto].
Qed.

Function all_instr_preserve (l : list instr) (lv : list Z) {struct l} : Prop :=
  match l with
    nil => True
  | i::tl => preserve_all i lv /\ all_instr_preserve tl lv
  end.

End Protected_variables.

Section peterson_common.

Variables flag0 flag1 turn : Z.
Hypothesis distinct : flag0 <> flag1 /\ flag0 <> turn /\ flag1 <> turn.

Variables i1 i2 i3 i4 : instr.
Hypothesis protected_vars :
  all_instr_preserve (i1::i2::i3::i4::nil) (flag0::flag1::turn::nil).

Variables b1 b2 : bexpr.

Section peterson_fragments.

Variables (b : bexpr) (i :instr) (f f' index : Z) (i' : instr).

Definition critical_head := 
  Eval lazy delta beta in
  (i'++assign f (aint 0))%i.

Definition wait_head :=
  Eval lazy delta beta in
  (while (band (beq (avar f') (aint 1))(beq (avar turn) (aint index))) skip++
    critical_head)%i.

Definition in_wait_head :=
  Eval lazy delta beta in
  ((skip++
    while (band (beq (avar f') (aint 1))(beq (avar turn) (aint index))) skip)++
    critical_head)%i.

Definition set_turn_head :=
  Eval lazy delta beta in
  (assign turn (aint index)++wait_head)%i.

Definition enter_head :=
  Eval lazy delta beta in
  (assign f (aint 1)++set_turn_head)%i.

Definition prefix_head :=
  Eval lazy delta beta in
  (i++enter_head)%i.

Definition peterson_scheme :=
  Eval lazy delta beta in
  (while b prefix_head).

End peterson_fragments.

Section peterson.

Definition p_scheme1 :=
  Eval lazy delta beta in
  peterson_scheme b1 i1 flag0 flag1 1 i2.

Definition p_scheme2 :=
  Eval lazy delta beta in
  peterson_scheme b2 i3 flag1 flag0 0 i4.

Definition peterson_program :=
  Eval lazy delta beta in
  (p_scheme1 || p_scheme2)%i.

Definition critical b i f f' index i' i''  :=
  Eval lazy delta beta in
  (critical_head f i''++peterson_scheme b i f f' index i')%i.

Definition end_critical b i f f' index i' :=
  Eval lazy delta beta in
  (assign f (aint 0)++peterson_scheme b i f f' index i')%i.

Definition restart b i f f' index i' :=
  (skip++peterson_scheme b i f f' index i')%i.

Definition end_wait b i f f' index i' :=
  ((skip++critical_head f i')++peterson_scheme b i f f' index i')%i.

Definition wait b i f f' index i' :=
  Eval lazy delta beta in
  (wait_head f f' index i'++peterson_scheme b i f f' index i')%i.

Definition start_wait b i f f' index i' :=
  Eval lazy delta beta in
  ((skip++wait_head f f' index i')++peterson_scheme b i f f' index i')%i.

Definition in_wait b i f f' index i' :=
  Eval lazy delta beta in
  (in_wait_head f f' index i'++peterson_scheme b i f f' index i')%i.

Definition set_turn b i f f' index i' :=
  Eval lazy delta beta in
  (set_turn_head f f' index i'++peterson_scheme b i f f' index i')%i.

Definition enter_middle b i f f' index i' :=
  Eval lazy delta beta in
  ((skip++set_turn_head f f' index i')++peterson_scheme b i f f' index i')%i.

Definition enter b i f f' index i':=
  Eval lazy delta beta in
  ((enter_head f f' index i')++peterson_scheme b i f f' index i')%i.

Definition prefix b i f f' index i' i'' := 
  Eval lazy delta beta in
  (prefix_head i'' f f' index i'++peterson_scheme b i f f' index i')%i.

Definition in_states b i f f' index i' i'' :=
  (exists i3, preserve_all i3 (flag0::flag1::turn::nil) /\
     i'' = prefix b i f f' index i' i3) \/
  (exists i3, preserve_all i3 (flag0::flag1::turn::nil) /\
     i'' = critical b i f f' index i' i3) \/
  In i'' (peterson_scheme b i f f' index i':: enter b i f f' index i'::
          enter_middle b i f f' index i':: set_turn b i f f' index i'::
          start_wait b i f f' index i' :: wait b i f f' index i'::
          in_wait b i f f' index i'::end_wait b i f f' index i'::
          end_critical b i f f' index i'::restart b i f f' index i'::skip::nil).

Inductive sos_star' (r:list (Z*Z)) (i:instr) : instr -> list (Z*Z) -> Prop :=
  SOS'6 : sos_star' r i i r
| SOS'7 : forall i' i'' r' r'', sos_star' r i i' r' -> sos_step r' i' i'' r'' ->
          sos_star' r i i'' r''.

Lemma sos_star_trans : 
  forall r r' r'' i i' i'', sos_star r i i' r' -> sos_star r' i' i'' r'' ->
    sos_star r i i'' r''.
intros r r' r'' i i' i'' H; revert r'' i''; induction H.
 intros; assumption.
solve[eauto].
Qed.

Lemma sos_star'_trans : 
  forall r r' r'' i i' i'', sos_star' r i i' r' -> sos_star' r' i' i'' r'' ->
    sos_star' r i i'' r''.
intros r r' r'' i i' i'' H H'; induction H'.
 intros; assumption.
apply SOS'7 with (1 := IHH'); assumption.
Qed.

Lemma star_star' : forall r i i' r', sos_star r i i' r' -> sos_star' r i i' r'.
induction 1.
  solve[constructor].
apply sos_star'_trans with (2:=IHsos_star).
apply SOS'7 with (2:=H);constructor.
Qed.

Lemma star'_star : forall r i i' r', sos_star' r i i' r' -> sos_star r i i' r'.
induction 1.
  solve[constructor].
apply sos_star_trans with (1:=IHsos_star').
apply SOS7 with (1:= H0);constructor.
Qed.

Ltac auto_eq :=
  try solve[repeat ((left; reflexivity) || right)].

Lemma states1 :
  forall b i f f' index i'  r j j' r',
  all_instr_preserve (i::i'::nil) (flag0::flag1::turn::nil) ->
  in_states b i f f' index i' j -> sos_step r j j'  r' ->
  in_states b i f f' index i' j'.
intros b i f f' index i' r j j' r' [aip [aip' _]] H H0.
repeat (destruct H as [H | H];
 [destruct H as [ip [ipp ipq]]; rewrite ipq in H0; inversion H0;
  (inversion H5;
      [red; simpl;solve[auto_eq] |
         match goal with id : sos_step r ip ?x r' |- _ =>
           assert (tmp:= preserve_all_star ip (flag0::flag1::turn::nil)
                    ipp r x r')
         end;
             (left; exists i1'0; solve[eauto using SOS7, SOS6]) ||
             (right; left; exists i1'0; solve[eauto using SOS7, SOS6])]) |]).
repeat (destruct H as [H | H];
          [rewrite <- H in H0; inversion H0; clear H0; red; simpl; auto_eq;
           try solve[try (match goal with id : sos_step _ _ _ _ |- _ => inversion id end);
                auto_eq;
           try (match goal with id : sos_step _ _ _ _ |- _ => inversion id end);
                auto_eq;
           try (match goal with id : sos_step _ _ _ _ |- _ => inversion id end);
                auto_eq |
             left; exists i; split; [simpl in aip; tauto | reflexivity] |
             match goal with id : sos_step _ _ _ _ |- _ => inversion id end;
             (match goal with id : sos_step _ skip _ _ |- _ => inversion id end)
             ||
             right; left; exists i'; split;[simpl in aip'; tauto | reflexivity]]
          | ]).
inversion H.
Qed.

Lemma states :
  forall r i r',
  sos_star r peterson_program i r' ->
  ((in_states b1 i1 flag0 flag1 1 i2 i \/ 
    in_states b2 i3 flag1 flag0 0 i4 i))\/
  exists j1, exists j2, i = (j1 || j2)%i /\
   in_states b1 i1 flag0 flag1 1 i2 j1 /\
   in_states b2 i3 flag1 flag0 0 i4 j2.
assert (pv := protected_vars); destruct pv as [aip1 [aip2 [aip3 [aip4 []]]]].
intros r i r' H; apply star_star' in H; induction H.
 right; exists p_scheme1; exists p_scheme2; split;[reflexivity | ].
 split; right; right; left; reflexivity.
destruct IHsos_star' as [[ins1 | ins2] | [j1 [j2 [q [ins1 ins2]]]]].
  do 2 left; apply states1 with r' i' r'';
   [split; [ | split; [ | exact I]] | | ];assumption.
 left; right; apply states1 with r' i' r'';
   [split; [ | split; [ | exact I]] | | ];assumption.
rewrite q in H0; inversion H0.
   left; right; subst i''; assumption.
  left; left; subst i''; assumption.
 right; exists i1'; exists j2;split;[reflexivity |split;[ |assumption ]].
 apply states1 with r' j1 r'';[split; [ | split; [ | exact I]] | | ];assumption.
right; exists j1; exists i2';split;[reflexivity | split;[assumption |]].
apply states1 with r' j2 r'';[split; [ | split; [ | exact I]] | |];assumption.
Qed.

Lemma not_in_states_par :
  forall b i f f' index i' j1 j2, ~in_states b i f f' index i' (j1 || j2).
intros b i f f' index i' j1 j2 H.
 destruct H as [[j' [_ q]] | [[j' [_ q]] | H]]; try discriminate.
 repeat (destruct H as [q | H]; try discriminate); contradiction.
Qed.

Lemma states' :
  forall r j1 j2 r', sos_star r peterson_program (j1||j2) r' ->
   in_states b1 i1 flag0 flag1 1 i2 j1 /\ in_states b2 i3 flag1 flag0 0 i4 j2.
intros r j1 j2 r' H; destruct (states _ _ _ H) as [[abs | abs] | H'];
 try case (not_in_states_par _ _ _ _ _ _ _ _ abs).
destruct H' as [j3 [j4 [q [ins1 ins2]]]].
  injection q; intros; subst; split; assumption.
Qed.

Lemma states'' :
  forall r i j1 j2 r' r'', sos_star r peterson_program i r' ->
   sos_step r' i (j1 || j2) r'' ->
   exists j3, exists j4, i = (j3|| j4)%i /\
   in_states b1 i1 flag0 flag1 1 i2 j3 /\ in_states b2 i3 flag1 flag0 0 i4 j4.
intros r i j1 j2 r' r'' H H'; inversion H'; subst.
    destruct (states _ _ _ H) as [[abs | abs] | aq];
      try (repeat (destruct abs as [aq | abs];try discriminate);
      try (destruct aq as [j [_ aq]]; try discriminate);contradiction).
    destruct aq as [j [j' [q [ab ab']]]]; discriminate.
   destruct (states _ _ _ H) as [[abs | abs] | [j3 [j4 [q [abs abs']]]]];
     try case (not_in_states_par _ _ _ _ _ _ _ _ abs);
     try (solve[injection q; do 2 intro;subst;
         case (not_in_states_par _ _ _ _ _ _ _ _ abs) ||
          case (not_in_states_par _ _ _ _ _ _ _ _ abs')]).
   destruct (states _ _ _ H) as [[abs | abs] | [j3 [j4 [q [abs abs']]]]];
      try case (not_in_states_par _ _ _ _ _ _ _ _ abs);
      try (solve[injection q; do 2 intro;subst;
           case (not_in_states_par _ _ _ _ _ _ _ _ abs) ||
           case (not_in_states_par _ _ _ _ _ _ _ _ abs')]).
 exists i0; exists j2;split;[reflexivity|apply (states' _ _ _ _ H)].
exists j1; exists i5;split;[reflexivity|apply (states' _ _ _ _ H)].
Qed.

Lemma in_state_preserve :
  forall b i f f' index i' i'', f' = flag0 \/ f' = flag1 ->
  f <> f' -> turn <> f' ->
  preserve i f' -> preserve i' f' -> 
  in_states b i f f' index i' i'' ->
    preserve i'' f'.
intros b i f f' index i' i'' fcases fnf' tnf pi pi'.
assert (pr1 : preserve skip f') by (simpl; auto).
assert (pr2 : preserve (assign f (aint 0)) f').
 simpl; case (Z_eq_dec f f');[intros;case fnf';assumption | solve[auto]].
assert (pr3 : forall j, preserve j f' -> preserve (j++assign f (aint 0)) f').
 intros j pj; simpl; split; assumption.
assert (pr4 : preserve (skip++critical_head f i') f').
 split;[exact I | apply pr3; assumption].
assert (pr5 : preserve (in_wait_head f f' index i') f').
 split;[simpl;solve[auto] | apply pr3; assumption].
assert (pr6 : preserve (wait_head f f' index i') f').
 split;[simpl;solve[auto] | apply pr3; assumption].
assert (pr7 : preserve (skip++wait_head f f' index i') f').
 split;[simpl;solve[auto] | exact pr6].
assert (pr8 : preserve (set_turn_head f f' index i') f').
 split;[simpl; destruct (Z_eq_dec turn f');
   [case tnf; assumption | exact I] | exact pr6].
assert (pr9 : preserve (skip++set_turn_head f f' index i') f').
 split;[simpl;solve[auto] | exact pr8].
assert (pr10 : preserve (enter_head f f' index i') f').
 split;[simpl;destruct (Z_eq_dec f f');[case fnf'; assumption | exact I] |
        exact pr8].
assert (pr11 :
         forall j, preserve j f' -> preserve (prefix_head j f f' index i') f').
 intros j pj;split;[exact pj | exact pr10].
assert (pr12 : preserve (peterson_scheme b i f f' index i') f').
 exact (pr11 i pi).
intros [[j [[pjf0 [pjf1 _]]q]] | H].
 rewrite q; split;[apply pr11; destruct fcases; subst f' | ]; assumption.
destruct H as [[j [[prjf0 [prjf1 _]] q]] | H].
 rewrite q; split;[apply pr3; destruct fcases; subst f' | ]; assumption.
repeat (destruct H as [H' | H];[rewrite <- H';split;assumption | ]).
destruct H.
Qed.

Definition large_critical b i f f' index i' j :=
  (exists i'', preserve_all i'' (flag0::flag1::turn::nil) /\
      j = critical b i f f' index i' i'') \/
  (end_wait b i f f' index i' = j).

Definition flag_zone b i f f' index i' j :=
  large_critical b i f f' index i' j \/
  enter_middle b i f f' index i' = j \/
  set_turn b i f f' index i' = j \/
  start_wait b i f f' index i' = j \/
  wait b i f f' index i' = j \/
  in_wait b i f f' index i' = j \/
  end_wait b i f f' index i' = j \/
  end_critical b i f f' index i' = j.
  
Lemma ptf0 : preserve (assign turn (aint 1)) flag0.
simpl; case (Z_eq_dec turn flag0); intros; subst; tauto.
Qed.

Lemma ptf1 : preserve (assign turn (aint 1)) flag1.
simpl; case (Z_eq_dec turn flag1); intros; subst; tauto.
Qed.

Lemma pwf : forall b v, preserve (while b skip) v. 
simpl;solve[auto].
Qed.

Lemma upwf : forall b v, preserve (skip++while b skip) v. 
simpl;solve[auto].
Qed.

Hint Resolve ptf0 ptf1 pwf upwf : preserves.

Lemma critical_pred :
  forall b i f f' index i' i'' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (critical b i f f' index i' i'')  r' ->
    (exists j, preserve_all j (flag0::flag1::turn::nil) /\
             i0 = critical b i f f' index i' j) \/
    end_wait b i f f' index i' = i0.
intros b i f f' index i' i'' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   match goal with id : sos_step _ _ _ _ |- _ => inversion id end) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;
       left; exists j'; solve[auto]).
Qed.

Lemma end_wait_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (end_wait b i f f' index i')  r' ->
    wait b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat match goal with id : sos_step _ _ _ _ |- _ => inversion id end) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end).
Qed.

Lemma end_critical_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (end_critical b i f f' index i')  r' ->
    critical b i f f' index i' skip = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat match goal with id : sos_step _ _ _ _ |- _ => inversion id end) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma in_wait_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (in_wait b i f f' index i')  r' ->
    wait b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat (match goal with id : sos_step _ _ _ _ |- _ => inversion id end)) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma wait_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (wait b i f f' index i')  r' ->
    in_wait b i f f' index i' = i0 \/ start_wait b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat (match goal with id : sos_step _ _ _ _ |- _ => inversion id end)) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma start_wait_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (start_wait b i f f' index i')  r' ->
    set_turn b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat (match goal with id : sos_step _ _ _ _ |- _ => inversion id end)) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma set_turn_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (set_turn b i f f' index i')  r' ->
    enter_middle b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat (match goal with id : sos_step _ _ _ _ |- _ => inversion id end)) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma enter_middle_pred :
  forall b i f f' index i' i0 r r',
    in_states b i f f' index i' i0 ->
    sos_step r i0 (enter_middle b i f f' index i')  r' ->
    enter b i f f' index i' = i0.
intros b i f f' index i' i0 r r' H.
repeat (destruct H as [H' | H] || destruct H); auto;
  (rewrite <- H'; intros H''; inversion H''; clear H'';
   repeat (match goal with id : sos_step _ _ _ _ |- _ => inversion id end)) ||
  (destruct H' as [j' [ajp q]]; rewrite q; intros H''; inversion H'';
       clear H'';
       match goal with id : sos_step _ _ _ _ |- _ => inversion id end;auto).
Qed.

Lemma flag_zone_flag1 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> flag_zone b1 i1 flag0 flag1 1 i2 j1 ->
    val r' flag0 = Some 1.
intros r i r' j1 j2 H; apply star_star' in H; revert j1 j2; induction H.
 intros j1 j2 qp; injection qp; intros q2 q1 [[[j3 [_ H']] | H'] | H'];
   [subst j1; discriminate | subst j1; discriminate | ].
 repeat (destruct H' as [H' | H']; [subst j1; discriminate | ]);
    subst j1; discriminate.
intros j1 j2 q; rewrite q in H0.
destruct (states'' _ _ _ _ _ _ (star'_star _ _ _ _ H) H0) 
  as [j3 [j4 [q' [ins1 ins2]]]].
rewrite q' in H0; inversion H0; clear H0;
  try (subst; case (not_in_states_par _ _ _ _ _ _ _ _ ins1) ||
           case (not_in_states_par _ _ _ _ _ _ _ _ ins2)).
assert (IH := IHsos_star' _ _ q').
 match goal with id : sos_step r' _ _ r''|- _ => rename id into tmp end.
 intros [[[jc [jcp jcq]] | H'] | H'];
 try (rewrite jcq in tmp; destruct 
      (critical_pred _ _ _ _ _ _ _ _ _ _ ins1 tmp) as
      [[jc' [jcp' jcq']] | w];[rewrite jcq' in tmp | rewrite <- w in tmp];
      inversion tmp; clear tmp;
      match goal with id : sos_step _ _ _ _ |- _ => inversion id end).
    assert (t2 : preserve jc' flag0) by (simpl in jcp'; tauto).
    rewrite <- (preserve_sem' jc' flag0 t2 r' jc r'');auto.
    apply IH; subst; left; left; exists jc'; solve[auto].
   replace r'' with r'; apply IH; rewrite <- w; red; simpl; solve[auto 10].
  rewrite <- H' in tmp; assert (t:=end_wait_pred _ _ _ _ _ _ _ _ _ ins1 tmp).
  rewrite <- t in tmp; inversion tmp; clear tmp.
  do 2 match goal with id : sos_step _ _ _ _ |- _ => inversion id end.
  replace r'' with r'; apply IH; rewrite <- t; red; simpl; solve[auto 10].
 assert (preserve (while (band (beq (avar flag1) (aint 1))
                               (beq (avar turn) (aint 1))) skip) flag0) by
   (simpl; auto).
 assert (preserve (assign turn (aint 1)) flag0) by
   (simpl; case (Z_eq_dec turn flag0);
    [intros tf; rewrite tf in distinct; tauto|auto]).
 repeat destruct H' as [q2 | H'];
 try rename H' into q2; rewrite <- q2 in tmp;
 try ((assert (t := enter_middle_pred _ _ _ _ _ _ _ _ _ ins1 tmp) ||
  assert (t := set_turn_pred _ _ _ _ _ _ _ _ _ ins1 tmp) ||
  assert (t := start_wait_pred  _ _ _ _ _ _ _ _ _ ins1 tmp) ||
  (assert (t := wait_pred _ _ _ _ _ _ _ _ _ ins1 tmp);destruct t as [t | t]) ||
  (assert (t := in_wait_pred _ _ _ _ _ _ _ _ _ ins1 tmp)) ||
  (assert (t := end_wait_pred _ _ _ _ _ _ _ _ _ ins1 tmp)) ||
  (assert (t := end_critical_pred _ _ _ _ _ _ _ _ _ ins1 tmp)));
 try (rewrite <- t in tmp; inversion tmp; clear tmp;
 repeat match goal with id : sos_step _ (_ ++ _) _ _ |- _ => inversion id;
   clear id end));
  (match goal with u : sos_step _ (assign flag0 _) _ _ |- _ => inversion u end;
  match goal with id1 : a_eval _ _ _ , id : s_update _ flag0 _ _ |- _ => 
   inversion id1; replace v with 1 in id; apply s_update_eq with (1:= id)
 end) ||
 (match goal with u : sos_step _ _ _ _ |- _ => rewrite <- preserve_sem'
   with (2:=u);[apply IH;subst; red; solve[auto 10] | assumption] end) ||
 (try (replace r'' with r';[apply IH;subst; red; solve[auto 10]])). 
 replace r'' with r'; apply IH; subst; left; left; exists skip; split;
  [simpl; auto | reflexivity].
assert (t1 : preserve i3 flag0) by (simpl in protected_vars; tauto).
assert (t2 : preserve i4 flag0) by (simpl in protected_vars; tauto).
assert (t3 : flag0 = flag0 \/ flag0 = flag1) by auto.
assert (tmp := in_state_preserve b2 i3 flag1 flag0 0 i4 j4 t3).
assert (t4 : flag1<>flag0) by (decompose [and] distinct; auto).
assert (t5 : turn <> flag0) by (decompose [and] distinct; auto).
intros fl.
assert (t6 : preserve j4 flag0) by auto.
match goal with id : sos_step _ _ _ _ |- _ =>
 rewrite <- preserve_sem' with (1:=t6) (2:= id)
end.
apply (IHsos_star' _ _ q'); subst; auto.
Qed.

Lemma large_critical_flag1 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> large_critical b1 i1 flag0 flag1 1 i2 j1 ->
    val r' flag0 = Some 1.
intros r i r' j1 j2 H qp H'; apply (flag_zone_flag1 r i r' j1 j2 H qp).
left; auto.
Qed.


Lemma flag_zone_flag2 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> flag_zone b2 i3 flag1 flag0 0 i4 j2 ->
    val r' flag1 = Some 1.
intros r i r' j1 j2 H; apply star_star' in H; revert j1 j2; induction H.
 intros j1 j2 qp; injection qp; intros q2 q1 [[[j3 [_ H']] | H'] | H'];
   [subst j2; discriminate | subst j2; discriminate | ].
 repeat (destruct H' as [H' | H']; [subst j2; discriminate | ]);
    subst j2; discriminate.
apply star'_star in H; destruct (states _ _ _ H) as [[H'| H']| H'];
   try (intros j1 j2 qp; rewrite qp in H0; 
     destruct H' as [[j [_ jq]] | [[j [_ jq]] | H']];
     (rewrite jq in H0; inversion H0) ||
     (try (repeat
          (destruct H' as [i'q | H']; [rewrite <-i'q in H0; inversion H0|]);
        contradiction))).
destruct H' as [j1 [j2 [i'q [ins1 ins2]]]]; intros j3 j4 i''q.
assert (IH := IHsos_star' _ _ i'q).
rewrite i'q, i''q in H0; inversion H0; clear H0.
   solve[subst; case (not_in_states_par _ _ _ _ _ _ _ _ ins2)].
  solve[subst; case (not_in_states_par _ _ _ _ _ _ _ _ ins1)].
 assert (t1 : preserve i1 flag1) by (simpl in protected_vars; tauto).
 assert (t2 : preserve i2 flag1) by (simpl in protected_vars; tauto).
 assert (t3 : flag1 = flag0 \/ flag1 = flag1) by auto.
 assert (tmp := in_state_preserve b1 i1 flag0 flag1 1 i2 j1 t3).
 assert (t4 : flag0<>flag1) by (decompose [and] distinct; auto).
 assert (t5 : turn <> flag1) by (decompose [and] distinct; auto).
 assert (t6 : preserve j1 flag1) by auto.
 intros fl; match goal with id : sos_step _ _ _ _ |- _ =>
   rewrite <- preserve_sem' with (1:=t6) (2:= id)
 end.
 apply IH; subst; auto.
match goal with id : sos_step r' j2 j4 r''|- _ => rename id into tmp end.
intros [[[jc [jcp jcq]] | H'] | H'];
 try (rewrite jcq in tmp; destruct 
      (critical_pred _ _ _ _ _ _ _ _ _ _ ins2 tmp) as
      [[jc' [jcp' jcq']] | w];[rewrite jcq' in tmp | rewrite <- w in tmp];
      inversion tmp; clear tmp;
      match goal with id : sos_step _ _ _ _ |- _ => inversion id end).
   assert (t2 : preserve jc' flag1) by (simpl in jcp'; tauto).
   rewrite <- (preserve_sem' jc' flag1 t2 r' jc r'');auto.
   apply IH; subst; left; left; exists jc'; solve[auto].
  replace r'' with r'; apply IH; rewrite <- w; red; simpl; solve[auto 10].
 rewrite <- H' in tmp; assert (t:=end_wait_pred _ _ _ _ _ _ _ _ _ ins2 tmp).
 rewrite <- t in tmp; inversion tmp; clear tmp.
 do 2 match goal with id : sos_step _ _ _ _ |- _ => inversion id end.
 replace r'' with r'; apply IH; rewrite <- t; red; simpl; solve[auto 10].
assert (preserve (while (band (beq (avar flag0) (aint 1))
                               (beq (avar turn) (aint 0))) skip) flag1) by
   (simpl; auto).
assert (preserve (assign turn (aint 0)) flag1) by
   (simpl; case (Z_eq_dec turn flag1);
    [intros tf; rewrite tf in distinct; tauto|auto]).
repeat destruct H' as [q | H']; try rename H' into q; rewrite <- q in tmp;
 try ((assert (t := enter_middle_pred _ _ _ _ _ _ _ _ _ ins2 tmp) ||
  assert (t := set_turn_pred _ _ _ _ _ _ _ _ _ ins2 tmp) ||
  assert (t := start_wait_pred  _ _ _ _ _ _ _ _ _ ins2 tmp) ||
  (assert (t := wait_pred _ _ _ _ _ _ _ _ _ ins2 tmp);destruct t as [t | t]) ||
  (assert (t := in_wait_pred _ _ _ _ _ _ _ _ _ ins2 tmp)) ||
  (assert (t := end_wait_pred _ _ _ _ _ _ _ _ _ ins2 tmp)) ||
  (assert (t := end_critical_pred _ _ _ _ _ _ _ _ _ ins2 tmp)));
 try (rewrite <- t in tmp; inversion tmp; clear tmp;
 repeat match goal with id : sos_step _ (_ ++ _) _ _ |- _ => inversion id;
   clear id end));
  (match goal with u : sos_step _ (assign flag1 _) _ _ |- _ => inversion u end;
  match goal with id1 : a_eval _ _ _ , id : s_update _ flag1 _ _ |- _ => 
   inversion id1; replace v with 1 in id; apply s_update_eq with (1:= id)
 end) ||
 (match goal with u : sos_step _ _ _ _ |- _ => rewrite <- preserve_sem'
   with (2:=u);[apply IH;subst; red; solve[auto 10] | assumption] end) ||
 (try (replace r'' with r';[apply IH;subst; red; solve[auto 10]])). 
 replace r'' with r'; apply IH; subst; left; left; exists skip; split;
  [simpl; auto | reflexivity].
Qed.

Lemma large_critical_flag2 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> large_critical b2 i3 flag1 flag0 0 i4 j2 ->
    val r' flag1 = Some 1.
intros r i r' j1 j2 H qp H'; apply (flag_zone_flag2 r i r' j1 j2 H qp).
left; auto.
Qed.

Definition large_wait b i f f' index i' j :=
  start_wait b i f f' index i' = j \/ 
  wait b i f f' index i' = j \/ in_wait b i f f' index i' = j
  \/ end_wait b i f f' index i' = j.

Lemma a_eval_val : forall r x v, a_eval r (avar x) v <-> val r x = Some v.
induction r as [ | [y v'] r' IH]; intros x v.
 split; intros H; inversion H.
simpl; split;[intros H; inversion H | ].
  case (Z_eq_dec x x);[ |intros abs; case abs];reflexivity.
 case (Z_eq_dec y x);[assert (y<>x) by auto; contradiction |].
 intros; rewrite <- IH; assumption.
case (Z_eq_dec y x);[intros q q'; injection q';intro; subst;constructor |].
intros ynx vval; constructor; auto; rewrite IH; auto.
Qed.

Lemma large_wait_preserve :
  forall b i f f' index i' j r j' r',
  large_wait b i f f' index i' j -> sos_step r j j' r' -> r = r'.
intros b i f f' index i' j r j' r' lw st; repeat destruct lw as [lw | lw];
repeat (subst; inversion st; auto; clear st; 
 match goal with u : sos_step _ _ _ _ |- _ => rename u into st end; auto).
Qed.

Lemma large_critical_pred :
  forall b i f f' index i' j j' r r',
  in_states b i f f' index i' j ->
  large_critical b i f f' index i' j' ->
  sos_step r j j' r' -> 
    (wait b i f f' index i' = j /\ r = r') \/ 
        (large_critical b i f f' index i' j /\
         val r turn = val r' turn).
intros b i f f' index i' j j' r r' ins [[j1 [_ lc]] | lc] st.
 rewrite lc in st.
 destruct (critical_pred _ _ _ _ _ _ _ _ _ _ ins st) as [[j2 [p c]] | w].
  right; split;[left; exists j2; solve[auto] |
   unfold critical in c; rewrite c in st].
  repeat (match goal with u : sos_step _ (_ ++ _) _ _ |- _ =>
             inversion u; clear u; subst
           end); apply preserve_sem' with j2 j1; simpl in p; tauto.
 right; split; [right; exact w | ].
 unfold critical in *; unfold end_wait in w; rewrite <- w in st;
 repeat (match goal with u : sos_step _ (_ ++ _) _ _ |- _ =>
             inversion u; clear u; subst
           end); solve[auto].
rewrite <- lc in st.
assert (t : wait b i f f' index i' = j).
 apply end_wait_pred with (2:=st);assumption.
left;split;[assumption | apply (large_wait_preserve b i f f' index i' j r j')].
 unfold large_wait; solve[auto].
rewrite <- lc; assumption.
Qed.

Lemma large_wait_pred :
  forall b i f f' index i' j j' r r',
  in_states b i f f' index i' j ->
  large_wait b i f f' index i' j' ->
  sos_step r j j' r' -> set_turn b i f f' index i' = j \/ 
        large_wait b i f f' index i' j.
intros b i f f' index i' j j' r r' ins [sw | lw] st.
 rewrite <- sw in st; left; apply start_wait_pred with (2:=st); assumption.
right; destruct lw as [lw | [ lw | lw]]; rewrite <- lw in st;
 red; eauto using in_wait_pred, end_wait_pred.
assert (t:= wait_pred _ _ _ _ _ _ _ _ _ ins st);tauto.
Qed.

Lemma assign_val_num : forall r x n  i r', 
  sos_step r (assign x (aint n)) i r' -> val r' x = Some n.
intros r x n i r' st; inversion st.
match goal with u : a_eval _ _ _ |- _ => inversion u; subst end.
match goal with u : s_update _ _ _ _ |- _ => apply s_update_eq with (1:=u) end.
Qed.

Lemma wait_exit_case : forall b i f  f' index i' j r r',
  val r' f' = Some 1 ->
  large_critical b i f f' index i' j ->
  sos_step r (wait b i f f' index i') j r' -> val r' turn <> Some index.
intros b i f f' index i' j r r' vf lc st.
do 3 match goal with u: sos_step _ _ _ _ |- _ => inversion u; clear u end.
 subst; clear -lc; destruct lc as [[j' [_ lc]] | lc]; discriminate.
match goal with u: b_eval _ _ _ |- _ => inversion u; clear u end.
 match goal with u : b_eval _ _ _ |- _ => inversion u; clear u end.
 match goal with u : a_eval _ (avar _) _ |- _ => rename u into t end.
 rewrite a_eval_val in t.
 match goal with u : a_eval _ _ _ |- _ => inversion u; clear u; subst end.
 rewrite t in vf; injection vf; intros; subst.
 match goal with u : _ <> _ |- _ => case u; reflexivity end.
match goal with u : b_eval _ (beq (avar turn) _) _ |- _ => inversion u end.
match goal with u : a_eval _ _ _ |- _ => 
   rewrite a_eval_val in u; rewrite u; clear u end.
match goal with u : a_eval _ _ _ |- _ => inversion u end.
intros ab; injection ab; intro; contradiction.
Qed.

Lemma wait_turn1 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> large_critical b1 i1 flag0 flag1 1 i2 j1 ->
    large_wait b2 i3 flag1 flag0 0 i4 j2 ->
    val r' turn <> Some 1.
intros r i r' j1 j2 H; revert j1 j2; apply star_star' in H.
induction H as [ | i' i'' r' r'' H IH H0].
 intros j1 j2 q lc lw; injection q; do 2 intro; subst.
 solve[repeat (destruct lw as [ab | lw]; try discriminate); destruct lw].
intros j1 j2 q lc lw; apply star'_star in H; rewrite q in H0.
destruct (states'' _ _ _ _ _ _ H H0) as [j3 [j4 [q' [ins3 ins4]]]].
inversion H0;try solve[subst; discriminate |
   subst; match goal with q : _ , ins : _|- _ => injection q; intros; subst;
      solve[case (not_in_states_par _ _ _ _ _ _ _ _ ins)]
   end]; clear H0.
 subst; match goal with q: _, u : _ |- _ => 
 injection q; intros; subst; rename u into st; clear q;
 destruct (large_critical_pred _ _ _ _ _ _ _ _ _ _ ins3 lc st) as
   [[jc3 t] | [j3q t]]
 end.
  rewrite <- jc3 in st.
  apply (wait_exit_case b1 i1 flag0 flag1 1 i2 j1 r'); auto.
  replace r'' with r'; apply (flag_zone_flag2 _ _ _ _ _ H (refl_equal _)).
  repeat (destruct lw as [lw | lw]; try solve[rewrite <- lw; red;auto 10]).
 rewrite <- t.
 apply (IH _ _ (refl_equal _)); solve[auto].
subst; match goal with q : _ = _ |- _ => injection q; intros; subst end.
assert (t:=large_wait_pred b2 i3 flag1 flag0 0 i4 j4 j2 r' r'' ins4 lw).
destruct t as [st4 | lw4];[ assumption | | ].
 match goal with u : sos_step _ _ _ _ |- _ => rewrite <- st4 in u end.
 do 2 match goal with u : sos_step _ _ _ _ |- _ => inversion u; clear u end.
 match goal with i : _ |- _ => 
   rewrite (assign_val_num r' turn 0 i r''); [discriminate | assumption]
 end.
match goal with u : _ |- _ =>
 rewrite <- (large_wait_preserve b2 i3 flag1 flag0 0 i4 j4 _ _ _ lw4 u)
end.
 apply (IH _ _ (refl_equal _) lc lw4).
Qed.

Lemma wait_turn2 :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i -> large_critical b2 i3 flag1 flag0 0 i4 j2 ->
    large_wait b1 i1 flag0 flag1 1 i2 j1 ->
    val r' turn <> Some 0.
intros r i r' j1 j2 H; revert j1 j2; apply star_star' in H.
induction H as [ | i' i'' r' r'' H IH H0].
 intros j1 j2 q lc lw; injection q; do 2 intro; subst.
 solve[repeat (destruct lw as [ab | lw]; try discriminate); destruct lw].
intros j1 j2 q lc lw; apply star'_star in H; rewrite q in H0.
destruct (states'' _ _ _ _ _ _ H H0) as [j3 [j4 [q' [ins3 ins4]]]].
inversion H0;try solve[subst; discriminate |
   subst; match goal with q : _ , ins : _|- _ => injection q; intros; subst;
      solve[case (not_in_states_par _ _ _ _ _ _ _ _ ins)]
   end]; clear H0.
 subst; match goal with q : _ = _ |- _ => injection q; intros; subst end.
 assert (t:=large_wait_pred b1 i1 flag0 flag1 1 i2 j3 j1 r' r'' ins3 lw).
 destruct t as [st3 | lw3];[ assumption | | ].
  match goal with u : sos_step _ _ _ _ |- _ => rewrite <- st3 in u end.
  do 2 match goal with u : sos_step _ _ _ _ |- _ => inversion u; clear u end.
  match goal with i : _ |- _ => 
    rewrite (assign_val_num r' turn 1 i r''); [discriminate | assumption]
  end.
 match goal with u : _ |- _ =>
  rewrite <- (large_wait_preserve b1 i1 flag0 flag1 1 i2 j3 _ _ _ lw3 u)
 end.
 apply (IH _ _ (refl_equal _) lc lw3).

subst; match goal with q: _, u : _ |- _ => 
  injection q; intros; subst; rename u into st; clear q;
  destruct (large_critical_pred _ _ _ _ _ _ _ _ _ _ ins4 lc st) as
    [[jc4 t] | [j4q t]]
end.
 rewrite <- jc4 in st.
 apply (wait_exit_case b2 i3 flag1 flag0 0 i4 j2 r'); auto.
 replace r'' with r'; apply (flag_zone_flag1 _ _ _ _ _ H (refl_equal _)).
 repeat (destruct lw as [lw | lw]; try solve[rewrite <- lw; red;auto 10]).
rewrite <- t.
apply (IH _ _ (refl_equal _)); solve[auto].
Qed.

Lemma in_states_turn_or :
  forall b i f f' index i' j j' r r', in_states b i f f' index i' j ->
   f <> turn ->
   sos_step r j j' r' -> val r' turn = val r turn \/ val r' turn = Some index.
intros b i f f' index i' j j' r r' [[j1 [j1p H]] | [ [j1 [j1p H]] | H]] fnt st;
  [apply sym_equal in H | apply sym_equal in H | ]; repeat 
    (destruct H as [H | H]); try contradiction; rewrite <- H in st;
   unfold prefix, wait, in_wait, enter, enter_middle, set_turn, start_wait,
       end_wait, critical, end_critical, peterson_scheme, restart in st;
   repeat (match goal with u : sos_step _ (_ ++ _)%i _ _ |- _ => 
                   inversion u; clear u
           | u: sos_step _ (while _ _) _ _ |- _ => inversion u;
               solve[replace r' with r;left; auto]
           | u: sos_step _ skip _ _ |- _ => inversion u
           end; try (solve[replace r' with r;[left; auto]|
                     match goal with u : sos_step _ ?j1 _ _ |- _ => 
                       assert (t1:preserve j1 turn) by 
                          (simpl in j1p; tauto);
                       rewrite <- (preserve_sem' _ _ t1 _ _ _ H11); auto
                     end |
                     match goal with
                       u : sos_step _ (assign _ (aint ?v)) _ _ |- _ =>
                       inversion u;
                       match goal with
                         h : a_eval _ (aint _) _ |- _ => inversion h; subst;
                         rewrite <- (s_update_diff r f v r');auto
                       end
                     end])).
solve[right; eapply (assign_val_num r turn index); eauto].
Qed.

Lemma wait_turn_or :
  forall r i r' j1 j2, sos_star r peterson_program i r' ->
    i = (j1||j2)%i ->
    large_wait b1 i1 flag0 flag1 1 i2 j1 \/
    (exists j, preserve_all j (flag0::flag1::turn::nil) /\
       critical b1 i1 flag0 flag1 1 i2 j = j1) ->
    val r' turn = Some 0 \/ val r' turn = Some 1.
intros r i r' j1 j2 H; apply star_star' in H; revert j1 j2.
induction H as [ | i' i'' r' r'' H IH H0].
 intros j1 j2 q; injection q; intros _ q1 [H' | [j0 [j0p H']]];
  rewrite <- q1 in H'.
  repeat destruct H' as [H' | H']; try discriminate.
 discriminate.
intros j1 j2 q; apply star'_star in H; rewrite q in H0.
destruct (states'' _ _ _ _ _ _ H H0) as [j3 [j4 [q' [ins3 ins4]]]].
inversion H0;try solve[subst; discriminate |
   subst; match goal with q : _ , ins : _|- _ => injection q; intros; subst;
      solve[case (not_in_states_par _ _ _ _ _ _ _ _ ins)]
   end]; clear H0;
   match goal with u : sos_step _ _ _ _ |- _ => rename u into st end.
 subst; match goal with u : _ = _ |- _ => injection u; do 2 intro; subst end.
 intros [[H' | H'] | [j0 [j0p H']]].
   rewrite <- H' in st.
   match goal with v : _ |- _ =>
        assert (t1 := start_wait_pred _ _ _ _ _ _ _ _ _ ins3 v) 
   end; rewrite <- t1 in st.
   do 2 match goal with u : sos_step _ _ _ _ |- _ => inversion u; clear u end.
   right; eapply assign_val_num; solve [eauto].
  repeat destruct H' as [H' | H'];
   rewrite <- H' in st;
   (destruct (wait_pred _ _ _ _ _ _ _ _ _ ins3 st) as [t1 | t1] ||
    assert (t1:= in_wait_pred _ _ _ _ _ _ _ _ _ ins3 st) ||
    assert (t1:= end_wait_pred _ _ _ _ _ _ _ _ _ ins3 st));
   assert (t2:large_wait b1 i1 flag0 flag1 1 i2 j3) by (red; auto);
   rewrite <- (large_wait_preserve _ _ _ _ _ _ _ _ _ _ t2 st);
   apply (IH _ _ (refl_equal _)); solve[auto].
 rewrite <- H' in st.
 destruct (critical_pred _ _ _ _ _ _ _ _ _ _ ins3 st) as [[j' [jp t1]] | t1].
  rewrite t1 in st; assert (jp' : preserve j' turn) by (simpl in jp; tauto).
  do 3 match goal with u:sos_step _ _ _ _ |- _ => 
       rewrite <- (preserve_sem' _ _ jp' _ _ _ u) || inversion u; clear u end.
  apply (IH _ _ (refl_equal _)); subst; right; exists j'; solve[auto].
 assert (t2 : large_wait b1 i1 flag0 flag1 1 i2 j3) by (red; tauto).
 rewrite <- (large_wait_preserve _ _ _ _ _ _ _ _ _ _ t2 st);
  apply (IH _ _ (refl_equal _)); left; assumption.
intros bigh.
subst; match goal with u : _ = _ |- _ => injection u; do 2 intro; subst end.
assert (t1:flag1 <> turn) by tauto.
destruct (in_states_turn_or b2 i3 flag1 flag0 0 i4 j4 j2 r' r'' ins4 t1 st)
 as [t|t].
 solve[rewrite t; apply (IH _ _ (refl_equal _)); auto].
rewrite t; auto.
Qed.
 
Definition peterson_sound_prop :=
  forall r i r',
  sos_star r peterson_program i r' ->
  forall i' i'', i <> ((critical b1 i1 flag0 flag1 1 i2 i')||
                       (critical b2 i3 flag1 flag0 0 i4 i''))%i.

Lemma exclusion:  forall r i r',
  sos_star r peterson_program i r' ->
  forall i' i'', i <> ((critical b1 i1 flag0 flag1 1 i2 i')||
                       (critical b2 i3 flag1 flag0 0 i4 i''))%i.
intros r i r' H; apply star_star' in H.
assert (p : forall i' i'',
            i = (critical b1 i1 flag0 flag1 1 i2 i' ||
                 critical b2 i3 flag1 flag0 0 i4 i'')%i ->
            preserve_all i' (flag0::flag1::turn::nil) /\
            preserve_all i'' (flag0::flag1::turn::nil)).
 intros i' i'' q; rewrite q in H; apply star'_star in H.
 assert (t := states' _ _ _ _ H); split.
  destruct t as [[[j [jp jq]] | [[j [jp jq]] | t]] _].
    discriminate.
   injection jq; intro; subst; assumption.
  repeat (destruct t as [tq | t]; [discriminate | ]); contradiction.
 destruct t as [_ [[j [jp jq]] | [[j [jp jq]] | t]]].
   discriminate.
  injection jq; intro; subst; assumption.
 repeat (destruct t as [tq | t]; [discriminate | ]); contradiction.
assert (Main: forall k k', i = (k || k')%i ->
  ~(large_critical b1 i1 flag0 flag1 1 i2 k /\
    large_critical b2 i3 flag1 flag0 0 i4 k'));
 [ | intros i' i'' q; apply (Main _ _ q);
     split; left;[exists i' | exists i''];
     (split;[destruct (p _ _ q); solve[auto]|reflexivity])].
clear p.
induction H as [|i' i'' r' r'' H IH H0].
 intros k k' q; injection q; do 2 intro; subst.
 intros [[[j [_ jq]] | w] _]; discriminate.
intros k k' q [lc1 lc2]; rewrite q in H0; apply star'_star in H.
destruct (states'' _ _ _ _ _ _ H H0) as [j1 [j2 [q' [ins1 ins2]]]].
rewrite q' in H0.
inversion H0;try (subst; (case (not_in_states_par _ _ _ _ _ _ _ _ ins2) ||
         case (not_in_states_par _ _ _ _ _ _ _ _ ins1))).
 match goal with u : _ |- _ =>
  destruct (large_critical_pred _ _ _ _ _ _ _ _ _ _ ins1 lc1 u) as
    [[w _]| [lc3 _]]; rename u into st
 end.
  subst.
  assert (t:val r' turn <> Some 0)
   by (apply (wait_turn2 r _ r' _ _ H (refl_equal _) lc2); red; simpl; auto).
  assert (t3 : sos_star r peterson_program (k || k') r'').
   apply sos_star_trans with (1:= H); apply (SOS7 _ _ _ _ _ _ H0 (SOS6 _ _)).
  assert (t1:=large_critical_flag2 r _ r'' _ _ t3 (refl_equal _) lc2).
  assert (t2:=wait_exit_case _ _ _ _ _ _ _ _ _ t1 lc1 st).
  assert (t4: large_wait b1 i1 flag0 flag1 1 i2 (wait b1 i1 flag0 flag1 1 i2))
    by (red; auto).
  assert (t5:=large_wait_preserve _ _ _ _ _ _ _ _ _ _ t4 st).
  destruct (wait_turn_or r _ _ _ _ H (refl_equal _));
     [left;auto| | ];subst;contradiction.
 subst.
 solve[apply (IH _ _ (refl_equal _)); auto].
match goal with u : _ |- _ =>
  destruct (large_critical_pred _ _ _ _ _ _ _ _ _ _ ins2 lc2 u) as
   [[w _]| [lc4 _]]; rename u into st
end.
 subst.
 assert (t:val r' turn <> Some 1)
   by (apply (wait_turn1 r _ r' _ _ H (refl_equal _) lc1); red; simpl; auto).
 assert (t3 : sos_star r peterson_program (k || k') r'').
  apply sos_star_trans with (1:= H); apply (SOS7 _ _ _ _ _ _ H0 (SOS6 _ _)).
 assert (t1:=large_critical_flag1 r _ r'' _ _ t3 (refl_equal _) lc1).
 assert (t2:=wait_exit_case _ _ _ _ _ _ _ _ _ t1 lc2 st).
 assert (t4: large_wait b2 i3 flag1 flag0 0 i4 (wait b2 i3 flag1 flag0 0 i4))
    by (red; auto).
 assert (t5:=large_wait_preserve _ _ _ _ _ _ _ _ _ _ t4 st).
 destruct (wait_turn_or r _ _ _ _ H (refl_equal _));try (subst; contradiction).
 destruct lc1 as [[j [jp jq]]|w].
  solve[right; exists j; split; auto].
 solve[left; red; auto].
subst.
solve[apply (IH _ _ (refl_equal _)); auto].
Qed.