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

remove algebra/ dependency on base_logic/

parent f4060bb5
......@@ -70,6 +70,7 @@ theories/base_logic/bi.v
theories/base_logic/derived.v
theories/base_logic/proofmode.v
theories/base_logic/base_logic.v
theories/base_logic/algebra.v
theories/base_logic/bupd_alt.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import list.
From iris.base_logic Require Import base_logic.
From iris Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
......@@ -257,18 +256,6 @@ Qed.
Lemma to_agree_op_valid_L `{!LeibnizEquiv A} a b : (to_agree a to_agree b) a = b.
Proof. rewrite to_agree_op_valid. by fold_leibniz. Qed.
(** Internalized properties *)
Lemma agree_equivI {M} a b : to_agree a to_agree b @{uPredI M} (a b).
Proof.
uPred.unseal. do 2 split.
- intros Hx. exact: (inj to_agree).
- intros Hx. exact: to_agree_ne.
Qed.
Lemma agree_validI {M} x y : (x y) @{uPredI M} x y.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
Lemma to_agree_uninjI {M} x : x @{uPredI M} a, to_agree a x.
Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
End agree.
Instance: Params (@to_agree) 1 := {}.
......
From iris.algebra Require Export view.
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import proofmode_classes big_op.
From iris Require Import options.
(** The authoritative camera with fractional authoritative elements *)
......@@ -239,29 +238,6 @@ Section auth.
a1 b1 a2 b2 a1 a2 b1 b2.
Proof. apply view_both_included. Qed.
(** Internalized properties *)
Lemma auth_auth_frac_validI {M} q a : ({q} a) @{uPredI M} q a.
Proof.
apply view_auth_frac_validI=> n. uPred.unseal; split; [|by intros [??]].
split; [|done]. apply ucmra_unit_leastN.
Qed.
Lemma auth_auth_validI {M} a : ( a) @{uPredI M} a.
Proof.
by rewrite auth_auth_frac_validI uPred.discrete_valid bi.pure_True // left_id.
Qed.
Lemma auth_frag_validI {M} a : ( a) @{uPredI M} a.
Proof. apply view_frag_validI. Qed.
Lemma auth_both_frac_validI {M} q a b :
({q} a b) @{uPredI M} q ( c, a b c) a.
Proof. apply view_both_frac_validI=> n. by uPred.unseal. Qed.
Lemma auth_both_validI {M} a b :
( a b) @{uPredI M} ( c, a b c) a.
Proof.
by rewrite auth_both_frac_validI uPred.discrete_valid bi.pure_True // left_id.
Qed.
(** Updates *)
Lemma auth_update a b a' b' :
(a,b) ~l~> (a',b') a b ~~> a' b'.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates.
From iris Require Import options.
Local Arguments pcore _ _ !_ /.
Local Arguments cmra_pcore _ !_ /.
Local Arguments validN _ _ _ !_ /.
......@@ -26,7 +26,7 @@ Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
match x with Cinr b => Some b | _ => None end.
Section cofe.
Section ofe.
Context {A B : ofeT}.
Implicit Types a : A.
Implicit Types b : B.
......@@ -108,19 +108,7 @@ Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
Global Instance Cinr_discrete b : Discrete b Discrete (Cinr b).
Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
(** Internalized properties *)
Lemma csum_equivI {M} (x y : csum A B) :
x y @{uPredI M} match x, y with
| Cinl a, Cinl a' => a a'
| Cinr b, Cinr b' => b b'
| CsumBot, CsumBot => True
| _, _ => False
end.
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
End cofe.
End ofe.
Arguments csumO : clear implicits.
......@@ -321,15 +309,6 @@ Proof.
- naive_solver by f_equiv.
Qed.
(** Internalized properties *)
Lemma csum_validI {M} (x : csum A B) :
x @{uPredI M} match x with
| Cinl a => a
| Cinr b => b
| CsumBot => False
end.
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
Lemma csum_update_l (a1 a2 : A) : a1 ~~> a2 Cinl a1 ~~> Cinl a2.
Proof.
......
From iris.algebra Require Export cmra.
From iris.base_logic Require Import base_logic.
From iris Require Import options.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
......@@ -94,20 +94,6 @@ Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
Global Instance excl_cmra_discrete : OfeDiscrete A CmraDiscrete exclR.
Proof. split. apply _. by intros []. Qed.
(** Internalized properties *)
Lemma excl_equivI {M} x y :
x y @{uPredI M} match x, y with
| Excl a, Excl b => a b
| ExclBot, ExclBot => True
| _, _ => False
end.
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI {M} x :
x @{uPredI M} if x is ExclBot then False else True.
Proof. uPred.unseal. by destruct x. Qed.
(** Exclusive *)
Global Instance excl_exclusive x : Exclusive x.
Proof. by destruct x; intros n []. Qed.
......
From stdpp Require Export list gmap.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates proofmode_classes big_op.
From iris Require Import options.
Section cofe.
Section ofe.
Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
......@@ -96,9 +95,7 @@ Lemma insert_idN n m i x :
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
(** Internalized properties *)
Lemma gmap_equivI {M} m1 m2 : m1 m2 @{uPredI M} i, m1 !! i m2 !! i.
Proof. by uPred.unseal. Qed.
End cofe.
End ofe.
Arguments gmapO _ {_ _} _.
......@@ -139,26 +136,6 @@ Proof.
destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
Lemma big_sepM2_ne_2 {PROP : bi} `{Countable K} (A B : ofeT)
(Φ Ψ : K A B PROP) m1 m2 m1' m2' n :
m1 {n} m1' m2 {n} m2'
( k y1 y1' y2 y2',
m1 !! k = Some y1 m1' !! k = Some y1' y1 {n} y1'
m2 !! k = Some y2 m2' !! k = Some y2' y2 {n} y2'
Φ k y1 y2 {n} Ψ k y1' y2')
([ map] k y1;y2 m1;m2, Φ k y1 y2)%I {n} ([ map] k y1;y2 m1';m2', Ψ k y1 y2)%I.
Proof.
intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
{ f_equiv; split; intros Hm k.
- trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
rewrite Hm. apply: is_Some_ne; by f_equiv.
- trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
apply big_opM_ne_2; [by f_equiv|].
intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
(?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
Qed.
(* CMRA *)
Section cmra.
Context `{Countable K} {A : cmraT}.
......@@ -253,18 +230,6 @@ Proof.
Qed.
Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
(** Internalized properties *)
Lemma gmap_validI {M} m : m @{uPredI M} i, (m !! i).
Proof. by uPred.unseal. Qed.
Lemma singleton_validI {M} i x : {[ i := x ]} @{uPredI M} x.
Proof.
rewrite gmap_validI. apply: anti_symm.
- rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
- apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+ rewrite lookup_singleton uPred.option_validI. done.
+ rewrite lookup_singleton_ne // uPred.option_validI.
apply bi.True_intro.
Qed.
End cmra.
Arguments gmapR _ {_ _} _.
......
From iris.algebra Require Export auth excl updates.
From iris.algebra Require Import local_updates.
From iris.base_logic Require Import base_logic.
From iris Require Import options.
(** Authoritative CMRA where the fragment is exclusively owned.
......@@ -60,13 +59,6 @@ Section excl_auth.
Lemma excl_auth_agree_L `{!LeibnizEquiv A} a b : (E a E b) a = b.
Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
Lemma excl_auth_agreeI {M} a b : (E a E b) @{uPredI M} (a b).
Proof.
rewrite auth_both_validI bi.and_elim_l.
apply bi.exist_elim=> -[[c|]|];
by rewrite option_equivI /= excl_equivI //= bi.False_elim.
Qed.
Lemma excl_auth_frag_validN_op_1_l n a b : {n} (E a E b) False.
Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
Lemma excl_auth_frag_valid_op_1_l a b : (E a E b) False.
......
From Coq.QArith Require Import Qcanon.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import view updates dfrac.
From iris.algebra Require Export gmap dfrac.
From iris.algebra Require Import local_updates proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris Require Import options.
(** * CMRA for a "view of a gmap".
......@@ -317,25 +315,6 @@ Section lemmas.
IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
(** Internalized properties *)
Lemma gmap_view_both_validI M m k dq v :
(gmap_view_auth m gmap_view_frag k dq v) @{uPredI M}
dq m !! k Some v.
Proof.
rewrite /gmap_view_auth /gmap_view_frag. apply view_both_validI_1.
intros n a. uPred.unseal. apply gmap_view_rel_lookup.
Qed.
Lemma gmap_view_frag_op_validI M k dq1 dq2 v1 v2 :
(gmap_view_frag k dq1 v1 gmap_view_frag k dq2 v2) @{uPredI M}
(dq1 dq2) v1 v2.
Proof.
rewrite /gmap_view_frag -view_frag_op view_frag_validI.
rewrite singleton_op singleton_validI -pair_op uPred.prod_validI /=.
apply bi.and_mono; first done.
rewrite agree_validI agree_equivI. done.
Qed.
End lemmas.
(** Functor *)
......
From stdpp Require Export list.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates local_updates.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Import updates local_updates big_op.
From iris Require Import options.
Section cofe.
Section ofe.
Context {A : ofeT}.
Implicit Types l : list A.
......@@ -94,10 +93,7 @@ Proof. inversion_clear 1; constructor. Qed.
Global Instance cons_discrete x l : Discrete x Discrete l Discrete (x :: l).
Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.
(** Internalized properties *)
Lemma list_equivI {M} l1 l2 : l1 l2 @{uPredI M} i, l1 !! i l2 !! i.
Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
End cofe.
End ofe.
Arguments listO : clear implicits.
......@@ -139,22 +135,6 @@ Proof.
destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
Lemma big_sepL2_ne_2 {PROP : bi} {A B : ofeT}
(Φ Ψ : nat A B PROP) l1 l2 l1' l2' n :
l1 {n} l1' l2 {n} l2'
( k y1 y1' y2 y2',
l1 !! k = Some y1 l1' !! k = Some y1' y1 {n} y1'
l2 !! k = Some y2 l2' !! k = Some y2' y2 {n} y2'
Φ k y1 y2 {n} Ψ k y1' y2')
([ list] k y1;y2 l1;l2, Φ k y1 y2)%I {n} ([ list] k y1;y2 l1';l2', Ψ k y1 y2)%I.
Proof.
intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
{ do 2 f_equiv; by apply: length_ne. }
apply big_opL_ne_2; [by f_equiv|].
intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
(?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
Qed.
(** Functor *)
Lemma list_fmap_ext_ne {A} {B : ofeT} (f g : A B) (l : list A) n :
( x, f x {n} g x) f <$> l {n} g <$> l.
......@@ -314,9 +294,6 @@ Section cmra.
Global Instance list_core_id l : ( x : A, CoreId x) CoreId l.
Proof. intros Hyp; by apply list_core_id'. Qed.
(** Internalized properties *)
Lemma list_validI {M} l : l @{uPredI M} i, (l !! i).
Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End cmra.
Arguments listR : clear implicits.
......
From iris.algebra Require Export cmra.
From iris.proofmode Require Export classes.
From iris Require Import options.
(* There are various versions of [IsOp] with different modes:
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Export frac agree local_updates.
From iris.algebra Require Import proofmode_classes.
From iris.base_logic Require Import base_logic.
From iris.algebra Require Export updates local_updates frac agree.
From iris.algebra Require Import proofmode_classes big_op.
From iris Require Import options.
(** The view camera with fractional authoritative elements *)
......@@ -428,62 +426,6 @@ Section cmra.
V a1 V b1 V a2 V b2 a1 a2 b1 b2.
Proof. rewrite view_both_frac_included. naive_solver. Qed.
(** Internalized properties *)
Lemma view_both_frac_validI_1 {M} (relI : uPred M) q a b :
( n (x : M), rel n a b relI n x)
(V{q} a V b) q relI.
Proof.
intros Hrel. uPred.unseal. split=> n x _ /=.
rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_frac_validI_2 {M} (relI : uPred M) q a b :
( n (x : M), relI n x rel n a b)
q relI (V{q} a V b).
Proof.
intros Hrel. uPred.unseal. split=> n x _ /=.
rewrite /uPred_holds /= view_both_frac_validN. by move=> [? /Hrel].
Qed.
Lemma view_both_frac_validI {M} (relI : uPred M) q a b :
( n (x : M), rel n a b relI n x)
(V{q} a V b) q relI.
Proof.
intros. apply (anti_symm _);
[apply view_both_frac_validI_1|apply view_both_frac_validI_2]; naive_solver.
Qed.
Lemma view_both_validI_1 {M} (relI : uPred M) a b :
( n (x : M), rel n a b relI n x)
(V a V b) relI.
Proof. intros. by rewrite view_both_frac_validI_1 // bi.and_elim_r. Qed.
Lemma view_both_validI_2 {M} (relI : uPred M) a b :
( n (x : M), relI n x rel n a b)
relI (V a V b).
Proof.
intros. rewrite -view_both_frac_validI_2 // uPred.discrete_valid.
apply bi.and_intro; [|done]. by apply bi.pure_intro.
Qed.
Lemma view_both_validI {M} (relI : uPred M) a b :
( n (x : M), rel n a b relI n x)
(V a V b) relI.
Proof.
intros. apply (anti_symm _);
[apply view_both_validI_1|apply view_both_validI_2]; naive_solver.
Qed.
Lemma view_auth_frac_validI {M} (relI : uPred M) q a :
( n (x : M), relI n x rel n a ε)
(V{q} a) q relI.
Proof.
intros. rewrite -(right_id ε op (V{q} a)). by apply view_both_frac_validI.
Qed.
Lemma view_auth_validI {M} (relI : uPred M) a :
( n (x : M), relI n x rel n a ε)
(V a) relI.
Proof. intros. rewrite -(right_id ε op (V a)). by apply view_both_validI. Qed.
Lemma view_frag_validI {M} b : (V b) @{uPredI M} b.
Proof. by uPred.unseal. Qed.
(** Updates *)
Lemma view_update a b a' b' :
( n bf, rel n a (b bf) rel n a' (b' bf))
......
From iris.algebra Require Import cmra view auth agree csum list excl gmap lib.excl_auth lib.gmap_view.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import bi derived.
From iris Require Import options.
(** Internalized properties of our CMRA constructions. *)
Section upred.
Context {M : ucmraT}.
Section gmap_ofe.
Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Lemma gmap_equivI m1 m2 : m1 m2 @{uPredI M} i, m1 !! i m2 !! i.
Proof. by uPred.unseal. Qed.
End gmap_ofe.
Section gmap_cmra.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K A.
Lemma gmap_validI m : m @{uPredI M} i, (m !! i).
Proof. by uPred.unseal. Qed.
Lemma singleton_validI i x : ({[ i := x ]} : gmap K A) @{uPredI M} x.
Proof.
rewrite gmap_validI. apply: anti_symm.
- rewrite (bi.forall_elim i) lookup_singleton uPred.option_validI. done.
- apply bi.forall_intro=>j. destruct (decide (i = j)) as [<-|Hne].
+ rewrite lookup_singleton uPred.option_validI. done.
+ rewrite lookup_singleton_ne // uPred.option_validI.
apply bi.True_intro.
Qed.
End gmap_cmra.
Section list_ofe.
Context {A : ofeT}.
Implicit Types l : list A.
Lemma list_equivI l1 l2 : l1 l2 @{uPredI M} i, l1 !! i l2 !! i.
Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
End list_ofe.
Section list_cmra.
Context {A : ucmraT}.
Implicit Types l : list A.
Lemma list_validI l : l @{uPredI M} i, (l !! i).
Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End list_cmra.
Section excl.
Context {A : ofeT}.
Implicit Types a b : A.
Implicit Types x y : excl A.
Lemma excl_equivI x y :
x y @{uPredI M} match x, y with
| Excl a, Excl b => a b
| ExclBot, ExclBot => True
| _, _ => False
end.
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
Lemma excl_validI x :
x @{uPredI M} if x is ExclBot then False else True.
Proof. uPred.unseal. by destruct x. Qed.
End excl.
Section agree.
Context {A : ofeT}.
Implicit Types a b : A.
Implicit Types x y : agree A.
Lemma agree_equivI a b : to_agree a to_agree b @{uPredI M} (a b).
Proof.
uPred.unseal. do 2 split.
- intros Hx. exact: (inj to_agree).
- intros Hx. exact: to_agree_ne.
Qed.
Lemma agree_validI x y : (x y) @{uPredI M} x y.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
Lemma to_agree_uninjI x : x @{uPredI M} a, to_agree a x.
Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
End agree.
Section csum_ofe.
Context {A B : ofeT}.
Implicit Types a : A.
Implicit Types b : B.
Lemma csum_equivI (x y : csum A B) :
x y @{uPredI M} match x, y with
| Cinl a, Cinl a' => a a'
| Cinr b, Cinr b' => b b'
| CsumBot, CsumBot => True
| _, _ => False
end.
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
End csum_ofe.
Section csum_cmra.
Context {A B : cmraT}.
Implicit Types a : A.
Implicit Types b : B.
Lemma csum_validI (x : csum A B) :
x @{uPredI M} match x with
| Cinl a => a
| Cinr b => b
| CsumBot => False
end.
Proof. uPred.unseal. by destruct x. Qed.
End csum_cmra.
Section view.