Commit a9ebd972 authored by Ralf Jung's avatar Ralf Jung
Browse files

unstage mono_list algebra

parent ec624937
...@@ -55,6 +55,7 @@ iris/algebra/lib/ufrac_auth.v ...@@ -55,6 +55,7 @@ iris/algebra/lib/ufrac_auth.v
iris/algebra/lib/dfrac_agree.v iris/algebra/lib/dfrac_agree.v
iris/algebra/lib/gmap_view.v iris/algebra/lib/gmap_view.v
iris/algebra/lib/mono_nat.v iris/algebra/lib/mono_nat.v
iris/algebra/lib/mono_list.v
iris/algebra/lib/gset_bij.v iris/algebra/lib/gset_bij.v
iris/si_logic/siprop.v iris/si_logic/siprop.v
iris/si_logic/bi.v iris/si_logic/bi.v
...@@ -174,7 +175,6 @@ iris_heap_lang/lib/arith.v ...@@ -174,7 +175,6 @@ iris_heap_lang/lib/arith.v
iris_heap_lang/lib/array.v iris_heap_lang/lib/array.v
iris_staging/algebra/list.v iris_staging/algebra/list.v
iris_staging/algebra/mono_list.v
iris_staging/base_logic/algebra.v iris_staging/base_logic/algebra.v
iris_staging/base_logic/mono_list.v iris_staging/base_logic/mono_list.v
iris_staging/heap_lang/interpreter.v iris_staging/heap_lang/interpreter.v
......
(* This file is still experimental. See its tracking issue
https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining
issues before stabilization. *)
From iris.algebra Require Export auth dfrac max_prefix_list.
From iris.algebra Require Import updates local_updates proofmode_classes.
From iris.prelude Require Import options.
(** Authoritative CMRA of append-only lists, where the fragment represents a (** Authoritative CMRA of append-only lists, where the fragment represents a
snap-shot of the list, and the authoritative element can only grow by snap-shot of the list, and the authoritative element can only grow by
appending. *) appending. *)
From iris.algebra Require Export auth dfrac max_prefix_list.
From iris.algebra Require Import updates local_updates proofmode_classes.
From iris.prelude Require Import options.
Definition mono_listR (A : ofe) : cmra := authR (max_prefix_listUR A). Definition mono_listR (A : ofe) : cmra := authR (max_prefix_listUR A).
Definition mono_listUR (A : ofe) : ucmra := authUR (max_prefix_listUR A). Definition mono_listUR (A : ofe) : ucmra := authUR (max_prefix_listUR A).
...@@ -192,7 +188,7 @@ Section mono_list_props. ...@@ -192,7 +188,7 @@ Section mono_list_props.
(** * Update *) (** * Update *)
Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 ML l1 ~~> ML l2. Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 ML l1 ~~> ML l2.
Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed. Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
Lemma mono_list_update_auth_persist dq l : ML{dq} l ~~> ●□ML l. Lemma mono_list_auth_persist dq l : ML{dq} l ~~> ●□ML l.
Proof. Proof.
rewrite /mono_list_auth. apply cmra_update_op; [|done]. rewrite /mono_list_auth. apply cmra_update_op; [|done].
by apply auth_update_auth_persist. by apply auth_update_auth_persist.
......
...@@ -16,7 +16,7 @@ which allows one to grow the auth element by appending only. At any time the ...@@ -16,7 +16,7 @@ which allows one to grow the auth element by appending only. At any time the
auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
persistent lower-bound. *) persistent lower-bound. *)
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.staging.algebra Require Import mono_list. From iris.algebra.lib Require Import mono_list.
From iris.bi.lib Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own. From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options. From iris.prelude Require Import options.
......
Supports Markdown
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