Library iris.algebra.csum
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred updates local_updates.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /.
Inductive csum (A B : Type) :=
| Cinl : A → csum A B
| Cinr : B → csum A B
| CsumBot : csum A B.
Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
Section cofe.
Context {A B : cofeT}.
Implicit Types a : A.
Implicit Types b : B.
Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
| Cinlr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
| CsumBot_equiv : CsumBot ≡ CsumBot.
Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
| Cinlr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
| CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
Existing Instance csum_dist.
Global Instance Cinl_ne n : Proper (dist n ==> dist n) (@Cinl A B).
Proof. by constructor. Qed.
Global Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B).
Proof. by constructor. Qed.
Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinr_ne n : Proper (dist n ==> dist n) (@Cinr A B).
Proof. by constructor. Qed.
Global Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B).
Proof. by constructor. Qed.
Global Instance Cinr_inj : Inj (≡) (≡) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
Program Definition csum_chain_l (c : chain (csum A B)) (a : A) : chain A :=
{| chain_car n := match c n return _ with Cinl a' ⇒ a' | _ ⇒ a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition csum_chain_r (c : chain (csum A B)) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' ⇒ b' | _ ⇒ b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance csum_compl : Compl (csum A B) := λ c,
match c 0 with
| Cinl a ⇒ Cinl (compl (csum_chain_l c a))
| Cinr b ⇒ Cinr (compl (csum_chain_r c b))
| CsumBot ⇒ CsumBot
end.
Definition csum_cofe_mixin : CofeMixin (csum A B).
Proof.
split.
- intros mx my; split.
+ by destruct 1; constructor; try apply equiv_dist.
+ intros Hxy; feed inversion (Hxy 0); subst; constructor; try done;
apply equiv_dist⇒ n; by feed inversion (Hxy n).
- intros n; split.
+ by intros [|a|]; 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 /csum_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+ rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
+ rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure csumC : cofeT := CofeT (csum A B) csum_cofe_mixin.
Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC.
Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
Global Instance csum_leibniz :
LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B).
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_timeless a : Timeless a → Timeless (Cinl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance Cinr_timeless b : Timeless b → Timeless (Cinr b).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
End cofe.
Arguments csumC : clear implicits.
Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
(x : csum A B) : csum A' B' :=
match x with
| Cinl a ⇒ Cinl (fA a)
| Cinr b ⇒ Cinr (fB b)
| CsumBot ⇒ CsumBot
end.
Instance: Params (@csum_map) 4.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
(g : B → B') (g' : B' → B'') (x : csum A B) :
csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
Proof. by destruct x. Qed.
Lemma csum_map_ext {A A' B B' : cofeT} (f f' : A → A') (g g' : B → B') x :
(∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
Proof. by destruct x; constructor. Qed.
Instance csum_map_cmra_ne {A A' B B' : cofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumC A B -n> csumC A' B' :=
CofeMor (csum_map f g).
Instance csumC_map_ne A A' B B' n :
Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B').
Proof. by intros f f' Hf g g' Hg []; constructor. Qed.
Section cmra.
Context {A B : cmraT}.
Implicit Types a : A.
Implicit Types b : B.
Instance csum_valid : Valid (csum A B) := λ x,
match x with
| Cinl a ⇒ ✓ a
| Cinr b ⇒ ✓ b
| CsumBot ⇒ False
end.
Instance csum_validN : ValidN (csum A B) := λ n x,
match x with
| Cinl a ⇒ ✓{n} a
| Cinr b ⇒ ✓{n} b
| CsumBot ⇒ False
end.
Instance csum_pcore : PCore (csum A B) := λ x,
match x with
| Cinl a ⇒ Cinl <$> pcore a
| Cinr b ⇒ Cinr <$> pcore b
| CsumBot ⇒ Some CsumBot
end.
Instance csum_op : Op (csum A B) := λ x y,
match x, y with
| Cinl a, Cinl a' ⇒ Cinl (a ⋅ a')
| Cinr b, Cinr b' ⇒ Cinr (b ⋅ b')
| _, _ ⇒ CsumBot
end.
Instance csum_stepN : StepN (csum A B) := λ n x y, True.
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
Proof. done. Qed.
Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
Proof. done. Qed.
Lemma csum_included x y :
x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
Proof.
split.
- intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto.
+ right; left; eexists _, _; split_and!; eauto. eexists; eauto.
+ right; right; eexists _, _; split_and!; eauto. eexists; eauto.
- intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+ destruct x; ∃ CsumBot; constructor.
+ ∃ (Cinl c); by constructor.
+ ∃ (Cinr c); by constructor.
Qed.
Lemma csum_cmra_mixin : CMRAMixin (csum A B).
Proof.
split.
- intros n []; destruct 1; constructor; by cofe_subst.
- intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
∃ (Cinl ca'); by repeat constructor.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
∃ (Cinr cb'); by repeat constructor.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; cofe_subst; done.
- intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- intros n [a|b|]; simpl; auto using cmra_validN_S.
- intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
- intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
- intros [a|b|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
constructor; eauto using cmra_pcore_l.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
constructor; eauto using cmra_pcore_l.
- intros [a|b|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
+ ∃ CsumBot. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
∃ (Cinl ca'). rewrite csum_included; eauto 10.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
∃ (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a|b|] [a'|b'|]; try (intros ??; inversion 1; done).
+ rewrite //=. intros ?? Hval.
destruct (pcore a) as [ca|] eqn:?; simplify_option_eq; try congruence.
destruct (pcore a') as [ca'|] eqn:?; simplify_option_eq; try congruence.
eapply cmra_pcore_distrib in Hval as (caa'&Hcaa'&Heq); eauto.
do 2 inversion 1; subst.
∃ (Cinl caa').
rewrite //= Hcaa'; split; eauto.
by rewrite Heq.
+ rewrite //=. intros ?? Hval.
destruct (pcore b) as [cb|] eqn:?; simplify_option_eq; try congruence.
destruct (pcore b') as [cb'|] eqn:?; simplify_option_eq; try congruence.
eapply cmra_pcore_distrib in Hval as (cbb'&Hcbb'&Heq); eauto.
do 2 inversion 1; subst.
∃ (Cinr cbb').
rewrite //= Hcbb'; split; eauto.
by rewrite Heq.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinl) in Hx'.
destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto.
∃ (Cinl z1, Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinr) in Hx'.
destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto.
∃ (Cinr z1, Cinr z2). by repeat constructor.
+ by ∃ (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
- by intros.
- by intros.
Qed.
Canonical Structure csumR :=
CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
Global Instance csum_cmra_discrete :
CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.
Proof.
split; first apply _.
by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
Qed.
Global Instance Cinl_persistent a : Persistent a → Persistent (Cinl a).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinr_persistent b : Persistent b → Persistent (Cinr b).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
Proof. by move⇒ H[]? =>[/H||]. Qed.
Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
Proof. by move⇒ H[]? =>[|/H|]. Qed.
From iris.algebra Require Import upred updates local_updates.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /.
Inductive csum (A B : Type) :=
| Cinl : A → csum A B
| Cinr : B → csum A B
| CsumBot : csum A B.
Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
Section cofe.
Context {A B : cofeT}.
Implicit Types a : A.
Implicit Types b : B.
Inductive csum_equiv : Equiv (csum A B) :=
| Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
| Cinlr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
| CsumBot_equiv : CsumBot ≡ CsumBot.
Existing Instance csum_equiv.
Inductive csum_dist : Dist (csum A B) :=
| Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
| Cinlr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
| CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
Existing Instance csum_dist.
Global Instance Cinl_ne n : Proper (dist n ==> dist n) (@Cinl A B).
Proof. by constructor. Qed.
Global Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B).
Proof. by constructor. Qed.
Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinr_ne n : Proper (dist n ==> dist n) (@Cinr A B).
Proof. by constructor. Qed.
Global Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B).
Proof. by constructor. Qed.
Global Instance Cinr_inj : Inj (≡) (≡) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
Proof. by inversion_clear 1. Qed.
Program Definition csum_chain_l (c : chain (csum A B)) (a : A) : chain A :=
{| chain_car n := match c n return _ with Cinl a' ⇒ a' | _ ⇒ a end |}.
Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Program Definition csum_chain_r (c : chain (csum A B)) (b : B) : chain B :=
{| chain_car n := match c n return _ with Cinr b' ⇒ b' | _ ⇒ b end |}.
Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance csum_compl : Compl (csum A B) := λ c,
match c 0 with
| Cinl a ⇒ Cinl (compl (csum_chain_l c a))
| Cinr b ⇒ Cinr (compl (csum_chain_r c b))
| CsumBot ⇒ CsumBot
end.
Definition csum_cofe_mixin : CofeMixin (csum A B).
Proof.
split.
- intros mx my; split.
+ by destruct 1; constructor; try apply equiv_dist.
+ intros Hxy; feed inversion (Hxy 0); subst; constructor; try done;
apply equiv_dist⇒ n; by feed inversion (Hxy n).
- intros n; split.
+ by intros [|a|]; 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 /csum_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+ rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
+ rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure csumC : cofeT := CofeT (csum A B) csum_cofe_mixin.
Global Instance csum_discrete : Discrete A → Discrete B → Discrete csumC.
Proof. by inversion_clear 3; constructor; apply (timeless _). Qed.
Global Instance csum_leibniz :
LeibnizEquiv A → LeibnizEquiv B → LeibnizEquiv (csumC A B).
Proof. by destruct 3; f_equal; apply leibniz_equiv. Qed.
Global Instance Cinl_timeless a : Timeless a → Timeless (Cinl a).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
Global Instance Cinr_timeless b : Timeless b → Timeless (Cinr b).
Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
End cofe.
Arguments csumC : clear implicits.
Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
(x : csum A B) : csum A' B' :=
match x with
| Cinl a ⇒ Cinl (fA a)
| Cinr b ⇒ Cinr (fB b)
| CsumBot ⇒ CsumBot
end.
Instance: Params (@csum_map) 4.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
(g : B → B') (g' : B' → B'') (x : csum A B) :
csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
Proof. by destruct x. Qed.
Lemma csum_map_ext {A A' B B' : cofeT} (f f' : A → A') (g g' : B → B') x :
(∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
Proof. by destruct x; constructor. Qed.
Instance csum_map_cmra_ne {A A' B B' : cofeT} n :
Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
(@csum_map A A' B B').
Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
csumC A B -n> csumC A' B' :=
CofeMor (csum_map f g).
Instance csumC_map_ne A A' B B' n :
Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B').
Proof. by intros f f' Hf g g' Hg []; constructor. Qed.
Section cmra.
Context {A B : cmraT}.
Implicit Types a : A.
Implicit Types b : B.
Instance csum_valid : Valid (csum A B) := λ x,
match x with
| Cinl a ⇒ ✓ a
| Cinr b ⇒ ✓ b
| CsumBot ⇒ False
end.
Instance csum_validN : ValidN (csum A B) := λ n x,
match x with
| Cinl a ⇒ ✓{n} a
| Cinr b ⇒ ✓{n} b
| CsumBot ⇒ False
end.
Instance csum_pcore : PCore (csum A B) := λ x,
match x with
| Cinl a ⇒ Cinl <$> pcore a
| Cinr b ⇒ Cinr <$> pcore b
| CsumBot ⇒ Some CsumBot
end.
Instance csum_op : Op (csum A B) := λ x y,
match x, y with
| Cinl a, Cinl a' ⇒ Cinl (a ⋅ a')
| Cinr b, Cinr b' ⇒ Cinr (b ⋅ b')
| _, _ ⇒ CsumBot
end.
Instance csum_stepN : StepN (csum A B) := λ n x y, True.
Lemma Cinl_op a a' : Cinl a ⋅ Cinl a' = Cinl (a ⋅ a').
Proof. done. Qed.
Lemma Cinr_op b b' : Cinr b ⋅ Cinr b' = Cinr (b ⋅ b').
Proof. done. Qed.
Lemma csum_included x y :
x ≼ y ↔ y = CsumBot ∨ (∃ a a', x = Cinl a ∧ y = Cinl a' ∧ a ≼ a')
∨ (∃ b b', x = Cinr b ∧ y = Cinr b' ∧ b ≼ b').
Proof.
split.
- intros [z Hy]; destruct x as [a|b|], z as [a'|b'|]; inversion_clear Hy; auto.
+ right; left; eexists _, _; split_and!; eauto. eexists; eauto.
+ right; right; eexists _, _; split_and!; eauto. eexists; eauto.
- intros [->|[(a&a'&->&->&c&?)|(b&b'&->&->&c&?)]].
+ destruct x; ∃ CsumBot; constructor.
+ ∃ (Cinl c); by constructor.
+ ∃ (Cinr c); by constructor.
Qed.
Lemma csum_cmra_mixin : CMRAMixin (csum A B).
Proof.
split.
- intros n []; destruct 1; constructor; by cofe_subst.
- intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
∃ (Cinl ca'); by repeat constructor.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_ne n b b' cb) as (cb'&->&?); auto.
∃ (Cinr cb'); by repeat constructor.
- intros ? [a|b|] [a'|b'|] H; inversion_clear H; cofe_subst; done.
- intros [a|b|]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O.
- intros n [a|b|]; simpl; auto using cmra_validN_S.
- intros [a1|b1|] [a2|b2|] [a3|b3|]; constructor; by rewrite ?assoc.
- intros [a1|b1|] [a2|b2|]; constructor; by rewrite 1?comm.
- intros [a|b|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
constructor; eauto using cmra_pcore_l.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
constructor; eauto using cmra_pcore_l.
- intros [a|b|] ? [=]; subst; auto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
+ ∃ CsumBot. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
∃ (Cinl ca'). rewrite csum_included; eauto 10.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
∃ (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a|b|] [a'|b'|]; try (intros ??; inversion 1; done).
+ rewrite //=. intros ?? Hval.
destruct (pcore a) as [ca|] eqn:?; simplify_option_eq; try congruence.
destruct (pcore a') as [ca'|] eqn:?; simplify_option_eq; try congruence.
eapply cmra_pcore_distrib in Hval as (caa'&Hcaa'&Heq); eauto.
do 2 inversion 1; subst.
∃ (Cinl caa').
rewrite //= Hcaa'; split; eauto.
by rewrite Heq.
+ rewrite //=. intros ?? Hval.
destruct (pcore b) as [cb|] eqn:?; simplify_option_eq; try congruence.
destruct (pcore b') as [cb'|] eqn:?; simplify_option_eq; try congruence.
eapply cmra_pcore_distrib in Hval as (cbb'&Hcbb'&Heq); eauto.
do 2 inversion 1; subst.
∃ (Cinr cbb').
rewrite //= Hcbb'; split; eauto.
by rewrite Heq.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinl) in Hx'.
destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto.
∃ (Cinl z1, Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinr) in Hx'.
destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto.
∃ (Cinr z1, Cinr z2). by repeat constructor.
+ by ∃ (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
- by intros.
- by intros.
Qed.
Canonical Structure csumR :=
CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
Global Instance csum_cmra_discrete :
CMRADiscrete A → CMRADiscrete B → CMRADiscrete csumR.
Proof.
split; first apply _.
by move=>[a|b|] HH /=; try apply cmra_discrete_valid.
Qed.
Global Instance Cinl_persistent a : Persistent a → Persistent (Cinl a).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinr_persistent b : Persistent b → Persistent (Cinr b).
Proof. rewrite /Persistent /=. inversion_clear 1; by repeat constructor. Qed.
Global Instance Cinl_exclusive a : Exclusive a → Exclusive (Cinl a).
Proof. by move⇒ H[]? =>[/H||]. Qed.
Global Instance Cinr_exclusive b : Exclusive b → Exclusive (Cinr b).
Proof. by move⇒ H[]? =>[|/H|]. Qed.
Internalized properties
Lemma csum_equivI {M} (x y : csum A B) :
x ≡ y ⊣⊢ (match x, y with
| Cinl a, Cinl a' ⇒ a ≡ a'
| Cinr b, Cinr b' ⇒ b ≡ b'
| CsumBot, CsumBot ⇒ True
| _, _ ⇒ False
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma csum_validI {M} (x : csum A B) :
✓ x ⊣⊢ (match x with
| Cinl a ⇒ ✓ a
| Cinr b ⇒ ✓ b
| CsumBot ⇒ False
end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
x ≡ y ⊣⊢ (match x, y with
| Cinl a, Cinl a' ⇒ a ≡ a'
| Cinr b, Cinr b' ⇒ b ≡ b'
| CsumBot, CsumBot ⇒ True
| _, _ ⇒ False
end : uPred M).
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma csum_validI {M} (x : csum A B) :
✓ x ⊣⊢ (match x with
| Cinl a ⇒ ✓ a
| Cinr b ⇒ ✓ b
| CsumBot ⇒ False
end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
Updates
Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 → Cinl a1 ~~> Cinl a2.
Proof.
intros Ha n [[a|b|]|] ?; simpl in *; auto.
- by apply (Ha n (Some a)).
- by apply (Ha n None).
Qed.
Lemma csum_update_r (b1 b2 : B) : b1 ~~> b2 → Cinr b1 ~~> Cinr b2.
Proof.
intros Hb n [[a|b|]|] ?; simpl in *; auto.
- by apply (Hb n (Some b)).
- by apply (Hb n None).
Qed.
Lemma csum_updateP_l (P : A → Prop) (Q : csum A B → Prop) a :
a ~~>: P → (∀ a', P a' → Q (Cinl a')) → Cinl a ~~>: Q.
Proof.
intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
- destruct (Hx n (Some a')) as (c&?&?); naive_solver.
- destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
Lemma csum_updateP_r (P : B → Prop) (Q : csum A B → Prop) b :
b ~~>: P → (∀ b', P b' → Q (Cinr b')) → Cinr b ~~>: Q.
Proof.
intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
- destruct (Hx n (Some b')) as (c&?&?); naive_solver.
- destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
Lemma csum_updateP'_l (P : A → Prop) a :
a ~~>: P → Cinl a ~~>: λ m', ∃ a', m' = Cinl a' ∧ P a'.
Proof. eauto using csum_updateP_l. Qed.
Lemma csum_updateP'_r (P : B → Prop) b :
b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
Proof. eauto using csum_updateP_r. Qed.
Lemma csum_local_update_l (a1 a2 : A) af :
(∀ af', af = Cinl <$> af' → a1 ¬l~> a2 @ af') → Cinl a1 ¬l~> Cinl a2 @ af.
Proof.
intros Ha. split; destruct af as [[af'| |]|]=>//=.
- by eapply (Ha (Some af')).
- by eapply (Ha None).
- destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
- destruct (Ha None (reflexivity _)) as [_ Ha'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
Qed.
Lemma csum_local_update_r (b1 b2 : B) bf :
(∀ bf', bf = Cinr <$> bf' → b1 ¬l~> b2 @ bf') → Cinr b1 ¬l~> Cinr b2 @ bf.
Proof.
intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
- by eapply (Hb (Some bf')).
- by eapply (Hb None).
- destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
- destruct (Hb None (reflexivity _)) as [_ Hb'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
Qed.
End cmra.
Arguments csumR : clear implicits.
Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CMRAMonotone f → CMRAMonotone g → CMRAMonotone (csum_map f g).
Proof.
split; try apply _.
- intros n [a|b|]; simpl; auto using validN_preserving.
- intros x y; rewrite !csum_included.
intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
eauto 10 using cmra_monotone.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}.
Next Obligation.
by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
Qed.
Next Obligation.
intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x).
apply csum_map_ext⇒y; apply rFunctor_id.
Qed.
Next Obligation.
intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose.
apply csum_map_ext⇒y; apply rFunctor_compose.
Qed.
Instance csumRF_contractive Fa Fb :
rFunctorContractive Fa → rFunctorContractive Fb →
rFunctorContractive (csumRF Fa Fb).
Proof.
by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive.
Qed.
Proof.
intros Ha n [[a|b|]|] ?; simpl in *; auto.
- by apply (Ha n (Some a)).
- by apply (Ha n None).
Qed.
Lemma csum_update_r (b1 b2 : B) : b1 ~~> b2 → Cinr b1 ~~> Cinr b2.
Proof.
intros Hb n [[a|b|]|] ?; simpl in *; auto.
- by apply (Hb n (Some b)).
- by apply (Hb n None).
Qed.
Lemma csum_updateP_l (P : A → Prop) (Q : csum A B → Prop) a :
a ~~>: P → (∀ a', P a' → Q (Cinl a')) → Cinl a ~~>: Q.
Proof.
intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
- destruct (Hx n (Some a')) as (c&?&?); naive_solver.
- destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
Lemma csum_updateP_r (P : B → Prop) (Q : csum A B → Prop) b :
b ~~>: P → (∀ b', P b' → Q (Cinr b')) → Cinr b ~~>: Q.
Proof.
intros Hx HP n mf Hm. destruct mf as [[a'|b'|]|]; try by destruct Hm.
- destruct (Hx n (Some b')) as (c&?&?); naive_solver.
- destruct (Hx n None) as (c&?&?); naive_solver eauto using cmra_validN_op_l.
Qed.
Lemma csum_updateP'_l (P : A → Prop) a :
a ~~>: P → Cinl a ~~>: λ m', ∃ a', m' = Cinl a' ∧ P a'.
Proof. eauto using csum_updateP_l. Qed.
Lemma csum_updateP'_r (P : B → Prop) b :
b ~~>: P → Cinr b ~~>: λ m', ∃ b', m' = Cinr b' ∧ P b'.
Proof. eauto using csum_updateP_r. Qed.
Lemma csum_local_update_l (a1 a2 : A) af :
(∀ af', af = Cinl <$> af' → a1 ¬l~> a2 @ af') → Cinl a1 ¬l~> Cinl a2 @ af.
Proof.
intros Ha. split; destruct af as [[af'| |]|]=>//=.
- by eapply (Ha (Some af')).
- by eapply (Ha None).
- destruct (Ha (Some af') (reflexivity _)) as [_ Ha'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
- destruct (Ha None (reflexivity _)) as [_ Ha'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Ha' n (Some mz)). by apply (Ha' n None).
Qed.
Lemma csum_local_update_r (b1 b2 : B) bf :
(∀ bf', bf = Cinr <$> bf' → b1 ¬l~> b2 @ bf') → Cinr b1 ¬l~> Cinr b2 @ bf.
Proof.
intros Hb. split; destruct bf as [[|bf'|]|]=>//=.
- by eapply (Hb (Some bf')).
- by eapply (Hb None).
- destruct (Hb (Some bf') (reflexivity _)) as [_ Hb'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
- destruct (Hb None (reflexivity _)) as [_ Hb'].
intros n [[mz|mz|]|] ?; inversion 1; subst; constructor.
by apply (Hb' n (Some mz)). by apply (Hb' n None).
Qed.
End cmra.
Arguments csumR : clear implicits.
Instance csum_map_cmra_monotone {A A' B B' : cmraT} (f : A → A') (g : B → B') :
CMRAMonotone f → CMRAMonotone g → CMRAMonotone (csum_map f g).
Proof.
split; try apply _.
- intros n [a|b|]; simpl; auto using validN_preserving.
- intros x y; rewrite !csum_included.
intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
eauto 10 using cmra_monotone.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
rFunctor_map A1 A2 B1 B2 fg := csumC_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
|}.
Next Obligation.
by intros Fa Fb A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_ne.
Qed.
Next Obligation.
intros Fa Fb A B x. rewrite /= -{2}(csum_map_id x).
apply csum_map_ext⇒y; apply rFunctor_id.
Qed.
Next Obligation.
intros Fa Fb A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -csum_map_compose.
apply csum_map_ext⇒y; apply rFunctor_compose.
Qed.
Instance csumRF_contractive Fa Fb :
rFunctorContractive Fa → rFunctorContractive Fb →
rFunctorContractive (csumRF Fa Fb).
Proof.
by intros ?? A1 A2 B1 B2 n f g Hfg; apply csumC_map_ne; try apply rFunctor_contractive.
Qed.