HyPre.pred.BarrierSync
From Coq Require Import
Classical_Prop
ClassicalChoice.
Lemma choice2 (A B C : Type) (R : A -> C -> B -> Prop)
: (forall (x : A) (z : C), exists y : B, R x z y) -> exists f : A -> C -> B, forall (x : A) (z : C), R x z (f x z).
Proof.
intros.
specialize (choice (uncurry R)) as Q.
exploit' Q.
- intros.
destruct x as [a c].
specialize (H a c).
destructH.
exists y.
cbn.
assumption.
- destructH.
exists (curry f).
intros.
specialize (Q (x,z)).
cbn in Q.
eapply Q.
Qed.
Lemma choice3 (A B C D : Type) (R : A -> B -> C -> D -> Prop)
: (forall (a : A) (b : B) (c : C), exists d : D, R a b c d) ->
exists f : A -> B -> C -> D, forall (a : A) (b : B) (c : C), R a b c (f a b c).
Proof.
intros.
specialize (choice (fun abc : A * B * C => let (ab,c) := abc in
let (a,b) := ab in
R a b c)) as Q.
exploit' Q.
- intros.
destruct x as [ [a b] c].
specialize (H a b c).
destructH.
exists d.
cbn.
assumption.
- destructH.
exists (fun a b c => f (a,b,c)).
intros.
specialize (Q (a,b,c)).
cbn in Q.
eapply Q.
Qed.
In this module we show that we can define a synchroniser barrier_sync,
using a function bl_step : Input -> list State -> State * list State.
Later we show that the existence of bl_step can be derived
if some property holds always eventually with choice.
Import VecNatNotations.
Section with_rad.
Context {k : nat}.
Context `{RS : rad_semantics}.
Context (state0 : State).
(* bl := barrier_lockstep *)
Context (bl_step : Vector.t Input k -> Vector.t (list State) k -> Vector.t (State * list State) k).
Definition vbl_nstep
: Vector.t Input k -> Vector.t nat k -> vecnat k
:= fun iv vn => Vector.map (fun x => S (length (snd x)))
(bl_step iv (Vector.map2 (construct_trace sem) vn iv)).
Lemma vex_bl_sync0 (P : Vector.t Input k -> vecnat k -> Prop)
: exists (bl_sync' : Vector.t Input k -> Vector.t nat k -> Vector.t nat k),
(forall i a, (fun i a z => (P i a -> z = vbl_nstep i a)
/\ (~ P i a -> z = Vector.const 1 k)) i a (bl_sync' i a)).
Proof.
eapply choice2.
intros.
destruct (classic (P x z)).
- exists (vbl_nstep x z).
firstorder.
- exists (Vector.const 1 k).
firstorder.
Qed.
Lemma vex_bl_sync' (P : Vector.t Input k -> vecnat k -> Prop)
: exists (bl_sync' : Vector.t Input k -> Vector.t nat k -> Vector.t nat k),
(forall i a, (P i a -> bl_sync' i a = vbl_nstep i a)
/\ (~ P i a -> bl_sync' i a = Vector.const 1 k))
/\ forall iv, Synchroniser (bl_sync' iv) (fun _ _ => 1).
Proof.
specialize vex_bl_sync0 with (P:=P) as Q.
destructH.
exists bl_sync'.
split_conj;eauto.
intros.
econstructor.
intros.
cbn.
rewrite Vec_nth_map2.
match goal with
|- _ < ?x + _ => enough (0 < x);[lia|]
end.
specialize (Q iv a).
destructH.
destruct (classic (P iv a)).
- rewrite Q0;eauto.
unfold vbl_nstep.
setoid_rewrite Vector.nth_map. 2:reflexivity.
lia.
- setoid_rewrite Q1;eauto.
setoid_rewrite Vector.const_nth.
lia.
Qed.
Definition vbl_cons
: Vector.t Input k -> Vector.t (list State) k -> Vector.t (list State) k
:= fun i a => Vector.map (fun bb : State * list State => let (b0,bs) := bb in b0 :: bs) (bl_step i a).
Lemma vbl_cons_vl_len a iv
(Hsem : Vector.Forall2 sem iv a)
: vl_len (vbl_cons iv a) = vbl_nstep iv (vl_len a).
Proof.
unfold vbl_nstep.
eapply Vector.eq_nth_iff.
intros.
subst p2.
setoid_rewrite Vector.nth_map. 2,3:reflexivity.
unfold vbl_cons.
setoid_rewrite Vector.nth_map. 2:reflexivity.
replace (Vector.map2 (construct_trace sem) (vl_len a) iv) with a.
- destruct (bl_step iv a [[p1]]).
cbn.
reflexivity.
- eapply Vector.eq_nth_iff.
intros.
subst p2.
setoid_rewrite Vector.nth_map2. 2,3:reflexivity.
setoid_rewrite Vector.nth_map. 2:reflexivity.
setoid_rewrite construct_trace_length;eauto.
eapply Vec_Forall2_forall2;eauto.
Qed.
Lemma vl_len_eq_vl_app_sem_eq (iv a b c : Vector.t _ k)
(Hb : Vector.Forall2 sem iv (b +vl+ a))
(Hc : Vector.Forall2 sem iv (c +vl+ a))
(Hlen : vl_len b = vl_len c)
: b = c.
Proof.
enough (b +vl+ a = c +vl+ a).
- eapply Vector.eq_nth_iff.
intros. subst p2.
eapply Vector.eq_nth_iff in H. 2:reflexivity.
setoid_rewrite veclist_app_nth in H.
eapply app_inv_tail;eauto.
- eapply vsem_leneq_eq;eauto.
setoid_rewrite vl_len_vl_app_vn_add.
rewrite Hlen.
reflexivity.
Qed.
Lemma vbl_sync_cons_eq b a iv
(Hbls_sem : Vector.Forall2 sem iv (vbl_cons iv a +vl+ a))
(Hbsem : Vector.Forall2 sem iv (b +vl+ a))
(Hlen : vl_len b = vbl_nstep iv (vl_len a))
: b = (let (b0, bs) := (vec_unzip (bl_step iv a)) in
b0 :vl: bs).
Proof.
setoid_rewrite <-vbl_cons_vl_len in Hlen.
2: eapply Forall2_vl_app22;eauto.
2: eapply sem_prefix_containing;eauto.
eapply vl_len_eq_vl_app_sem_eq in Hlen;eauto.
unfold vbl_cons in *.
rewrite Hlen.
setoid_rewrite surjective_pairing with (p:=vec_unzip (bl_step iv a)).
setoid_rewrite vec_unzip_fst.
setoid_rewrite vec_unzip_snd.
generalize (bl_step iv a).
intros.
clear.
dependent induction t;cbn.
- reflexivity.
- f_equal.
+ destruct h;cbn.
reflexivity.
+ eapply IHt.
Qed.
End with_rad.
Section with_rad.
Context `{RS : rad_semantics}.
Context (state0 : State).
(* bl := barrier_lockstep *)
Context (bl_step : Input -> list State -> State * list State).
Definition bl_nstep
: Input -> nat -> nat
:= fun i n => S (length (snd (bl_step i (construct_trace sem n i)))).
Definition Q {P : _ -> _ -> Prop} (i : Input) (n : nat) c : Prop
:= (P i n -> c = bl_nstep i n) /\ (~ (P i n) -> c = 1).
Lemma ex_bl_nstep' (P : Input -> nat -> Prop)
: exists (bl_nstep' : Input -> nat -> nat),
forall i n, @Q P i n (bl_nstep' i n).
Proof.
eapply choice2 with (R:=@Q P).
intros.
unfold Q.
destruct (classic (P x z)).
- exists (bl_nstep x z).
firstorder.
- exists 1.
firstorder.
Qed.
Definition bl_cons
: Input -> list State -> list State
:= fun i a => let (b0,bs) := bl_step i a in b0 :: bs.
Lemma bl_cons_eq i a
(Hbl_sem : sem i a -> sem i (bl_cons i a ++ a))
: forall b, sem i (b ++ a)
-> length b = bl_nstep i (length a)
-> b = bl_cons i a.
Proof.
clear state0.
intros ? Hsemb Hbar.
eapply sem_safe_app in Hsemb as Hsem;eauto.
unfold bl_nstep in Hbar.
assert (construct_trace sem (length a) i = a).
{
eapply sem_leneq_eq;eauto.
- eapply construct_trace_sem.
- eapply construct_trace_len.
}
setoid_rewrite H in Hbar.
eapply Hbl_sem in Hsem.
unfold bl_cons in *.
destruct (bl_step i a) as [b0 bs].
cbn in Hbar.
enough (b ++ a = (b0 :: bs) ++ a).
{
clear - H0.
eapply length_app_eq in H0;eauto.
destruct H0;eauto.
}
eapply sem_leneq_eq;eauto.
setoid_rewrite app_length.
cbn.
lia.
Qed.
Section with_k.
Context {k : nat}.
Definition bl_sync (iv : Vector.t Input k)
: Vector.t nat k -> Vector.t nat k
:= fun vn => Vector.map2 bl_nstep iv vn.
(* Lemma vec_forall2_map2_eq (k : nat) (X Y Z : Type) (f : X -> Y -> Z) (xl1 xl2 : Vector.t X k)
: Vector.Forall2 (fun x1 y : X => f x1 y1 = f x2 y2) xl1 xl2 -> Vector.map f xl1 = Vector.map f xl2*)
Lemma ex_bl_sync' (P : Input -> nat -> Prop)
: exists (bl_sync' : Vector.t Input k -> Vector.t nat k -> Vector.t nat k),
(forall i a, (Vec_Forall3 (fun x y z => (P x y -> z = bl_nstep x y)
/\ (~ P x y -> z = 1)) i a (bl_sync' i a)))
/\ forall iv, Synchroniser (bl_sync' iv) (fun _ _ => 1).
Proof.
specialize (ex_bl_nstep' P) as Q'.
destructH.
unfold Q in *.
exists (Vector.map2 bl_nstep').
split.
- intros.
eapply vec_forall3_forall.
intros.
specialize (Q' (i [[i0]]) (a[[i0]])).
split;intros.
+ destruct Q' as [Q' _].
rewrite Vec_nth_map2.
now firstorder.
+ destruct Q' as [_ Q'].
rewrite Vec_nth_map2.
now firstorder.
- econstructor.
intros.
cbn.
specialize (Q' (iv [[i]]) (a [[i]])).
destruct Q' as [Q1 Q2].
destruct (classic (P (iv [[i]]) (a [[i]]))).
+ eapply Q1 in H0.
rewrite Vec_nth_map2.
rewrite Vec_nth_map2.
rewrite H0.
cbn.
lia.
+ eapply Q2 in H0.
rewrite Vec_nth_map2.
rewrite Vec_nth_map2.
rewrite H0.
lia.
Qed.
(* What does this lemma mean?
if bl_step is semantic preserving
and bl_sync corresponds to the vl-length of b
and b satisfies semantics
then b can be written using vec_unzip and bl_step
*)
Lemma bl_sync_cons_eq b a iv
(Hbls_sem : Vector.Forall2 (fun i a => sem i a -> sem i (bl_cons i a ++ a)) iv a)
(Hsem : Vector.Forall2 sem iv (b +vl+ a))
(Hlen : vl_len b = bl_sync iv (vl_len a))
: b = (let (b0, bs) := vec_unzip (Vector.map2 (fun i a => bl_step i a) iv a) in
b0 :vl: bs).
Proof.
setoid_rewrite vec_unzip_map2.
eapply Vector.eq_nth_iff.
intros. subst p2. rename p1 into i.
eapply Vector.eq_nth_iff with (p1:=i) (p2:=i) in Hlen. 2:reflexivity.
setoid_rewrite Vec_nth_map2.
setoid_rewrite Vec_nth_map2 in Hlen.
setoid_rewrite Vector.nth_map in Hlen. 2,3:reflexivity.
eapply bl_cons_eq in Hlen.
- rewrite Hlen.
unfold bl_cons.
setoid_rewrite Vec_nth_map2.
destruct (bl_step (iv[[i]]) (a[[i]])) as [b0 bs].
cbn.
reflexivity.
- intros.
eapply Vec_Forall2_forall2 in Hbls_sem.
eapply Hbls_sem;eauto.
- eapply Vec_Forall2_forall2 in Hsem.
setoid_rewrite Vec_nth_map2 in Hsem.
eassumption.
Qed.
Global Instance bl_Sync (iv : Vector.t Input k)
: Synchroniser (bl_sync iv) (fun _ _ => 1).
Proof.
econstructor.
intros.
cbn.
rewrite Vec_nth_map2.
match goal with
|- _ < ?x + _ => enough (0 < x);[lia|]
end.
setoid_rewrite Vec_nth_map2.
unfold bl_nstep.
lia.
Qed.
End with_k.
End with_rad.
Require ClassicalChoice.
From Coq Require Import Classical_Prop.
Import VectorListNotations.
Module BarrierSyncChoice.
In this module, AC is used
to derive the existence of some bl_step function from an always-eventually property
Export ClassicalChoice.
Section with_rad.
Context `{RS : rad_semantics}.
Context {k : nat}.
Context (is_B : Fin.t k -> Vector.t (list State) k -> State -> bool).
Section with_live_barrier.
Definition live_B (j : Fin.t k) (i : Input) (a : Vector.t (list State) k)
:= sem i (a[[j]]) -> exists b0 bs, sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true.
(* Lemma live_B_extended i a
: live_B i a -> exists b0 bs, (sem i a -> sem i (b0 :: bs ++ a)) /\ is_B b0.
Proof.
intros.
destruct (dec_sem sem i a).
- eapply H in s.
destructH.
exists b0, bs.
split;auto.
- specialize (live_B i ).
exploit' live_B;eapply rooted|.
destruct live_B,H.
exists x, x0. split.
+ intro. contradiction.
+ tauto.
Qed.*)
Lemma is_not_B_dec
: forall j a b, {is_B j a b = false} + {~ is_B j a b= false}.
Proof.
intros.
destruct (is_B j a b).
- right.
intro N.
congruence.
- left.
congruence.
Qed.
Lemma Exists_last {Y : Type} (P : Y -> Prop) (Hdec : forall x, {P x} + {~ P x}) xl
(Hex : Exists P xl)
: exists xl1 x xl2, xl = xl1 ++ x :: xl2 /\ P x /\ Forall (fun y => ~ P y) xl2.
Proof.
clear - Hex Hdec.
induction xl;inversion Hex.
- subst a l.
specialize (Exists_dec P xl Hdec) as Q.
destruct Q.
+ eapply IHxl in e.
destructH.
exists (x :: xl1), x0, xl2.
split_conj;eauto.
cbn.
f_equal.
assumption.
+ eapply Forall_Exists_neg in n.
exists [], x, xl.
split_conj;eauto.
- subst a l.
eapply IHxl in H0.
destructH.
exists (x :: xl1), x0, xl2.
split_conj;eauto.
cbn.
f_equal.
assumption.
Qed.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
Lemma live_B_minimal
: forall j i a, live_B j i a -> exists b0 bs, sem i (a[[j]]) -> sem i (b0 :: bs ++ a[[j]])
/\ is_B j a b0 = true
/\ (Forall (fun b => is_B j a b = false)) bs.
Proof.
intros.
destruct (dec_sem dec_St sem i (a[[j]])).
- unfold live_B in H.
eapply H in s.
destructH.
revert b0 s0 s1.
induction bs;intros.
+ cbn in s0.
exists b0, [].
intros.
cbn.
split_conj;eauto.
+ specialize (Forall_dec (fun b : State => is_B j a b = false) (is_not_B_dec j a) (a0 :: bs)) as Q.
destruct Q as [Q|Q].
* exists b0, (a0 :: bs).
intros.
split_conj;eauto.
* eapply neg_Forall_Exists_neg in Q. 2:eapply is_not_B_dec.
eapply Exists_impl in Q.
2: intro;eapply Bool.not_false_is_true.
eapply Exists_last in Q;eauto.
destructH.
eexists;eexists;intros;eauto.
split_conj;cycle 1.
-- eapply Q2.
-- eapply Forall_impl. 2: eapply Q3.
clear. intros.
eapply Bool.not_true_is_false;eauto.
-- rewrite Q0 in s0.
rewrite app_comm_cons in s0.
rewrite app_comm_cons in s0.
rewrite <-app_assoc in s0.
eapply sem_safe_app in s0;eauto.
-- clear;intros.
destruct (is_B j a x);[left|right];eauto.
- exists state0, (a[[j]]).
intros.
contradiction.
Qed.
Definition live_B_minimal_def' (jia : Fin.t k * Input * Vector.t (list State) k) (bb : State * list State)
:= let (ji,a) := jia in
let (j,i) := ji in
let (b0,bs) := bb in
sem i (a[[j]]) -> sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true /\ Forall (fun b => is_B j a b = false) bs.
Lemma bl_ex_step'
(Hlive : forall i a x, live_B i a x)
: exists (bl_step' : (Fin.t k * Input * Vector.t (list State) k) -> (State * list State)),
forall (jia : Fin.t k * Input * Vector.t (list State) k), live_B_minimal_def' jia (bl_step' jia).
Proof.
eapply choice.
intros.
destruct x as [ [j i] a ].
specialize (live_B_minimal j i a (Hlive j i a)) as Hspec.
destructH.
exists (b0,bs).
firstorder.
Qed.
Lemma bl_ex_step
(Hlive : forall i a x, live_B i a x)
: exists (bl_step : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall j (i : Input) (a : Vector.t (list State) k), live_B_minimal_def' (j,i,a) (bl_step j i a).
Proof.
specialize (bl_ex_step' Hlive) as Hspec.
destructH.
exists (fun j i a => bl_step' (j,i,a)).
intros.
specialize (Hspec (j,i,a)).
assumption.
Qed.
Definition live_or_not j (i : Input) (a : Vector.t (list State) k) (bb : State * list State)
:= live_B_minimal_def' (j,i,a) bb
\/ forall bs, sem i (bs ++ a[[j]]) -> Forall (fun b => is_B j a b = false) bs.
Lemma bl_ex_step_or
: exists (bl_step' : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall j (i : Input) (a : Vector.t (list State) k), live_or_not j i a (bl_step' j i a).
Proof.
eapply choice3.
intros.
rename a into j.
rename b into i.
rename c into a.
destruct (classic (sem i (a[[j]]) -> exists b0 bs, sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true)).
all: unfold live_or_not.
- specialize (live_B_minimal j i a H) as Hspec.
destructH.
exists (b0,bs).
left.
firstorder.
- exists (state0,[]).
right.
intros.
cbn in H0.
eapply not_imply_elim2 in H.
specialize (not_ex_all_not)
with (P:=fun (bb : State * list State)
=> sem i (fst bb :: snd bb ++ a[[j]]) /\ is_B j a (fst bb) = true) as Q.
exploit' Q.
{
contradict H.
clear - H.
destructH.
destruct n as [b0 bs].
exists b0, bs.
split;auto.
}
induction bs as [|b0 bs].
1: econstructor.
econstructor.
+ specialize (Q (b0,bs)).
eapply not_and_or in Q.
destruct Q.
* cbn in H1.
contradiction.
* cbn in H1.
eapply Bool.not_true_is_false.
assumption.
+ eapply IHbs.
cbn in H0.
eapply safe;eauto.
Qed.
Lemma bl_ex_step_or2
: exists (bl_step' : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall (i : Vector.t Input k) (a : Vector.t (list State) k) j, live_or_not j (i[[j]]) a (bl_step' j (i[[j]]) a).
Proof.
specialize bl_ex_step_or as Q.
destructH.
exists bl_step'.
intros.
eapply Q.
Qed.
End with_live_barrier.
End with_rad.
End BarrierSyncChoice.
Import BarrierSyncChoice.
Section with_si.
Context {Input State : Type}.
Context (sem : Input -> list State -> Prop).
Context {Hrad : rad_semantics sem}.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
Context (is_B : State -> bool).
Definition live_B0 (i : Input) (a : list State)
:= sem i a -> exists b0 bs, sem i (b0 :: bs ++ a) /\ is_B b0 = true.
Definition live_B_minimal_def0 (ia : Input * list State) (bb : State * list State)
:= let (i,a) := ia in
let (b0,bs) := bb in
sem i a -> sem i (b0 :: bs ++ a) /\ is_B b0 = true /\ Forall (fun b => is_B b = false) bs.
Definition fun_vec1 {X Y : Type} (f : X -> Y)
: Fin.t 1 -> Vector.t X 1 -> Y.
Proof.
intros.
inversion X0.
exact (f h).
Defined.
Definition f1 : Fin.t 1 := (@Fin.F1 0).
Definition v1 {X : Type} (x : X) := (Vector.cons _ x _ (Vector.nil _)).
Definition t1 {X Y Z : Type} (f : Fin.t 1 -> X -> Vector.t Y 1 -> Z)
: X -> Y -> Z
:= fun x y => f f1 x (v1 y).
Lemma bl_ex_step0
: (forall (i : Input) (a : list State), live_B0 i a) ->
exists bl_step : Input -> list State -> State * list State,
forall (i : Input) (a : list State),
live_B_minimal_def0 (i, a) (bl_step i a).
Proof.
intros.
assert (forall (j : Fin.t 1) (i : Input) (a : Vector.t (list State) 1), live_B (sem:=sem) (k:=1) (fun _ _ => is_B) j i (a)) as Q.
- unfold live_B, live_B0 in *.
intros.
eapply H in H0.
destructH.
eexists;eauto.
- eapply bl_ex_step in Q. 2: eapply state0. 2: eapply dec_St.
destructH.
eexists;eauto.
unfold live_B_minimal_def', live_B_minimal_def0 in *.
intros.
specialize (Q f1 i (v1 a)).
instantiate (1:=t1 bl_step).
unfold t1.
eapply Q.
Qed.
Definition live_or_not0 (i : Input) (a : list State) (bb : State * list State)
:= live_B_minimal_def0 (i,a) bb
\/ forall bs, sem i (bs ++ a) -> Forall (fun b => is_B b = false) bs.
Lemma bl_ex_step_or0
: exists (bl_step' : Input -> list State -> (State * list State)),
forall (i : Input) (a : list State), live_or_not0 i a (bl_step' i a).
Proof.
specialize (@bl_ex_step_or Input State sem Hrad 1 (fun _ _ => is_B) state0 dec_St) as Q.
destructH.
eexists;eauto.
unfold live_or_not, live_or_not0, live_B_minimal_def', live_B_minimal_def0 in *.
intros;eauto.
instantiate (1:=t1 bl_step').
unfold t1.
eapply Q.
Qed.
End with_si.
Section with_rad.
Context `{RS : rad_semantics}.
Context {k : nat}.
Context (is_B : Fin.t k -> Vector.t (list State) k -> State -> bool).
Section with_live_barrier.
Definition live_B (j : Fin.t k) (i : Input) (a : Vector.t (list State) k)
:= sem i (a[[j]]) -> exists b0 bs, sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true.
(* Lemma live_B_extended i a
: live_B i a -> exists b0 bs, (sem i a -> sem i (b0 :: bs ++ a)) /\ is_B b0.
Proof.
intros.
destruct (dec_sem sem i a).
- eapply H in s.
destructH.
exists b0, bs.
split;auto.
- specialize (live_B i ).
exploit' live_B;eapply rooted|.
destruct live_B,H.
exists x, x0. split.
+ intro. contradiction.
+ tauto.
Qed.*)
Lemma is_not_B_dec
: forall j a b, {is_B j a b = false} + {~ is_B j a b= false}.
Proof.
intros.
destruct (is_B j a b).
- right.
intro N.
congruence.
- left.
congruence.
Qed.
Lemma Exists_last {Y : Type} (P : Y -> Prop) (Hdec : forall x, {P x} + {~ P x}) xl
(Hex : Exists P xl)
: exists xl1 x xl2, xl = xl1 ++ x :: xl2 /\ P x /\ Forall (fun y => ~ P y) xl2.
Proof.
clear - Hex Hdec.
induction xl;inversion Hex.
- subst a l.
specialize (Exists_dec P xl Hdec) as Q.
destruct Q.
+ eapply IHxl in e.
destructH.
exists (x :: xl1), x0, xl2.
split_conj;eauto.
cbn.
f_equal.
assumption.
+ eapply Forall_Exists_neg in n.
exists [], x, xl.
split_conj;eauto.
- subst a l.
eapply IHxl in H0.
destructH.
exists (x :: xl1), x0, xl2.
split_conj;eauto.
cbn.
f_equal.
assumption.
Qed.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
Lemma live_B_minimal
: forall j i a, live_B j i a -> exists b0 bs, sem i (a[[j]]) -> sem i (b0 :: bs ++ a[[j]])
/\ is_B j a b0 = true
/\ (Forall (fun b => is_B j a b = false)) bs.
Proof.
intros.
destruct (dec_sem dec_St sem i (a[[j]])).
- unfold live_B in H.
eapply H in s.
destructH.
revert b0 s0 s1.
induction bs;intros.
+ cbn in s0.
exists b0, [].
intros.
cbn.
split_conj;eauto.
+ specialize (Forall_dec (fun b : State => is_B j a b = false) (is_not_B_dec j a) (a0 :: bs)) as Q.
destruct Q as [Q|Q].
* exists b0, (a0 :: bs).
intros.
split_conj;eauto.
* eapply neg_Forall_Exists_neg in Q. 2:eapply is_not_B_dec.
eapply Exists_impl in Q.
2: intro;eapply Bool.not_false_is_true.
eapply Exists_last in Q;eauto.
destructH.
eexists;eexists;intros;eauto.
split_conj;cycle 1.
-- eapply Q2.
-- eapply Forall_impl. 2: eapply Q3.
clear. intros.
eapply Bool.not_true_is_false;eauto.
-- rewrite Q0 in s0.
rewrite app_comm_cons in s0.
rewrite app_comm_cons in s0.
rewrite <-app_assoc in s0.
eapply sem_safe_app in s0;eauto.
-- clear;intros.
destruct (is_B j a x);[left|right];eauto.
- exists state0, (a[[j]]).
intros.
contradiction.
Qed.
Definition live_B_minimal_def' (jia : Fin.t k * Input * Vector.t (list State) k) (bb : State * list State)
:= let (ji,a) := jia in
let (j,i) := ji in
let (b0,bs) := bb in
sem i (a[[j]]) -> sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true /\ Forall (fun b => is_B j a b = false) bs.
Lemma bl_ex_step'
(Hlive : forall i a x, live_B i a x)
: exists (bl_step' : (Fin.t k * Input * Vector.t (list State) k) -> (State * list State)),
forall (jia : Fin.t k * Input * Vector.t (list State) k), live_B_minimal_def' jia (bl_step' jia).
Proof.
eapply choice.
intros.
destruct x as [ [j i] a ].
specialize (live_B_minimal j i a (Hlive j i a)) as Hspec.
destructH.
exists (b0,bs).
firstorder.
Qed.
Lemma bl_ex_step
(Hlive : forall i a x, live_B i a x)
: exists (bl_step : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall j (i : Input) (a : Vector.t (list State) k), live_B_minimal_def' (j,i,a) (bl_step j i a).
Proof.
specialize (bl_ex_step' Hlive) as Hspec.
destructH.
exists (fun j i a => bl_step' (j,i,a)).
intros.
specialize (Hspec (j,i,a)).
assumption.
Qed.
Definition live_or_not j (i : Input) (a : Vector.t (list State) k) (bb : State * list State)
:= live_B_minimal_def' (j,i,a) bb
\/ forall bs, sem i (bs ++ a[[j]]) -> Forall (fun b => is_B j a b = false) bs.
Lemma bl_ex_step_or
: exists (bl_step' : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall j (i : Input) (a : Vector.t (list State) k), live_or_not j i a (bl_step' j i a).
Proof.
eapply choice3.
intros.
rename a into j.
rename b into i.
rename c into a.
destruct (classic (sem i (a[[j]]) -> exists b0 bs, sem i (b0 :: bs ++ a[[j]]) /\ is_B j a b0 = true)).
all: unfold live_or_not.
- specialize (live_B_minimal j i a H) as Hspec.
destructH.
exists (b0,bs).
left.
firstorder.
- exists (state0,[]).
right.
intros.
cbn in H0.
eapply not_imply_elim2 in H.
specialize (not_ex_all_not)
with (P:=fun (bb : State * list State)
=> sem i (fst bb :: snd bb ++ a[[j]]) /\ is_B j a (fst bb) = true) as Q.
exploit' Q.
{
contradict H.
clear - H.
destructH.
destruct n as [b0 bs].
exists b0, bs.
split;auto.
}
induction bs as [|b0 bs].
1: econstructor.
econstructor.
+ specialize (Q (b0,bs)).
eapply not_and_or in Q.
destruct Q.
* cbn in H1.
contradiction.
* cbn in H1.
eapply Bool.not_true_is_false.
assumption.
+ eapply IHbs.
cbn in H0.
eapply safe;eauto.
Qed.
Lemma bl_ex_step_or2
: exists (bl_step' : Fin.t k -> Input -> Vector.t (list State) k -> (State * list State)),
forall (i : Vector.t Input k) (a : Vector.t (list State) k) j, live_or_not j (i[[j]]) a (bl_step' j (i[[j]]) a).
Proof.
specialize bl_ex_step_or as Q.
destructH.
exists bl_step'.
intros.
eapply Q.
Qed.
End with_live_barrier.
End with_rad.
End BarrierSyncChoice.
Import BarrierSyncChoice.
Section with_si.
Context {Input State : Type}.
Context (sem : Input -> list State -> Prop).
Context {Hrad : rad_semantics sem}.
Context {state0 : State}.
Context (dec_St : forall x y : State, {x = y} + {x <> y}).
Context (is_B : State -> bool).
Definition live_B0 (i : Input) (a : list State)
:= sem i a -> exists b0 bs, sem i (b0 :: bs ++ a) /\ is_B b0 = true.
Definition live_B_minimal_def0 (ia : Input * list State) (bb : State * list State)
:= let (i,a) := ia in
let (b0,bs) := bb in
sem i a -> sem i (b0 :: bs ++ a) /\ is_B b0 = true /\ Forall (fun b => is_B b = false) bs.
Definition fun_vec1 {X Y : Type} (f : X -> Y)
: Fin.t 1 -> Vector.t X 1 -> Y.
Proof.
intros.
inversion X0.
exact (f h).
Defined.
Definition f1 : Fin.t 1 := (@Fin.F1 0).
Definition v1 {X : Type} (x : X) := (Vector.cons _ x _ (Vector.nil _)).
Definition t1 {X Y Z : Type} (f : Fin.t 1 -> X -> Vector.t Y 1 -> Z)
: X -> Y -> Z
:= fun x y => f f1 x (v1 y).
Lemma bl_ex_step0
: (forall (i : Input) (a : list State), live_B0 i a) ->
exists bl_step : Input -> list State -> State * list State,
forall (i : Input) (a : list State),
live_B_minimal_def0 (i, a) (bl_step i a).
Proof.
intros.
assert (forall (j : Fin.t 1) (i : Input) (a : Vector.t (list State) 1), live_B (sem:=sem) (k:=1) (fun _ _ => is_B) j i (a)) as Q.
- unfold live_B, live_B0 in *.
intros.
eapply H in H0.
destructH.
eexists;eauto.
- eapply bl_ex_step in Q. 2: eapply state0. 2: eapply dec_St.
destructH.
eexists;eauto.
unfold live_B_minimal_def', live_B_minimal_def0 in *.
intros.
specialize (Q f1 i (v1 a)).
instantiate (1:=t1 bl_step).
unfold t1.
eapply Q.
Qed.
Definition live_or_not0 (i : Input) (a : list State) (bb : State * list State)
:= live_B_minimal_def0 (i,a) bb
\/ forall bs, sem i (bs ++ a) -> Forall (fun b => is_B b = false) bs.
Lemma bl_ex_step_or0
: exists (bl_step' : Input -> list State -> (State * list State)),
forall (i : Input) (a : list State), live_or_not0 i a (bl_step' i a).
Proof.
specialize (@bl_ex_step_or Input State sem Hrad 1 (fun _ _ => is_B) state0 dec_St) as Q.
destructH.
eexists;eauto.
unfold live_or_not, live_or_not0, live_B_minimal_def', live_B_minimal_def0 in *.
intros;eauto.
instantiate (1:=t1 bl_step').
unfold t1.
eapply Q.
Qed.
End with_si.