Library iris.program_logic.adequacy_inf
From iris.prelude Require Export irelations.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
From iris.program_logic Require Import adequacy.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (@eq coPset _ _) ⇒ eassumption || set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Section compact.
From iris.prelude Require Import set.
From Coq Require Import Classical_Pred_Type.
Context {A: Type}.
Context (P: nat → A → Prop).
Context (P_le: ∀ x n n', P n x → n' ≤ n → P n' x).
Implicit Type n: nat.
Implicit Type x: A.
Lemma not_all_all_stop:
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∀ x, ∃ n, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hnf x. specialize (Hnf x).
apply not_all_not_ex.
intro Hnf'.
eapply all_not_not_ex in Hnf'.
eapply Hnf'.
eapply not_all_ex_not in Hnf.
destruct Hnf as (nb&Hnb).
∃ nb.
intros n' Hgt.
intro Hn'. eapply Hnb. eapply P_le; eauto.
Qed.
Lemma not_all_all_stop_common:
set_finite {[ x | ∃ n, P n x ]} →
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∃ n, ∀ x, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hfin Hnf.
destruct Hfin as (l&Hin).
cut (∃ n, ∀ x n', n ≤ n' → x ∈ l → ¬ P n' x).
{
intros (np&Hnp).
∃ np. intros x n' Hle HP.
eapply Hnp; eauto. eapply Hin. econstructor; eauto.
}
clear -Hnf P_le.
induction l as [| a l IHl]; intros.
× ∃ O. intros x n' Hle Hin. inversion Hin.
× edestruct IHl as (nl&Hnl).
eapply not_all_all_stop with a in Hnf.
edestruct Hnf as (na&Hna).
∃ (na + nl).
intros x n' Hle Hin.
inversion Hin; subst.
** eapply Hna; eauto.
** eapply Hnl; eauto.
Qed.
Lemma compact_forall:
set_finite {[ x | ∃ n, P n x ]} →
(∀ n, ∃ x, P n x) →
(∃ x, ∀ n, P n x).
Proof.
intros Hfin Halln. apply not_all_not_ex.
intro Hnf.
edestruct (not_all_all_stop_common Hfin Hnf) as (np&Hnp).
edestruct (Halln np) as (xnp&HP).
eapply Hnp; eauto.
Qed.
End compact.
Section compact_setoid.
From iris.prelude Require Import set.
From Coq Require Import Classical_Pred_Type.
Definition set_finite_setoid `{Equiv A} {B} {H : ElemOf A B} (X : B) : Prop :=
∃ l : list A, ∀ x : A, x ∈ X → ∃ x' : A, x ≡ x' ∧ x' ∈ l.
Instance set_finite_setoid_subseteq `{Equiv A} `{Equiv B}
{Equ: @Equivalence A equiv} {H: ElemOf A B}:
Proper (subseteq --> impl) (@set_finite_setoid A _ B _).
Proof.
intros X Y. rewrite /flip. intros Hsub (l&Hfin_in).
∃ l. intros x HinY.
edestruct Hfin_in; eauto.
Qed.
Lemma set_finite_setoid_inj `{Equiv A, Equiv A'}
{Equiv: Equivalence ((≡): relation A')}
(X: set A) (f: A → A') (f_proper: ∀ x y, x ∈ X → x ≡ y → f x ≡ f y)
(f_inj: ∀ x y, x ∈ X → y ∈ X → f x ≡ f y → x ≡ y):
set_finite_setoid (fmap f X) →
set_finite_setoid X.
Proof.
intros (l&Hfin_in).
assert (∀ x, x ∈ X → ∃ a, a ∈ l ∧ f x ≡ a) as Hcover.
{
intros. edestruct Hfin_in as (a&?&?).
eapply elem_of_fmap_2; eauto. ∃ a; split; auto.
}
assert (∃ l : list A, (∀ a, a ∈ l → a ∈ X) ∧
(∀ a', a' ∈ fmap f X → ∃ a, a ∈ l ∧ a' ≡ f a)) as (lx&Hxs&Hall).
{
clear -f_proper f_inj Hfin_in Equiv.
revert X f_inj Hfin_in f_proper.
induction l; intros.
- ∃ [].
split; set_solver.
- destruct (Classical_Prop.classic (∃ x, x ∈ X ∧ f x ≡ a)) as [(x&HinX&Heq)|Hno_match].
× edestruct (IHl {[ x' | x' ∈ X ∧ ¬ (x' ≡ x)]}) as (l'&Hinl'&HinXminus).
{
intros x' y' (Hin&_) (Hin'&_).
eapply f_inj; eauto.
}
{
intros a' (x'&?&(?&Hneq))%elem_of_fmap_1. subst.
edestruct (Hfin_in (f x')) as (a'&Hequiv&Hin'); eauto.
{ subst. apply elem_of_fmap_2; eauto. }
inversion Hin' as [|Hin]; subst.
** exfalso. eapply Hneq. eapply f_inj; eauto.
rewrite Heq Hequiv. eauto.
** eexists; split; eauto.
}
{
intros x' y' (Hin&_) Hequiv.
eapply f_proper; eauto.
}
∃ (x :: l'). split; eauto.
** intros a'; inversion 1; subst; eauto.
edestruct (Hinl' a') as (?&?); eauto.
** intros ? (x'&->&?)%elem_of_fmap_1.
destruct (Classical_Prop.classic (f x' ≡ a)).
*** ∃ x; split; eauto. left.
etransitivity; eauto.
*** edestruct (HinXminus (f x')) as (a''&?&?).
{
eapply elem_of_fmap_2. econstructor; eauto.
intros Hequiv. apply (f_proper) in Hequiv; auto. rewrite Heq in Hequiv ×.
auto.
}
∃ a''. split; auto; right; auto.
× eapply (IHl X); eauto.
{
intros a' HinfX.
edestruct Hfin_in as (x'&?&Hin); eauto.
eapply elem_of_fmap_1 in HinfX as (x&->&?).
inversion Hin; subst.
** exfalso. eapply Hno_match. ∃ x; split; eauto.
** eexists; split; eauto.
}
}
∃ lx. intros x HinX.
edestruct (Hall (f x)) as (x0&?Hinlx&Hequiv); first eapply elem_of_fmap_2; eauto.
Qed.
Context `{Equiv A, !Equivalence (≡)}.
Context (P: nat → A → Prop).
Context (P_proper: ∀ n, Proper ((≡) ==> iff) (P n)).
Context (P_le: ∀ x n n', P n x → n' ≤ n → P n' x).
Implicit Type n: nat.
Implicit Type x: A.
Lemma not_all_all_stop_common_setoid:
set_finite_setoid {[ x | ∃ n, P n x ]} →
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∃ n, ∀ x, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hfin Hnf.
destruct Hfin as (l&Hin).
cut (∃ n, ∀ x n', n ≤ n' → x ∈ l → ¬ P n' x).
{
intros (np&Hnp).
∃ np. intros x n' Hle HP.
destruct (Hin x) as (x'&Hequiv&Hin'); first (econstructor; eauto).
eapply Hnp; eauto.
rewrite -Hequiv; eauto.
}
clear -Hnf P_le.
induction l as [| a l IHl]; intros.
× ∃ O. intros x n' Hle Hin. inversion Hin.
× edestruct IHl as (nl&Hnl).
specialize (@not_all_all_stop A P P_le Hnf a). intros (na&Hna).
∃ (na + nl).
intros x n' Hle Hin.
inversion Hin; subst.
** eapply Hna; eauto.
** eapply Hnl; eauto.
Qed.
Lemma compact_forall_setoid:
set_finite_setoid {[ x | ∃ n, P n x ]} →
(∀ n, ∃ x, P n x) →
(∃ x, ∀ n, P n x).
Proof.
intros Hfin Halln. apply not_all_not_ex.
intro Hnf.
edestruct (not_all_all_stop_common_setoid Hfin Hnf) as (np&Hnp).
edestruct (Halln np) as (xnp&HP).
eapply Hnp; eauto.
Qed.
End compact_setoid.
Section idx_stepN_lemmas.
Context {M: cmraT}.
Context {Λ : language} {Σ : rFunctor}.
Implicit Types rs robs : list M.
Inductive idx_stepN' (n: nat): nat → list M → list M → Prop :=
| idx_stepN_alt_hd_atomic r1 r2 rs rs' :
stepN n r1 r2 →
rs ≡ rs' →
idx_stepN' n 0 (r1 :: rs) (r2 :: rs')
| idx_stepN_alt_hd_fork r1 r2 rf rs rs':
stepN n r1 (r2 ⋅ rf) →
rs ≡ rs' →
idx_stepN' n 0 (r1 :: rs) (r2 :: rs' ++ [rf])
| idx_stepN_alt_cons k r0 r0' rs1 rs2:
idx_stepN' n k rs1 rs2 →
r0 ≡ r0' →
idx_stepN' n (S k) (r0 :: rs1) (r0' :: rs2).
Lemma idx_stepN_equiv n k rs1 rs2:
idx_stepN n k rs1 rs2 ↔ idx_stepN' n k rs1 rs2.
Proof.
split; intro Hs.
- inversion Hs.
× revert k rs1 rs2 r1 r2 t2 t1' t2' H H0 H1 H2 H3 H4 Hs.
induction t1; intros.
** simpl in ×. subst. inversion H3; subst. econstructor; eauto.
** destruct k; simpl in *; try omega.
subst. inversion H3; subst.
econstructor; eauto.
eapply IHt1; eauto.
inversion H3; subst.
econstructor; eauto.
× revert k rs1 rs2 r1 r2 t2 t1' t2' H H0 H1 H2 H3 H4 Hs.
induction t1; intros.
** simpl in ×. subst. inversion H3. subst. eapply idx_stepN_alt_hd_fork; eauto.
** destruct k; simpl in *; try omega.
subst. inversion H3; subst.
econstructor; eauto.
eapply IHt1; eauto.
inversion H3; subst.
eapply idx_stepN_fork; eauto.
- induction Hs.
× eapply (idx_stepN_atomic _ _ _ _ _ _ nil rs); eauto using app_nil_l.
× eapply (idx_stepN_fork _ _ _ _ _ _ _ nil rs); eauto using app_nil_l.
× inversion IHHs.
** rewrite H0 H1.
eapply (idx_stepN_atomic _ _ _ _ _ _ (r0 :: t1) t2 (r0' :: t1') t2');
rewrite ?app_comm_cons; simpl; auto.
econstructor; eauto.
** rewrite H0 H1.
eapply (idx_stepN_fork _ _ _ _ _ _ _ (r0 :: t1) t2 (r0' :: t1') t2');
rewrite ?app_comm_cons; simpl; auto.
econstructor; eauto.
Qed.
Lemma list_equiv_app_inv `{Equiv A, !Equivalence (≡)}:
∀ (l l1 l2: list A), l1 ++ l2 ≡ l →
∃ l1' l2', l = l1' ++ l2' ∧ l1 ≡ l1' ∧ l2 ≡ l2'.
Proof.
intros l l1 l2. remember (l1 ++ l2) as l' eqn:Heql'.
intros Hequiv.
revert l1 l2 Heql'.
induction Hequiv.
- ∃ [], []. symmetry in Heql'.
apply app_eq_nil in Heql' as (?&?); subst; split_and!; eauto.
- intros l1 l2 Heql'.
destruct l1 as [| x' l1].
× destruct l2 as [| y' l2].
** simpl in Heql'. congruence.
** simpl in Heql'. inversion Heql'. subst.
∃ [], (y :: k); split_and!; simpl; auto.
econstructor; eauto.
× simpl in Heql'. inversion Heql'; subst.
edestruct IHHequiv as (l1' & l2' & ? & ? & ?); eauto.
∃ (y :: l1'), l2'. split_and!; subst; auto.
econstructor; eauto.
Qed.
Lemma list_equiv_singleton_inv `{Equiv A, !Equivalence (≡)}:
∀ (l: list A) a, [a] ≡ l → ∃ a', l = [a'] ∧ a ≡ a'.
Proof.
intros l a. remember [a] as l' eqn:Heql'.
intros Hequiv. revert Heql'.
induction Hequiv.
- congruence.
- intros. inversion Heql'. subst. inversion H1. subst. eexists; split; eauto.
Qed.
Global Instance idx_stepN'_proper: Proper ((≡) ==> (≡) ==> iff) (idx_stepN' n i).
Proof.
intros n i.
cut (Proper ((≡) ==> (≡) ==> impl) (@idx_stepN' n i)).
{
intros Hcut rs1 rs1' Heq1 rs2 rs2' Heq2.
split; eapply Hcut; eauto.
}
intros rs1 rs1' Heq1 rs2 rs2' Heq2.
intros Hs. revert rs1' rs2' Heq1 Heq2.
induction Hs; intros.
- inversion Heq1. inversion Heq2. subst.
econstructor; eauto; setoid_subst; eauto.
- inversion Heq1. inversion Heq2.
eapply list_equiv_app_inv in H10 as (l1'&l2'&?&?&Hsingl).
eapply list_equiv_singleton_inv in Hsingl as (rf'&?&?).
subst.
eapply (idx_stepN_alt_hd_fork).
× setoid_subst; auto.
× setoid_subst; auto.
- inversion Heq1. inversion Heq2. subst.
econstructor.
× eauto.
× etransitivity. symmetry. eauto.
transitivity r0' ; eauto.
Qed.
Global Instance idx_stepN_proper: Proper ((≡) ==> (≡) ==> iff) (@idx_stepN M n i).
Proof.
intros n i x y Heq x' y' Heq'.
rewrite ?idx_stepN_equiv.
rewrite Heq Heq'. eauto.
Qed.
Lemma idx_stepN_app:
∀ n l rs rs' i,
idx_stepN n i rs rs' ↔
idx_stepN n (length l + i) (l ++ rs) (l ++ rs').
Proof.
intros. rewrite ?idx_stepN_equiv.
split.
- intros. induction l; simpl; auto; econstructor; auto.
- induction l; intros; simpl in *; auto.
inversion H. subst. eauto.
Qed.
Lemma idx_stepN_cons:
∀ n i rs rs' x,
idx_stepN n i rs rs' ↔
idx_stepN n (S i) (x :: rs) (x :: rs').
Proof.
intros.
replace (x :: rs) with ([x] ++ rs); auto.
replace (x :: rs') with ([x] ++ rs'); auto.
replace (S i) with (length [x] + i); auto.
eapply idx_stepN_app.
Qed.
Lemma enabled_idx_stepN_cons:
∀ r rs n i,
enabled (idx_stepN n) (r :: rs) (S i)
↔ enabled (idx_stepN n) rs i.
Proof.
rewrite /enabled. intros; split.
- intros (?&His).
rewrite idx_stepN_equiv in His ×.
intros His. inversion His. subst.
eexists; rewrite idx_stepN_equiv; eauto.
- intros (rs'&His).
rewrite idx_stepN_equiv in His ×.
intros His.
∃ (r :: rs'); rewrite idx_stepN_equiv; econstructor; eauto.
Qed.
Lemma coenabled_helper (σ: state Λ) ts rs n:
Forall2 (λ e r, reducible e σ ↔ relations.red (stepN n) r) ts rs →
∀ i, enabled idx_step (ts, σ) i ↔ enabled (idx_stepN n) rs i.
Proof.
induction 1.
- intros; split; intros He; inversion He as (?&Hs);
inversion Hs; subst; destruct t1; simpl in *; discriminate.
- intros i. destruct i.
× split; intros He; inversion He as (?&Hs).
** inversion Hs; subst. destruct t1; simpl in *; try (omega; done).
edestruct H. inversion H1. subst. edestruct H2. econstructor; do 2 eexists; eauto.
econstructor.
eapply (idx_stepN_atomic _ _ _ _ _ _ nil l');
simpl; eauto.
** inversion Hs; subst; destruct t1; simpl in *; try (omega; done).
edestruct H. inversion H1. subst.
edestruct H7.
∃ r2; eauto.
destruct H8 as (?&?&?).
econstructor.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil l);
simpl; eauto.
edestruct H. inversion H1; subst. edestruct H7. ∃ (r2 ⋅ rf); eauto.
destruct H8 as (?&?&?).
econstructor.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil l);
simpl; eauto.
× rewrite enabled_idx_step_cons enabled_idx_stepN_cons; auto.
Qed.
End idx_stepN_lemmas.
Section adequacy_inf.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types Φs : list (val Λ → iProp Λ Σ).
Implicit Types m : iGst Λ Σ.
Implicit Types r rob : iRes Λ Σ.
Implicit Types rs robs : list (iRes Λ Σ).
Notation wptp n := (Forall4 (λ e Φ r rl, uPred_holds (wp ⊤ e Φ) n r rl)).
Notation estop Φs :=
(Forall (λ Φ, (∀ v, upred.uPred_entails (Φ v) upred.uPred_stopped)) Φs).
Notation rnf n r := (∀ n', n' ≤ n → relations.nf (stepN n') r).
Lemma wptp_coenabled n tσ Φs rs robs rf rfl:
wptp (S (S n)) (tσ.1) Φs rs robs →
estop Φs →
wsat (S (S n)) ⊤ (tσ.2) (big_op rs ⋅ rf) (big_op robs ⋅ rfl) →
(∀ i, enabled idx_step tσ i ↔ enabled (idx_stepN n) robs i).
Proof.
intros Hwptp Hestop Hwsat. destruct tσ as (ts, σ); simpl in ×. eapply coenabled_helper.
revert rf rfl Hwsat Hestop.
induction Hwptp as [| x y z a l k k' k'' Hwp Hwtp IH]; intros rf rfl Hwsat Hstopped.
- econstructor.
- apply Forall2_cons; eauto.
× split.
** intros (v&Hv). rewrite wp_eq in Hwp.
inversion Hwp as [? r rob v' Hpvs| ? ? ? ? Hnv Hgo]; subst; auto.
*** exfalso; edestruct Hv as (?&?&?).
cut (to_val (of_val v') = None); first (rewrite to_of_val; congruence).
eapply val_stuck. eauto.
*** edestruct (Hgo (S n) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (Hsafe&Hstep); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
destruct Hsafe as (?&?&?&?).
edestruct Hstep as (?&?&?&?&?&?&?&?&?); eauto.
econstructor. eapply cmra_stepN_S; eauto.
** intros (v&Hv). rewrite wp_eq in Hwp.
inversion Hwp as [? r rob v' Hpvs| ? ? ? ? Hnv Hgo]; subst; auto.
*** rewrite pvs_eq in Hpvs.
edestruct (Hpvs (S (S n)) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (?&(Hob&?)); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
eapply Forall_cons in Hstopped.
destruct Hstopped as (Hstopped&?).
specialize (Hstopped v').
rewrite upred.uPred_stopped_eq in Hstopped.
exfalso.
edestruct Hstopped.
edestruct (uPred_in_entails n x a); eauto using uPred_closed.
*** edestruct (Hgo (S n) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (Hsafe&Hstep); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
× eapply Forall_cons in Hstopped. destruct Hstopped as (?&?).
apply (IH (z ⋅ rf) (a ⋅ rfl)); auto.
simpl in Hwsat. rewrite (comm _ z) (comm _ a) in Hwsat ×.
rewrite -(assoc _ _ z).
by rewrite (assoc _ _ a).
Qed.
Section bounded_nondet_hom2.
Lemma elem_of_map {A B: Type} (f: A → B) (l: list A) x:
x ∈ l → f x ∈ map f l.
Proof.
induction l.
- simpl. set_solver+.
- simpl. inversion 1; subst.
× left.
× right. eauto.
Qed.
Lemma elem_of_map_inv {A B: Type} (f: A → B) (l: list A) x:
x ∈ map f l → ∃ y, y ∈ l ∧ f y = x.
Proof.
induction l.
- simpl. set_solver+.
- simpl. inversion 1; subst.
× eexists. split; eauto. left.
× edestruct IHl as (?&?&?); eauto. eexists; split; eauto. right. eauto.
Qed.
Implicit Types rw: gmap positive (iRes Λ Σ).
Context (B: cofeT).
Context (B_idx_step: nat → relation (option B)).
Context (F: nat → list (iRes Λ Σ) → option B).
Context (F_proper: ∀ n, Proper ((≡) ==> (≡)) (F n)).
Context (B_idx_step_proper: ∀ n, Proper ((≡) ==> (≡) ==> iff) (B_idx_step n)).
Context (F_spec_step: ∀ n i robs robs',
✓{S n} (big_op robs) →
✓{S n} (big_op robs') →
idx_stepN (S n) i robs robs' →
F (S n) robs ≠ None →
F (S n) robs' ≠ None ∧
B_idx_step i (F (S n) robs) (F (S n) robs')).
Context (F_spec_enabled_reflecting: ∀ n i robs,
enabled B_idx_step (F (S n) robs) i →
enabled (idx_stepN (S n)) robs i).
Context (F_spec_def_le:
∀ n robs, ✓{S n} (big_op robs) →
∀ n', n' ≤ n → F (S n) robs ≡
F (S n') robs).
Context (F_spec_step_le: ∀ n i robs robs',
B_idx_step i (F (S n) robs) (F (S n) robs') →
∀ n', n' ≤ n →
B_idx_step i (F (S n') robs) (F (S n) robs')).
Context (B_step_fin: ∀ ob,
set_finite_setoid {[ ob' | ∃ i, B_idx_step i ob ob']}).
Lemma B_step_fin_some: ∀ b,
set_finite_setoid {[ b' | ∃ i, B_idx_step i (Some b) (Some b')]}.
Proof.
intros b. specialize (B_step_fin (Some b)).
destruct B_step_fin as (l&Hin).
pose (l' := map (λ ob, match ob with | None ⇒ b | Some b' ⇒ b' end) l).
∃ l'. set_unfold. intros b' (i&Hs).
edestruct (Hin (Some b')) as (ob'' & Hequiv & Hb''_in).
{ eexists; eauto. }
inversion Hequiv as [? b''|]; subst.
∃ b''; split; eauto.
unfold l'.
eapply (elem_of_map (λ ob, match ob with | None ⇒ b | Some b' ⇒ b' end) _ (Some b''));
auto.
Qed.
Lemma isteps_wptp_comp_hom2 i tσ1 tσ2 ob1:
idx_step i tσ1 tσ2 →
(∀ n n0, n ≤ n0 →
∃ robs1 rs1 Φs,
Some ob1 ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ1.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ1.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
∃ ob2, ∀ n0, ∃ robs1 rs1 Φs, ∀ n,
S (S n) ≤ S (S n0) →
Some ob1 ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ1.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ1.2) (big_op rs1) (big_op robs1) ∧
estop Φs ∧
∃ robs2 rs2 Φs',
Some ob2 ≡ F (S (S n)) robs2
∧ wptp (S (S n)) (tσ2.1) (Φs ++ Φs') rs2 robs2
∧ wsat (S (S n)) ⊤ (tσ2.2) (big_op rs2) (big_op robs2)
∧ B_idx_step i (Some ob1) (Some ob2)
∧ estop (Φs ++ Φs').
Proof.
intros Histeps Hnon_vac.
apply compact_forall_setoid.
- intros n x y Hequiv; split.
× intros Hwn.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φs'&?&?&?&?&?&Hx&?&?&?&?); eauto.
split_and!; eauto.
do 3 eexists. split_and!; eauto;
rewrite -Hequiv; auto.
× intros Hwn.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φs'&?&?&?&?&?&Hx&?&?&?&?); eauto.
split_and!; eauto.
do 3 eexists. split_and!; eauto;
rewrite Hequiv; auto.
- intros ? n n' Hwn Hle.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φobs'Φs'&?&?&?&?&?); eauto.
- eapply set_finite_setoid_subseteq; last apply B_step_fin_some.
simpl. intros x (n&Hx).
edestruct Hx as (rs1&Φs&rf0&Hx'); eauto.
∃ i.
edestruct (Hx' n) as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- intros n.
edestruct (Hnon_vac (S (S n)) (S (S n))) as (robs0&rs0&Φs0&Heq&Hnon_vac'); eauto.
edestruct (Hnon_vac') as (Hwptp&Hwsat&?); eauto.
edestruct (isteps_wptp Φs0 [i] (S (S n)) tσ1 tσ2 robs0 rs0 ∅)
as (l'&robs2&rs2&?&?Hwptp'&Hwsat'&Hsteps_once&Heq_map&?&?); eauto.
{ eapply isteps_once. auto. }
{ simpl. eapply wptp_le; eauto. }
{ rewrite right_id. eauto using wsat_le. }
setoid_subst.
rewrite right_id in Hwsat' ×. intros Hwsat'.
eapply isteps_aux'_erase in Hsteps_once; rewrite Heq_map in Hsteps_once.
eapply isteps_once in Hsteps_once.
edestruct F_spec_step as (Hnot_none&HB_step); eauto; auto.
{ unfold not. intro Hfalse.
assert (F (S (S n)) robs0 ≡ None) as Hfalse_equiv by (rewrite Hfalse; auto).
erewrite F_spec_def_le in Heq. erewrite Hfalse_equiv in Heq.
inversion Heq. auto. omega.
}
assert (∃ b, F (S (S n)) robs2 = Some b) as (b & Heq_b).
{ destruct (F (S (S n)) robs2).
- eexists; eauto.
- congruence. }
∃ b.
do 3 eexists. intros.
split_and!.
etransitivity; last eapply F_spec_def_le; eauto.
eapply wptp_le; try eapply Hwptp; eauto.
eapply wsat_le; eauto.
eauto.
∃ robs2, rs2.
do 1 eexists; split_and!; eauto using wsat_le, isteps_idx_stepN_le.
× rewrite -Heq_b. eapply F_spec_def_le; eauto.
× eapply wptp_le; try eapply Hwptp'; eauto.
× rewrite -Heq_b Heq.
erewrite F_spec_def_le; eauto.
× eapply Forall_app; auto.
Qed.
Require Import ClassicalEpsilon.
Lemma trace_wptp_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
trace (B_idx_step) (Some b).
Proof.
revert tσ e b.
cofix.
intros tσ e b Hex.
inversion e; subst.
intros.
assert (idx_step i tσ y) as Hi by auto.
eapply (isteps_wptp_comp_hom2 _ _ _ b) in Hi; last eauto.
eapply constructive_indefinite_description in Hi.
destruct Hi as (ob'&Hwptp).
econstructor.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_hom2; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
do 3 eexists. split_and!; eauto.
Qed.
Instance enabled_B_idx_step_proper2: Proper ((≡) ==> eq ==> iff) (enabled B_idx_step).
Proof.
intros x y Heq ? ? ?. subst.
rewrite /enabled.
setoid_subst.
auto.
Qed.
Lemma trace_wptp_co_se_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ (F (S (S n)) robs1) ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
co_se_trace _ B_idx_step e (Some b).
Proof.
revert tσ e b.
cofix.
intros tσ e b Hex.
destruct e as [? tσ1 tσ2 ? ]; subst.
assert (idx_step i tσ1 tσ2) as Hi by auto.
eapply (isteps_wptp_comp_hom2 _ _ _ b) in Hi; last eauto.
eapply constructive_indefinite_description in Hi.
destruct Hi as (ob'&Hwptp).
econstructor.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&Hws'&?&?&?&?&?&?&?&?&?); eauto.
intros.
assert (Some b ≡ F 2 robs1) as Heqob.
{ erewrite <-F_spec_def_le. eauto. auto. omega. }
rewrite (wptp_coenabled 2 _ _ _ _ ∅ ∅); eauto.
eapply F_spec_enabled_reflecting.
erewrite <-Heqob. eauto.
rewrite ?right_id. eauto.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_co_se_hom2; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
do 3 eexists. split_and!; eauto.
Qed.
Lemma trace_wptp_pres_fair_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ (F (S (S n)) robs1) ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
∃ (e': trace B_idx_step (Some b)), fair_pres _ _ e e'.
Proof.
intros. eapply co_se_trace_fair_pres.
- intros. eapply excluded_middle_informative.
- intros. eapply excluded_middle_informative.
- eapply trace_wptp_co_se_hom2; eauto.
Qed.
Import uPred.
Lemma ht_adequacy_own_inf_hom2 Φ (e: expr Λ) (σ: state Λ)
(tr: trace idx_step ([e], σ)) m1 m2 (n: nat):
2 < n →
F n ([Res ∅ ∅ m1]) ≠ None →
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ ★ ownG m2 }} e {{ Φ }} →
estop [Φ] →
∃ (tr': trace (B_idx_step) (F n ([Res ∅ ∅ m1]))),
fair_pres _ _ tr tr'.
Proof.
intros Hlt Hnot_none Hval Hht Hstop.
destruct n; try omega.
destruct n; try omega.
assert (∃ b, F (S (S n)) [Res ∅ ∅ m1] = Some b) as (b&Heq_b).
{ destruct (F _).
- eexists; eauto.
- exfalso. congruence.
}
rewrite Heq_b.
eapply trace_wptp_pres_fair_hom2; auto.
intros n'.
∃ ([Res ∅ ∅ m1]), [(Res ∅ (Excl' σ) m2)].
∃ [Φ].
split_and!; eauto.
- case (decide (n' ≤ n)).
× etransitivity; last eapply (F_spec_def_le (S n)).
rewrite Heq_b. eauto.
simpl. rewrite right_id.
eapply cmra_valid_validN. split_and!; simpl.
** apply ucmra_unit_valid.
** apply ucmra_unit_valid.
** solve_valid.
** omega.
× intros. assert (S n ≤ S n') as Hle' by omega. symmetry.
etransitivity; first eapply (F_spec_def_le (S n')).
eapply cmra_valid_validN. split_and!; simpl.
** rewrite right_id. apply ucmra_unit_valid.
** rewrite right_id. apply ucmra_unit_valid.
** solve_valid.
** eauto.
** rewrite Heq_b. auto.
- econstructor; [|econstructor].
rewrite /ht wp_eq in Hht ×.
rewrite uPred.relevant_elim affine_elim in Hht *=>Hht.
eapply wand_entails in Hht.
eapply Hht.
× split_and!; simpl; try econstructor; auto.
eapply cmra_valid_validN; solve_valid.
× split_and!; simpl; try econstructor; auto.
eapply cmra_valid_validN; solve_valid.
× rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
∃ (Res ∅ ∅ ∅), (Res ∅ (Excl' σ) m2), (Res ∅ ∅ m1), (∅: iRes Λ Σ); split_and?.
** by rewrite Res_op ?left_id ?right_id.
** by rewrite Res_op ?left_id ?right_id.
** by apply ownGl_spec.
** ∃ (Res ∅ (Excl' σ) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
*** by rewrite Res_op ?left_id ?right_id.
*** by rewrite Res_op ?left_id ?right_id.
*** split; auto. rewrite /uPred_holds //=.
*** by apply ownG_spec.
- simpl. rewrite right_id. rewrite /op //= /cmra_op //=.
rewrite /res_op. simpl. rewrite ?right_id.
eapply wsat_init. eapply cmra_valid_validN; solve_valid.
Qed.
End bounded_nondet_hom2.
End adequacy_inf.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
From iris.program_logic Require Import adequacy.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 100 (@eq coPset _ _) ⇒ eassumption || set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Section compact.
From iris.prelude Require Import set.
From Coq Require Import Classical_Pred_Type.
Context {A: Type}.
Context (P: nat → A → Prop).
Context (P_le: ∀ x n n', P n x → n' ≤ n → P n' x).
Implicit Type n: nat.
Implicit Type x: A.
Lemma not_all_all_stop:
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∀ x, ∃ n, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hnf x. specialize (Hnf x).
apply not_all_not_ex.
intro Hnf'.
eapply all_not_not_ex in Hnf'.
eapply Hnf'.
eapply not_all_ex_not in Hnf.
destruct Hnf as (nb&Hnb).
∃ nb.
intros n' Hgt.
intro Hn'. eapply Hnb. eapply P_le; eauto.
Qed.
Lemma not_all_all_stop_common:
set_finite {[ x | ∃ n, P n x ]} →
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∃ n, ∀ x, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hfin Hnf.
destruct Hfin as (l&Hin).
cut (∃ n, ∀ x n', n ≤ n' → x ∈ l → ¬ P n' x).
{
intros (np&Hnp).
∃ np. intros x n' Hle HP.
eapply Hnp; eauto. eapply Hin. econstructor; eauto.
}
clear -Hnf P_le.
induction l as [| a l IHl]; intros.
× ∃ O. intros x n' Hle Hin. inversion Hin.
× edestruct IHl as (nl&Hnl).
eapply not_all_all_stop with a in Hnf.
edestruct Hnf as (na&Hna).
∃ (na + nl).
intros x n' Hle Hin.
inversion Hin; subst.
** eapply Hna; eauto.
** eapply Hnl; eauto.
Qed.
Lemma compact_forall:
set_finite {[ x | ∃ n, P n x ]} →
(∀ n, ∃ x, P n x) →
(∃ x, ∀ n, P n x).
Proof.
intros Hfin Halln. apply not_all_not_ex.
intro Hnf.
edestruct (not_all_all_stop_common Hfin Hnf) as (np&Hnp).
edestruct (Halln np) as (xnp&HP).
eapply Hnp; eauto.
Qed.
End compact.
Section compact_setoid.
From iris.prelude Require Import set.
From Coq Require Import Classical_Pred_Type.
Definition set_finite_setoid `{Equiv A} {B} {H : ElemOf A B} (X : B) : Prop :=
∃ l : list A, ∀ x : A, x ∈ X → ∃ x' : A, x ≡ x' ∧ x' ∈ l.
Instance set_finite_setoid_subseteq `{Equiv A} `{Equiv B}
{Equ: @Equivalence A equiv} {H: ElemOf A B}:
Proper (subseteq --> impl) (@set_finite_setoid A _ B _).
Proof.
intros X Y. rewrite /flip. intros Hsub (l&Hfin_in).
∃ l. intros x HinY.
edestruct Hfin_in; eauto.
Qed.
Lemma set_finite_setoid_inj `{Equiv A, Equiv A'}
{Equiv: Equivalence ((≡): relation A')}
(X: set A) (f: A → A') (f_proper: ∀ x y, x ∈ X → x ≡ y → f x ≡ f y)
(f_inj: ∀ x y, x ∈ X → y ∈ X → f x ≡ f y → x ≡ y):
set_finite_setoid (fmap f X) →
set_finite_setoid X.
Proof.
intros (l&Hfin_in).
assert (∀ x, x ∈ X → ∃ a, a ∈ l ∧ f x ≡ a) as Hcover.
{
intros. edestruct Hfin_in as (a&?&?).
eapply elem_of_fmap_2; eauto. ∃ a; split; auto.
}
assert (∃ l : list A, (∀ a, a ∈ l → a ∈ X) ∧
(∀ a', a' ∈ fmap f X → ∃ a, a ∈ l ∧ a' ≡ f a)) as (lx&Hxs&Hall).
{
clear -f_proper f_inj Hfin_in Equiv.
revert X f_inj Hfin_in f_proper.
induction l; intros.
- ∃ [].
split; set_solver.
- destruct (Classical_Prop.classic (∃ x, x ∈ X ∧ f x ≡ a)) as [(x&HinX&Heq)|Hno_match].
× edestruct (IHl {[ x' | x' ∈ X ∧ ¬ (x' ≡ x)]}) as (l'&Hinl'&HinXminus).
{
intros x' y' (Hin&_) (Hin'&_).
eapply f_inj; eauto.
}
{
intros a' (x'&?&(?&Hneq))%elem_of_fmap_1. subst.
edestruct (Hfin_in (f x')) as (a'&Hequiv&Hin'); eauto.
{ subst. apply elem_of_fmap_2; eauto. }
inversion Hin' as [|Hin]; subst.
** exfalso. eapply Hneq. eapply f_inj; eauto.
rewrite Heq Hequiv. eauto.
** eexists; split; eauto.
}
{
intros x' y' (Hin&_) Hequiv.
eapply f_proper; eauto.
}
∃ (x :: l'). split; eauto.
** intros a'; inversion 1; subst; eauto.
edestruct (Hinl' a') as (?&?); eauto.
** intros ? (x'&->&?)%elem_of_fmap_1.
destruct (Classical_Prop.classic (f x' ≡ a)).
*** ∃ x; split; eauto. left.
etransitivity; eauto.
*** edestruct (HinXminus (f x')) as (a''&?&?).
{
eapply elem_of_fmap_2. econstructor; eauto.
intros Hequiv. apply (f_proper) in Hequiv; auto. rewrite Heq in Hequiv ×.
auto.
}
∃ a''. split; auto; right; auto.
× eapply (IHl X); eauto.
{
intros a' HinfX.
edestruct Hfin_in as (x'&?&Hin); eauto.
eapply elem_of_fmap_1 in HinfX as (x&->&?).
inversion Hin; subst.
** exfalso. eapply Hno_match. ∃ x; split; eauto.
** eexists; split; eauto.
}
}
∃ lx. intros x HinX.
edestruct (Hall (f x)) as (x0&?Hinlx&Hequiv); first eapply elem_of_fmap_2; eauto.
Qed.
Context `{Equiv A, !Equivalence (≡)}.
Context (P: nat → A → Prop).
Context (P_proper: ∀ n, Proper ((≡) ==> iff) (P n)).
Context (P_le: ∀ x n n', P n x → n' ≤ n → P n' x).
Implicit Type n: nat.
Implicit Type x: A.
Lemma not_all_all_stop_common_setoid:
set_finite_setoid {[ x | ∃ n, P n x ]} →
(∀ x : A, ¬ (∀ n : nat, P n x)) →
(∃ n, ∀ x, ∀ n', n ≤ n' → ¬ P n' x).
Proof.
intros Hfin Hnf.
destruct Hfin as (l&Hin).
cut (∃ n, ∀ x n', n ≤ n' → x ∈ l → ¬ P n' x).
{
intros (np&Hnp).
∃ np. intros x n' Hle HP.
destruct (Hin x) as (x'&Hequiv&Hin'); first (econstructor; eauto).
eapply Hnp; eauto.
rewrite -Hequiv; eauto.
}
clear -Hnf P_le.
induction l as [| a l IHl]; intros.
× ∃ O. intros x n' Hle Hin. inversion Hin.
× edestruct IHl as (nl&Hnl).
specialize (@not_all_all_stop A P P_le Hnf a). intros (na&Hna).
∃ (na + nl).
intros x n' Hle Hin.
inversion Hin; subst.
** eapply Hna; eauto.
** eapply Hnl; eauto.
Qed.
Lemma compact_forall_setoid:
set_finite_setoid {[ x | ∃ n, P n x ]} →
(∀ n, ∃ x, P n x) →
(∃ x, ∀ n, P n x).
Proof.
intros Hfin Halln. apply not_all_not_ex.
intro Hnf.
edestruct (not_all_all_stop_common_setoid Hfin Hnf) as (np&Hnp).
edestruct (Halln np) as (xnp&HP).
eapply Hnp; eauto.
Qed.
End compact_setoid.
Section idx_stepN_lemmas.
Context {M: cmraT}.
Context {Λ : language} {Σ : rFunctor}.
Implicit Types rs robs : list M.
Inductive idx_stepN' (n: nat): nat → list M → list M → Prop :=
| idx_stepN_alt_hd_atomic r1 r2 rs rs' :
stepN n r1 r2 →
rs ≡ rs' →
idx_stepN' n 0 (r1 :: rs) (r2 :: rs')
| idx_stepN_alt_hd_fork r1 r2 rf rs rs':
stepN n r1 (r2 ⋅ rf) →
rs ≡ rs' →
idx_stepN' n 0 (r1 :: rs) (r2 :: rs' ++ [rf])
| idx_stepN_alt_cons k r0 r0' rs1 rs2:
idx_stepN' n k rs1 rs2 →
r0 ≡ r0' →
idx_stepN' n (S k) (r0 :: rs1) (r0' :: rs2).
Lemma idx_stepN_equiv n k rs1 rs2:
idx_stepN n k rs1 rs2 ↔ idx_stepN' n k rs1 rs2.
Proof.
split; intro Hs.
- inversion Hs.
× revert k rs1 rs2 r1 r2 t2 t1' t2' H H0 H1 H2 H3 H4 Hs.
induction t1; intros.
** simpl in ×. subst. inversion H3; subst. econstructor; eauto.
** destruct k; simpl in *; try omega.
subst. inversion H3; subst.
econstructor; eauto.
eapply IHt1; eauto.
inversion H3; subst.
econstructor; eauto.
× revert k rs1 rs2 r1 r2 t2 t1' t2' H H0 H1 H2 H3 H4 Hs.
induction t1; intros.
** simpl in ×. subst. inversion H3. subst. eapply idx_stepN_alt_hd_fork; eauto.
** destruct k; simpl in *; try omega.
subst. inversion H3; subst.
econstructor; eauto.
eapply IHt1; eauto.
inversion H3; subst.
eapply idx_stepN_fork; eauto.
- induction Hs.
× eapply (idx_stepN_atomic _ _ _ _ _ _ nil rs); eauto using app_nil_l.
× eapply (idx_stepN_fork _ _ _ _ _ _ _ nil rs); eauto using app_nil_l.
× inversion IHHs.
** rewrite H0 H1.
eapply (idx_stepN_atomic _ _ _ _ _ _ (r0 :: t1) t2 (r0' :: t1') t2');
rewrite ?app_comm_cons; simpl; auto.
econstructor; eauto.
** rewrite H0 H1.
eapply (idx_stepN_fork _ _ _ _ _ _ _ (r0 :: t1) t2 (r0' :: t1') t2');
rewrite ?app_comm_cons; simpl; auto.
econstructor; eauto.
Qed.
Lemma list_equiv_app_inv `{Equiv A, !Equivalence (≡)}:
∀ (l l1 l2: list A), l1 ++ l2 ≡ l →
∃ l1' l2', l = l1' ++ l2' ∧ l1 ≡ l1' ∧ l2 ≡ l2'.
Proof.
intros l l1 l2. remember (l1 ++ l2) as l' eqn:Heql'.
intros Hequiv.
revert l1 l2 Heql'.
induction Hequiv.
- ∃ [], []. symmetry in Heql'.
apply app_eq_nil in Heql' as (?&?); subst; split_and!; eauto.
- intros l1 l2 Heql'.
destruct l1 as [| x' l1].
× destruct l2 as [| y' l2].
** simpl in Heql'. congruence.
** simpl in Heql'. inversion Heql'. subst.
∃ [], (y :: k); split_and!; simpl; auto.
econstructor; eauto.
× simpl in Heql'. inversion Heql'; subst.
edestruct IHHequiv as (l1' & l2' & ? & ? & ?); eauto.
∃ (y :: l1'), l2'. split_and!; subst; auto.
econstructor; eauto.
Qed.
Lemma list_equiv_singleton_inv `{Equiv A, !Equivalence (≡)}:
∀ (l: list A) a, [a] ≡ l → ∃ a', l = [a'] ∧ a ≡ a'.
Proof.
intros l a. remember [a] as l' eqn:Heql'.
intros Hequiv. revert Heql'.
induction Hequiv.
- congruence.
- intros. inversion Heql'. subst. inversion H1. subst. eexists; split; eauto.
Qed.
Global Instance idx_stepN'_proper: Proper ((≡) ==> (≡) ==> iff) (idx_stepN' n i).
Proof.
intros n i.
cut (Proper ((≡) ==> (≡) ==> impl) (@idx_stepN' n i)).
{
intros Hcut rs1 rs1' Heq1 rs2 rs2' Heq2.
split; eapply Hcut; eauto.
}
intros rs1 rs1' Heq1 rs2 rs2' Heq2.
intros Hs. revert rs1' rs2' Heq1 Heq2.
induction Hs; intros.
- inversion Heq1. inversion Heq2. subst.
econstructor; eauto; setoid_subst; eauto.
- inversion Heq1. inversion Heq2.
eapply list_equiv_app_inv in H10 as (l1'&l2'&?&?&Hsingl).
eapply list_equiv_singleton_inv in Hsingl as (rf'&?&?).
subst.
eapply (idx_stepN_alt_hd_fork).
× setoid_subst; auto.
× setoid_subst; auto.
- inversion Heq1. inversion Heq2. subst.
econstructor.
× eauto.
× etransitivity. symmetry. eauto.
transitivity r0' ; eauto.
Qed.
Global Instance idx_stepN_proper: Proper ((≡) ==> (≡) ==> iff) (@idx_stepN M n i).
Proof.
intros n i x y Heq x' y' Heq'.
rewrite ?idx_stepN_equiv.
rewrite Heq Heq'. eauto.
Qed.
Lemma idx_stepN_app:
∀ n l rs rs' i,
idx_stepN n i rs rs' ↔
idx_stepN n (length l + i) (l ++ rs) (l ++ rs').
Proof.
intros. rewrite ?idx_stepN_equiv.
split.
- intros. induction l; simpl; auto; econstructor; auto.
- induction l; intros; simpl in *; auto.
inversion H. subst. eauto.
Qed.
Lemma idx_stepN_cons:
∀ n i rs rs' x,
idx_stepN n i rs rs' ↔
idx_stepN n (S i) (x :: rs) (x :: rs').
Proof.
intros.
replace (x :: rs) with ([x] ++ rs); auto.
replace (x :: rs') with ([x] ++ rs'); auto.
replace (S i) with (length [x] + i); auto.
eapply idx_stepN_app.
Qed.
Lemma enabled_idx_stepN_cons:
∀ r rs n i,
enabled (idx_stepN n) (r :: rs) (S i)
↔ enabled (idx_stepN n) rs i.
Proof.
rewrite /enabled. intros; split.
- intros (?&His).
rewrite idx_stepN_equiv in His ×.
intros His. inversion His. subst.
eexists; rewrite idx_stepN_equiv; eauto.
- intros (rs'&His).
rewrite idx_stepN_equiv in His ×.
intros His.
∃ (r :: rs'); rewrite idx_stepN_equiv; econstructor; eauto.
Qed.
Lemma coenabled_helper (σ: state Λ) ts rs n:
Forall2 (λ e r, reducible e σ ↔ relations.red (stepN n) r) ts rs →
∀ i, enabled idx_step (ts, σ) i ↔ enabled (idx_stepN n) rs i.
Proof.
induction 1.
- intros; split; intros He; inversion He as (?&Hs);
inversion Hs; subst; destruct t1; simpl in *; discriminate.
- intros i. destruct i.
× split; intros He; inversion He as (?&Hs).
** inversion Hs; subst. destruct t1; simpl in *; try (omega; done).
edestruct H. inversion H1. subst. edestruct H2. econstructor; do 2 eexists; eauto.
econstructor.
eapply (idx_stepN_atomic _ _ _ _ _ _ nil l');
simpl; eauto.
** inversion Hs; subst; destruct t1; simpl in *; try (omega; done).
edestruct H. inversion H1. subst.
edestruct H7.
∃ r2; eauto.
destruct H8 as (?&?&?).
econstructor.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil l);
simpl; eauto.
edestruct H. inversion H1; subst. edestruct H7. ∃ (r2 ⋅ rf); eauto.
destruct H8 as (?&?&?).
econstructor.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil l);
simpl; eauto.
× rewrite enabled_idx_step_cons enabled_idx_stepN_cons; auto.
Qed.
End idx_stepN_lemmas.
Section adequacy_inf.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types Φs : list (val Λ → iProp Λ Σ).
Implicit Types m : iGst Λ Σ.
Implicit Types r rob : iRes Λ Σ.
Implicit Types rs robs : list (iRes Λ Σ).
Notation wptp n := (Forall4 (λ e Φ r rl, uPred_holds (wp ⊤ e Φ) n r rl)).
Notation estop Φs :=
(Forall (λ Φ, (∀ v, upred.uPred_entails (Φ v) upred.uPred_stopped)) Φs).
Notation rnf n r := (∀ n', n' ≤ n → relations.nf (stepN n') r).
Lemma wptp_coenabled n tσ Φs rs robs rf rfl:
wptp (S (S n)) (tσ.1) Φs rs robs →
estop Φs →
wsat (S (S n)) ⊤ (tσ.2) (big_op rs ⋅ rf) (big_op robs ⋅ rfl) →
(∀ i, enabled idx_step tσ i ↔ enabled (idx_stepN n) robs i).
Proof.
intros Hwptp Hestop Hwsat. destruct tσ as (ts, σ); simpl in ×. eapply coenabled_helper.
revert rf rfl Hwsat Hestop.
induction Hwptp as [| x y z a l k k' k'' Hwp Hwtp IH]; intros rf rfl Hwsat Hstopped.
- econstructor.
- apply Forall2_cons; eauto.
× split.
** intros (v&Hv). rewrite wp_eq in Hwp.
inversion Hwp as [? r rob v' Hpvs| ? ? ? ? Hnv Hgo]; subst; auto.
*** exfalso; edestruct Hv as (?&?&?).
cut (to_val (of_val v') = None); first (rewrite to_of_val; congruence).
eapply val_stuck. eauto.
*** edestruct (Hgo (S n) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (Hsafe&Hstep); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
destruct Hsafe as (?&?&?&?).
edestruct Hstep as (?&?&?&?&?&?&?&?&?); eauto.
econstructor. eapply cmra_stepN_S; eauto.
** intros (v&Hv). rewrite wp_eq in Hwp.
inversion Hwp as [? r rob v' Hpvs| ? ? ? ? Hnv Hgo]; subst; auto.
*** rewrite pvs_eq in Hpvs.
edestruct (Hpvs (S (S n)) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (?&(Hob&?)); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
eapply Forall_cons in Hstopped.
destruct Hstopped as (Hstopped&?).
specialize (Hstopped v').
rewrite upred.uPred_stopped_eq in Hstopped.
exfalso.
edestruct Hstopped.
edestruct (uPred_in_entails n x a); eauto using uPred_closed.
*** edestruct (Hgo (S n) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (Hsafe&Hstep); eauto.
{
rewrite right_id_L. simpl in Hwsat. simpl.
by rewrite ?assoc in Hwsat ×.
}
× eapply Forall_cons in Hstopped. destruct Hstopped as (?&?).
apply (IH (z ⋅ rf) (a ⋅ rfl)); auto.
simpl in Hwsat. rewrite (comm _ z) (comm _ a) in Hwsat ×.
rewrite -(assoc _ _ z).
by rewrite (assoc _ _ a).
Qed.
Section bounded_nondet_hom2.
Lemma elem_of_map {A B: Type} (f: A → B) (l: list A) x:
x ∈ l → f x ∈ map f l.
Proof.
induction l.
- simpl. set_solver+.
- simpl. inversion 1; subst.
× left.
× right. eauto.
Qed.
Lemma elem_of_map_inv {A B: Type} (f: A → B) (l: list A) x:
x ∈ map f l → ∃ y, y ∈ l ∧ f y = x.
Proof.
induction l.
- simpl. set_solver+.
- simpl. inversion 1; subst.
× eexists. split; eauto. left.
× edestruct IHl as (?&?&?); eauto. eexists; split; eauto. right. eauto.
Qed.
Implicit Types rw: gmap positive (iRes Λ Σ).
Context (B: cofeT).
Context (B_idx_step: nat → relation (option B)).
Context (F: nat → list (iRes Λ Σ) → option B).
Context (F_proper: ∀ n, Proper ((≡) ==> (≡)) (F n)).
Context (B_idx_step_proper: ∀ n, Proper ((≡) ==> (≡) ==> iff) (B_idx_step n)).
Context (F_spec_step: ∀ n i robs robs',
✓{S n} (big_op robs) →
✓{S n} (big_op robs') →
idx_stepN (S n) i robs robs' →
F (S n) robs ≠ None →
F (S n) robs' ≠ None ∧
B_idx_step i (F (S n) robs) (F (S n) robs')).
Context (F_spec_enabled_reflecting: ∀ n i robs,
enabled B_idx_step (F (S n) robs) i →
enabled (idx_stepN (S n)) robs i).
Context (F_spec_def_le:
∀ n robs, ✓{S n} (big_op robs) →
∀ n', n' ≤ n → F (S n) robs ≡
F (S n') robs).
Context (F_spec_step_le: ∀ n i robs robs',
B_idx_step i (F (S n) robs) (F (S n) robs') →
∀ n', n' ≤ n →
B_idx_step i (F (S n') robs) (F (S n) robs')).
Context (B_step_fin: ∀ ob,
set_finite_setoid {[ ob' | ∃ i, B_idx_step i ob ob']}).
Lemma B_step_fin_some: ∀ b,
set_finite_setoid {[ b' | ∃ i, B_idx_step i (Some b) (Some b')]}.
Proof.
intros b. specialize (B_step_fin (Some b)).
destruct B_step_fin as (l&Hin).
pose (l' := map (λ ob, match ob with | None ⇒ b | Some b' ⇒ b' end) l).
∃ l'. set_unfold. intros b' (i&Hs).
edestruct (Hin (Some b')) as (ob'' & Hequiv & Hb''_in).
{ eexists; eauto. }
inversion Hequiv as [? b''|]; subst.
∃ b''; split; eauto.
unfold l'.
eapply (elem_of_map (λ ob, match ob with | None ⇒ b | Some b' ⇒ b' end) _ (Some b''));
auto.
Qed.
Lemma isteps_wptp_comp_hom2 i tσ1 tσ2 ob1:
idx_step i tσ1 tσ2 →
(∀ n n0, n ≤ n0 →
∃ robs1 rs1 Φs,
Some ob1 ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ1.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ1.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
∃ ob2, ∀ n0, ∃ robs1 rs1 Φs, ∀ n,
S (S n) ≤ S (S n0) →
Some ob1 ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ1.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ1.2) (big_op rs1) (big_op robs1) ∧
estop Φs ∧
∃ robs2 rs2 Φs',
Some ob2 ≡ F (S (S n)) robs2
∧ wptp (S (S n)) (tσ2.1) (Φs ++ Φs') rs2 robs2
∧ wsat (S (S n)) ⊤ (tσ2.2) (big_op rs2) (big_op robs2)
∧ B_idx_step i (Some ob1) (Some ob2)
∧ estop (Φs ++ Φs').
Proof.
intros Histeps Hnon_vac.
apply compact_forall_setoid.
- intros n x y Hequiv; split.
× intros Hwn.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φs'&?&?&?&?&?&Hx&?&?&?&?); eauto.
split_and!; eauto.
do 3 eexists. split_and!; eauto;
rewrite -Hequiv; auto.
× intros Hwn.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φs'&?&?&?&?&?&Hx&?&?&?&?); eauto.
split_and!; eauto.
do 3 eexists. split_and!; eauto;
rewrite Hequiv; auto.
- intros ? n n' Hwn Hle.
edestruct Hwn as (rs1&Φs&rf0&Hwn').
do 3 eexists. intros n0 Hle0.
destruct (Hwn' n0) as (r2&Φobs'Φs'&?&?&?&?&?); eauto.
- eapply set_finite_setoid_subseteq; last apply B_step_fin_some.
simpl. intros x (n&Hx).
edestruct Hx as (rs1&Φs&rf0&Hx'); eauto.
∃ i.
edestruct (Hx' n) as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- intros n.
edestruct (Hnon_vac (S (S n)) (S (S n))) as (robs0&rs0&Φs0&Heq&Hnon_vac'); eauto.
edestruct (Hnon_vac') as (Hwptp&Hwsat&?); eauto.
edestruct (isteps_wptp Φs0 [i] (S (S n)) tσ1 tσ2 robs0 rs0 ∅)
as (l'&robs2&rs2&?&?Hwptp'&Hwsat'&Hsteps_once&Heq_map&?&?); eauto.
{ eapply isteps_once. auto. }
{ simpl. eapply wptp_le; eauto. }
{ rewrite right_id. eauto using wsat_le. }
setoid_subst.
rewrite right_id in Hwsat' ×. intros Hwsat'.
eapply isteps_aux'_erase in Hsteps_once; rewrite Heq_map in Hsteps_once.
eapply isteps_once in Hsteps_once.
edestruct F_spec_step as (Hnot_none&HB_step); eauto; auto.
{ unfold not. intro Hfalse.
assert (F (S (S n)) robs0 ≡ None) as Hfalse_equiv by (rewrite Hfalse; auto).
erewrite F_spec_def_le in Heq. erewrite Hfalse_equiv in Heq.
inversion Heq. auto. omega.
}
assert (∃ b, F (S (S n)) robs2 = Some b) as (b & Heq_b).
{ destruct (F (S (S n)) robs2).
- eexists; eauto.
- congruence. }
∃ b.
do 3 eexists. intros.
split_and!.
etransitivity; last eapply F_spec_def_le; eauto.
eapply wptp_le; try eapply Hwptp; eauto.
eapply wsat_le; eauto.
eauto.
∃ robs2, rs2.
do 1 eexists; split_and!; eauto using wsat_le, isteps_idx_stepN_le.
× rewrite -Heq_b. eapply F_spec_def_le; eauto.
× eapply wptp_le; try eapply Hwptp'; eauto.
× rewrite -Heq_b Heq.
erewrite F_spec_def_le; eauto.
× eapply Forall_app; auto.
Qed.
Require Import ClassicalEpsilon.
Lemma trace_wptp_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ F (S (S n)) robs1 ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
trace (B_idx_step) (Some b).
Proof.
revert tσ e b.
cofix.
intros tσ e b Hex.
inversion e; subst.
intros.
assert (idx_step i tσ y) as Hi by auto.
eapply (isteps_wptp_comp_hom2 _ _ _ b) in Hi; last eauto.
eapply constructive_indefinite_description in Hi.
destruct Hi as (ob'&Hwptp).
econstructor.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_hom2; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
do 3 eexists. split_and!; eauto.
Qed.
Instance enabled_B_idx_step_proper2: Proper ((≡) ==> eq ==> iff) (enabled B_idx_step).
Proof.
intros x y Heq ? ? ?. subst.
rewrite /enabled.
setoid_subst.
auto.
Qed.
Lemma trace_wptp_co_se_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ (F (S (S n)) robs1) ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
co_se_trace _ B_idx_step e (Some b).
Proof.
revert tσ e b.
cofix.
intros tσ e b Hex.
destruct e as [? tσ1 tσ2 ? ]; subst.
assert (idx_step i tσ1 tσ2) as Hi by auto.
eapply (isteps_wptp_comp_hom2 _ _ _ b) in Hi; last eauto.
eapply constructive_indefinite_description in Hi.
destruct Hi as (ob'&Hwptp).
econstructor.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&Hws'&?&?&?&?&?&?&?&?&?); eauto.
intros.
assert (Some b ≡ F 2 robs1) as Heqob.
{ erewrite <-F_spec_def_le. eauto. auto. omega. }
rewrite (wptp_coenabled 2 _ _ _ _ ∅ ∅); eauto.
eapply F_spec_enabled_reflecting.
erewrite <-Heqob. eauto.
rewrite ?right_id. eauto.
- destruct (Hwptp 2) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' 2). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
- eapply trace_wptp_co_se_hom2; eauto.
intros.
destruct (Hwptp (S (S n))) as (robs1&rs1&Φs&Hwptp').
specialize (Hwptp' n). edestruct Hwptp' as (?&?&?&?&?&?&?&?&?&?&?&?); eauto.
do 3 eexists. split_and!; eauto.
Qed.
Lemma trace_wptp_pres_fair_hom2 (tσ: cfg Λ) (e: trace (idx_step) tσ) b:
(∀ n,
∃ robs1 rs1 Φs,
Some b ≡ (F (S (S n)) robs1) ∧
wptp (S (S n)) (tσ.1) Φs rs1 robs1 ∧
wsat (S (S n)) ⊤ (tσ.2) (big_op rs1) (big_op robs1) ∧
estop Φs) →
∃ (e': trace B_idx_step (Some b)), fair_pres _ _ e e'.
Proof.
intros. eapply co_se_trace_fair_pres.
- intros. eapply excluded_middle_informative.
- intros. eapply excluded_middle_informative.
- eapply trace_wptp_co_se_hom2; eauto.
Qed.
Import uPred.
Lemma ht_adequacy_own_inf_hom2 Φ (e: expr Λ) (σ: state Λ)
(tr: trace idx_step ([e], σ)) m1 m2 (n: nat):
2 < n →
F n ([Res ∅ ∅ m1]) ≠ None →
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ ★ ownG m2 }} e {{ Φ }} →
estop [Φ] →
∃ (tr': trace (B_idx_step) (F n ([Res ∅ ∅ m1]))),
fair_pres _ _ tr tr'.
Proof.
intros Hlt Hnot_none Hval Hht Hstop.
destruct n; try omega.
destruct n; try omega.
assert (∃ b, F (S (S n)) [Res ∅ ∅ m1] = Some b) as (b&Heq_b).
{ destruct (F _).
- eexists; eauto.
- exfalso. congruence.
}
rewrite Heq_b.
eapply trace_wptp_pres_fair_hom2; auto.
intros n'.
∃ ([Res ∅ ∅ m1]), [(Res ∅ (Excl' σ) m2)].
∃ [Φ].
split_and!; eauto.
- case (decide (n' ≤ n)).
× etransitivity; last eapply (F_spec_def_le (S n)).
rewrite Heq_b. eauto.
simpl. rewrite right_id.
eapply cmra_valid_validN. split_and!; simpl.
** apply ucmra_unit_valid.
** apply ucmra_unit_valid.
** solve_valid.
** omega.
× intros. assert (S n ≤ S n') as Hle' by omega. symmetry.
etransitivity; first eapply (F_spec_def_le (S n')).
eapply cmra_valid_validN. split_and!; simpl.
** rewrite right_id. apply ucmra_unit_valid.
** rewrite right_id. apply ucmra_unit_valid.
** solve_valid.
** eauto.
** rewrite Heq_b. auto.
- econstructor; [|econstructor].
rewrite /ht wp_eq in Hht ×.
rewrite uPred.relevant_elim affine_elim in Hht *=>Hht.
eapply wand_entails in Hht.
eapply Hht.
× split_and!; simpl; try econstructor; auto.
eapply cmra_valid_validN; solve_valid.
× split_and!; simpl; try econstructor; auto.
eapply cmra_valid_validN; solve_valid.
× rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
∃ (Res ∅ ∅ ∅), (Res ∅ (Excl' σ) m2), (Res ∅ ∅ m1), (∅: iRes Λ Σ); split_and?.
** by rewrite Res_op ?left_id ?right_id.
** by rewrite Res_op ?left_id ?right_id.
** by apply ownGl_spec.
** ∃ (Res ∅ (Excl' σ) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
*** by rewrite Res_op ?left_id ?right_id.
*** by rewrite Res_op ?left_id ?right_id.
*** split; auto. rewrite /uPred_holds //=.
*** by apply ownG_spec.
- simpl. rewrite right_id. rewrite /op //= /cmra_op //=.
rewrite /res_op. simpl. rewrite ?right_id.
eapply wsat_init. eapply cmra_valid_validN; solve_valid.
Qed.
End bounded_nondet_hom2.
End adequacy_inf.