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

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 817a80f9 b16c37e4
From algebra Require Export upred. From algebra Require Export upred.
From prelude Require Import fin_maps. From prelude Require Import fin_maps fin_collections.
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:= (** * Big ops over lists *)
match Ps with [] => True | P :: Ps => P uPred_big_and Ps end%I. (* These are the basic building blocks for other big ops *)
Instance: Params (@uPred_big_and) 1. Fixpoint uPred_list_and {M} (Ps : list (uPred M)) : uPred M:=
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope. match Ps with [] => True | P :: Ps => P uPred_list_and Ps end%I.
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M := Instance: Params (@uPred_list_and) 1.
match Ps with [] => True | P :: Ps => P uPred_big_sep Ps end%I. Notation "'Π∧' Ps" := (uPred_list_and Ps) (at level 20) : uPred_scope.
Instance: Params (@uPred_big_sep) 1. Fixpoint uPred_list_sep {M} (Ps : list (uPred M)) : uPred M :=
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope. match Ps with [] => True | P :: Ps => P uPred_list_sep Ps end%I.
Instance: Params (@uPred_list_sep) 1.
Notation "'Π★' Ps" := (uPred_list_sep Ps) (at level 20) : uPred_scope.
Definition uPred_big_sepM {M : cmraT} `{FinMapToList K A MA} (** * Other big ops *)
(P : K A uPred M) (m : MA) : uPred M := (** We use a type class to obtain overloaded notations *)
uPred_big_sep (curry P <$> map_to_list m). Class UPredBigSep (M : cmraT) (A B : Type) :=
Instance: Params (@uPred_big_sepM) 5. uPred_big_sep : A B uPred M.
Notation "'Π★{' P } m" := (uPred_big_sepM P m) Instance: Params (@uPred_big_sep) 4.
(at level 20, P at level 10, m at level 20, format "Π★{ P } m") : uPred_scope. Notation "'Π★{' x } P" := (uPred_big_sep x P)
(at level 20, x at level 10, format "Π★{ x } P") : uPred_scope.
Instance uPred_big_sepM {M} `{FinMapToList K A MA} :
UPredBigSep M MA (K A uPred M) := λ m P,
uPred_list_sep (curry P <$> map_to_list m).
Instance uPred_big_sepC {M} `{Elements A C} :
UPredBigSep M C (A uPred M) := λ X P, uPred_list_sep (P <$> elements X).
(** * Always stability for lists *)
Class AlwaysStableL {M} (Ps : list (uPred M)) := Class AlwaysStableL {M} (Ps : list (uPred M)) :=
always_stableL : Forall AlwaysStable Ps. always_stableL : Forall AlwaysStable Ps.
Arguments always_stableL {_} _ {_}. Arguments always_stableL {_} _ {_}.
...@@ -28,45 +38,47 @@ Implicit Types Ps Qs : list (uPred M). ...@@ -28,45 +38,47 @@ Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type. Implicit Types A : Type.
(* Big ops *) (* Big ops *)
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M). Global Instance list_and_proper : Proper (() ==> ()) (@uPred_list_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M). Global Instance list_sep_proper : Proper (() ==> ()) (@uPred_list_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed. Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M). Global Instance list_and_perm : Proper (() ==> ()) (@uPred_list_and M).
Proof. Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH. * by rewrite IH.
* by rewrite !assoc (comm _ P). * by rewrite !assoc (comm _ P).
* etransitivity; eauto. * etransitivity; eauto.
Qed. Qed.
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M). Global Instance list_sep_perm : Proper (() ==> ()) (@uPred_list_sep M).
Proof. Proof.
induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto. induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
* by rewrite IH. * by rewrite IH.
* by rewrite !assoc (comm _ P). * by rewrite !assoc (comm _ P).
* etransitivity; eauto. * etransitivity; eauto.
Qed. Qed.
Lemma big_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I. Lemma list_and_app Ps Qs : (Π (Ps ++ Qs))%I (Π Ps Π Qs)%I.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I (Π★ Ps Π★ Qs)%I. Lemma list_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I (Π★ Ps Π★ Qs)%I.
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed. Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_and Ps : (Π★ Ps) (Π Ps). Lemma list_sep_and Ps : (Π★ Ps) (Π Ps).
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed. Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
Lemma big_and_elem_of Ps P : P Ps (Π Ps) P. Lemma list_and_elem_of Ps P : P Ps (Π Ps) P.
Proof. induction 1; simpl; auto with I. Qed. Proof. induction 1; simpl; auto with I. Qed.
Lemma big_sep_elem_of Ps P : P Ps (Π★ Ps) P. Lemma list_sep_elem_of Ps P : P Ps (Π★ Ps) P.
Proof. induction 1; simpl; auto with I. Qed. Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *) (* Big ops over finite maps *)
Section fin_map. Section fin_map.
Context `{FinMap K Ma} {A} (P : K A uPred M). Context `{FinMap K Ma} {A} (P : K A uPred M).
Lemma big_sepM_empty : (Π★{P} )%I True%I. Lemma big_sepM_empty : (Π★{} P)%I True%I.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed. Proof. by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert (m : Ma A) i x : Lemma big_sepM_insert (m : Ma A) i x :
m !! i = None (Π★{P} (<[i:=x]> m))%I (P i x Π★{P} m)%I. m !! i = None (Π★{<[i:=x]> m} P)%I (P i x Π★{m} P)%I.
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed. Proof.
Lemma big_sepM_singleton i x : (Π★{P} {[i x]})%I (P i x)%I. intros ?; by rewrite /uPred_big_sep /uPred_big_sepM map_to_list_insert.
Qed.
Lemma big_sepM_singleton i x : (Π★{{[i x]}} P)%I (P i x)%I.
Proof. Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty. rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id. by rewrite big_sepM_empty right_id.
...@@ -76,9 +88,9 @@ End fin_map. ...@@ -76,9 +88,9 @@ End fin_map.
(* Always stable *) (* Always stable *)
Local Notation AS := AlwaysStable. Local Notation AS := AlwaysStable.
Local Notation ASL := AlwaysStableL. Local Notation ASL := AlwaysStableL.
Global Instance big_and_always_stable Ps : ASL Ps AS (Π Ps). Global Instance list_and_always_stable Ps : ASL Ps AS (Π Ps).
Proof. induction 1; apply _. Qed. Proof. induction 1; apply _. Qed.
Global Instance big_sep_always_stable Ps : ASL Ps AS (Π★ Ps). Global Instance list_sep_always_stable Ps : ASL Ps AS (Π★ Ps).
Proof. induction 1; apply _. Qed. Proof. induction 1; apply _. Qed.
Global Instance nil_always_stable : ASL (@nil (uPred M)). Global Instance nil_always_stable : ASL (@nil (uPred M)).
......
...@@ -72,7 +72,7 @@ Section heap. ...@@ -72,7 +72,7 @@ Section heap.
Qed. Qed.
Lemma heap_alloc N σ : Lemma heap_alloc N σ :
ownP σ pvs N N ( γ, heap_ctx HeapI γ N Π★{heap_mapsto HeapI γ} σ). ownP σ pvs N N ( γ, heap_ctx HeapI γ N Π★{σ} heap_mapsto HeapI γ).
Proof. Proof.
rewrite -{1}(from_to_heap σ); etransitivity; rewrite -{1}(from_to_heap σ); etransitivity;
first apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid. first apply (auth_alloc (ownP of_heap) N (to_heap σ)), to_heap_valid.
......
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