Library iris.program_logic.resources
From iris.algebra Require Export gmap agree excl.
From iris.algebra Require Import upred.
From iris.program_logic Require Export language.
Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
wld : gmapR positive (agreeR A);
pst : optionR (exclR (stateC Λ) trivial_stepN trivial_stepN_ustep);
gst : M;
}.
Add Printing Constructor res.
Arguments Res {_ _ _} _ _ _.
Arguments wld {_ _ _} _.
Arguments pst {_ _ _} _.
Arguments gst {_ _ _} _.
Instance: Params (@Res) 3.
Instance: Params (@wld) 3.
Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
Section res.
Context {Λ : language} {A : cofeT} {M : ucmraT}.
Implicit Types r : res Λ A M.
Inductive res_equiv' (r1 r2 : res Λ A M) := Res_equiv :
wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2.
Instance res_equiv : Equiv (res Λ A M) := res_equiv'.
Inductive res_dist' (n : nat) (r1 r2 : res Λ A M) := Res_dist :
wld r1 ≡{n}≡ wld r2 → pst r1 ≡{n}≡ pst r2 → gst r1 ≡{n}≡ gst r2 →
res_dist' n r1 r2.
Instance res_dist : Dist (res Λ A M) := res_dist'.
Global Instance Res_ne n :
Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ A M).
Proof. done. Qed.
Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ A M).
Proof. done. Qed.
Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ A M).
Proof. by destruct 1. Qed.
Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ A M).
Proof. by destruct 1. Qed.
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ A M).
Proof. by destruct 1. Qed.
Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ A M).
Proof. destruct 1; apply: timeless; apply dist_le with n; auto with lia. Qed.
Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ A M).
Proof. by destruct 1; unfold_leibniz. Qed.
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ A M).
Proof. by destruct 1. Qed.
Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ A M).
Proof. by destruct 1. Qed.
Instance res_compl : Compl (res Λ A M) := λ c,
Res (compl (chain_map wld c))
(compl (chain_map pst c)) (compl (chain_map gst c)).
Definition res_cofe_mixin : CofeMixin (res Λ A M).
Proof.
split.
- intros w1 w2; split.
+ by destruct 1; constructor; apply equiv_dist.
+ by intros Hw; constructor; apply equiv_dist⇒n; destruct (Hw n).
- intros n; split.
+ done.
+ by destruct 1; constructor.
+ do 2 destruct 1; constructor; etrans; eauto.
- by destruct 1; constructor; apply dist_S.
- intros n c; constructor.
+ apply (conv_compl n (chain_map wld c)).
+ apply (conv_compl n (chain_map pst c)).
+ apply (conv_compl n (chain_map gst c)).
Qed.
Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
Global Instance res_timeless r :
Timeless (wld r) → Timeless (gst r) → Timeless r.
Proof. destruct 3; constructor; by apply (timeless _). Qed.
Instance res_op : Op (res Λ A M) := λ r1 r2,
Res (wld r1 ⋅ wld r2) (pst r1 ⋅ pst r2) (gst r1 ⋅ gst r2).
Instance res_pcore : PCore (res Λ A M) := λ r,
Some $ Res (core (wld r)) (core (pst r)) (core (gst r)).
Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
Instance res_validN : ValidN (res Λ A M) := λ n r,
✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
Lemma res_included (r1 r2 : res Λ A M) :
r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
Proof.
split; [|by intros ([w ?]&[σ ?]&[m ?]); ∃ (Res w σ m)].
intros [r Hr]; split_and?;
[∃ (wld r)|∃ (pst r)|∃ (gst r)]; apply Hr.
Qed.
Lemma res_includedN (r1 r2 : res Λ A M) n :
r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
Proof.
split; [|by intros ([w ?]&[σ ?]&[m ?]); ∃ (Res w σ m)].
intros [r Hr]; split_and?;
[∃ (wld r)|∃ (pst r)|∃ (gst r)]; apply Hr.
Qed.
Instance res_stepN : StepN (res Λ A M) := λ n r1 r2,
gst r1 ⤳_(n) gst r2.
Definition res_cmra_mixin : CMRAMixin (res Λ A M).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n x [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
- intros r; split.
+ intros (?&?&?) n; split_and!; by apply cmra_valid_validN.
+ intros Hr; split_and!; apply cmra_valid_validN⇒ n; apply Hr.
- by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
- intros n x y Heq x' y' Heq' Hs.
rewrite /stepN /res_stepN in Hs *; rewrite -Heq -Heq'; auto.
- intros n x y Hs.
rewrite /stepN /res_stepN in Hs *; eapply cmra_stepN_S; eauto.
- by intros ???; constructor; rewrite /= assoc.
- by intros ??; constructor; rewrite /= comm.
- by intros ?; constructor; rewrite /= cmra_core_l.
- by intros ?; constructor; rewrite /= cmra_core_idemp.
- intros r1 r2; rewrite !res_included.
by intros (?&?&?); split_and!; apply cmra_core_mono.
- intros n [???] [???] (?&?&?).
econstructor; rewrite /= cmra_core_distrib; done.
- intros n r1 r2 (?&?&?);
split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
- intros n r r1 r2 (?&?&?) [???]; simpl in ×.
destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
(cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
(cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
by ∃ (Res w σ m, Res w' σ' m').
Qed.
Canonical Structure resR := CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
Definition res_ucmra_mixin : UCMRAMixin (res Λ A M).
Proof.
split.
- split_and!; apply ucmra_unit_valid.
- by split; rewrite /= left_id.
- apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure resUR :=
UCMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin res_ucmra_mixin.
Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
Res (wld r) (Excl' σ) (gst r).
Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
Res (wld r) (pst r) m.
Definition del_wld (i : positive) (r : res Λ A M) : res Λ A M :=
Res (delete i (wld r)) (pst r) (gst r).
Instance update_gst_proper: Proper (dist n ==> dist n ==> dist n) update_gst.
Proof.
intros n m1 m2 Heqm r1 r2 [Heq1 Heq2 Heq3].
rewrite /update_gst. rewrite Heqm Heq1 Heq2 //=.
Qed.
Lemma wld_validN n r : ✓{n} r → ✓{n} wld r.
Proof. by intros (?&?&?). Qed.
Lemma gst_validN n r : ✓{n} r → ✓{n} gst r.
Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
Res w1 σ1 m1 ⋅ Res w2 σ2 m2 = Res (w1 ⋅ w2) (σ1 ⋅ σ2) (m1 ⋅ m2).
Proof. done. Qed.
Lemma Res_core w σ m : core (Res w σ m) = Res (core w) (core σ) (core m).
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
✓{n} (r1⋅r2) → wld r1 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
Global Instance Res_persistent w m: Persistent m → Persistent (@Res Λ A M w ∅ m).
Proof. do 2 constructor; apply (persistent_core _). Qed.
From iris.algebra Require Import upred.
From iris.program_logic Require Export language.
Record res (Λ : language) (A : cofeT) (M : cmraT) := Res {
wld : gmapR positive (agreeR A);
pst : optionR (exclR (stateC Λ) trivial_stepN trivial_stepN_ustep);
gst : M;
}.
Add Printing Constructor res.
Arguments Res {_ _ _} _ _ _.
Arguments wld {_ _ _} _.
Arguments pst {_ _ _} _.
Arguments gst {_ _ _} _.
Instance: Params (@Res) 3.
Instance: Params (@wld) 3.
Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
Section res.
Context {Λ : language} {A : cofeT} {M : ucmraT}.
Implicit Types r : res Λ A M.
Inductive res_equiv' (r1 r2 : res Λ A M) := Res_equiv :
wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2.
Instance res_equiv : Equiv (res Λ A M) := res_equiv'.
Inductive res_dist' (n : nat) (r1 r2 : res Λ A M) := Res_dist :
wld r1 ≡{n}≡ wld r2 → pst r1 ≡{n}≡ pst r2 → gst r1 ≡{n}≡ gst r2 →
res_dist' n r1 r2.
Instance res_dist : Dist (res Λ A M) := res_dist'.
Global Instance Res_ne n :
Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Λ A M).
Proof. done. Qed.
Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Λ A M).
Proof. done. Qed.
Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Λ A M).
Proof. by destruct 1. Qed.
Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Λ A M).
Proof. by destruct 1. Qed.
Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Λ A M).
Proof. by destruct 1. Qed.
Global Instance pst_ne' n : Proper (dist n ==> (≡)) (@pst Λ A M).
Proof. destruct 1; apply: timeless; apply dist_le with n; auto with lia. Qed.
Global Instance pst_proper : Proper ((≡) ==> (=)) (@pst Λ A M).
Proof. by destruct 1; unfold_leibniz. Qed.
Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Λ A M).
Proof. by destruct 1. Qed.
Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Λ A M).
Proof. by destruct 1. Qed.
Instance res_compl : Compl (res Λ A M) := λ c,
Res (compl (chain_map wld c))
(compl (chain_map pst c)) (compl (chain_map gst c)).
Definition res_cofe_mixin : CofeMixin (res Λ A M).
Proof.
split.
- intros w1 w2; split.
+ by destruct 1; constructor; apply equiv_dist.
+ by intros Hw; constructor; apply equiv_dist⇒n; destruct (Hw n).
- intros n; split.
+ done.
+ by destruct 1; constructor.
+ do 2 destruct 1; constructor; etrans; eauto.
- by destruct 1; constructor; apply dist_S.
- intros n c; constructor.
+ apply (conv_compl n (chain_map wld c)).
+ apply (conv_compl n (chain_map pst c)).
+ apply (conv_compl n (chain_map gst c)).
Qed.
Canonical Structure resC : cofeT := CofeT (res Λ A M) res_cofe_mixin.
Global Instance res_timeless r :
Timeless (wld r) → Timeless (gst r) → Timeless r.
Proof. destruct 3; constructor; by apply (timeless _). Qed.
Instance res_op : Op (res Λ A M) := λ r1 r2,
Res (wld r1 ⋅ wld r2) (pst r1 ⋅ pst r2) (gst r1 ⋅ gst r2).
Instance res_pcore : PCore (res Λ A M) := λ r,
Some $ Res (core (wld r)) (core (pst r)) (core (gst r)).
Instance res_valid : Valid (res Λ A M) := λ r, ✓ wld r ∧ ✓ pst r ∧ ✓ gst r.
Instance res_validN : ValidN (res Λ A M) := λ n r,
✓{n} wld r ∧ ✓{n} pst r ∧ ✓{n} gst r.
Lemma res_included (r1 r2 : res Λ A M) :
r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
Proof.
split; [|by intros ([w ?]&[σ ?]&[m ?]); ∃ (Res w σ m)].
intros [r Hr]; split_and?;
[∃ (wld r)|∃ (pst r)|∃ (gst r)]; apply Hr.
Qed.
Lemma res_includedN (r1 r2 : res Λ A M) n :
r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
Proof.
split; [|by intros ([w ?]&[σ ?]&[m ?]); ∃ (Res w σ m)].
intros [r Hr]; split_and?;
[∃ (wld r)|∃ (pst r)|∃ (gst r)]; apply Hr.
Qed.
Instance res_stepN : StepN (res Λ A M) := λ n r1 r2,
gst r1 ⤳_(n) gst r2.
Definition res_cmra_mixin : CMRAMixin (res Λ A M).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros n x [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???]; constructor; cofe_subst.
- by intros n [???] ? [???] (?&?&?); split_and!; cofe_subst.
- intros r; split.
+ intros (?&?&?) n; split_and!; by apply cmra_valid_validN.
+ intros Hr; split_and!; apply cmra_valid_validN⇒ n; apply Hr.
- by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
- intros n x y Heq x' y' Heq' Hs.
rewrite /stepN /res_stepN in Hs *; rewrite -Heq -Heq'; auto.
- intros n x y Hs.
rewrite /stepN /res_stepN in Hs *; eapply cmra_stepN_S; eauto.
- by intros ???; constructor; rewrite /= assoc.
- by intros ??; constructor; rewrite /= comm.
- by intros ?; constructor; rewrite /= cmra_core_l.
- by intros ?; constructor; rewrite /= cmra_core_idemp.
- intros r1 r2; rewrite !res_included.
by intros (?&?&?); split_and!; apply cmra_core_mono.
- intros n [???] [???] (?&?&?).
econstructor; rewrite /= cmra_core_distrib; done.
- intros n r1 r2 (?&?&?);
split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
- intros n r r1 r2 (?&?&?) [???]; simpl in ×.
destruct (cmra_extend n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?),
(cmra_extend n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?),
(cmra_extend n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto.
by ∃ (Res w σ m, Res w' σ' m').
Qed.
Canonical Structure resR := CMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin.
Instance res_empty : Empty (res Λ A M) := Res ∅ ∅ ∅.
Definition res_ucmra_mixin : UCMRAMixin (res Λ A M).
Proof.
split.
- split_and!; apply ucmra_unit_valid.
- by split; rewrite /= left_id.
- apply _.
- do 2 constructor; simpl; apply (persistent_core _).
Qed.
Canonical Structure resUR :=
UCMRAT (res Λ A M) res_cofe_mixin res_cmra_mixin res_ucmra_mixin.
Definition update_pst (σ : state Λ) (r : res Λ A M) : res Λ A M :=
Res (wld r) (Excl' σ) (gst r).
Definition update_gst (m : M) (r : res Λ A M) : res Λ A M :=
Res (wld r) (pst r) m.
Definition del_wld (i : positive) (r : res Λ A M) : res Λ A M :=
Res (delete i (wld r)) (pst r) (gst r).
Instance update_gst_proper: Proper (dist n ==> dist n ==> dist n) update_gst.
Proof.
intros n m1 m2 Heqm r1 r2 [Heq1 Heq2 Heq3].
rewrite /update_gst. rewrite Heqm Heq1 Heq2 //=.
Qed.
Lemma wld_validN n r : ✓{n} r → ✓{n} wld r.
Proof. by intros (?&?&?). Qed.
Lemma gst_validN n r : ✓{n} r → ✓{n} gst r.
Proof. by intros (?&?&?). Qed.
Lemma Res_op w1 w2 σ1 σ2 m1 m2 :
Res w1 σ1 m1 ⋅ Res w2 σ2 m2 = Res (w1 ⋅ w2) (σ1 ⋅ σ2) (m1 ⋅ m2).
Proof. done. Qed.
Lemma Res_core w σ m : core (Res w σ m) = Res (core w) (core σ) (core m).
Proof. done. Qed.
Lemma lookup_wld_op_l n r1 r2 i P :
✓{n} (r1⋅r2) → wld r1 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof.
move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
Qed.
Lemma lookup_wld_op_r n r1 r2 i P :
✓{n} (r1⋅r2) → wld r2 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
Proof. rewrite (comm _ r1) (comm _ (wld r1)); apply lookup_wld_op_l. Qed.
Global Instance Res_timeless eσ m : Timeless m → Timeless (@Res Λ A M ∅ eσ m).
Proof. by intros ? ? [???]; constructor; apply (timeless _). Qed.
Global Instance Res_persistent w m: Persistent m → Persistent (@Res Λ A M w ∅ m).
Proof. do 2 constructor; apply (persistent_core _). Qed.
Internalized properties
Lemma res_equivI {M'} r1 r2 :
r1 ≡ r2 ⊣⊢ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2 : uPred M').
Proof.
uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
Qed.
Lemma res_validI {M'} r : ✓ r ⊣⊢ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M').
Proof. by uPred.unseal. Qed.
End res.
Arguments resC : clear implicits.
Arguments resR : clear implicits.
Arguments resUR : clear implicits.
Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
(f : A → A') (g : M → M') (r : res Λ A M) : res Λ A' M' :=
Res (agree_map f <$> wld r) (pst r) (g $ gst r).
Instance res_map_ne {Λ} {A A': cofeT} {M M' : ucmraT} (f : A → A') (g : M → M'):
(∀ n, Proper (dist n ==> dist n) f) → (∀ n, Proper (dist n ==> dist n) g) →
∀ n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
Proof. intros Hf n [] ? [???]; constructor; by cofe_subst. Qed.
Lemma res_map_id {Λ A} {M : ucmraT} (r : res Λ A M) : res_map id id r ≡ r.
Proof.
constructor; rewrite /res_map /=; f_equal.
rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext⇒ i y ? /=.
by rewrite -{2}(agree_map_id y).
Qed.
Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : ucmraT}
(f : A1 → A2) (f' : A2 → A3) (g : M1 → M2) (g' : M2 → M3) (r : res Λ A1 M1) :
res_map (f' ∘ f) (g' ∘ g) r ≡ res_map f' g' (res_map f g r).
Proof.
constructor; rewrite /res_map /=; f_equal.
rewrite -map_fmap_compose; apply map_fmap_setoid_ext⇒ i y _ /=.
by rewrite -agree_map_compose.
Qed.
Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : ucmraT}
(f f' : A → A') (g g' : M → M') (r : res Λ A M) :
(∀ x, f x ≡ f' x) → (∀ m, g m ≡ g' m) → res_map f g r ≡ res_map f' g' r.
Proof.
intros Hf Hg; split; simpl; auto.
by apply map_fmap_setoid_ext⇒i x ?; apply agree_map_ext.
Qed.
Instance res_map_cmra_monotone {Λ}
{A A' : cofeT} {M M': ucmraT} (f: A → A') (g: M → M') :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone g →
CMRAMonotone (@res_map Λ _ _ _ _ f g).
Proof.
split; first apply _.
- intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
Qed.
Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
CofeMor (res_map f g : resC Λ A M → resC Λ A' M').
Instance resC_map_ne {Λ A A' M M'} n :
Proper (dist n ==> dist n ==> dist n) (@resC_map Λ A A' M M').
Proof.
intros f g Hfg r; split; simpl; auto.
by apply (gmapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
Qed.
Program Definition resURF (Λ : language)
(F1 : cFunctor) (F2 : urFunctor) : urFunctor := {|
urFunctor_car A B := resUR Λ (cFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros Λ F1 F2 A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_ne.
- by apply urFunctor_ne.
Qed.
Next Obligation.
intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
apply res_map_ext⇒y. apply cFunctor_id. apply urFunctor_id.
Qed.
Next Obligation.
intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
apply res_map_ext⇒y. apply cFunctor_compose. apply urFunctor_compose.
Qed.
Instance resRF_contractive Λ F1 F2 :
cFunctorContractive F1 → urFunctorContractive F2 →
urFunctorContractive (resURF Λ F1 F2).
Proof.
intros ?? A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_contractive.
- by apply urFunctor_contractive.
Qed.
r1 ≡ r2 ⊣⊢ (wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2 : uPred M').
Proof.
uPred.unseal. do 2 split. by destruct 1. by intros (?&?&?); by constructor.
Qed.
Lemma res_validI {M'} r : ✓ r ⊣⊢ (✓ wld r ∧ ✓ pst r ∧ ✓ gst r : uPred M').
Proof. by uPred.unseal. Qed.
End res.
Arguments resC : clear implicits.
Arguments resR : clear implicits.
Arguments resUR : clear implicits.
Definition res_map {Λ} {A A' : cofeT} {M M' : cmraT}
(f : A → A') (g : M → M') (r : res Λ A M) : res Λ A' M' :=
Res (agree_map f <$> wld r) (pst r) (g $ gst r).
Instance res_map_ne {Λ} {A A': cofeT} {M M' : ucmraT} (f : A → A') (g : M → M'):
(∀ n, Proper (dist n ==> dist n) f) → (∀ n, Proper (dist n ==> dist n) g) →
∀ n, Proper (dist n ==> dist n) (@res_map Λ _ _ _ _ f g).
Proof. intros Hf n [] ? [???]; constructor; by cofe_subst. Qed.
Lemma res_map_id {Λ A} {M : ucmraT} (r : res Λ A M) : res_map id id r ≡ r.
Proof.
constructor; rewrite /res_map /=; f_equal.
rewrite -{2}(map_fmap_id (wld r)). apply map_fmap_setoid_ext⇒ i y ? /=.
by rewrite -{2}(agree_map_id y).
Qed.
Lemma res_map_compose {Λ} {A1 A2 A3 : cofeT} {M1 M2 M3 : ucmraT}
(f : A1 → A2) (f' : A2 → A3) (g : M1 → M2) (g' : M2 → M3) (r : res Λ A1 M1) :
res_map (f' ∘ f) (g' ∘ g) r ≡ res_map f' g' (res_map f g r).
Proof.
constructor; rewrite /res_map /=; f_equal.
rewrite -map_fmap_compose; apply map_fmap_setoid_ext⇒ i y _ /=.
by rewrite -agree_map_compose.
Qed.
Lemma res_map_ext {Λ} {A A' : cofeT} {M M' : ucmraT}
(f f' : A → A') (g g' : M → M') (r : res Λ A M) :
(∀ x, f x ≡ f' x) → (∀ m, g m ≡ g' m) → res_map f g r ≡ res_map f' g' r.
Proof.
intros Hf Hg; split; simpl; auto.
by apply map_fmap_setoid_ext⇒i x ?; apply agree_map_ext.
Qed.
Instance res_map_cmra_monotone {Λ}
{A A' : cofeT} {M M': ucmraT} (f: A → A') (g: M → M') :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone g →
CMRAMonotone (@res_map Λ _ _ _ _ f g).
Proof.
split; first apply _.
- intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
Qed.
Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
CofeMor (res_map f g : resC Λ A M → resC Λ A' M').
Instance resC_map_ne {Λ A A' M M'} n :
Proper (dist n ==> dist n ==> dist n) (@resC_map Λ A A' M M').
Proof.
intros f g Hfg r; split; simpl; auto.
by apply (gmapC_map_ne _ (agreeC_map f) (agreeC_map g)), agreeC_map_ne.
Qed.
Program Definition resURF (Λ : language)
(F1 : cFunctor) (F2 : urFunctor) : urFunctor := {|
urFunctor_car A B := resUR Λ (cFunctor_car F1 A B) (urFunctor_car F2 A B);
urFunctor_map A1 A2 B1 B2 fg :=resC_map (cFunctor_map F1 fg) (urFunctor_map F2 fg)
|}.
Next Obligation.
intros Λ F1 F2 A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_ne.
- by apply urFunctor_ne.
Qed.
Next Obligation.
intros Λ F Σ A B x. rewrite /= -{2}(res_map_id x).
apply res_map_ext⇒y. apply cFunctor_id. apply urFunctor_id.
Qed.
Next Obligation.
intros Λ F Σ A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -res_map_compose.
apply res_map_ext⇒y. apply cFunctor_compose. apply urFunctor_compose.
Qed.
Instance resRF_contractive Λ F1 F2 :
cFunctorContractive F1 → urFunctorContractive F2 →
urFunctorContractive (resURF Λ F1 F2).
Proof.
intros ?? A1 A2 B1 B2 n f g Hfg; apply resC_map_ne.
- by apply cFunctor_contractive.
- by apply urFunctor_contractive.
Qed.