Skip to content
GitLab
Commit 7f0bdb3c authored by Ike Mulder's avatar Ike Mulder
Browse files

Merged master back in.

parents b7a6d2b0 326964bd
Pipeline #60391 passed with stage
in 7 minutes and 31 seconds
Expand all Show whitespace changes
Inline Side-by-side
.gitlab-ci.yml
View file @ 7f0bdb3c
......@@ -40,3 +40,8 @@ build-coq.8.14.1:
variables:
OPAM_PINS: "coq version 8.14.1"
build-coq.8.14.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.14.1"
theories/biabd/biabd_local_updates.v
View file @ 7f0bdb3c
......@@ -327,7 +327,9 @@ Section other.
End other.
Class IsValidOp {A : cmra} (a a1 a2 : A) Σ (P : iPropI Σ) := {
From iris_automation.biabd Require Export proofmode_classes proofmode_instances.
(*Class IsValidOp {A : cmra} (a a1 a2 : A) Σ (P : iPropI Σ) := {
is_valid_merge : ✓ (a1 ⋅ a2) ⊢ □ P ;
is_valid_op : ✓ (a1 ⋅ a2) ⊢@{iPropI Σ} a ≡ a1 ⋅ a2 ;
}.
......@@ -353,7 +355,7 @@ Class NonUnital {A : cmra} (a : A) Σ :=
non_unital_element b : a ≡ a ⋅ b ⊢@{iPropI Σ} False.
Class HasRightId {A : cmra} (a : A) :=
has_right_id : ∃ c, a ≡ a ⋅ c.
has_right_id : ∃ c, a ≡ a ⋅ c. *)
Class CmraSubtract {A : cmra} (a b : A) (φ : Prop) (c : option A) :=
cmra_subtract : φ → default b (c' ← c; Some $ b ⋅ c') ≡ a.
......@@ -382,7 +384,7 @@ From iris.proofmode Require Import base classes reduction tactics.
From iris.algebra Require Import agree frac.
Section validity.
Implicit Types Σ : gFunctors.
Implicit Types Σ : gFunctors. (*
Lemma from_isop {A : cmra} (a a1 a2 : A) {Σ} :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I.
Proof.
......@@ -406,7 +408,7 @@ Section validity.
Global Instance merge_unital_proper a1 a2 Σ : Proper ((≡@{iPropI Σ}) ==> (iff)) (IsIncludedMergeUnital a1 a2).
Proof. solve_proper. Qed.
End proper.
End proper. *)
Section base_instances_cmra.
Context {A : cmra}.
......@@ -427,7 +429,7 @@ Section validity.
split =>//.
move => c /cmra_valid_validN Hn.
by eapply H.
Qed.
Qed. (*
Lemma is_included_merge' (a1 a2 : A) {Σ} (P : iPropI Σ) :
IsIncludedMerge a1 a2 P →
......@@ -467,26 +469,26 @@ Section validity.
rewrite H.
iLeft.
by iApply "H✓".
Qed.
Qed. *)
End base_instances_cmra.
Section base_instances_ucmra.
Context {A : ucmra}.
Context {A : ucmra}. (*
Global Instance valid_op_unit_left (a : A) Σ :
IsValidOp a ε a Σ True%I | 5.
Proof. apply from_isop. rewrite /IsOp left_id //. Qed.
Global Instance valid_op_unit_right (a : A) Σ:
IsValidOp a a ε Σ True%I | 5.
Proof. apply from_isop. rewrite /IsOp right_id //. Qed.
Proof. apply from_isop. rewrite /IsOp right_id //. Qed. *)
Global Instance ucmra_subtract_all (a : A) : UcmraSubtract a a True ε | 100.
(* this one may glance over pcore like info we can actually keep *)
Proof. by rewrite /UcmraSubtract /CmraSubtract /= right_id => _. Qed.
Global Instance ucmra_subtract_unit (a : A) : UcmraSubtract a ε True a | 101.
Proof. rewrite /UcmraSubtract /CmraSubtract /= left_id //. Qed.
Proof. rewrite /UcmraSubtract /CmraSubtract /= left_id //. Qed. (*
Global Instance included_merge_unital_from_reg (a1 a2 : A) {Σ} (P : iProp Σ) :
IsIncludedMerge a1 a2 P →
......@@ -502,7 +504,7 @@ Section validity.
iLeft. by iApply "H✓".
Qed.
Global Instance ucmra_has_right_id (a : A) : HasRightId a.
Proof. exists ε. by rewrite right_id. Qed.
Proof. exists ε. by rewrite right_id. Qed. *)
Global Instance find_local_update_from_subtract (x x' : A) r φ :
UcmraSubtract x' x φ r →
......@@ -539,14 +541,14 @@ Section validity.
Qed.
End base_instances_ucmra.
Section numbers.
Section numbers. (*
Global Instance nat_valid_op (a a1 a2 : nat) Σ:
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I | 10.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance ucmra_subtract_nat (a1 a2 : nat) :
TCIf (SolveSepSideCondition (a1 < a2)%nat) False TCTrue → (* guards against obviously impossible things *)
UcmraSubtract a1 a2 (a2 ≤ a1) (a1 - a2)%nat.
Proof. rewrite /UcmraSubtract /CmraSubtract /= nat_op => _ Ha. fold_leibniz. lia. Qed.
Proof. rewrite /UcmraSubtract /CmraSubtract /= nat_op => _ Ha. fold_leibniz. lia. Qed. (*
Global Instance nat_included_merge (a1 a2 : nat) {Σ} : IsIncludedMerge a1 a2 (Σ := Σ) ⌜a1 ≤ a2⌝%I.
Proof.
rewrite /IsIncludedMerge.
......@@ -557,13 +559,13 @@ Section validity.
Global Instance nat_max_valid_op (a a1 a2 : max_nat) Σ :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I | 10.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance ucmra_subtract_max_nat (a1 a2 : nat) :
UcmraSubtract (MaxNat a1) (MaxNat a2) (a2 ≤ a1) (MaxNat a1).
Proof.
rewrite /UcmraSubtract /CmraSubtract /= max_nat_op => Ha.
fold_leibniz. f_equal. lia.
Qed.
Qed. (*
Global Instance nat_max_included_merge (a1 a2 : nat) {Σ} : IsIncludedMerge (MaxNat a1) (MaxNat a2) (Σ := Σ) ⌜a1 ≤ a2⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
......@@ -573,32 +575,32 @@ Section validity.
Global Instance nat_min_valid_op (a a1 a2 : min_nat) Σ :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance cmra_subtract_min_nat (a1 a2 : nat) :
CmraSubtract (MinNat a1) (MinNat a2) (a1 ≤ a2) (Some $ MinNat a1).
Proof.
rewrite /UcmraSubtract /CmraSubtract /= min_nat_op_min => Ha.
fold_leibniz. f_equal. lia.
Qed.
Qed. (*
Global Instance nat_min_included_merge (a1 a2 : nat) {Σ} : IsIncludedMerge (MinNat a1) (MinNat a2) (Σ := Σ) ⌜a2 ≤ a1⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
- by iDestruct 1 as %?%min_nat_included.
- iIntros "%". iExists (MinNat a2). rewrite min_nat_op_min. iPureIntro. fold_leibniz. f_equal. lia.
Qed.
Qed. *)
Lemma nat_min_coalloc n : CoAllocate (MinNat n) (Some $ MinNat 0).
(* 0 is the maximal element for minnat. This is not an instance - we don't usually want to coallocate 0 with n *)
Proof.
split => //.
move => [c] /min_nat_included /= /le_n_0_eq <- _ m.
apply min_nat_included => /=. lia.
Qed.
Qed. (*
Global Instance min_nat_has_right_id n : HasRightId (MinNat n).
Proof. exists (MinNat n). rewrite min_nat_op_min. fold_leibniz. f_equal. lia. Qed.
Global Instance positive_valid_op (a a1 a2 : positive) Σ :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance cmra_subtract_positive_lt (a1 a2 : positive) :
SolveSepSideCondition (a2 < a1)%positive →
CmraSubtract a1 a2 True (Some (a1 - a2)%positive).
......@@ -609,7 +611,7 @@ Section validity.
Global Instance cmra_subtract_positive_eq (a1 a2 : positive) :
SolveSepSideCondition (a2 = a1) →
CmraSubtract a1 a2 True None.
Proof. by rewrite /CmraSubtract /= => ->. Qed.
Proof. by rewrite /CmraSubtract /= => ->. Qed. (*
Global Instance positive_included_merge (a1 a2 : positive) {Σ} : IsIncludedMerge a1 a2 (Σ := Σ) ⌜(a1 < a2)%positive⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
......@@ -636,7 +638,7 @@ Section validity.
rewrite /IsOp; split; last first.
{ rewrite H; eauto. }
by iDestruct 1 as %?%frac_valid.
Qed.
Qed. *)
Global Instance frac_subtract_half (q : Qp) :
CmraSubtract q (q/2)%Qp True (Some (q/2)%Qp) | 10.
Proof. rewrite /CmraSubtract /= => _. by rewrite frac_op Qp_div_2. Qed.
......@@ -667,7 +669,7 @@ Section validity.
Proof.
rewrite /CmraSubtract /= => Hφ1 Hφ2.
case => /Hφ1 <- /Hφ2 <- //.
Qed.
Qed. (*
Global Instance frac_included_merge (q1 q2 : Qp) {Σ} : IsIncludedMerge q1 q2 (Σ := Σ) ⌜(q1 < q2)%Qp⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_" ; iSplit.
......@@ -692,7 +694,7 @@ Section validity.
Proof.
rewrite /NonUnital => q. iIntros "%". fold_leibniz.
rewrite frac_op in H. apply eq_sym in H. by apply Qp_add_id_free in H.
Qed.
Qed. *)
Global Instance frac_coallocate_half :
CoAllocate (1/2)%Qp (Some $ 1/2)%Qp.
......@@ -732,7 +734,7 @@ Section validity.
End numbers.
Section sets.
Context `{Countable K}.
Context `{Countable K}. (*
Global Instance set_is_op_emp_l (X : gset K) :
IsOp X ∅ X | 10.
Proof. rewrite /IsOp. set_solver. Qed.
......@@ -745,11 +747,11 @@ Section validity.
Global Instance set_is_valid_op (a a1 a2 : gset K) Σ :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I | 10.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance ucmra_set_subtract_refl (a : gset K): UcmraSubtract a a True a | 10.
Proof. rewrite /UcmraSubtract /CmraSubtract /= gset_op. set_solver. Qed.
Global Instance ucmra_set_subtract (a1 a2 : gset K) : UcmraSubtract a1 a2 (a2 ⊆ a1) a1 | 20.
Proof. rewrite /UcmraSubtract /CmraSubtract /= gset_op. set_solver. Qed.
Proof. rewrite /UcmraSubtract /CmraSubtract /= gset_op. set_solver. Qed. (*
Global Instance set_included_merge (a1 a2 : gset K) {Σ} : IsIncludedMerge a1 a2 (Σ := Σ) ⌜a1 ⊆ a2⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
......@@ -770,7 +772,7 @@ Section validity.
Proof. apply from_isop. rewrite /IsOp. rewrite gset_disj_union; [f_equal | ]; set_solver. Qed.
Global Instance set_disj_valid_op_emp_r (X Y : gset K) Σ :
IsValidOp (GSet X) (GSet ∅) (GSet X) Σ True%I | 10.
Proof. apply from_isop. rewrite /IsOp. rewrite gset_disj_union; [f_equal | ]; set_solver. Qed.
Proof. apply from_isop. rewrite /IsOp. rewrite gset_disj_union; [f_equal | ]; set_solver. Qed. *)
Global Instance ucmra_disjoint_set_subtract_refl (a : gset K) :
UcmraSubtract (GSet a) (GSet a) True ε | 10.
Proof. eapply ucmra_subtract_all. Qed.
......@@ -788,7 +790,7 @@ Section validity.
rewrite decide_True //.
intros. f_equal.
by rewrite -union_difference_L.
Qed.
Qed. (*
Global Instance disj_set_included_merge (a1 a2 : gset K) {Σ} : IsIncludedMerge (GSet a1) (GSet a2) (Σ := Σ) ⌜a1 ⊆ a2⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
......@@ -797,13 +799,13 @@ Section validity.
iExists (GSet (a2 ∖ a1)).
iPureIntro. rewrite gset_disj_union; [|set_solver].
fold_leibniz. f_equal. by apply union_difference_L.
Qed.
Qed. *)
(* no coallocate for both: gset is all _finite_ sets, these have no maximum element *)
End sets.
Section multisets.
Context `{Countable K}.
Context `{Countable K}. (*
Global Instance multiset_is_op_emp_l (X : gmultiset K) :
IsOp X ∅ X | 10.
Proof. rewrite /IsOp. multiset_solver. Qed.
......@@ -816,7 +818,7 @@ Section validity.
Global Instance multiset_is_valid_op (a a1 a2 : gmultiset K) Σ :
IsOp a a1 a2 → IsValidOp a a1 a2 Σ True%I | 10.
Proof. apply from_isop. Qed.
Proof. apply from_isop. Qed. *)
Global Instance ucmra_multiset_subtract_refl (a : gmultiset K) :
UcmraSubtract a a True ε | 10.
Proof. apply ucmra_subtract_all. Qed.
......@@ -828,17 +830,17 @@ Section validity.
Proof. eapply ucmra_subtract_unit. Qed.
Global Instance ucmra_multiset_subtract (a1 a2 : gmultiset K) :
UcmraSubtract a1 a2 (a2 ⊆ a1) (a1 ∖ a2) | 20.
Proof. rewrite /UcmraSubtract /CmraSubtract /= gmultiset_op. multiset_solver. Qed.
Proof. rewrite /UcmraSubtract /CmraSubtract /= gmultiset_op. multiset_solver. Qed. (*
Global Instance multiset_included_merge (a1 a2 : gmultiset K) {Σ} : IsIncludedMerge a1 a2 (Σ := Σ) ⌜a1 ⊆ a2⌝%I.
Proof.
rewrite /IsIncludedMerge. iIntros "_"; iSplit.
- by iDestruct 1 as %?%gmultiset_included.
- iIntros "%". iExists (a2 ∖ a1). iPureIntro. fold_leibniz. rewrite gmultiset_op. multiset_solver.
Qed.
Qed. *)
End multisets.
Section recursive.
Implicit Types A : cmra.
Implicit Types A : cmra. (*
Global Instance option_some_valid_op {A} (a a1 a2 : A) Σ P :
IsValidOp a a1 a2 Σ P → IsValidOp (Some a) (Some a1) (Some a2) Σ P.
......@@ -846,14 +848,14 @@ Section validity.
case => HP Ha.
split; rewrite -Some_op option_validI //.
by rewrite Ha option_equivI.
Qed.
Qed. *)
Global Instance option_subtract {A} (a b : A) φ c :
CmraSubtract a b φ c →
UcmraSubtract (Some a) (Some b) φ c.
Proof.
rewrite /UcmraSubtract /CmraSubtract /= => Hφ /Hφ <-.
by destruct c.
Qed.
Qed. (*
Global Instance option_included_merge {A} (a1 a2 : A) {Σ} (P : iProp Σ):
IsIncludedMergeUnital a1 a2 P →
IsIncludedMerge (Some a1) (Some a2) P | 100.
......@@ -901,7 +903,7 @@ Section validity.
apply (Some_equiv_eq _ (a ⋅ c)) in H as [x [xH _]] => //.
- rewrite Some_op_opM /= in H.
apply (Some_equiv_eq _ a) in H as [x [xH _]] => //.
Qed.
Qed. *)
Global Instance option_some_coalloc {A} (a : A) (mb : option A) :
CoAllocate a mb →
CoAllocate (Some a) (Some mb).
......@@ -928,7 +930,7 @@ Section validity.
{ intros. exists None. by rewrite right_id. }
rewrite -Some_op Some_valid.
move => /Hmb //.
Qed.
Qed. (*
Global Instance sum_inl_valid_op {A1 A2} (a a1 a2 : A1) Σ P :
IsValidOp a a1 a2 Σ P → IsValidOp (Cinl a) (Cinl (B := A2) a1) (Cinl (B := A2) a2) Σ P.
......@@ -961,7 +963,7 @@ Section validity.
split; rewrite /op /= /cmra_op //=; eauto.
rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
rewrite /validN /= /cmra_validN //=.
Qed.
Qed. *)
Lemma sum_inl_subtract {A1 A2} (a b : A1) φ c :
CmraSubtract a b φ c →
CmraSubtract (Cinl (B := A2) a) (Cinl (B := A2) b) φ (fmap Cinl c).
......@@ -1001,7 +1003,7 @@ Section validity.
Proof.
move => /sum_inr_subtract /= Hc.
apply Hc.
Qed.
Qed. (*
Global Instance sum_inl_included_merge {A1 A2} (a1 a2 : A1) {Σ} (P : iProp Σ):
IsIncludedMerge a1 a2 P →
IsIncludedMerge (Cinl (B := A2) a1) (Cinl (B := A2) a2) (P)%I | 100.
......@@ -1126,7 +1128,7 @@ Section validity.
rewrite /MakeAnd. split; rewrite -pair_op prod_validI /=.
- rewrite -H bi.intuitionistically_and -HP1 -HP2 //.
- rewrite prod_equivI /= -Hxs -Hys //.
Qed.
Qed. *)
Global Instance prod_subtract_Some {A1 A2} (a1 b1 c1 : A1) (a2 b2 c2 : A2) φ1 φ2 :
CmraSubtract a1 b1 φ1 (Some c1) →
CmraSubtract a2 b2 φ2 (Some c2) →
......@@ -1142,7 +1144,7 @@ Section validity.
UcmraSubtract a2 b2 φ2 c2 →
TCEq p (c1, c2) → (* avoids some unification troubles *)
UcmraSubtract (a1, a2) (b1, b2) (φ1 ∧ φ2) p.
Proof. rewrite /UcmraSubtract /CmraSubtract => Hφ1 Hφ2 -> [/Hφ1 <- /Hφ2 <-] //=. Qed.
Proof. rewrite /UcmraSubtract /CmraSubtract => Hφ1 Hφ2 -> [/Hφ1 <- /Hφ2 <-] //=. Qed. (*
Global Instance prod_included_merge {A1 A2} (x1 x2 : A1) (y1 y2 : A2) {Σ} P1 P2 P :
IsIncludedMerge x1 x2 (Σ := Σ) P1 →
IsIncludedMerge y1 y2 (Σ := Σ) P2 →
......@@ -1384,7 +1386,7 @@ Section validity.
eapply prod_included_merge_unital => //.
- right. split => //.
- right. split => //.
Qed.
Qed. *)
Global Instance prod_coalloc {A1 A2} x1 mx2 y1 my2 :
CoAllocate (A := A1) x1 mx2 →
CoAllocate (A := A2) y1 my2 →
......@@ -1409,7 +1411,7 @@ Section validity.
case => a1 a2.
rewrite -pair_op => /pair_valid.
case => /Hxmax //.
Qed.
Qed. (*
Global Instance prod_left_non_unital {A1 A2} (x1 : A1) (x2 : A2) Σ :
NonUnital x1 Σ → NonUnital (x1, x2) Σ.
Proof.
......@@ -1434,11 +1436,14 @@ Section validity.
Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ:
IsValidOp ExclBot a1 a2 Σ False%I.
Proof. split; rewrite excl_validI /=; eauto. Qed.
Proof. split; rewrite excl_validI /=; eauto. Qed. *)
Lemma excl_subtract {O : ofe} (o1 o2 : O) : (* this one is bad for recursive instances *)
TCIf (SolveSepSideCondition (¬ (o1 ≡ o2))) False TCTrue →
CmraSubtract (Excl o1) (Excl o2) (o1 ≡ o2) None.
Proof. rewrite /CmraSubtract => _ -> //=. Qed.
Proof. rewrite /CmraSubtract => _ -> //=. Qed. (*
Global Instance excl_non_unital {O : ofe} (a : O) Σ :
NonUnital (Excl a) Σ.
Proof. rewrite /NonUnital => [[b| ]] /=; rewrite excl_equivI /op /cmra_op /= /excl_op_instance //. Qed.
Global Instance excl_included_merge {O : ofe} (o1 o2 : excl O) {Σ} :
IsIncludedMerge o1 o2 (Σ := Σ) False%I.
Proof.
......@@ -1464,7 +1469,7 @@ Section validity.
iIntros "H".
iRewrite "H".
by rewrite agree_idemp.
Qed.
Qed. *)
Global Instance agree_subtract {O : ofe} (a : O) :
CmraSubtract (to_agree a) (to_agree a) True (Some $ to_agree a).
Proof. rewrite /CmraSubtract /= agree_idemp //. Qed.
......@@ -1475,7 +1480,7 @@ Section validity.
move => c _ /agree_op_inv Hac n.
exists c.
by rewrite Hac agree_idemp.
Qed.
Qed. (*
Global Instance agree_has_right_id {O : ofe} (a : O) : HasRightId (to_agree a).
Proof. exists (to_agree a). by rewrite agree_idemp. Qed.
Global Instance agree_included_merge {O : ofe} Σ (o1 o2 : O) :
......@@ -1519,7 +1524,7 @@ Section validity.
apply to_agree_included.
exists (to_agree o1).
rewrite agree_idemp. by rewrite H.
Qed.
Qed. *)
Lemma auth_inv {A : ucmra} (a : auth A) :
✓ a → ∃ b1, a ≡ ◯ b1 ∨ ∀ n : nat, ∃ q b2, a ≡{n}≡ ●{q} b2 ⋅ ◯ b1.
......@@ -1553,7 +1558,7 @@ Section validity.
Lemma auth_frag_monoN {A : ucmra} (a1 a2 : A) n :
a1 ≼{n} a2 ↔ (◯ a1 ≼{n} ◯ a2).
Proof. apply view_frag_monoN. Qed.
Proof. apply view_frag_monoN. Qed. (*
Global Instance auth_frag_valid_op {A : ucmra} (a a1 a2 : A) Σ P :
IsValidOp a a1 a2 Σ P →
......@@ -1564,7 +1569,7 @@ Section validity.
rewrite Ha.
iIntros "H".
by iRewrite "H".
Qed.
Qed. *)
Global Instance auth_frag_subtract {A : ucmra} (a1 a2 a3 : A) φ :
UcmraSubtract a1 a2 φ a3 →
UcmraSubtract (◯ a1) (◯ a2) φ (◯ a3).
......@@ -1577,7 +1582,7 @@ Section validity.
move => /dfrac_valid_own_l.
move => /Qp_lt_nge HQp.
by apply HQp.
Qed.
Qed. (*
Lemma auth_auth_dfrac_op_validI Σ {A : ucmra} dq1 dq2 (a1 a2 : A) : ✓ (●{dq1} a1 ⋅ ●{dq2} a2) ⊣⊢@{iPropI Σ} ⌜✓ (dq1 ⋅ dq2)%Qp⌝ ∧ ✓ a1 ∧ (a1 ≡ a2).
Proof.
eapply (anti_symm _); last first.
......@@ -1626,7 +1631,7 @@ Section validity.
iIntros "(% & _ & #Ha)".
iRewrite -"Ha".
by rewrite -auth_auth_dfrac_op dfrac_op_discarded.
Qed.
Qed. *)
Global Instance auth_coalloc {A : ucmra} (a : A) :
CoAllocate (● a) (Some $ ◯ a).
Proof.
......@@ -1760,7 +1765,7 @@ Section validity.
Qed.
Global Instance auth_frac_coalloc {A : cmra} (a : A) :
CoAllocate (●F a) (Some $ ◯F a).
Proof. apply auth_coalloc. Qed.
Proof. apply auth_coalloc. Qed. (*
Global Instance auth_frac_frag_valid_op {A : cmra} (a a1 a2 : A) (q q1 q2 : Qp) Σ P1 P2 :
IsValidOp q q1 q2 Σ P1 →
......@@ -1770,7 +1775,7 @@ Section validity.
intros.
apply auth_frag_valid_op, option_some_valid_op.
by eapply prod_valid_op.
Qed.
Qed. *)
Global Instance auth_frac_frag_subtract_part {A : cmra} (a a1 a2 : A) (q q1 q2 : Qp) φq φa :
CmraSubtract q1 q2 φq (Some q) →
CmraSubtract a1 a2 φa (Some a) →
......
theories/biabd/proofmode_classes.v 0 → 100644
View file @ 7f0bdb3c
From iris.algebra Require Import cmra auth frac_auth.
From iris.base_logic Require Import own.
From iris.proofmode Require Import proofmode.
Class IsValidOp {A : cmra} (a a1 a2 : A) Σ (P : iProp Σ) := {
is_valid_merge : ✓ (a1 ⋅ a2) ⊢ □ P ;
is_valid_op : ✓ (a1 ⋅ a2) ⊢@{iPropI Σ} a ≡ a1 ⋅ a2 ;
}.
Global Hint Mode IsValidOp ! - ! ! ! - : typeclass_instances.
Definition includedI {M : ucmra} {A : cmra} (a b : A) : uPred M
:= (∃ c, b ≡ a ⋅ c)%I.
Notation "a ≼ b" := (includedI a b) : bi_scope.
Class IsIncludedMerge {A : cmra} (a1 a2 : A) {Σ} (P : iPropI Σ) :=
is_included_merge : ✓ a2 ⊢ a1 ≼ a2 ↔ □ P.
Global Hint Mode IsIncludedMerge ! ! ! ! - : typeclass_instances.
Class HasRightId {A : cmra} (a : A) :=
has_right_id : a ≼ a.
Global Hint Mode HasRightId ! ! : typeclass_instances.
Class IsIncludedMergeUnital {A : cmra} (a1 a2 : A) {Σ} (P_lt P_le : iProp Σ) := {
included_merge_from_unital : IsIncludedMerge a1 a2 P_lt;
is_included_merge_unital : ✓ a2 ⊢ □ P_lt ∨ a1 ≡ a2 ↔ □ P_le;
}.
Global Hint Mode IsIncludedMergeUnital ! ! ! ! - - : typeclass_instances.
Lemma own_valid_op {A : cmra} (a a1 a2 : A) γ `{!inG Σ A} (P : iProp Σ) :
IsValidOp a a1 a2 Σ P →
own γ a1 -∗ own γ a2 -∗ own γ a ∗ □ P.
Proof.
case => HP Ha.
iIntros "Ha1 Ha2".
iAssert (✓ (a1 ⋅ a2))%I as "#H✓".
{ iApply (own_valid_2 with "Ha1 Ha2"). }
iSplit; last by iApply HP.
iAssert (a ≡ a1 ⋅ a2)%I with "[Ha1 Ha2]" as "#Heq"; first by iApply Ha.
iRewrite "Heq".
rewrite own_op; iFrame.
Qed.
Lemma is_included_auth {A : ucmra} (a1 a2 : A) dq γ `{!inG Σ $ authUR A} (P : iProp Σ) :
IsIncludedMerge a1 a2 P →
own γ (●{dq} a2) -∗ own γ (◯ a1) -∗ □ P.
Proof.
rewrite /IsIncludedMerge => HP.
iIntros "Ha1 Ha2".
iCombine "Ha1 Ha2" as "Ha".
rewrite own_valid auth_both_dfrac_validI.
iDestruct "Ha" as "(_ & [%c #Hc] & #H✓)".
iApply (HP with "H✓").
iExists c. iApply "Hc".
Qed.
Lemma bi_iff_trans {PROP : bi} (P Q R : PROP) : (P ↔ Q) ∧ (Q ↔ R) ⊢ P ↔ R.
Proof.
iIntros "HPQR"; iSplit; iStopProof;
eapply bi.impl_intro_r.
- rewrite /bi_iff.
rewrite (bi.and_elim_l (P → Q)).
rewrite (bi.and_elim_l (Q → R)).
rewrite bi.and_comm bi.and_assoc.
rewrite !bi.impl_elim_r //.
- rewrite /bi_iff.
rewrite (bi.and_elim_r (P → Q)).
rewrite (bi.and_elim_r (Q → R)).
rewrite -bi.and_assoc.
rewrite !bi.impl_elim_l //.
Qed.
Lemma bi_iff_wand_iff {PROP : bi} (P Q : PROP) :
BiAffine PROP →
Persistent P →
Persistent Q →
(P ↔ Q) ⊣⊢ (P ∗-∗ Q).
Proof.
intros.
apply (anti_symm _);
iIntros "HPQ"; iSplit; iIntros "#H";
by iApply "HPQ".
Qed.
Lemma bi_wand_iff_trans {PROP : bi} (P Q R : PROP) :
(P ∗-∗ Q) -∗ (Q ∗-∗ R) -∗ (P ∗-∗ R).
Proof.
iIntros "HPQ HQR"; iSplit; iIntros "H".
- iApply "HQR". by iApply "HPQ".
- iApply "HPQ". by iApply "HQR".
Qed.
Lemma bi_wand_iff_rew {PROP : bi} (P Q R : PROP) :
(P ∗-∗ Q) -∗ (Q ∗-∗ R) ∗-∗ (P ∗-∗ R).
Proof.
iIntros "HPQ"; iSplit; iIntros "H".
- iApply (bi_wand_iff_trans with "HPQ H").
- iApply (bi_wand_iff_trans with "[HPQ] H").
by iApply bi.wand_iff_sym.
Qed.
Lemma persistent_dup {PROP : bi} (P : PROP) :
Persistent P →
P ⊢ P ∗ P.
Proof.
move => HP.
assert (P ⊢ P ∧ P) as HPdup by eauto.
rewrite {1}HPdup {1}HP.
rewrite bi.persistently_and_sep_elim //.
Qed.
Lemma lift_iff_wand_iffs {PROP : bi} (P Q S : PROP) :
Persistent P →
(P ⊢ Q ∗-∗ S) →
(P ⊢ Q) ↔ (P ⊢ S)%I.