Library iris.algebra.step
From iris.algebra Require Export base.
From iris.algebra Require Import cofe.
Section cofe_rel.
Context `{A: cofeT}.
Lemma rel_properN_iff_impl:
∀ (P: nat → A → A → Prop),
(∀ n, Proper (dist n ==> dist n ==> iff) (P n)) →
(∀ n, Proper (dist n ==> dist n ==> impl) (P n)).
Proof.
intros P Hpr n ? ? Heq ? ? Heq' Hp.
eapply Hpr; [ | | apply Hp]; eauto.
Qed.
Global Instance rel_properN_impl_iff (R: nat → A → A → Prop)
(resp: ∀ n, Proper (dist n ==> dist n ==> impl) (R n)):
∀ n, Proper (dist n ==> dist n ==> iff) (R n).
Proof.
intros x y n Heq x' y' Heq'.
split.
× intros HR. rewrite <-Heq, <-Heq'; auto.
× intros HR. rewrite <-Heq, <-Heq' in HR; auto.
Qed.
Context `(R : nat → A → A → Prop).
Context (resp: ∀ n, Proper (dist n ==> dist n ==> iff) (R n)).
Existing Instance resp.
Section union.
Context `(R' : nat → relation A).
Context (resp': ∀ n, Proper (dist n ==> dist n ==> iff) (R' n)).
Existing Instance resp'.
Definition unionN (r r': nat → relation A) : nat → relation A :=
λ n, Relation_Operators.union _ (r n) (r' n).
Global Instance rel_unionN_properN:
∀ n, Proper (dist n ==> dist n ==> iff) ((unionN R R') n).
Proof.
intros n x y Hd x' y' Hd'.
split.
× intros [HR | HR']; [ left | right ]; rewrite <- Hd, <- Hd'; auto.
× intros [HR | HR']; [ left | right ]; rewrite Hd Hd'; auto.
Qed.
End union.
Definition tcN (r: nat → relation A) : nat → relation A :=
λ n, tc (r n).
Global Instance tcN_properN:
∀ n, Proper (dist n ==> dist n ==> iff) (tcN R n).
Proof.
intros n x y Heq x' y' Heq'.
split.
× intros HR. revert HR y Heq y' Heq'.
induction 1; intros.
** eapply tc_once; rewrite -Heq -Heq'; eauto.
** eapply tc_l.
rewrite <- Heq; eauto.
eapply IHHR; auto; reflexivity.
× intros HR. revert HR x Heq x' Heq'.
induction 1; intros.
** eapply tc_once; rewrite Heq Heq'; eauto.
** eapply tc_l.
rewrite Heq; eauto.
eapply IHHR; auto; reflexivity.
Qed.
End cofe_rel.
Class StepN (A : Type) := stepN : nat → A → A → Prop.
Instance: Params (@stepN) 3.
Infix "⤳_( n )" := (stepN n) (at level 51, left associativity) : C_scope.
Class uStep (A: cofeT) `{StepN A} := {
ustep_ne n : Proper (dist n ==> dist n ==> impl) (stepN n);
ustep_S n x y: x ⤳_(S n) y → x ⤳_(n) y
}.
Class Step (A : Type) := step : A → A → Prop.
Instance: Params (@step) 2.
Infix "⤳ " := step (at level 51, left associativity) : C_scope.
Instance stepN_step `{StepN A} : Step A := λ x y, ∀ n, x ⤳_(n) y.
From iris.algebra Require Import cofe.
Section cofe_rel.
Context `{A: cofeT}.
Lemma rel_properN_iff_impl:
∀ (P: nat → A → A → Prop),
(∀ n, Proper (dist n ==> dist n ==> iff) (P n)) →
(∀ n, Proper (dist n ==> dist n ==> impl) (P n)).
Proof.
intros P Hpr n ? ? Heq ? ? Heq' Hp.
eapply Hpr; [ | | apply Hp]; eauto.
Qed.
Global Instance rel_properN_impl_iff (R: nat → A → A → Prop)
(resp: ∀ n, Proper (dist n ==> dist n ==> impl) (R n)):
∀ n, Proper (dist n ==> dist n ==> iff) (R n).
Proof.
intros x y n Heq x' y' Heq'.
split.
× intros HR. rewrite <-Heq, <-Heq'; auto.
× intros HR. rewrite <-Heq, <-Heq' in HR; auto.
Qed.
Context `(R : nat → A → A → Prop).
Context (resp: ∀ n, Proper (dist n ==> dist n ==> iff) (R n)).
Existing Instance resp.
Section union.
Context `(R' : nat → relation A).
Context (resp': ∀ n, Proper (dist n ==> dist n ==> iff) (R' n)).
Existing Instance resp'.
Definition unionN (r r': nat → relation A) : nat → relation A :=
λ n, Relation_Operators.union _ (r n) (r' n).
Global Instance rel_unionN_properN:
∀ n, Proper (dist n ==> dist n ==> iff) ((unionN R R') n).
Proof.
intros n x y Hd x' y' Hd'.
split.
× intros [HR | HR']; [ left | right ]; rewrite <- Hd, <- Hd'; auto.
× intros [HR | HR']; [ left | right ]; rewrite Hd Hd'; auto.
Qed.
End union.
Definition tcN (r: nat → relation A) : nat → relation A :=
λ n, tc (r n).
Global Instance tcN_properN:
∀ n, Proper (dist n ==> dist n ==> iff) (tcN R n).
Proof.
intros n x y Heq x' y' Heq'.
split.
× intros HR. revert HR y Heq y' Heq'.
induction 1; intros.
** eapply tc_once; rewrite -Heq -Heq'; eauto.
** eapply tc_l.
rewrite <- Heq; eauto.
eapply IHHR; auto; reflexivity.
× intros HR. revert HR x Heq x' Heq'.
induction 1; intros.
** eapply tc_once; rewrite Heq Heq'; eauto.
** eapply tc_l.
rewrite Heq; eauto.
eapply IHHR; auto; reflexivity.
Qed.
End cofe_rel.
Class StepN (A : Type) := stepN : nat → A → A → Prop.
Instance: Params (@stepN) 3.
Infix "⤳_( n )" := (stepN n) (at level 51, left associativity) : C_scope.
Class uStep (A: cofeT) `{StepN A} := {
ustep_ne n : Proper (dist n ==> dist n ==> impl) (stepN n);
ustep_S n x y: x ⤳_(S n) y → x ⤳_(n) y
}.
Class Step (A : Type) := step : A → A → Prop.
Instance: Params (@step) 2.
Infix "⤳ " := step (at level 51, left associativity) : C_scope.
Instance stepN_step `{StepN A} : Step A := λ x y, ∀ n, x ⤳_(n) y.
General properties
Section step.
Context {A: Type} `{S: Step A} `{E: Equiv A}.
Implicit Types x y: A.
Record shift_admissible (r: relation A) := {
shift_adm_proper: Proper ((≡) ==> (≡) ==> impl) r;
shift_adm_step_l x y z : step x y → r y z → step x z;
shift_adm_step_r x y z : r x y → step y z → step x z;
shift_adm_refl: Reflexive r;
shift_adm_trans: Transitive r;
}.
Definition shift x y :=
∃ r, shift_admissible r ∧ r x y.
Context `{!Equivalence equiv}.
Context (Step_Proper: Proper (equiv ==> equiv ==> impl) (step)).
Existing Instances shift_adm_proper shift_adm_refl shift_adm_trans.
Lemma equiv_is_admissible: shift_admissible equiv.
Proof.
split.
× intros x x' Heqx y y' Heqy Hequiv.
setoid_subst; auto.
× intros x y z ? ?;
setoid_subst; auto.
× intros x y z ? ?;
setoid_subst; auto.
× intros x; setoid_subst; auto.
× intros x y z ? ?; setoid_subst; auto.
Qed.
Lemma tcunion_is_admissible (r r': relation A):
shift_admissible r → shift_admissible r' → shift_admissible (tc (Relation_Operators.union _ r r')).
Proof.
intros Hadm Hadm'; split.
× eapply rel_proper_iff_impl.
eapply tc_proper. eapply rel_union_proper;
eapply rel_proper_impl_iff; eapply shift_adm_proper; eauto.
× intros x y z Hs.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shift_adm_step_l r) | eapply (shift_adm_step_l r')]; eauto.
** eapply IHtc.
destruct Hu; [ eapply (shift_adm_step_l r) | eapply (shift_adm_step_l r')]; eauto.
× intros x y z Htc Hs.
revert Htc.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shift_adm_step_r r) | eapply (shift_adm_step_r r')]; eauto.
** destruct Hu; [ eapply (shift_adm_step_r r) | eapply (shift_adm_step_r r')]; eauto.
× intros x. eapply tc_once. left; eapply (shift_adm_refl); eauto.
× intros x y z; eapply tc_transitive.
Qed.
Lemma rc_trans_step_is_admissible:
Transitive (step) → shift_admissible (λ x y, (x ≡ y) ∨ step x y).
Proof.
split.
× intros x y Heq x' y' Heq' [Heq'' | Hs].
** left; setoid_subst; auto.
** right. setoid_subst; auto.
× intros x y z ? [Heq | Hs].
** setoid_subst; auto.
** setoid_subst; etransitivity; eauto.
× intros x y z [Heq | Hs] ?.
** setoid_subst; auto.
** setoid_subst; etransitivity; eauto.
× intros x; left; auto.
× intros x y z [Heq | Hs] [Heq' | Hs'];
setoid_subst; eauto.
Qed.
Lemma shift_is_admissible: shift_admissible shift.
Proof.
split.
× intros x x' Heqx y y' Heqy [r (Hadm&Hr)].
∃ r; split; auto.
eapply (shift_adm_proper r); eauto.
× intros x y z ? [r (Hadm&Hr)].
eapply (shift_adm_step_l r); eauto.
× intros x y z [r (Hadm&Hr)] ?.
eapply (shift_adm_step_r r); eauto.
× ∃ ((≡)); split; eauto using equiv_is_admissible.
× intros x y z [r (Hadm&Hr)] [r' (Hadm'&Hr')].
∃ (tc (Relation_Operators.union _ r r')).
split; first apply tcunion_is_admissible; auto.
eapply tc_l; first left; eauto.
econstructor; right; auto.
Qed.
Lemma shift_proper: Proper (equiv ==> equiv ==> impl) shift.
Proof. exact (shift_adm_proper _ shift_is_admissible). Qed.
Lemma shift_reflexive: Reflexive shift.
Proof. exact (shift_adm_refl _ shift_is_admissible). Qed.
Lemma shift_transitive: Transitive shift.
Proof. exact (shift_adm_trans _ shift_is_admissible). Qed.
End step.
Section stepn.
Context {A: cofeT} `{St: StepN A}.
Context `{@uStep A St}.
Implicit Types x y: A.
Implicit Types n k: nat.
Lemma stepN_le n n' x y : x ⤳_(n) y → n' ≤ n → x ⤳_(n') y.
Proof. induction 2; eauto using ustep_S. Qed.
Record shiftN_admissible (r: nat → relation A) := {
shiftN_adm_ne n: Proper (dist n ==> (dist n) ==> impl) (r (n));
shiftN_adm_S n x y: r (S n) x y → r n x y;
shiftN_adm_step_l n x y z : stepN n x y → r n y z → stepN n x z;
shiftN_adm_step_r n x y z : r n x y → stepN n y z → stepN n x z;
shiftN_adm_refl n: Reflexive (r n);
shiftN_adm_trans n: Transitive (r n);
}.
Existing Instances ustep_ne shiftN_adm_ne shiftN_adm_refl shiftN_adm_trans.
Global Instance stepN_proper n: Proper ((≡) ==> (≡) ==> impl) (stepN n).
Proof.
intros x y Hd x' y' Hd' Hs.
eapply ustep_ne; try apply equiv_dist; eauto.
Qed.
Global Instance shiftN_adm_proper r (H: shiftN_admissible r) n: Proper ((≡) ==> (≡) ==> impl) (r n).
Proof.
intros x y Hd x' y' Hd' Hs.
eapply shiftN_adm_ne; try apply equiv_dist; eauto.
Qed.
Definition shiftN n x y := ∃ r, shiftN_admissible r ∧ r n x y.
Lemma dist_is_admissibleN: shiftN_admissible dist.
Proof.
split.
× intros n x x' Hdx y y' Hdy Hd.
rewrite -Hdx -Hdy; auto.
× intros n x y Hd. eapply dist_S; auto.
× intros n x y z ? ?.
cofe_subst; auto.
× intros n x y z ? ?;
cofe_subst; auto.
× intros n x; eauto with ×.
× intros n x y z ? ?; etransitivity; eauto.
Qed.
Lemma tcNunionN_is_admissibleN (r r': nat → relation A):
shiftN_admissible r → shiftN_admissible r' → shiftN_admissible (tcN (unionN r r')).
Proof.
intros Hadm Hadm'; econstructor.
× eapply rel_properN_iff_impl.
eapply tcN_properN. eapply rel_unionN_properN;
eapply rel_properN_impl_iff; eapply shiftN_adm_ne; eauto.
× intros n x y Hs. rewrite /tcN /unionN in Hs ×.
induction Hs as [? ? Hs_once | ? ? ? Hs_once Htrans]; subst.
** inversion Hs_once; eapply tc_once; [ left | right ];
try eapply (shiftN_adm_S _ Hadm); auto.
try eapply (shiftN_adm_S _ Hadm'); auto.
** eapply tc_l.
*** inversion Hs_once; [ left | right ];
try eapply (shiftN_adm_S _ Hadm); eauto.
try eapply (shiftN_adm_S _ Hadm'); eauto.
*** eapply IHHtrans.
× intros n x y z Hs.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shiftN_adm_step_l r) | eapply (shiftN_adm_step_l r')]; eauto.
** eapply IHtc.
destruct Hu; [ eapply (shiftN_adm_step_l r) | eapply (shiftN_adm_step_l r')]; eauto.
× intros n x y z Htc Hs.
revert Htc.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shiftN_adm_step_r r) | eapply (shiftN_adm_step_r r')]; eauto.
** destruct Hu; [ eapply (shiftN_adm_step_r r) | eapply (shiftN_adm_step_r r')]; eauto.
× intros n x. eapply tc_once. left; eapply (shiftN_adm_refl); eauto.
× intros n x y z; eapply tc_transitive.
Qed.
Lemma shiftN_is_shiftN_admissible: shiftN_admissible shiftN.
Proof.
econstructor.
× intros n x y Hd x' y' Hd' (r&Hadm&Hr).
∃ r; split_and?; auto. eapply shiftN_adm_ne; eauto.
× intros n x y (r&Hadm&Hr).
∃ r; split_and?; auto. eapply shiftN_adm_S; eauto.
× intros n x y z ? (r&Hadm&Hr).
eapply shiftN_adm_step_l; eauto.
× intros n x y z (r&Hadm&Hr) ?.
eapply shiftN_adm_step_r; eauto.
× intros n x; ∃ dist; split; first apply dist_is_admissibleN.
reflexivity.
× intros n x y z [r (Hadm&Hr)] [r' (Hadm'&Hr')].
∃ (tcN (unionN r r')).
split; first apply tcNunionN_is_admissibleN; auto.
eapply tc_l; first left; eauto.
econstructor; right; auto.
Qed.
Lemma stepN_step_proper: Proper (equiv ==> equiv ==> impl) step.
Proof. intros x y Heq x' y' Heq' Hs n.
rewrite -Heq -Heq'; eauto.
Qed.
Lemma shiftN_ne n: Proper (dist n ==> dist n ==> impl) (shiftN n).
Proof. eapply shiftN_adm_ne, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_proper n: Proper (equiv ==> equiv ==> impl) (shiftN n).
Proof. eapply shiftN_adm_proper, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_S n x y: shiftN (S n) x y → shiftN n x y.
Proof. eapply shiftN_adm_S, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_le n n' x y : shiftN n x y → n' ≤ n → shiftN n' x y.
Proof. induction 2; eauto using shiftN_S. Qed.
Lemma shiftN_reflexive n: Reflexive (shiftN n).
Proof. eapply shiftN_adm_refl, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_transitive n: Transitive (shiftN n).
Proof. eapply shiftN_adm_trans, shiftN_is_shiftN_admissible. Qed.
Section shiftN_shift_discrete.
Context `{Discrete A}.
Context {Discrete_stepN: ∀ n x y, stepN 0 x y → stepN n x y}.
Lemma stepN_iff_step: ∀ n x y , stepN n x y ↔ step x y.
Proof.
split.
× intros Hsn n'. eapply Discrete_stepN.
eapply stepN_le; eauto; omega.
× eauto.
Qed.
Lemma discrete_shiftN_up: ∀ n x y, shiftN 0 x y → shiftN n x y.
Proof.
intros n x y Hs.
∃ (λ n x y, shiftN 0 x y); split; auto.
clear n x y Hs; econstructor.
× intros n x y Hd x' y' Hd' Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
× intros n x y Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
× intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_l; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
× intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_r; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
× intros n; eapply shiftN_reflexive.
× intros n; eapply shiftN_transitive.
Qed.
Instance discrete_step_proper:
Proper (equiv ==> equiv ==> impl) step.
Proof.
intros x y Heq x' y' Heq' Hs.
rewrite /step /stepN_step in Hs ×.
intros n. specialize (Hs n). setoid_subst; auto.
Qed.
Lemma discrete_shift_shiftN_admissible:
shiftN_admissible (λ (n: nat) (x y: A), shift x y).
Proof.
econstructor; auto.
× intros n' x y Hd x' y' Hd' Hs.
eapply shift_proper; try apply discrete_step_proper; last apply Hs;
eapply timeless_iff; eauto.
× intros n x y z Hs1 Hs2.
eapply stepN_iff_step.
eapply shift_adm_step_l. eapply shift_is_admissible, discrete_step_proper.
** eapply stepN_iff_step; eauto.
** eauto.
× intros n x y z Hs1 Hs2.
eapply stepN_iff_step.
eapply shift_adm_step_r. eapply shift_is_admissible, discrete_step_proper.
** eauto.
** eapply stepN_iff_step; eauto.
× intros n x; eapply shift_reflexive;
eauto using shift_is_admissible, discrete_step_proper.
× intros n x y z ? ?; eapply shift_transitive;
eauto using shift_is_admissible, discrete_step_proper.
Qed.
Lemma discrete_shiftN_shift_admissible:
shift_admissible (λ (x y: A), shiftN 0 x y).
Proof.
econstructor; auto.
× intros x y Hd x' y' Hd' Hs.
eapply shiftN_proper; eauto.
× intros x y z Hs1 Hs2.
eapply (stepN_iff_step 0).
eapply (stepN_iff_step 0) in Hs1.
eapply shiftN_adm_step_l; first eapply shiftN_is_shiftN_admissible; eauto.
× intros x y z Hs1 Hs2.
eapply (stepN_iff_step 0).
eapply (stepN_iff_step 0) in Hs2.
eapply shiftN_adm_step_r; first eapply shiftN_is_shiftN_admissible; eauto.
× intros x; eapply shiftN_reflexive.
× intros x y z ? ?; eapply shiftN_transitive; eauto.
Qed.
Lemma discrete_shift_shiftN n x y: shift x y → shiftN n x y.
Proof.
intros. ∃ (λ n, shift); split; auto.
apply discrete_shift_shiftN_admissible.
Qed.
Lemma discrete_shiftN_shift n x y: shiftN n x y → shift x y.
Proof.
intros. ∃ (shiftN 0); split; first apply discrete_shiftN_shift_admissible.
eapply shiftN_le; eauto; omega.
Qed.
End shiftN_shift_discrete.
End stepn.
Section relational.
Context {A B: cofeT}.
Context {SA: StepN A} `{@uStep A SA}.
Variable R: nat → A → B → Prop.
Variable R_inter_shiftN: ∀ n a a' b, R n a b → R n a' b → shiftN n a a'.
Variable R_S: ∀ n a b, R (S n) a b → R n a b.
Variable R_ne: ∀ n, Proper (dist n ==> dist n ==> impl) (R n).
Implicit Types rb : nat → relation B.
Implicit Types ax az : A.
Implicit Types bx bz : B.
Record stepN_rel_admissible rb := {
stepN_rel_adm_ne n : Proper (dist n ==> dist n ==> impl) (rb n);
stepN_rel_adm_S n x y: rb (S n) x y → rb n x y;
stepN_rel_adm_extract n n' b1 b2:
S n' ≤ n →
nsteps (rb n) (S n') b1 b2 →
∃ a1 a2, R n a1 b1 ∧ R n a2 b2 ∧ nsteps (stepN n) (S n') a1 a2
}.
Definition stepN_rel : StepN B := λ n bx bz, ∃ rb, stepN_rel_admissible rb ∧ rb n bx bz.
Lemma nsteps_stepN_shift n (a1 a2 a1' a2': A) m:
nsteps (stepN n) (S m) a1 a2
→ shiftN n a1' a1
→ shiftN n a2 a2'
→ nsteps (stepN n) (S m) a1' a2'.
Proof.
intros Hnsteps. assert (S m ≠ 0) as Hnonzero by omega. revert Hnonzero a1' a2'.
induction Hnsteps as [| m' a1 amid a2 Hstep]; intros Hnz a1' a2' Hshift1 Hshift2; try congruence.
destruct m'.
× inversion Hnsteps; subst.
econstructor; last econstructor.
eapply (shiftN_adm_step_r);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
eapply (shiftN_adm_step_l);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
× assert (S m' ≠ 0) as Hnz' by omega. specialize (IHHnsteps Hnz' amid a2').
econstructor; last eapply IHHnsteps.
** eapply (shiftN_adm_step_r);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
** apply shiftN_reflexive.
** eauto.
Qed.
Lemma stepN_rel_is_stepN_rel_admissible: stepN_rel_admissible stepN_rel.
Proof.
econstructor.
× intros n x y Hd x' y' Hd' (r&Hadm&Hr).
∃ r; split; eauto.
destruct Hadm as [Hr_ne ? ?].
eapply Hr_ne; eauto.
× intros n x y (r&Hadm&Hr).
∃ r; split; eauto.
destruct Hadm as [? Hr_S ?].
eapply Hr_S; eauto.
× intros n n' b1 b2 Hle.
intros Hstep. assert (S n' ≠ 0) as Hnonz by omega. revert Hnonz.
induction Hstep as [| n'' b1 b2 b3 (r&Hadm&Hr) Hnstep]; intros; try congruence; destruct n''.
** inversion Hnstep; subst.
assert (nsteps (r n) 1 b1 b3) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
edestruct Hr' as (a1&a3&?&?&?).
∃ a1, a3; split_and!; eauto.
** edestruct IHHnstep as (a2&a3&?&?&?); try omega.
assert (nsteps (r n) 1 b1 b2) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
edestruct Hr' as (a1&a2'&?&?&Hs).
∃ a1, a3; split_and!; eauto.
econstructor; eauto.
eapply (shiftN_adm_step_l);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
inversion Hs as [| ? ? ? ? ? Hs']; subst; eauto.
inversion Hs'; subst; eauto.
Qed.
End relational.
Context {A: Type} `{S: Step A} `{E: Equiv A}.
Implicit Types x y: A.
Record shift_admissible (r: relation A) := {
shift_adm_proper: Proper ((≡) ==> (≡) ==> impl) r;
shift_adm_step_l x y z : step x y → r y z → step x z;
shift_adm_step_r x y z : r x y → step y z → step x z;
shift_adm_refl: Reflexive r;
shift_adm_trans: Transitive r;
}.
Definition shift x y :=
∃ r, shift_admissible r ∧ r x y.
Context `{!Equivalence equiv}.
Context (Step_Proper: Proper (equiv ==> equiv ==> impl) (step)).
Existing Instances shift_adm_proper shift_adm_refl shift_adm_trans.
Lemma equiv_is_admissible: shift_admissible equiv.
Proof.
split.
× intros x x' Heqx y y' Heqy Hequiv.
setoid_subst; auto.
× intros x y z ? ?;
setoid_subst; auto.
× intros x y z ? ?;
setoid_subst; auto.
× intros x; setoid_subst; auto.
× intros x y z ? ?; setoid_subst; auto.
Qed.
Lemma tcunion_is_admissible (r r': relation A):
shift_admissible r → shift_admissible r' → shift_admissible (tc (Relation_Operators.union _ r r')).
Proof.
intros Hadm Hadm'; split.
× eapply rel_proper_iff_impl.
eapply tc_proper. eapply rel_union_proper;
eapply rel_proper_impl_iff; eapply shift_adm_proper; eauto.
× intros x y z Hs.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shift_adm_step_l r) | eapply (shift_adm_step_l r')]; eauto.
** eapply IHtc.
destruct Hu; [ eapply (shift_adm_step_l r) | eapply (shift_adm_step_l r')]; eauto.
× intros x y z Htc Hs.
revert Htc.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shift_adm_step_r r) | eapply (shift_adm_step_r r')]; eauto.
** destruct Hu; [ eapply (shift_adm_step_r r) | eapply (shift_adm_step_r r')]; eauto.
× intros x. eapply tc_once. left; eapply (shift_adm_refl); eauto.
× intros x y z; eapply tc_transitive.
Qed.
Lemma rc_trans_step_is_admissible:
Transitive (step) → shift_admissible (λ x y, (x ≡ y) ∨ step x y).
Proof.
split.
× intros x y Heq x' y' Heq' [Heq'' | Hs].
** left; setoid_subst; auto.
** right. setoid_subst; auto.
× intros x y z ? [Heq | Hs].
** setoid_subst; auto.
** setoid_subst; etransitivity; eauto.
× intros x y z [Heq | Hs] ?.
** setoid_subst; auto.
** setoid_subst; etransitivity; eauto.
× intros x; left; auto.
× intros x y z [Heq | Hs] [Heq' | Hs'];
setoid_subst; eauto.
Qed.
Lemma shift_is_admissible: shift_admissible shift.
Proof.
split.
× intros x x' Heqx y y' Heqy [r (Hadm&Hr)].
∃ r; split; auto.
eapply (shift_adm_proper r); eauto.
× intros x y z ? [r (Hadm&Hr)].
eapply (shift_adm_step_l r); eauto.
× intros x y z [r (Hadm&Hr)] ?.
eapply (shift_adm_step_r r); eauto.
× ∃ ((≡)); split; eauto using equiv_is_admissible.
× intros x y z [r (Hadm&Hr)] [r' (Hadm'&Hr')].
∃ (tc (Relation_Operators.union _ r r')).
split; first apply tcunion_is_admissible; auto.
eapply tc_l; first left; eauto.
econstructor; right; auto.
Qed.
Lemma shift_proper: Proper (equiv ==> equiv ==> impl) shift.
Proof. exact (shift_adm_proper _ shift_is_admissible). Qed.
Lemma shift_reflexive: Reflexive shift.
Proof. exact (shift_adm_refl _ shift_is_admissible). Qed.
Lemma shift_transitive: Transitive shift.
Proof. exact (shift_adm_trans _ shift_is_admissible). Qed.
End step.
Section stepn.
Context {A: cofeT} `{St: StepN A}.
Context `{@uStep A St}.
Implicit Types x y: A.
Implicit Types n k: nat.
Lemma stepN_le n n' x y : x ⤳_(n) y → n' ≤ n → x ⤳_(n') y.
Proof. induction 2; eauto using ustep_S. Qed.
Record shiftN_admissible (r: nat → relation A) := {
shiftN_adm_ne n: Proper (dist n ==> (dist n) ==> impl) (r (n));
shiftN_adm_S n x y: r (S n) x y → r n x y;
shiftN_adm_step_l n x y z : stepN n x y → r n y z → stepN n x z;
shiftN_adm_step_r n x y z : r n x y → stepN n y z → stepN n x z;
shiftN_adm_refl n: Reflexive (r n);
shiftN_adm_trans n: Transitive (r n);
}.
Existing Instances ustep_ne shiftN_adm_ne shiftN_adm_refl shiftN_adm_trans.
Global Instance stepN_proper n: Proper ((≡) ==> (≡) ==> impl) (stepN n).
Proof.
intros x y Hd x' y' Hd' Hs.
eapply ustep_ne; try apply equiv_dist; eauto.
Qed.
Global Instance shiftN_adm_proper r (H: shiftN_admissible r) n: Proper ((≡) ==> (≡) ==> impl) (r n).
Proof.
intros x y Hd x' y' Hd' Hs.
eapply shiftN_adm_ne; try apply equiv_dist; eauto.
Qed.
Definition shiftN n x y := ∃ r, shiftN_admissible r ∧ r n x y.
Lemma dist_is_admissibleN: shiftN_admissible dist.
Proof.
split.
× intros n x x' Hdx y y' Hdy Hd.
rewrite -Hdx -Hdy; auto.
× intros n x y Hd. eapply dist_S; auto.
× intros n x y z ? ?.
cofe_subst; auto.
× intros n x y z ? ?;
cofe_subst; auto.
× intros n x; eauto with ×.
× intros n x y z ? ?; etransitivity; eauto.
Qed.
Lemma tcNunionN_is_admissibleN (r r': nat → relation A):
shiftN_admissible r → shiftN_admissible r' → shiftN_admissible (tcN (unionN r r')).
Proof.
intros Hadm Hadm'; econstructor.
× eapply rel_properN_iff_impl.
eapply tcN_properN. eapply rel_unionN_properN;
eapply rel_properN_impl_iff; eapply shiftN_adm_ne; eauto.
× intros n x y Hs. rewrite /tcN /unionN in Hs ×.
induction Hs as [? ? Hs_once | ? ? ? Hs_once Htrans]; subst.
** inversion Hs_once; eapply tc_once; [ left | right ];
try eapply (shiftN_adm_S _ Hadm); auto.
try eapply (shiftN_adm_S _ Hadm'); auto.
** eapply tc_l.
*** inversion Hs_once; [ left | right ];
try eapply (shiftN_adm_S _ Hadm); eauto.
try eapply (shiftN_adm_S _ Hadm'); eauto.
*** eapply IHHtrans.
× intros n x y z Hs.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shiftN_adm_step_l r) | eapply (shiftN_adm_step_l r')]; eauto.
** eapply IHtc.
destruct Hu; [ eapply (shiftN_adm_step_l r) | eapply (shiftN_adm_step_l r')]; eauto.
× intros n x y z Htc Hs.
revert Htc.
induction 1 as [ ? ? Hu | ? ? ? Hu Htc IHtc].
** destruct Hu; [ eapply (shiftN_adm_step_r r) | eapply (shiftN_adm_step_r r')]; eauto.
** destruct Hu; [ eapply (shiftN_adm_step_r r) | eapply (shiftN_adm_step_r r')]; eauto.
× intros n x. eapply tc_once. left; eapply (shiftN_adm_refl); eauto.
× intros n x y z; eapply tc_transitive.
Qed.
Lemma shiftN_is_shiftN_admissible: shiftN_admissible shiftN.
Proof.
econstructor.
× intros n x y Hd x' y' Hd' (r&Hadm&Hr).
∃ r; split_and?; auto. eapply shiftN_adm_ne; eauto.
× intros n x y (r&Hadm&Hr).
∃ r; split_and?; auto. eapply shiftN_adm_S; eauto.
× intros n x y z ? (r&Hadm&Hr).
eapply shiftN_adm_step_l; eauto.
× intros n x y z (r&Hadm&Hr) ?.
eapply shiftN_adm_step_r; eauto.
× intros n x; ∃ dist; split; first apply dist_is_admissibleN.
reflexivity.
× intros n x y z [r (Hadm&Hr)] [r' (Hadm'&Hr')].
∃ (tcN (unionN r r')).
split; first apply tcNunionN_is_admissibleN; auto.
eapply tc_l; first left; eauto.
econstructor; right; auto.
Qed.
Lemma stepN_step_proper: Proper (equiv ==> equiv ==> impl) step.
Proof. intros x y Heq x' y' Heq' Hs n.
rewrite -Heq -Heq'; eauto.
Qed.
Lemma shiftN_ne n: Proper (dist n ==> dist n ==> impl) (shiftN n).
Proof. eapply shiftN_adm_ne, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_proper n: Proper (equiv ==> equiv ==> impl) (shiftN n).
Proof. eapply shiftN_adm_proper, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_S n x y: shiftN (S n) x y → shiftN n x y.
Proof. eapply shiftN_adm_S, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_le n n' x y : shiftN n x y → n' ≤ n → shiftN n' x y.
Proof. induction 2; eauto using shiftN_S. Qed.
Lemma shiftN_reflexive n: Reflexive (shiftN n).
Proof. eapply shiftN_adm_refl, shiftN_is_shiftN_admissible. Qed.
Lemma shiftN_transitive n: Transitive (shiftN n).
Proof. eapply shiftN_adm_trans, shiftN_is_shiftN_admissible. Qed.
Section shiftN_shift_discrete.
Context `{Discrete A}.
Context {Discrete_stepN: ∀ n x y, stepN 0 x y → stepN n x y}.
Lemma stepN_iff_step: ∀ n x y , stepN n x y ↔ step x y.
Proof.
split.
× intros Hsn n'. eapply Discrete_stepN.
eapply stepN_le; eauto; omega.
× eauto.
Qed.
Lemma discrete_shiftN_up: ∀ n x y, shiftN 0 x y → shiftN n x y.
Proof.
intros n x y Hs.
∃ (λ n x y, shiftN 0 x y); split; auto.
clear n x y Hs; econstructor.
× intros n x y Hd x' y' Hd' Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
× intros n x y Hs.
eapply shiftN_ne; last apply Hs;
eapply dist_le; eauto; omega.
× intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_l; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
× intros n x y z Hs1 Hs2.
eapply Discrete_stepN.
eapply shiftN_adm_step_r; first eapply shiftN_is_shiftN_admissible; eauto.
eapply stepN_le; eauto; omega.
× intros n; eapply shiftN_reflexive.
× intros n; eapply shiftN_transitive.
Qed.
Instance discrete_step_proper:
Proper (equiv ==> equiv ==> impl) step.
Proof.
intros x y Heq x' y' Heq' Hs.
rewrite /step /stepN_step in Hs ×.
intros n. specialize (Hs n). setoid_subst; auto.
Qed.
Lemma discrete_shift_shiftN_admissible:
shiftN_admissible (λ (n: nat) (x y: A), shift x y).
Proof.
econstructor; auto.
× intros n' x y Hd x' y' Hd' Hs.
eapply shift_proper; try apply discrete_step_proper; last apply Hs;
eapply timeless_iff; eauto.
× intros n x y z Hs1 Hs2.
eapply stepN_iff_step.
eapply shift_adm_step_l. eapply shift_is_admissible, discrete_step_proper.
** eapply stepN_iff_step; eauto.
** eauto.
× intros n x y z Hs1 Hs2.
eapply stepN_iff_step.
eapply shift_adm_step_r. eapply shift_is_admissible, discrete_step_proper.
** eauto.
** eapply stepN_iff_step; eauto.
× intros n x; eapply shift_reflexive;
eauto using shift_is_admissible, discrete_step_proper.
× intros n x y z ? ?; eapply shift_transitive;
eauto using shift_is_admissible, discrete_step_proper.
Qed.
Lemma discrete_shiftN_shift_admissible:
shift_admissible (λ (x y: A), shiftN 0 x y).
Proof.
econstructor; auto.
× intros x y Hd x' y' Hd' Hs.
eapply shiftN_proper; eauto.
× intros x y z Hs1 Hs2.
eapply (stepN_iff_step 0).
eapply (stepN_iff_step 0) in Hs1.
eapply shiftN_adm_step_l; first eapply shiftN_is_shiftN_admissible; eauto.
× intros x y z Hs1 Hs2.
eapply (stepN_iff_step 0).
eapply (stepN_iff_step 0) in Hs2.
eapply shiftN_adm_step_r; first eapply shiftN_is_shiftN_admissible; eauto.
× intros x; eapply shiftN_reflexive.
× intros x y z ? ?; eapply shiftN_transitive; eauto.
Qed.
Lemma discrete_shift_shiftN n x y: shift x y → shiftN n x y.
Proof.
intros. ∃ (λ n, shift); split; auto.
apply discrete_shift_shiftN_admissible.
Qed.
Lemma discrete_shiftN_shift n x y: shiftN n x y → shift x y.
Proof.
intros. ∃ (shiftN 0); split; first apply discrete_shiftN_shift_admissible.
eapply shiftN_le; eauto; omega.
Qed.
End shiftN_shift_discrete.
End stepn.
Section relational.
Context {A B: cofeT}.
Context {SA: StepN A} `{@uStep A SA}.
Variable R: nat → A → B → Prop.
Variable R_inter_shiftN: ∀ n a a' b, R n a b → R n a' b → shiftN n a a'.
Variable R_S: ∀ n a b, R (S n) a b → R n a b.
Variable R_ne: ∀ n, Proper (dist n ==> dist n ==> impl) (R n).
Implicit Types rb : nat → relation B.
Implicit Types ax az : A.
Implicit Types bx bz : B.
Record stepN_rel_admissible rb := {
stepN_rel_adm_ne n : Proper (dist n ==> dist n ==> impl) (rb n);
stepN_rel_adm_S n x y: rb (S n) x y → rb n x y;
stepN_rel_adm_extract n n' b1 b2:
S n' ≤ n →
nsteps (rb n) (S n') b1 b2 →
∃ a1 a2, R n a1 b1 ∧ R n a2 b2 ∧ nsteps (stepN n) (S n') a1 a2
}.
Definition stepN_rel : StepN B := λ n bx bz, ∃ rb, stepN_rel_admissible rb ∧ rb n bx bz.
Lemma nsteps_stepN_shift n (a1 a2 a1' a2': A) m:
nsteps (stepN n) (S m) a1 a2
→ shiftN n a1' a1
→ shiftN n a2 a2'
→ nsteps (stepN n) (S m) a1' a2'.
Proof.
intros Hnsteps. assert (S m ≠ 0) as Hnonzero by omega. revert Hnonzero a1' a2'.
induction Hnsteps as [| m' a1 amid a2 Hstep]; intros Hnz a1' a2' Hshift1 Hshift2; try congruence.
destruct m'.
× inversion Hnsteps; subst.
econstructor; last econstructor.
eapply (shiftN_adm_step_r);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
eapply (shiftN_adm_step_l);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
× assert (S m' ≠ 0) as Hnz' by omega. specialize (IHHnsteps Hnz' amid a2').
econstructor; last eapply IHHnsteps.
** eapply (shiftN_adm_step_r);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
** apply shiftN_reflexive.
** eauto.
Qed.
Lemma stepN_rel_is_stepN_rel_admissible: stepN_rel_admissible stepN_rel.
Proof.
econstructor.
× intros n x y Hd x' y' Hd' (r&Hadm&Hr).
∃ r; split; eauto.
destruct Hadm as [Hr_ne ? ?].
eapply Hr_ne; eauto.
× intros n x y (r&Hadm&Hr).
∃ r; split; eauto.
destruct Hadm as [? Hr_S ?].
eapply Hr_S; eauto.
× intros n n' b1 b2 Hle.
intros Hstep. assert (S n' ≠ 0) as Hnonz by omega. revert Hnonz.
induction Hstep as [| n'' b1 b2 b3 (r&Hadm&Hr) Hnstep]; intros; try congruence; destruct n''.
** inversion Hnstep; subst.
assert (nsteps (r n) 1 b1 b3) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
edestruct Hr' as (a1&a3&?&?&?).
∃ a1, a3; split_and!; eauto.
** edestruct IHHnstep as (a2&a3&?&?&?); try omega.
assert (nsteps (r n) 1 b1 b2) as Hr' by (econstructor; eauto; econstructor).
apply (stepN_rel_adm_extract r Hadm) in Hr'; last omega.
edestruct Hr' as (a1&a2'&?&?&Hs).
∃ a1, a3; split_and!; eauto.
econstructor; eauto.
eapply (shiftN_adm_step_l);
first (eapply (shiftN_is_shiftN_admissible)); eauto.
inversion Hs as [| ? ? ? ? ? Hs']; subst; eauto.
inversion Hs'; subst; eauto.
Qed.
End relational.
Trivial step
Section trivial_stepN.
Context {A: cofeT}.
Instance trivial_stepN : StepN A := λ n x y, True.
Instance trivial_stepN_ustep : uStep A.
Proof.
econstructor; auto; rewrite /stepN /trivial_stepN. intros ? ? ? ? ? ? ? ?; auto.
Qed.
Lemma trivial_shiftN_trivial: ∀ n (x y: A), shiftN n x y.
Proof.
intros x y. ∃ (λ n x y, True). split; auto.
econstructor.
× by intros.
× by intros.
× by intros.
× by intros.
× by intros.
× by intros.
Qed.
End trivial_stepN.
Section later.
Context {A : cofeT} {St: StepN A}.
Context `{@uStep A St}.
Global Instance later_stepN: StepN (later A) := λ n x y,
match n with 0 ⇒ True | S n ⇒ later_car x ⤳_(n) later_car y end.
Global Instance later_step_proper: uStep (laterC A).
econstructor; rewrite /stepN /later_stepN.
× intros ? ? ? Heq ? ? Heq' Hs.
rewrite /dist /cofe_dist in Heq Heq'; simpl in ×.
rewrite /later_dist in Heq Heq'.
destruct n; auto.
eapply ustep_ne; last eapply Hs; eauto.
× intros n x y Hs. destruct n; auto.
eapply ustep_S; eauto.
Qed.
End later.
Context {A: cofeT}.
Instance trivial_stepN : StepN A := λ n x y, True.
Instance trivial_stepN_ustep : uStep A.
Proof.
econstructor; auto; rewrite /stepN /trivial_stepN. intros ? ? ? ? ? ? ? ?; auto.
Qed.
Lemma trivial_shiftN_trivial: ∀ n (x y: A), shiftN n x y.
Proof.
intros x y. ∃ (λ n x y, True). split; auto.
econstructor.
× by intros.
× by intros.
× by intros.
× by intros.
× by intros.
× by intros.
Qed.
End trivial_stepN.
Section later.
Context {A : cofeT} {St: StepN A}.
Context `{@uStep A St}.
Global Instance later_stepN: StepN (later A) := λ n x y,
match n with 0 ⇒ True | S n ⇒ later_car x ⤳_(n) later_car y end.
Global Instance later_step_proper: uStep (laterC A).
econstructor; rewrite /stepN /later_stepN.
× intros ? ? ? Heq ? ? Heq' Hs.
rewrite /dist /cofe_dist in Heq Heq'; simpl in ×.
rewrite /later_dist in Heq Heq'.
destruct n; auto.
eapply ustep_ne; last eapply Hs; eauto.
× intros n x y Hs. destruct n; auto.
eapply ustep_S; eauto.
Qed.
End later.