Library iris.algebra.excl
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A → excl A
| ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclBot {_}.
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a ⇒ Some a | _ ⇒ None end.
Section excl.
Context {A : cofeT}.
Context {stepA: StepN A} `{@uStep A _}.
Implicit Types a b : A.
Implicit Types x y : excl A.
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
| ExclBot_equiv : ExclBot ≡ ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
Existing Instance excl_dist.
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A :=
{| chain_car n := match c n return _ with Excl y ⇒ y | _ ⇒ a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance excl_compl : Compl (excl A) := λ c,
match c 0 with Excl a ⇒ Excl (compl (excl_chain c a)) | x ⇒ x end.
Definition excl_cofe_mixin : CofeMixin (excl A).
Proof.
split.
- intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- intros n; split.
+ by intros []; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
- intros n c; rewrite /compl /excl_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
Global Instance excl_discrete : Discrete A → Discrete exclC.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless a : Timeless a → Timeless (Excl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ ⇒ True | ExclBot ⇒ False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ ⇒ True | ExclBot ⇒ False end.
Instance excl_pcore : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot.
Instance excl_stepN : StepN (excl A) := λ n x y,
match x, y with
| Excl a, Excl b ⇒ stepN n a b
| _, _ ⇒ False
end.
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split; try discriminate.
- by intros n []; destruct 1; constructor.
- by destruct 1; intros ?.
- intros x; split. done. by move⇒ /(_ 0).
- intros n [?|]; simpl; auto with lia.
- by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor.
- by intros n [?|] [?|].
- intros n x y1 y2 ? Hx.
by ∃ match y1, y2 with
| Excl a1, Excl a2 ⇒ (Excl a1, Excl a2)
| ExclBot, _ ⇒ (ExclBot, y2) | _, ExclBot ⇒ (y1, ExclBot)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
- intros n;
inversion_clear 1 as [? ? ? Hd |];
inversion_clear 1 as [? ? ? Hd' |];
intros Hstep;
rewrite /stepN /excl_stepN in Hstep *; eauto with *;
eapply ustep_ne; eauto.
- intros n [|] [|] Hs; try (exfalso; auto; done).
rewrite /stepN /excl_stepN in Hs *; eapply ustep_S; eauto.
Qed.
Canonical Structure exclR :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
Proof. split. apply _. by intros []. Qed.
From iris.algebra Require Import upred.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Inductive excl (A : Type) :=
| Excl : A → excl A
| ExclBot : excl A.
Arguments Excl {_} _.
Arguments ExclBot {_}.
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).
Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
match x with Excl a ⇒ Some a | _ ⇒ None end.
Section excl.
Context {A : cofeT}.
Context {stepA: StepN A} `{@uStep A _}.
Implicit Types a b : A.
Implicit Types x y : excl A.
Inductive excl_equiv : Equiv (excl A) :=
| Excl_equiv a b : a ≡ b → Excl a ≡ Excl b
| ExclBot_equiv : ExclBot ≡ ExclBot.
Existing Instance excl_equiv.
Inductive excl_dist : Dist (excl A) :=
| Excl_dist a b n : a ≡{n}≡ b → Excl a ≡{n}≡ Excl b
| ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
Existing Instance excl_dist.
Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
Proof. by constructor. Qed.
Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
Proof. by inversion_clear 1. Qed.
Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
Proof. by inversion_clear 1. Qed.
Program Definition excl_chain (c : chain (excl A)) (a : A) : chain A :=
{| chain_car n := match c n return _ with Excl y ⇒ y | _ ⇒ a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance excl_compl : Compl (excl A) := λ c,
match c 0 with Excl a ⇒ Excl (compl (excl_chain c a)) | x ⇒ x end.
Definition excl_cofe_mixin : CofeMixin (excl A).
Proof.
split.
- intros x y; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- intros n; split.
+ by intros []; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
- intros n c; rewrite /compl /excl_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (excl_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure exclC : cofeT := CofeT (excl A) excl_cofe_mixin.
Global Instance excl_discrete : Discrete A → Discrete exclC.
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
Global Instance Excl_timeless a : Timeless a → Timeless (Excl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance ExclBot_timeless : Timeless (@ExclBot A).
Proof. by inversion_clear 1; constructor. Qed.
Instance excl_valid : Valid (excl A) := λ x,
match x with Excl _ ⇒ True | ExclBot ⇒ False end.
Instance excl_validN : ValidN (excl A) := λ n x,
match x with Excl _ ⇒ True | ExclBot ⇒ False end.
Instance excl_pcore : PCore (excl A) := λ _, None.
Instance excl_op : Op (excl A) := λ x y, ExclBot.
Instance excl_stepN : StepN (excl A) := λ n x y,
match x, y with
| Excl a, Excl b ⇒ stepN n a b
| _, _ ⇒ False
end.
Lemma excl_cmra_mixin : CMRAMixin (excl A).
Proof.
split; try discriminate.
- by intros n []; destruct 1; constructor.
- by destruct 1; intros ?.
- intros x; split. done. by move⇒ /(_ 0).
- intros n [?|]; simpl; auto with lia.
- by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor.
- by intros n [?|] [?|].
- intros n x y1 y2 ? Hx.
by ∃ match y1, y2 with
| Excl a1, Excl a2 ⇒ (Excl a1, Excl a2)
| ExclBot, _ ⇒ (ExclBot, y2) | _, ExclBot ⇒ (y1, ExclBot)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
- intros n;
inversion_clear 1 as [? ? ? Hd |];
inversion_clear 1 as [? ? ? Hd' |];
intros Hstep;
rewrite /stepN /excl_stepN in Hstep *; eauto with *;
eapply ustep_ne; eauto.
- intros n [|] [|] Hs; try (exfalso; auto; done).
rewrite /stepN /excl_stepN in Hs *; eapply ustep_S; eauto.
Qed.
Canonical Structure exclR :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
Global Instance excl_cmra_discrete : Discrete A → CMRADiscrete exclR.
Proof. split. apply _. by intros []. Qed.
Internalized properties
Lemma excl_equivI {M} (x y : excl A) :
x ≡ y ⊣⊢ (match x, y with
| Excl a, Excl b ⇒ a ≡ b
| ExclBot, ExclBot ⇒ True
| _, _ ⇒ False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
x ≡ y ⊣⊢ (match x, y with
| Excl a, Excl b ⇒ a ≡ b
| ExclBot, ExclBot ⇒ True
| _, _ ⇒ False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} (x : excl A) :
✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
Exclusive
Option excl
Lemma excl_validN_inv_l n mx a : ✓{n} (Excl' a ⋅ mx) → mx = None.
Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
Proof. by destruct mx. Qed.
Lemma Excl_includedN n a mx : ✓{n} mx → Excl' a ≼{n} mx ↔ mx ≡{n}≡ Excl' a.
Proof.
intros Hvalid; split; [|by intros ->].
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Qed.
End excl.
Arguments exclC : clear implicits.
Arguments exclR : clear implicits.
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
match x with Excl a ⇒ Excl (f a) | ExclBot ⇒ ExclBot end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
excl_map (g ∘ f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
Instance excl_map_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Section functor.
Context {A B: cofeT}.
Context {stepA: StepN A} {PSA: @uStep A _}.
Context {stepB: StepN B} {PSB: @uStep B _}.
Instance excl_map_cmra_monotone (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
Proof.
split; try apply _.
- by intros n [a|].
- intros x y [z Hy]; ∃ (excl_map f z); apply equiv_dist⇒ n.
move: Hy⇒ /equiv_dist /(_ n) ->; by destruct x, z.
Qed.
Definition exclC_map (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
Instance exclC_map_ne n : Proper (dist n ==> dist n) (exclC_map).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
End functor.
Definition exclRADS (A: cofeT) := exclR A trivial_stepN trivial_stepN_ustep.
Program Definition exclRF (F : cFunctor) : rFunctor := {|
rFunctor_car A B := exclR (cFunctor_car F A B) trivial_stepN trivial_stepN_ustep;
rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F A B x; simpl. rewrite -{2}(excl_map_id x).
apply excl_map_ext⇒y. by rewrite cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
apply excl_map_ext⇒y; apply cFunctor_compose.
Qed.
Next Obligation. intros. econstructor; intros; simpl; eapply excl_map_cmra_monotone; eauto with ×. Qed.
Instance exclRF_contractive F :
cFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.
Proof. by destruct mx. Qed.
Lemma excl_validN_inv_r n mx a : ✓{n} (mx ⋅ Excl' a) → mx = None.
Proof. by destruct mx. Qed.
Lemma Excl_includedN n a mx : ✓{n} mx → Excl' a ≼{n} mx ↔ mx ≡{n}≡ Excl' a.
Proof.
intros Hvalid; split; [|by intros ->].
intros [z ?]; cofe_subst. by rewrite (excl_validN_inv_l n z a).
Qed.
End excl.
Arguments exclC : clear implicits.
Arguments exclR : clear implicits.
Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
match x with Excl a ⇒ Excl (f a) | ExclBot ⇒ ExclBot end.
Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
Proof. by destruct x. Qed.
Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
excl_map (g ∘ f) x = excl_map g (excl_map f x).
Proof. by destruct x. Qed.
Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
(∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
Proof. by destruct x; constructor. Qed.
Instance excl_map_ne {A B : cofeT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
Section functor.
Context {A B: cofeT}.
Context {stepA: StepN A} {PSA: @uStep A _}.
Context {stepB: StepN B} {PSB: @uStep B _}.
Instance excl_map_cmra_monotone (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
Proof.
split; try apply _.
- by intros n [a|].
- intros x y [z Hy]; ∃ (excl_map f z); apply equiv_dist⇒ n.
move: Hy⇒ /equiv_dist /(_ n) ->; by destruct x, z.
Qed.
Definition exclC_map (f : A -n> B) : exclC A -n> exclC B :=
CofeMor (excl_map f).
Instance exclC_map_ne n : Proper (dist n ==> dist n) (exclC_map).
Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
End functor.
Definition exclRADS (A: cofeT) := exclR A trivial_stepN trivial_stepN_ustep.
Program Definition exclRF (F : cFunctor) : rFunctor := {|
rFunctor_car A B := exclR (cFunctor_car F A B) trivial_stepN trivial_stepN_ustep;
rFunctor_map A1 A2 B1 B2 fg := exclC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros F A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F A B x; simpl. rewrite -{2}(excl_map_id x).
apply excl_map_ext⇒y. by rewrite cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -excl_map_compose.
apply excl_map_ext⇒y; apply cFunctor_compose.
Qed.
Next Obligation. intros. econstructor; intros; simpl; eapply excl_map_cmra_monotone; eauto with ×. Qed.
Instance exclRF_contractive F :
cFunctorContractive F → rFunctorContractive (exclRF F).
Proof.
intros A1 A2 B1 B2 n x1 x2 ??. by apply exclC_map_ne, cFunctor_contractive.
Qed.