Commit 93df90de authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

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

parents 315ef81d f972b5a9
......@@ -320,10 +320,10 @@ Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
Lemma cmra_pcore_idemp' x cx : pcore x Some cx pcore cx Some cx.
Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
Lemma cmra_pcore_pcore x cx : pcore x = Some cx cx cx cx.
Proof. eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
Lemma cmra_pcore_pcore' x cx : pcore x Some cx cx cx cx.
Proof. eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
Lemma cmra_pcore_dup x cx : pcore x = Some cx cx cx cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
Lemma cmra_pcore_dup' x cx : pcore x Some cx cx cx cx.
Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp'. Qed.
Lemma cmra_pcore_validN n x cx : {n} x pcore x = Some cx {n} cx.
Proof.
intros Hvx Hx%cmra_pcore_l. move: Hvx; rewrite -Hx. apply cmra_validN_op_l.
......@@ -333,6 +333,10 @@ Proof.
intros Hv Hx%cmra_pcore_l. move: Hv; rewrite -Hx. apply cmra_valid_op_l.
Qed.
(** ** Persistent elements *)
Lemma persistent_dup x `{!Persistent x} : x x x.
Proof. by apply cmra_pcore_dup' with x. Qed.
(** ** Order *)
Lemma cmra_included_includedN n x y : x y x {n} y.
Proof. intros [z ->]. by exists z. Qed.
......@@ -428,8 +432,8 @@ Section total_core.
Lemma cmra_core_r x : x core x x.
Proof. by rewrite (comm _ x) cmra_core_l. Qed.
Lemma cmra_core_core x : core x core x core x.
Proof. by rewrite -{2}(cmra_core_idemp x) cmra_core_r. Qed.
Lemma cmra_core_dup x : core x core x core x.
Proof. by rewrite -{3}(cmra_core_idemp x) cmra_core_r. Qed.
Lemma cmra_core_validN n x : {n} x {n} core x.
Proof. rewrite -{1}(cmra_core_l x); apply cmra_validN_op_l. Qed.
Lemma cmra_core_valid x : x core x.
......
......@@ -876,7 +876,7 @@ Proof. by unseal. Qed.
Lemma always_and_sep_1 P Q : (P Q) (P Q).
Proof.
unseal; split=> n x ? [??].
exists (core x), (core x); rewrite cmra_core_core; auto.
exists (core x), (core x); rewrite -cmra_core_dup; auto.
Qed.
Lemma always_and_sep_l_1 P Q : ( P Q) ( P Q).
Proof.
......
......@@ -112,7 +112,7 @@ Section gmap.
Implicit Types Φ Ψ : K A uPred M.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
m2 m1 ( k x, m2 !! k = Some x Φ k x Ψ k x)
([ map] k x m1, Φ k x) ([ map] k x m2, Ψ k x).
Proof.
intros HX HΦ. trans ([ map] kx m2, Φ k x)%I.
......@@ -121,7 +121,7 @@ Section gmap.
apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
Qed.
Lemma big_sepM_proper Φ Ψ m1 m2 :
m1 m2 ( x k, m1 !! k = Some x m2 !! k = Some x Φ k x ⊣⊢ Ψ k x)
m1 m2 ( k x, m1 !! k = Some x m2 !! k = Some x Φ k x ⊣⊢ Ψ k x)
([ map] k x m1, Φ k x) ⊣⊢ ([ map] k x m2, Ψ k x).
Proof.
(* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
......@@ -149,14 +149,30 @@ Section gmap.
Lemma big_sepM_empty Φ : ([ map] kx , Φ k x) ⊣⊢ True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
m !! i = None
([ map] ky <[i:=x]> m, Φ k y) ⊣⊢ (Φ i x [ map] ky m, Φ k y).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_fn_insert (Ψ : K A uPred M uPred M) (Φ : K uPred M) m i x P :
m !! i = None
([ map] ky <[i:=x]> m, Ψ k y (<[i:=P]> Φ k))
⊣⊢ (Ψ i x P [ map] ky m, Ψ k y (Φ k)).
Proof.
intros. rewrite big_sepM_insert // fn_lookup_insert.
apply sep_proper, big_sepM_proper; auto=> k y ??.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_sepM_fn_insert' (Φ : K uPred M) m i x P :
m !! i = None
([ map] ky <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P [ map] ky m, Φ k).
Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
Lemma big_sepM_delete Φ (m : gmap K A) i x :
m !! i = Some x
([ map] ky m, Φ k y) ⊣⊢ (Φ i x [ map] ky delete i m, Φ k y).
Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
Lemma big_sepM_singleton Φ i x : ([ map] ky {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
......@@ -222,7 +238,7 @@ Section gset.
Lemma big_sepS_insert Φ X x :
x X ([ set] y {[ x ]} X, Φ y) ⊣⊢ (Φ x [ set] y X, Φ y).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_insert' (Ψ : A uPred M uPred M) Φ X x P :
Lemma big_sepS_fn_insert (Ψ : A uPred M uPred M) Φ X x P :
x X
([ set] y {[ x ]} X, Ψ y (<[x:=P]> Φ y))
⊣⊢ (Ψ x P [ set] y X, Ψ y (Φ y)).
......@@ -231,9 +247,9 @@ Section gset.
apply sep_proper, big_sepS_proper; auto=> y ??.
by rewrite fn_lookup_insert_ne; last set_solver.
Qed.
Lemma big_sepS_insert'' Φ X x P :
Lemma big_sepS_fn_insert' Φ X x P :
x X ([ set] y {[ x ]} X, <[x:=P]> Φ y) ⊣⊢ (P [ set] y X, Φ y).
Proof. apply (big_sepS_insert' (λ y, id)). Qed.
Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
Lemma big_sepS_delete Φ X x :
x X ([ set] y X, Φ y) ⊣⊢ (Φ x [ set] y X {[ x ]}, Φ y).
......
......@@ -88,9 +88,9 @@ Proof.
iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
rewrite -assoc_L !big_sepS_insert''; [|abstract set_solver ..].
rewrite -assoc_L !big_sepS_fn_insert'; [|abstract set_solver ..].
by iFrame "HR1 HR2".
- rewrite -assoc_L !big_sepS_insert'; [|abstract set_solver ..].
- rewrite -assoc_L !big_sepS_fn_insert; [|abstract set_solver ..].
by repeat iSplit.
Qed.
......
......@@ -316,7 +316,6 @@ Arguments compose _ _ _ _ _ _ /.
Arguments flip _ _ _ _ _ _ /.
Arguments const _ _ _ _ /.
Typeclasses Transparent id compose flip const.
Instance: Params (@pair) 2.
Definition fun_map {A A' B B'} (f: A' A) (g: B B') (h : A B) : A' B' :=
g h f.
......@@ -402,6 +401,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").
Instance: Params (@pair) 2.
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
Definition curry3 {A B C D} (f : A B C D) (p : A * B * C) : D :=
......
......@@ -717,14 +717,34 @@ Qed.
Class SepDestruct (p : bool) (P Q1 Q2 : uPred M) :=
sep_destruct : ?p P ?p (Q1 Q2).
Arguments sep_destruct : clear implicits.
Class OpDestruct {A : cmraT} (a b1 b2 : A) :=
op_destruct : a b1 b2.
Arguments op_destruct {_} _ _ _ {_}.
Global Instance op_destruct_op {A : cmraT} (a b : A) : OpDestruct (a b) a b.
Proof. by rewrite /OpDestruct. Qed.
Global Instance op_destruct_persistent {A : cmraT} (a : A) :
Persistent a OpDestruct a a a.
Proof. intros; apply (persistent_dup a). Qed.
Global Instance op_destruct_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
OpDestruct a b1 b2 OpDestruct a' b1' b2'
OpDestruct (a,a') (b1,b1') (b2,b2').
Proof. by constructor. Qed.
Global Instance op_destruct_Some {A : cmraT} (a : A) b1 b2 :
OpDestruct a b1 b2 OpDestruct (Some a) (Some b1) (Some b2).
Proof. by constructor. Qed.
Lemma sep_destruct_spatial p P Q1 Q2 : P (Q1 Q2) SepDestruct p P Q1 Q2.
Proof. rewrite /SepDestruct=> ->. by rewrite always_if_sep. Qed.
Global Instance sep_destruct_sep p P Q : SepDestruct p (P Q) P Q.
Proof. by apply sep_destruct_spatial. Qed.
Global Instance sep_destruct_ownM p (a b : M) :
SepDestruct p (uPred_ownM (a b)) (uPred_ownM a) (uPred_ownM b).
Proof. apply sep_destruct_spatial. by rewrite ownM_op. Qed.
Proof. rewrite /SepDestruct. by rewrite always_if_sep. Qed.
Global Instance sep_destruct_ownM p (a b1 b2 : M) :
OpDestruct a b1 b2
SepDestruct p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
rewrite /OpDestruct /SepDestruct=> ->. by rewrite ownM_op always_if_sep.
Qed.
Global Instance sep_destruct_and P Q : SepDestruct true (P Q) P Q.
Proof. by rewrite /SepDestruct /= always_and_sep. Qed.
......
......@@ -6,9 +6,9 @@ Section ghost.
Context `{inG Λ Σ A}.
Implicit Types a b : A.
Global Instance sep_destruct_own p γ a b :
SepDestruct p (own γ (a b)) (own γ a) (own γ b).
Proof. apply sep_destruct_spatial. by rewrite own_op. Qed.
Global Instance sep_destruct_own p γ a b1 b2 :
OpDestruct a b1 b2 SepDestruct p (own γ a) (own γ b1) (own γ b2).
Proof. rewrite /OpDestruct /SepDestruct => ->. by rewrite own_op. Qed.
Global Instance sep_split_own γ a b :
SepSplit (own γ (a b)) (own γ a) (own γ b) | 90.
Proof. by rewrite /SepSplit own_op. Qed.
......
......@@ -768,3 +768,4 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ _) => by iPureIntro.
Hint Extern 0 (of_envs _ _) => iAssumption.
Hint Resolve uPred.eq_refl'. (* Maybe make an [iReflexivity] tactic *)
......@@ -67,9 +67,9 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
( z, P z y) (P - (x,x) (y,x)).
Proof.
iIntros "H1 H2".
iRewrite (uPred.eq_sym x x with "[#]"). iApply uPred.eq_refl.
iRewrite (uPred.eq_sym x x with "[#]"); first done.
iRewrite -("H1" $! _ with "[#]"); first done.
iApply uPred.eq_refl.
done.
Qed.
Lemma demo_6 (M : ucmraT) (P Q : uPred M) :
......
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