Commit 6fbff46e authored by Robbert Krebbers's avatar Robbert Krebbers

Generic big operators that are no longer tied to CMRAs.

Instead, I have introduced a type class `Monoid` that is used by the big operators:

    Class Monoid {M : ofeT} (o : M → M → M) := {
      monoid_unit : M;
      monoid_ne : NonExpansive2 o;
      monoid_assoc : Assoc (≡) o;
      monoid_comm : Comm (≡) o;
      monoid_left_id : LeftId (≡) monoid_unit o;
      monoid_right_id : RightId (≡) monoid_unit o;
    }.

Note that the operation is an argument because we want to have multiple monoids over
the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However,
we do bundle the unit because:

- If we would not, the unit would appear explicitly in an implicit argument of the
  big operators, which confuses rewrite. By bundling the unit in the `Monoid` class
  it is hidden, and hence rewrite won't even see it.
- The unit is unique.

We could in principle have big ops over setoids instead of OFEs. However, since we do
not have a canonical structure for bundled setoids, I did not go that way.
parent c52ff261
-Q theories iris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/algebra/monoid.v
theories/algebra/cmra.v
theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/cmra_tactics.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/gmap.v
......
......@@ -203,7 +203,8 @@ Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_frag_mono a b : a b a b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_cmra_homomorphism : UCMRAHomomorphism (Auth None).
Global Instance auth_frag_sep_homomorphism : MonoidHomomorphism op op (Auth None).
Proof. done. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b a b.
......
This diff is collapsed.
From iris.algebra Require Export ofe.
From iris.algebra Require Export ofe monoid.
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
......@@ -243,20 +243,6 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
Arguments cmra_monotone_validN {_ _} _ {_} _ _ _.
Arguments cmra_monotone {_ _} _ {_} _ _ _.
(* Not all intended homomorphisms preserve validity, in particular it does not
hold for the [ownM] and [own] connectives. *)
Class CMRAHomomorphism {A B : cmraT} (f : A B) := {
cmra_homomorphism_ne :> NonExpansive f;
cmra_homomorphism x y : f (x y) f x f y
}.
Arguments cmra_homomorphism {_ _} _ _ _ _.
Class UCMRAHomomorphism {A B : ucmraT} (f : A B) := {
ucmra_homomorphism :> CMRAHomomorphism f;
ucmra_homomorphism_unit : f
}.
Arguments ucmra_homomorphism_unit {_ _} _ _.
(** * Properties **)
Section cmra.
Context {A : cmraT}.
......@@ -633,9 +619,12 @@ Section ucmra.
Qed.
Global Instance empty_cancelable : Cancelable (:A).
Proof. intros ???. by rewrite !left_id. Qed.
(* For big ops *)
Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := |}.
End ucmra.
Hint Immediate cmra_unit_total.
Hint Immediate cmra_unit_total.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
......@@ -752,26 +741,6 @@ Section cmra_monotone.
Proof. rewrite !cmra_valid_validN; eauto using cmra_monotone_validN. Qed.
End cmra_monotone.
Instance cmra_homomorphism_id {A : cmraT} : CMRAHomomorphism (@id A).
Proof. repeat split; by try apply _. Qed.
Instance cmra_homomorphism_compose {A B C : cmraT} (f : A B) (g : B C) :
CMRAHomomorphism f CMRAHomomorphism g CMRAHomomorphism (g f).
Proof.
split.
- apply _.
- move=> x y /=. rewrite -(cmra_homomorphism g).
by apply (ne_proper _), cmra_homomorphism.
Qed.
Instance cmra_homomorphism_proper {A B : cmraT} (f : A B) :
CMRAHomomorphism f Proper (() ==> ()) f := λ _, ne_proper _.
Instance ucmra_homomorphism_id {A : ucmraT} : UCMRAHomomorphism (@id A).
Proof. repeat split; by try apply _. Qed.
Instance ucmra_homomorphism_compose {A B C : ucmraT} (f : A B) (g : B C) :
UCMRAHomomorphism f UCMRAHomomorphism g UCMRAHomomorphism (g f).
Proof. split. apply _. by rewrite /= !ucmra_homomorphism_unit. Qed.
(** Functors *)
Structure rFunctor := RFunctor {
rFunctor_car : ofeT ofeT cmraT;
......@@ -1316,8 +1285,6 @@ Section option.
(** Misc *)
Global Instance Some_cmra_monotone : CMRAMonotone Some.
Proof. split; [apply _|done|intros x y [z ->]; by exists (Some z)]. Qed.
Global Instance Some_cmra_homomorphism : CMRAHomomorphism Some.
Proof. split. apply _. done. Qed.
Lemma op_None mx my : mx my = None mx = None my = None.
Proof. destruct mx, my; naive_solver. Qed.
......
This diff is collapsed.
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
Set Default Proof Using "Type".
(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
Context {A : ucmraT}.
Inductive expr :=
| EVar : nat expr
| EEmpty : expr
| EOp : expr expr expr.
Fixpoint eval (Σ : list A) (e : expr) : A :=
match e with
| EVar n => from_option id (Σ !! n)
| EEmpty =>
| EOp e1 e2 => eval Σ e1 eval Σ e2
end.
Fixpoint flatten (e : expr) : list nat :=
match e with
| EVar n => [n]
| EEmpty => []
| EOp e1 e2 => flatten e1 ++ flatten e2
end.
Lemma eval_flatten Σ e :
eval Σ e [ list] n flatten e, from_option id (Σ !! n).
Proof.
induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
by rewrite IH1 IH2 big_opL_app.
Qed.
Lemma flatten_correct Σ e1 e2 :
flatten e1 + flatten e2 eval Σ e1 eval Σ e2.
Proof.
by intros He; rewrite !eval_flatten; apply big_opL_submseteq; rewrite ->He.
Qed.
Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
Global Instance quote_empty: Quote E1 E1 EEmpty.
Global Instance quote_var Σ1 Σ2 e i:
rlist.QuoteLookup Σ1 Σ2 e i Quote Σ1 Σ2 e (EVar i) | 1000.
Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
Quote Σ1 Σ2 x1 e1 Quote Σ2 Σ3 x2 e2 Quote Σ1 Σ3 (x1 x2) (EOp e1 e2).
End ra_reflection.
Ltac quote :=
match goal with
| |- @included _ _ _ ?x ?y =>
lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
change (eval Σ3 e1 eval Σ3 e2)
end end
end.
End ra_reflection.
Ltac solve_included :=
ra_reflection.quote;
apply ra_reflection.flatten_correct, (bool_decide_unpack _);
vm_compute; apply I.
Ltac solve_validN :=
match goal with
| H : {?n} ?y |- {?n'} ?x =>
let Hn := fresh in let Hx := fresh in
assert (n' n) as Hn by omega;
assert (x y) as Hx by solve_included;
eapply cmra_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
end.
......@@ -281,11 +281,6 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
Global Instance Cinr_id_free b : IdFree b IdFree (Cinr b).
Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
Global Instance Cinl_cmra_homomorphism : CMRAHomomorphism Cinl.
Proof. split. apply _. done. Qed.
Global Instance Cinr_cmra_homomorphism : CMRAHomomorphism Cinr.
Proof. split. apply _. done. Qed.
(** Internalized properties *)
Lemma csum_equivI {M} (x y : csum A B) :
x y (match x, y with
......
......@@ -200,9 +200,9 @@ Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
Global Instance lookup_cmra_homomorphism :
UCMRAHomomorphism (lookup i : gmap K A option A).
Proof. split. split. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
Global Instance lookup_op_homomorphism :
MonoidHomomorphism op op (lookup i : gmap K A option A).
Proof. split; [split|]. apply _. intros m1 m2; by rewrite lookup_op. done. Qed.
Lemma lookup_opM m1 mm2 i : (m1 ? mm2) !! i = m1 !! i (mm2 = (!! i)).
Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
......@@ -247,9 +247,6 @@ Qed.
Lemma op_singleton (i : K) (x y : A) :
{[ i := x ]} {[ i := y ]} = ({[ i := x y ]} : gmap K A).
Proof. by apply (merge_singleton _ _ _ x y). Qed.
Global Instance singleton_cmra_homomorphism :
CMRAHomomorphism (singletonM i : A gmap K A).
Proof. split. apply _. intros. by rewrite op_singleton. Qed.
Global Instance gmap_persistent m : ( x : A, Persistent x) Persistent m.
Proof.
......
......@@ -464,3 +464,63 @@ Instance listURF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
Qed.
(** * Persistence and timelessness of lists of uPreds *)
Class PersistentL {M} (Ps : list (uPred M)) :=
persistentL : Forall PersistentP Ps.
Arguments persistentL {_} _ {_}.
Hint Mode PersistentL + ! : typeclass_instances.
Class TimelessL {M} (Ps : list (uPred M)) :=
timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.
Hint Mode TimelessP + ! : typeclass_instances.
Section persistent_timeless.
Context {M : ucmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.
Global Instance nil_persistentL : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_persistentL P Ps :
PersistentP P PersistentL Ps PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_persistentL Ps Ps' :
PersistentL Ps PersistentL Ps' PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance fmap_persistentL {A} (f : A uPred M) xs :
( x, PersistentP (f x)) PersistentL (f <$> xs).
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
Global Instance zip_with_persistentL {A B} (f : A B uPred M) xs ys :
( x y, PersistentP (f x y)) PersistentL (zip_with f xs ys).
Proof.
unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
Global Instance imap_persistentL {A} (f : nat A uPred M) xs :
( i x, PersistentP (f i x)) PersistentL (imap f xs).
Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
(** ** Timelessness *)
Global Instance nil_timelessL : TimelessL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_timelessL P Ps :
TimelessP P TimelessL Ps TimelessL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_timelessL Ps Ps' :
TimelessL Ps TimelessL Ps' TimelessL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.
Global Instance fmap_timelessL {A} (f : A uPred M) xs :
( x, TimelessP (f x)) TimelessL (f <$> xs).
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
Global Instance zip_with_timelessL {A B} (f : A B uPred M) xs ys :
( x y, TimelessP (f x y)) TimelessL (zip_with f xs ys).
Proof.
unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
Global Instance imap_timelessL {A} (f : nat A uPred M) xs :
( i x, TimelessP (f i x)) TimelessL (imap f xs).
Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
End persistent_timeless.
From iris.algebra Require Export ofe.
Set Default Proof Using "Type".
(** The Monoid class that is used for generic big operators in the file
[algebra/big_op]. The operation is an argument because we want to have multiple
monoids over the same type (for example, on [uPred]s we have monoids for [∗],
[∧], and [∨]). However, we do bundle the unit because:
- If we would not, it would appear explicitly in an argument of the big
operators, which confuses rewrite. Now it is hidden in the class, and hence
rewrite won't even see it.
- The unit is unique.
We could in principle have big ops over setoids instead of OFEs. However, since
we do not have a canonical structure for setoids, we do not go that way.
Note that we do not declare any of the projections as type class instances. That
is because we only need them in the [big_op] file, and nowhere else. Hence, we
declare these instances locally there to avoid them being used elsewhere. *)
Class Monoid {M : ofeT} (o : M M M) := {
monoid_unit : M;
monoid_ne : NonExpansive2 o;
monoid_assoc : Assoc () o;
monoid_comm : Comm () o;
monoid_left_id : LeftId () monoid_unit o;
monoid_right_id : RightId () monoid_unit o;
}.
Lemma monoid_proper `{Monoid M o} : Proper (() ==> () ==> ()) o.
Proof. apply ne_proper_2, monoid_ne. Qed.
(** The [Homomorphism] classes give rise to generic lemmas about big operators
commuting with each other. *)
Class WeakMonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 M1 M1) (o2 : M2 M2 M2)
`{Monoid M1 o1, Monoid M2 o2} (f : M1 M2) := {
monoid_homomorphism_ne : NonExpansive f;
monoid_homomorphism x y : f (o1 x y) o2 (f x) (f y)
}.
Class MonoidHomomorphism {M1 M2 : ofeT} (o1 : M1 M1 M1) (o2 : M2 M2 M2)
`{Monoid M1 o1, Monoid M2 o2} (f : M1 M2) := {
monoid_homomorphism_weak :> WeakMonoidHomomorphism o1 o2 f;
monoid_homomorphism_unit : f monoid_unit monoid_unit
}.
Lemma weak_monoid_homomorphism_proper
`{WeakMonoidHomomorphism M1 M2 o1 o2 f} : Proper (() ==> ()) f.
Proof. apply ne_proper, monoid_homomorphism_ne. Qed.
This diff is collapsed.
......@@ -889,5 +889,64 @@ Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global Instance from_option_persistent {A} P (Ψ : A uPred M) (mx : option A) :
( x, PersistentP (Ψ x)) PersistentP P PersistentP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
(* For big ops *)
Global Instance uPred_and_monoid : Monoid (@uPred_and M) :=
{| monoid_unit := True%I |}.
Global Instance uPred_or_monoid : Monoid (@uPred_or M) :=
{| monoid_unit := False%I |}.
Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
{| monoid_unit := True%I |}.
Global Instance uPred_always_and_homomorphism :
MonoidHomomorphism uPred_and uPred_and (@uPred_always M).
Proof. split; [split|]. apply _. apply always_and. apply always_pure. Qed.
Global Instance uPred_always_if_and_homomorphism b :
MonoidHomomorphism uPred_and uPred_and (@uPred_always_if M b).
Proof. split; [split|]. apply _. apply always_if_and. apply always_if_pure. Qed.
Global Instance uPred_later_monoid_and_homomorphism :
MonoidHomomorphism uPred_and uPred_and (@uPred_later M).
Proof. split; [split|]. apply _. apply later_and. apply later_True. Qed.
Global Instance uPred_laterN_and_homomorphism n :
MonoidHomomorphism uPred_and uPred_and (@uPred_laterN M n).
Proof. split; [split|]. apply _. apply laterN_and. apply laterN_True. Qed.
Global Instance uPred_except_0_and_homomorphism :
MonoidHomomorphism uPred_and uPred_and (@uPred_except_0 M).
Proof. split; [split|]. apply _. apply except_0_and. apply except_0_True. Qed.
Global Instance uPred_always_or_homomorphism :
MonoidHomomorphism uPred_or uPred_or (@uPred_always M).
Proof. split; [split|]. apply _. apply always_or. apply always_pure. Qed.
Global Instance uPred_always_if_or_homomorphism b :
MonoidHomomorphism uPred_or uPred_or (@uPred_always_if M b).
Proof. split; [split|]. apply _. apply always_if_or. apply always_if_pure. Qed.
Global Instance uPred_later_monoid_or_homomorphism :
WeakMonoidHomomorphism uPred_or uPred_or (@uPred_later M).
Proof. split. apply _. apply later_or. Qed.
Global Instance uPred_laterN_or_homomorphism n :
WeakMonoidHomomorphism uPred_or uPred_or (@uPred_laterN M n).
Proof. split. apply _. apply laterN_or. Qed.
Global Instance uPred_except_0_or_homomorphism :
WeakMonoidHomomorphism uPred_or uPred_or (@uPred_except_0 M).
Proof. split. apply _. apply except_0_or. Qed.
Global Instance uPred_always_sep_homomorphism :
MonoidHomomorphism uPred_sep uPred_sep (@uPred_always M).
Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
Global Instance uPred_always_if_sep_homomorphism b :
MonoidHomomorphism uPred_sep uPred_sep (@uPred_always_if M b).
Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
Global Instance uPred_later_monoid_sep_homomorphism :
MonoidHomomorphism uPred_sep uPred_sep (@uPred_later M).
Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
Global Instance uPred_laterN_sep_homomorphism n :
MonoidHomomorphism uPred_sep uPred_sep (@uPred_laterN M n).
Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
Global Instance uPred_except_0_sep_homomorphism :
MonoidHomomorphism uPred_sep uPred_sep (@uPred_except_0 M).
Proof. split; [split|]. apply _. apply except_0_sep. apply except_0_True. Qed.
Global Instance uPred_ownM_sep_homomorphism :
MonoidHomomorphism op uPred_sep (@uPred_ownM M).
Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
End derived.
End uPred.
......@@ -94,9 +94,10 @@ Section auth.
Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
Lemma auth_own_valid γ a : auth_own γ a a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ).
Global Instance auth_own_sep_homomorphism γ :
WeakMonoidHomomorphism op uPred_sep (auth_own γ).
Proof. split. apply _. apply auth_own_op. Qed.
Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
Proof. intros a1 a2. apply auth_own_mono. Qed.
......
......@@ -86,8 +86,6 @@ Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
Lemma own_mono γ a1 a2 : a2 a1 own γ a1 own γ a2.
Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.
Global Instance own_cmra_homomorphism : CMRAHomomorphism (own γ).
Proof. split. apply _. apply own_op. Qed.
Global Instance own_mono' γ : Proper (flip () ==> ()) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
......@@ -178,6 +176,11 @@ Proof.
- intros x; destruct inG_prf. by rewrite left_id.
Qed.
(** Big op class instances *)
Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
WeakMonoidHomomorphism op uPred_sep (own γ).
Proof. split. apply _. apply own_op. Qed.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{inG Σ A}.
......
......@@ -67,8 +67,7 @@ Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iNext; iIntros (v2 σ2 efs) "%".
iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst.
by iApply big_sepL_nil.
iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
Qed.
Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
......@@ -86,7 +85,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
(|={E,E'}=> WP e2 @ E {{ Φ }}) WP e1 @ E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
Qed.
Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
......
......@@ -211,7 +211,7 @@ Section ectx_lifting.
{{{ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
Proof.
intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
rewrite /= right_id. by apply uPred.wand_intro_r.
Qed.
Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
......@@ -229,6 +229,6 @@ Section ectx_lifting.
( σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' σ1 = σ2 e2 = e2' [] = efs')
WP e2 @ E {{ Φ }} WP e1 @ E {{ Φ }}.
Proof using Hinh.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
Qed.
End ectx_lifting.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment