Commit ff61f8a8 authored by Robbert Krebbers's avatar Robbert Krebbers

Update to latest stdpp, and set Hint Mode of classes.

parent de11579b
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 24aef2fea9481e65d1f6658005ddde25ae9a64ee
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 7d7c9871312719a4e1296d52eb95ea0ac959249f
......@@ -2,9 +2,11 @@ From iris.algebra Require Export ofe monoid.
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
Hint Mode PCore ! : typeclass_instances.
Instance: Params (@pcore) 2.
Class Op (A : Type) := op : A A A.
Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2.
Infix "⋅" := op (at level 50, left associativity) : C_scope.
Notation "(⋅)" := op (only parsing) : C_scope.
......@@ -21,11 +23,13 @@ Hint Extern 0 (_ ≼ _) => reflexivity.
Instance: Params (@included) 3.
Class ValidN (A : Type) := validN : nat A Prop.
Hint Mode ValidN ! : typeclass_instances.
Instance: Params (@validN) 3.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A Prop.
Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2.
Notation "✓ x" := (valid x) (at level 20) : C_scope.
......@@ -165,8 +169,10 @@ Instance: Params (@IdFree) 1.
(** The function [core] may return a dummy when used on CMRAs without total
core. *)
Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Hint Mode CMRATotal ! : typeclass_instances.
Class Core (A : Type) := core : A A.
Hint Mode Core ! : typeclass_instances.
Instance: Params (@core) 2.
Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
......@@ -233,6 +239,7 @@ Class CMRADiscrete (A : cmraT) := {
cmra_discrete :> Discrete A;
cmra_discrete_valid (x : A) : {0} x x
}.
Hint Mode CMRADiscrete ! : typeclass_instances.
(** * Morphisms *)
Class CMRAMorphism {A B : cmraT} (f : A B) := {
......@@ -690,8 +697,8 @@ End ucmra_leibniz.
(** * Constructing a CMRA with total core *)
Section cmra_total.
Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
Context (total : x, is_Some (pcore x)).
Context (op_ne : (x : A), NonExpansive (op x)).
Context (total : x : A, is_Some (pcore x)).
Context (op_ne : x : A, NonExpansive (op x)).
Context (core_ne : NonExpansive (@core A _)).
Context (validN_ne : n, Proper (dist n ==> impl) (@validN A _ n)).
Context (valid_validN : (x : A), x n, {n} x).
......@@ -885,8 +892,8 @@ Notation discreteR A ra_mix :=
Section ra_total.
Local Set Default Proof Using "Type*".
Context A `{Equiv A, PCore A, Op A, Valid A}.
Context (total : x, is_Some (pcore x)).
Context (op_proper : (x : A), Proper (() ==> ()) (op x)).
Context (total : x : A, is_Some (pcore x)).
Context (op_proper : x : A, Proper (() ==> ()) (op x)).
Context (core_proper: Proper (() ==> ()) (@core A _)).
Context (valid_proper : Proper (() ==> impl) (@valid A _)).
Context (op_assoc : Assoc () (@op A _)).
......@@ -1217,6 +1224,7 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
Implicit Types a : A.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
......
......@@ -146,7 +146,7 @@ Proof.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
{ exists , . split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
{ eexists , . split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
{ intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
......@@ -347,10 +347,10 @@ Section freshness.
assert (i I i dom (gset K) m i dom (gset K) mf) as [?[??]].
{ rewrite -not_elem_of_union -dom_op -not_elem_of_union; apply is_fresh. }
exists (<[i:=x]>m); split.
{ by apply HQ; last done; apply not_elem_of_dom. }
rewrite insert_singleton_op; last by apply not_elem_of_dom.
{ apply HQ; last done. by eapply not_elem_of_dom. }
rewrite insert_singleton_op; last by eapply not_elem_of_dom.
rewrite -assoc -insert_singleton_op;
last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
last by eapply (not_elem_of_dom (D:=gset K)); rewrite dom_op not_elem_of_union.
by apply insert_validN; [apply cmra_valid_validN|].
Qed.
Lemma alloc_updateP (Q : gmap K A Prop) m x :
......
......@@ -298,16 +298,17 @@ Section properties.
Global Instance list_singletonM_proper i :
Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Lemma elem_of_list_singletonM i z x : z {[i := x]} z = z = x.
Lemma elem_of_list_singletonM i z x : z ({[i := x]} : list A) z = z = x.
Proof.
rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
Qed.
Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
Proof. induction i; by f_equal/=. Qed.
Lemma list_lookup_singletonM_ne i j x :
i j {[ i := x ]} !! j = None {[ i := x ]} !! j = Some .
i j
({[ i := x ]} : list A) !! j = None ({[ i := x ]} : list A) !! j = Some .
Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
Lemma list_singletonM_validN n i x : {n} {[ i := x ]} {n} x.
Lemma list_singletonM_validN n i x : {n} ({[ i := x ]} : list A) {n} x.
Proof.
rewrite list_lookup_validN. split.
{ move=> /(_ i). by rewrite list_lookup_singletonM. }
......@@ -316,7 +317,7 @@ Section properties.
- destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
Qed.
Lemma list_singleton_valid i x : {[ i := x ]} x.
Lemma list_singleton_valid i x : ({[ i := x ]} : list A) x.
Proof.
rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
Qed.
......@@ -336,7 +337,8 @@ Section properties.
rewrite /singletonM /list_singletonM /=.
induction i; constructor; rewrite ?left_id; auto.
Qed.
Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
Lemma list_alter_singletonM f i x :
alter f i ({[i := x]} : list A) = {[i := f x]}.
Proof.
rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
Qed.
......
......@@ -105,6 +105,7 @@ Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
Class Discrete (A : ofeT) := discrete_timeless (x : A) :> Timeless x.
Hint Mode Discrete ! : typeclass_instances.
(** OFEs with a completion *)
Record chain (A : ofeT) := {
......
......@@ -7,7 +7,7 @@ Import uPred.
(** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N ownI i P)%I.
( i, i (N:coPset) ownI i P)%I.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := unseal inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := seal_eq inv_aux.
......@@ -34,7 +34,7 @@ Proof. apply ne_proper, _. Qed.
Global Instance inv_persistent N P : PersistentP (inv N P).
Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma fresh_inv_name (E : gset positive) N : i, i E i N.
Lemma fresh_inv_name (E : gset positive) N : i, i E i (N:coPset).
Proof.
exists (coPpick ( N coPset.of_gset E)).
rewrite -coPset.elem_of_of_gset (comm and) -elem_of_difference.
......@@ -46,7 +46,7 @@ Qed.
Lemma inv_alloc N E P : P ={E}= inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
iMod (ownI_alloc ( N) P with "[$HP $Hw]")
iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
as (i) "(% & $ & ?)"; auto using fresh_inv_name.
Qed.
......@@ -54,7 +54,7 @@ Lemma inv_alloc_open N E P :
N E True ={E, E∖↑N}= inv N P (P ={E∖↑N, E}= True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open ( N) P with "Hw")
iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
as (i) "(% & Hw & #Hi & HD)"; auto using fresh_inv_name.
iAssert (ownE {[i]} ownE ( N {[i]}) ownE (E N))%I
with "[HE]" as "(HEi & HEN\i & HE\N)".
......
......@@ -22,7 +22,7 @@ Section defs.
own p (CoPset E, ).
Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i N
( i, i (N:coPset)
inv N (P own p (, GSet {[i]}) na_own p {[i]}))%I.
End defs.
......@@ -71,7 +71,7 @@ Section proofs.
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i N)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i (N:coPset))).
intros Ef. exists (coPpick ( N coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
......
......@@ -37,7 +37,7 @@ Section namespace.
Lemma nclose_nroot : nroot = .
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N N.
Lemma encode_nclose N : encode N (N:coPset).
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
......@@ -54,7 +54,7 @@ Section namespace.
Lemma nclose_subseteq' E N x : N E N.@x E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N.@x) N.
Lemma ndot_nclose N x : encode (N.@x) (N:coPset).
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite ( N : coPset).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
......
......@@ -314,7 +314,7 @@ Proof.
Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in
let l := fresh (dom (gset loc) σ) in
to_val e = Some v head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
......
......@@ -138,7 +138,7 @@ Proof.
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
wp_load. destruct p.
- iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
- iMod ("Hclose" $! (State Low I) with "[Hl Hr]") as "Hγ".
{ iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
{ iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
......@@ -169,8 +169,7 @@ Proof.
iMod (saved_prop_alloc_strong (R2: %CF (iProp Σ)) (I {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]}))
{[Change i1; Change i2 ]} with "[-]") as "Hγ".
iMod ("Hclose" $! (State p ({[i1; i2]} I {[i]})) with "[-]") as "Hγ".
{ iSplit; first by eauto using split_step.
rewrite /barrier_inv /=. iNext. iFrame "Hl".
by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
......
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