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

algebra/upred.v

@@ -552,6 +552,19 @@ Proof.
 Qed.
 Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I.
 Proof. by rewrite -!(commutative _ R) and_or_l. Qed.
+Lemma and_exist_l {A} P (Q : A → uPred M) : (P ∧ ∃ a, Q a)%I ≡ (∃ a, P ∧ Q a)%I.
+Proof.
+  apply (anti_symmetric (⊑)).
+  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
+    by rewrite -(exist_intro a).
+  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
+    by rewrite -(exist_intro a) and_elim_r.
+Qed.
+Lemma and_exist_r {A} P (Q : A → uPred M) : ((∃ a, Q a) ∧ P)%I ≡ (∃ a, Q a ∧ P)%I.
+Proof.
+  rewrite -(commutative _ P) and_exist_l.
+  apply exist_proper=>a. by rewrite commutative.
+Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
@@ -588,10 +601,6 @@ Proof.
 Qed.
 Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
 Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
-Lemma sep_or_l_1 P Q R : (P ★ (Q ∨ R)) ⊑ (P ★ Q ∨ P ★ R).
-Proof. by intros x n ? (x1&x2&Hx&?&[?|?]); [left|right]; exists x1, x2. Qed.
-Lemma sep_exist_l_1 {A} P (Q : A → uPred M) : (P ★ ∃ b, Q b) ⊑ (∃ b, P ★ Q b).
-Proof. by intros x [|n] ?; [done|intros (x1&x2&?&?&[a ?]); exists a,x1,x2]. Qed.
 
 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
@@ -643,13 +652,20 @@ Proof. auto. Qed.
 Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊑ ((P ★ R) ∧ (Q ★ R)).
 Proof. auto. Qed.
 Lemma sep_or_l P Q R : (P ★ (Q ∨ R))%I ≡ ((P ★ Q) ∨ (P ★ R))%I.
-Proof. apply (anti_symmetric (⊑)); eauto 10 using sep_or_l_1. Qed.
+Proof.
+  apply (anti_symmetric (⊑)); last by eauto 8.
+  apply wand_elim_r', or_elim; apply wand_intro_l.
+  - by apply or_intro_l.
+  - by apply or_intro_r.
+Qed.
 Lemma sep_or_r P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
 Proof. by rewrite -!(commutative _ R) sep_or_l. Qed.
 Lemma sep_exist_l {A} P (Q : A → uPred M) : (P ★ ∃ a, Q a)%I ≡ (∃ a, P ★ Q a)%I.
 Proof.
-  intros; apply (anti_symmetric (⊑)); eauto using sep_exist_l_1.
-  apply exist_elim=> a; apply sep_mono; auto using exist_intro.
+  intros; apply (anti_symmetric (⊑)).
+  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
+    by rewrite -(exist_intro a).
+  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
 Qed.
 Lemma sep_exist_r {A} (P: A → uPred M) Q: ((∃ a, P a) ★ Q)%I ≡ (∃ a, P a ★ Q)%I.
 Proof. setoid_rewrite (commutative _ _ Q); apply sep_exist_l. Qed.

heap_lang/sugar.v

@@ -11,6 +11,22 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
 Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
 
+(* Prove and "register" compatibility with substitution. *)
+Lemma Lam_subst e s : (Lam e).[s] = Lam e.[up s].
+Proof. by unfold Lam; asimpl. Qed.
+Hint Rewrite Lam_subst : autosubst.
+Global Opaque Lam.
+
+Lemma Let_subst e1 e2 s : (Let e1 e2).[s] = Let e1.[s] e2.[up s].
+Proof. by unfold Let; asimpl. Qed.
+Hint Rewrite Let_subst : autosubst.
+Global Opaque Let.
+
+Lemma Seq_subst e1 e2 s : (Seq e1 e2).[s] = Seq e1.[s] e2.[s].
+Proof. by unfold Seq; asimpl. Qed.
+Hint Rewrite Seq_subst : autosubst.
+Global Opaque Seq.
+
 Module notations.
   Delimit Scope lang_scope with L.
   Bind Scope lang_scope with expr.
@@ -73,6 +89,12 @@ Proof.
   by rewrite -wp_lam //= to_of_val.
 Qed.
 
+Lemma wp_seq E e1 e2 Q :
+  wp E e1 (λ _, ▷wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
+Proof.
+  rewrite -wp_let. apply wp_mono=>v. by asimpl.
+Qed.
+
 Lemma wp_le E (n1 n2 : nat) P Q :
   (n1 ≤ n2 → P ⊑ ▷ Q (LitV true)) →
   (n1 > n2 → P ⊑ ▷ Q (LitV false)) →

heap_lang/tests.v

@@ -12,7 +12,11 @@ Module LangTests.
   Proof. Set Printing All. intros; do_step done. Qed.
   Definition lam : expr := λ: #0 + Lit 21.
   Goal ∀ σ, prim_step (lam (Lit 21)) σ add σ None.
-  Proof. intros; do_step done. Qed.
+  Proof.
+    (* FIXME WTF why does it print all the "S (S (S..."?? *)
+    rewrite /lam /Lam.
+    intros; do_step done.
+  Qed.
 End LangTests.
 
 Module LiftingTests.
@@ -20,7 +24,6 @@ Module LiftingTests.
   Implicit Types P : iProp heap_lang Σ.
   Implicit Types Q : val → iProp heap_lang Σ.
 
-  (* FIXME: Fix levels so that we do not need the parenthesis here. *)
   Definition e  : expr := let: ref (Lit 1) in #0 <- !#0 + Lit 1; !#0.
   Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitV 2))).
   Proof.
@@ -30,9 +33,8 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    (* TODO RJ: If you go here, you can see how the sugar does not print
-       all so nicely. *)
     rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
+    (* FIXME: doing simpl here kills the Seq, turns it all the way into Rec *)
     rewrite -(wp_bindi (StoreRCtx (LocV _))).
     rewrite -(wp_bindi (BinOpLCtx PlusOp _)).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
@@ -43,20 +45,15 @@ Module LiftingTests.
     { by rewrite lookup_insert. }
     { done. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    rewrite -wp_lam // -later_intro. asimpl.
+    rewrite -wp_seq -wp_value -later_intro.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
     { by rewrite lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
 
-  (* TODO: once asimpl preserves notation, we don't need
-     FindPred' anymore. *)
-  (* FIXME: fix notation so that we do not need parenthesis or %L *)
-  Definition FindPred' (n1 Sn1 n2 f : expr) : expr :=
-    if Sn1 < n2 then f Sn1 else n1.
   Definition FindPred (n2 : expr) : expr :=
-    rec:: (let: #1 + Lit 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
+    rec:: (let: #1 + Lit 1 in if #0 < n2.[ren(+3)] then #1 #0 else #2).
   Definition Pred : expr :=
     λ: (if #0 ≤ Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
 
@@ -70,11 +67,7 @@ Module LiftingTests.
     { apply and_mono; first done. by rewrite -later_intro. }
     apply later_mono.
     (* Go on *)
-    (* FIXME "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
-    fail after we changed # n to use ids instead of Var *)
-    pose proof (wp_let (Σ:=Σ) E (Lit n1 + Lit 1)%L
-                   (FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2))) Q).
-    unfold Let, Lam in H; rewrite -H.
+    rewrite -wp_let.
     rewrite -wp_bin_op //. asimpl.
     rewrite -(wp_bindi (IfCtx _ _)).
     rewrite -!later_intro /=.

prelude/co_pset.v

@@ -332,6 +332,12 @@ Proof.
   * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
 Qed.
 
+Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
+Proof.
+  rewrite coPset_finite_spec; simpl.
+  (* FIXME no time to finish right now, but I think it holds *)
+Abort. 
+
 (** * Splitting of infinite sets *)
 Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
   match t with

program_logic/namespace.v

 Require Export algebra.base prelude.countable prelude.co_pset.
 Require Import program_logic.ownership.
 Require Export program_logic.pviewshifts.
+Import uPred.
+
+Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
+Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
+Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
+Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
@@ -34,7 +40,63 @@ Proof.
   induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
 Qed.
 
+Local Hint Resolve nclose_subseteq ndot_nclose.
+
 (** Derived forms and lemmas about them. *)
 Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
-  ownI (encode N) P.
-(* TODO: Add lemmas about inv here. *)
+  (∃ i : positive, ■(i ∈ nclose N) ∧ ownI i P)%I.
+
+Section inv.
+Context {Λ : language} {Σ : iFunctor}.
+Implicit Types i : positive.
+Implicit Types N : namespace.
+Implicit Types P Q R : iProp Λ Σ.
+
+Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
+Proof.
+  intros n ? ? EQ. apply exists_ne=>i.
+  apply and_ne; first done.
+  by apply ownI_contractive.
+Qed.
+
+Global Instance inv_always_stable N P : AlwaysStable (inv N P) := _.
+
+Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
+Proof. by rewrite always_always. Qed.
+
+(* We actually pretty much lose the abolity to deal with mask-changing view
+   shifts when using `inv`. This is because we cannot exactly name the invariants
+   any more. But that's okay; all this means is that sugar like the atomic
+   triples will have to prove its own version of the open_close rule
+   by unfolding `inv`. *)
+Lemma pvs_open_close E N P Q R :
+  nclose N ⊆ E →
+  P ⊑ (inv N R ∧ (▷R -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷R ★ Q)))%I →
+  P ⊑ pvs E E Q.
+Proof.
+  move=>HN -> {P}.
+  rewrite /inv and_exist_r. apply exist_elim=>i.
+  rewrite -associative. apply const_elim_l=>HiN.
+  (* Add this to the local context, so that solve_elem_of finds it. *)
+  assert ({[encode i]} ⊆ nclose N) by eauto.
+  rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)).
+  rewrite {1}pvs_openI !pvs_frame_r.
+  (* TODO is there a common pattern here in the way we combine pvs_trans
+     and pvs_mask_frame_mono? *)
+  rewrite -(pvs_trans E (E ∖ {[ encode i ]}));
+    last by solve_elem_of. (* FIXME: Shouldn't eauto work, since I added a Hint Extern? *)
+  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  rewrite (commutative _ (▷R)%I) -associative wand_elim_r pvs_frame_l.
+  rewrite -(pvs_trans _ (E ∖ {[ encode i ]}) E); last by solve_elem_of.
+  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
+  apply pvs_mask_frame'; solve_elem_of.
+Qed.
+
+Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P).
+Proof.
+  rewrite /inv (pvs_allocI N); first done.
+  (* FIXME use coPset_suffixes_infinite. *)
+Abort.
+
+End inv.

program_logic/ownership.v

@@ -19,20 +19,20 @@ Implicit Types P : iProp Λ Σ.
 Implicit Types m : iGst Λ Σ.
 
 (* Invariants *)
-Global Instance inv_contractive i : Contractive (@ownI Λ Σ i).
+Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
 Proof.
   intros n P Q HPQ.
   apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
   by unfold ownI; rewrite HPQ.
 Qed.
-Lemma always_inv i P : (□ ownI i P)%I ≡ ownI i P.
+Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P.
 Proof.
   apply uPred.always_own.
   by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
 Qed.
-Global Instance inv_always_stable i P : AlwaysStable (ownI i P).
-Proof. by rewrite /AlwaysStable always_inv. Qed.
-Lemma inv_sep_dup i P : ownI i P ≡ (ownI i P ★ ownI i P)%I.
+Global Instance ownI_always_stable i P : AlwaysStable (ownI i P).
+Proof. by rewrite /AlwaysStable always_ownI. Qed.
+Lemma ownI_sep_dup i P : ownI i P ≡ (ownI i P ★ ownI i P)%I.
 Proof. apply (uPred.always_sep_dup' _). Qed.
 
 (* physical state *)
@@ -63,7 +63,7 @@ Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
 (* inversion lemmas *)
-Lemma inv_spec r n i P :
+Lemma ownI_spec r n i P :
   ✓{n} r →
   (ownI i P) n r ↔ wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
 Proof.

program_logic/pviewshifts.v

@@ -79,20 +79,20 @@ Proof.
   exists (r' ⋅ r2); split; last by rewrite -(associative _).
   exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto.
 Qed.
-Lemma pvs_open i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P).
+Lemma pvs_openI i P : ownI i P ⊑ pvs {[ i ]} ∅ (▷ P).
 Proof.
   intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia.
-  apply inv_spec in Hinv; last auto.
+  apply ownI_spec in Hinv; last auto.
   destruct (wsat_open k Ef σ (r ⋅ rf) i P) as (rP&?&?); auto.
   { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
   exists (rP ⋅ r); split; last by rewrite (left_id_L _ _) -(associative _).
   eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
 Qed.
-Lemma pvs_close i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
+Lemma pvs_closeI i P : (ownI i P ∧ ▷ P) ⊑ pvs ∅ {[ i ]} True.
 Proof.
   intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
   rewrite (left_id _ _); apply wsat_close with P r.
-  * apply inv_spec, uPred_weaken with r (S n); auto.
+  * apply ownI_spec, uPred_weaken with r (S n); auto.
   * solve_elem_of +HE.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
@@ -116,7 +116,7 @@ Proof.
       auto using option_update_None. }
   by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
 Qed.
-Lemma pvs_alloc E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P).
+Lemma pvs_allocI E P : ¬set_finite E → ▷ P ⊑ pvs E E (∃ i, ■ (i ∈ E) ∧ ownI i P).
 Proof.
   intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
   destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
@@ -144,13 +144,29 @@ Lemma pvs_impl_l E1 E2 P Q : (□ (P → Q) ∧ pvs E1 E2 P) ⊑ pvs E1 E2 Q.
 Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
 Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P ∧ □ (P → Q)) ⊑ pvs E1 E2 Q.
 Proof. by rewrite (commutative _) pvs_impl_l. Qed.
+
+Lemma pvs_mask_frame' E1 E1' E2 E2' P :
+  E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P.
+Proof.
+  intros HE1 HE2 HEE. rewrite (pvs_mask_frame _ _ (E1 ∖ E1')).
+  - rewrite {2}HEE =>{HEE}. by rewrite -!union_difference_L.
+  - solve_elem_of.
+Qed. 
+
+Lemma pvs_mask_frame_mono E1 E1' E2 E2' P Q :
+  E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' →
+  P ⊑ Q → pvs E1' E2' P ⊑ pvs E1 E2 Q.
+Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
+
 Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
 Proof.
-  intros; rewrite (union_difference_L E1 E2) //; apply pvs_mask_frame; auto.
+  intros. apply pvs_mask_frame'; solve_elem_of.
 Qed.
+
 Lemma pvs_ownG_update E m m' : m ~~> m' → ownG m ⊑ pvs E E (ownG m').
 Proof.
   intros; rewrite (pvs_ownG_updateP E _ (m' =)); last by apply cmra_update_updateP.
   by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
 Qed.
+
 End pvs.

program_logic/viewshifts.v

@@ -87,7 +87,7 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → P >{E}> Q ⊑ P >{E ∪ Ef}> Q.
 Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 Lemma vs_open i P : ownI i P >{{[i]},∅}> ▷ P.
-Proof. intros; apply vs_alt, pvs_open. Qed.
+Proof. intros; apply vs_alt, pvs_openI. Qed.
 
 Lemma vs_open' E i P : i ∉ E → ownI i P >{{[i]} ∪ E,E}> ▷ P.
 Proof.
@@ -96,7 +96,7 @@ Proof.
 Qed.
 
 Lemma vs_close i P : (ownI i P ∧ ▷ P) >{∅,{[i]}}> True.
-Proof. intros; apply vs_alt, pvs_close. Qed.
+Proof. intros; apply vs_alt, pvs_closeI. Qed.
 
 Lemma vs_close' E i P : i ∉ E → (ownI i P ∧ ▷ P) >{E,{[i]} ∪ E}> True.
 Proof.
@@ -116,6 +116,6 @@ Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed.
 Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
 Proof. by intros; apply vs_alt, pvs_ownG_update. Qed.
 Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ ownI i P).
-Proof. by intros; apply vs_alt, pvs_alloc. Qed.
+Proof. by intros; apply vs_alt, pvs_allocI. Qed.
 
 End vs.