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

algebra/auth.v

 Require Export algebra.excl.
-Require Import algebra.functor algebra.option.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
@@ -148,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
 Proof. by rewrite /op /auth_op /= left_id. Qed.
 
 (* FIXME tentative name. Or maybe remove this notion entirely. *)
-Definition auth_step a a' b b' :=
+Definition auth_step (a a' b b' : A) : Prop :=
   ∀ n af, ✓{n} a → a ≡{n}≡ a' ⋅ af → b ≡{n}≡ b' ⋅ af ∧ ✓{n} b.
 
 Lemma auth_update a a' b b' :
@@ -160,27 +160,31 @@ Proof.
   { by rewrite Ha left_id associative. }
   split; [by rewrite Ha' left_id associative; apply cmra_includedN_l|done].
 Qed.
-Lemma auth_update_op_l a a' b :
-  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
+
+(* FIXME: are the following lemmas derivable from each other? *)
+Lemma auth_local_update_l f `{!LocalUpdate P f} a a' :
+  P a → ✓ (f a ⋅ a') →
+  ● (a ⋅ a') ⋅ ◯ a ~~> ● (f a ⋅ a') ⋅ ◯ f a.
+Proof.
+  intros; apply auth_update=>n af ? EQ; split; last done.
+  by rewrite -(local_updateN f) // EQ -(local_updateN f) // -EQ.
+Qed.
+
+Lemma auth_local_update f `{!LocalUpdate P f} a a' :
+  P a → ✓ (f a') →
+  ● a' ⋅ ◯ a ~~> ● f a' ⋅ ◯ f a.
 Proof.
-  intros; apply auth_update.
-  by intros n af ? Ha; split; [by rewrite Ha associative|].
+  intros; apply auth_update=>n af ? EQ; split; last done.
+  by rewrite EQ (local_updateN f) // -EQ.
 Qed.
+
+Lemma auth_update_op_l a a' b :
+  ✓ (b ⋅ a) → ● a ⋅ ◯ a' ~~> ● (b ⋅ a) ⋅ ◯ (b ⋅ a').
+Proof. by intros; apply (auth_local_update _). Qed.
 Lemma auth_update_op_r a a' b :
   ✓ (a ⋅ b) → ● a ⋅ ◯ a' ~~> ● (a ⋅ b) ⋅ ◯ (a' ⋅ b).
 Proof. rewrite -!(commutative _ b); apply auth_update_op_l. Qed.
 
-Lemma auth_local_update (L : LocalUpdate A) `{!LocalUpdateSpec L} a a' b :
-  L a = Some b → ✓(b ⋅ a') →
-  ● (a ⋅ a') ⋅ ◯ a ~~> ● (b ⋅ a') ⋅ ◯ b.
-Proof.
-  intros Hlv Hv. apply auth_update=>n af Hab EQ.
-  split; last done.
-  apply (injective (R:=(≡)) Some).
-  rewrite !Some_op -Hlv.
-  rewrite -!local_update_spec //; eauto; last by rewrite -EQ; [].
-  by rewrite EQ.
-Qed.
 End cmra.
 
 Arguments authRA : clear implicits.

algebra/cmra.v

@@ -128,6 +128,7 @@ Class CMRAIdentity (A : cmraT) `{Empty A} : Prop := {
   cmra_empty_left_id :> LeftId (≡) ∅ (⋅);
   cmra_empty_timeless :> Timeless ∅
 }.
+Instance cmra_identity_inhabited `{CMRAIdentity A} : Inhabited A := populate ∅.
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
@@ -135,6 +136,13 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
   validN_preserving n x : ✓{n} x → ✓{n} (f x)
 }.
 
+(** * Local updates *)
+Class LocalUpdate {A : cmraT} (P : A → Prop) (f : A → A) := {
+  local_update_ne n :> Proper (dist n ==> dist n) f;
+  local_updateN n x y : P x → ✓{n} (x ⋅ y) → f (x ⋅ y) ≡{n}≡ f x ⋅ y
+}.
+Arguments local_updateN {_ _} _ {_} _ _ _ _ _.
+
 (** * Frame preserving updates *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ z n,
   ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
@@ -313,6 +321,18 @@ Section identity.
   Proof. by rewrite -{2}(cmra_unit_l ∅) right_id. Qed.
 End identity.
 
+(** ** Local updates *)
+Global Instance local_update_proper P (f : A → A) :
+  LocalUpdate P f → Proper ((≡) ==> (≡)) f.
+Proof. intros; apply (ne_proper _). Qed.
+
+Lemma local_update f `{!LocalUpdate P f} x y :
+  P x → ✓ (x ⋅ y) → f (x ⋅ y) ≡ f x ⋅ y.
+Proof. by rewrite equiv_dist=>?? n; apply (local_updateN f). Qed.
+
+Global Instance local_update_op x : LocalUpdate (λ _, True) (op x).
+Proof. split. apply _. by intros n y1 y2 _ _; rewrite associative. Qed.
+
 (** ** Updates *)
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.

algebra/excl.v

 Require Export algebra.cmra.
-Require Import algebra.functor algebra.option.
+Require Import algebra.functor.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 
@@ -138,23 +138,16 @@ Proof.
   by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
 Qed.
 
-(* Updates *)
+(** ** Local updates *)
+Global Instance excl_local_update b :
+  LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
+Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
+
+(** Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
 Proof. by destruct y; intros ? [?| |]. Qed.
 Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P.
 Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
-
-Definition excl_local_update_to (b : A) : LocalUpdate exclRA :=
-  λ a, if a is Excl _ then Some (Excl b) else None.
-Global Instance excl_local_update_to_spec b :
-  LocalUpdateSpec (excl_local_update_to b).
-Proof.
-  split.
-  - move=>? a a' EQ. destruct EQ; done.
-  - move=>a a' n [b' Hlv] Hv /=. destruct a; try discriminate Hlv; [].
-    destruct a'; try contradiction Hv; []. reflexivity.
-Qed.
-
 End excl.
 
 Arguments exclC : clear implicits.

algebra/fin_maps.v

@@ -34,6 +34,12 @@ Global Instance lookup_ne n k :
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
+Global Instance alter_ne f k n :
+  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
+Proof.
+  intros ? m m' Hm k'.
+  by destruct (decide (k = k')); simplify_map_equality; rewrite (Hm k').
+Qed.
 Global Instance insert_ne i n :
   Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
 Proof.
@@ -280,47 +286,18 @@ Lemma map_updateP_alloc' m x :
 Proof. eauto using map_updateP_alloc. Qed.
 End freshness.
 
-Section local.
-Definition map_local_alloc i x : LocalUpdate (mapRA K A) :=
-  local_update_op {[ i ↦ x ]}.
-
 (* Deallocation is not a local update. The trouble is that if we own {[ i ↦ x ]},
    then the frame could always own "unit x", and prevent deallocation. *)
-
-Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
-Definition map_local_update i : LocalUpdate (mapRA K A) :=
-  λ m, x ← m !! i; y ← L x; Some (<[i:=y]>m).
-Global Instance map_local_update_spec i : LocalUpdateSpec (map_local_update i).
+Global Instance map_alter_update `{!LocalUpdate P f} i :
+  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ P x) (alter f i).
 Proof.
-  rewrite /map_local_update. split.
-  - (* FIXME Oh wow, this is harder than expected... *)
-    move=>n f g EQ. move:(EQ i).
-    case _:(f !! i)=>[fi|]; case _:(g !! i)=>[gi|]; move=>EQi;
-      inversion EQi; subst; simpl; last done.
-    assert (EQL : L fi ≡{n}≡ L gi) by (by apply local_update_ne). move: EQL.
-    case _:(L fi)=>[Lfi|] /=; case _:(L gi)=>[Lgi|]; move=>EQL;
-      inversion EQL; subst; simpl; last done.
-    apply Some_ne, insert_ne; done.
-  - move=>f g n [b Hlv] Hv. rewrite lookup_op. move:Hlv.
-    case EQf:(f !! i)=>[fi|]; simpl; last discriminate.
-    case EQL:(L fi)=>[Lfi|]; simpl; last discriminate.
-    case=>?. subst b.
-    case EQg:(g !! i)=>[gi|]; simpl.
-    + assert (L (fi ⋅ gi) ≡{n}≡ L fi ⋅ Some gi) as EQLi.
-      { apply local_update_spec; first by eauto.
-        move:(Hv i). rewrite lookup_op EQf EQg -Some_op. done. }
-      rewrite EQL -Some_op in EQLi.
-      destruct (L (fi ⋅ gi)) as [Lfgi|]; inversion EQLi; subst; simpl.
-      rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
-      destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
-      rewrite EQg -Some_op. apply Some_ne. done.
-    + rewrite EQL /=.
-      rewrite -Some_op. apply Some_ne. move=>j. rewrite lookup_op.
-      destruct (decide (i = j)); simplify_map_equality; last by rewrite lookup_op.
-      by rewrite EQg.
+  split; first apply _.
+  intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
+  - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
+    move: (Hm j); rewrite lookup_op Hix.
+    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN f).
+  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
 Qed.
-End local.
-
 End properties.
 
 (** Functor *)
@@ -358,4 +335,3 @@ Next Obligation.
   intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
   apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
 Qed.
-

algebra/option.v

@@ -187,28 +187,3 @@ Next Obligation.
   intros Σ A B C f g x. rewrite /= -option_fmap_compose.
   apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
 Qed.
-
-(** * Local CMRA Updates *)
-(* FIXME: These need the CMRA structure on option, hence they are defined here. Or maybe moe option to cmra.v? *)
-(* TODO: Probably needs some more magic flags. What about notation? *)
-Section local_update.
-  Context {A : cmraT}.
-  (* Do we need more step-indexing here? *)
-  Definition LocalUpdate := A → option A.
-  Class LocalUpdateSpec (L : LocalUpdate) := {
-    local_update_ne n :> Proper ((dist n) ==> (dist n)) L;
-    local_update_spec a b n : is_Some (L a) → ✓{n}(a ⋅ b) → L (a ⋅ b) ≡{n}≡ (L a) ⋅ Some b
-  }.
-
-  Definition local_update_op (b : A) : LocalUpdate
-    := λ a, Some (b ⋅ a).
-  Global Instance local_update_op_spec b : LocalUpdateSpec (local_update_op b).
-  Proof.
-    rewrite /local_update_op. split.
-    - move=>? ? ? EQ /=. by rewrite EQ.
-    - move=>a a' n Hlv Hv /=. by rewrite associative.
-  Qed.
-End local_update.
-Arguments LocalUpdate : clear implicits.
-
-

heap_lang/lifting.v

@@ -3,6 +3,57 @@ Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
+(** The substitution operation [gsubst e x ev] behaves just as [subst] but
+in case [e] does not contain the free variable [x] it will return [e] in a
+way that is syntactically equal (i.e. without any Coq-level delta reduction
+performed) *)
+Definition gsubst_lift {A B C} (f : A → B → C)
+    (x : A) (y : B) (mx : option A) (my : option B) : option C :=
+  match mx, my with
+  | Some x, Some y => Some (f x y)
+  | Some x, None => Some (f x y)
+  | None, Some y => Some (f x y)
+  | None, None => None
+  end.
+Fixpoint gsubst_go (e : expr) (x : string) (ev : expr) : option expr :=
+  match e with
+  | Var y => if decide (x = y ∧ x ≠ "") then Some ev else None
+  | Rec f y e =>
+     if decide (x ≠ f ∧ x ≠ y) then Rec f y <$> gsubst_go e x ev else None
+  | App e1 e2 => gsubst_lift App e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Lit l => None
+  | UnOp op e => UnOp op <$> gsubst_go e x ev
+  | BinOp op e1 e2 =>
+     gsubst_lift (BinOp op) e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | If e0 e1 e2 =>
+     gsubst_lift id (If e0 e1) e2
+       (gsubst_lift If e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
+       (gsubst_go e2 x ev)
+  | Pair e1 e2 => gsubst_lift Pair e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Fst e => Fst <$> gsubst_go e x ev
+  | Snd e => Snd <$> gsubst_go e x ev
+  | InjL e => InjL <$> gsubst_go e x ev
+  | InjR e => InjR <$> gsubst_go e x ev
+  | Case e0 x1 e1 x2 e2 =>
+     gsubst_lift id (Case e0 x1 e1 x2) e2
+       (gsubst_lift (λ e0' e1', Case e0' x1 e1' x2) e0 e1
+         (gsubst_go e0 x ev)
+         (if decide (x ≠ x1) then gsubst_go e1 x ev else None))
+       (if decide (x ≠ x2) then gsubst_go e2 x ev else None)
+  | Fork e => Fork <$> gsubst_go e x ev
+  | Loc l => None
+  | Alloc e => Alloc <$> gsubst_go e x ev
+  | Load e => Load <$> gsubst_go e x ev
+  | Store e1 e2 => gsubst_lift Store e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Cas e0 e1 e2 =>
+     gsubst_lift id (Cas e0 e1) e2
+       (gsubst_lift Cas e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
+       (gsubst_go e2 x ev)
+  end.
+Definition gsubst (e : expr) (x : string) (ev : expr) : expr :=
+  from_option e (gsubst_go e x ev).
+Arguments gsubst !_ _ _/.
+
 Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
@@ -10,6 +61,20 @@ Implicit Types Q : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
 Implicit Types ef : option expr.
 
+Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None → e = subst e x v.
+Proof.
+  induction e; simpl; unfold gsubst_lift; intros;
+    repeat (simplify_option_equality || case_match); f_equal; auto.
+Qed.
+Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v.
+Proof.
+  unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl;
+    last by apply gsubst_None.
+  revert e' He; induction e; simpl; unfold gsubst_lift; intros;
+    repeat (simplify_option_equality || case_match);
+    f_equal; auto using gsubst_None.
+Qed.
+
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
   wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
@@ -83,20 +148,25 @@ Qed.
 
 Lemma wp_rec E f x e1 e2 v Q :
   to_val e2 = Some v →
-  ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Q ⊑ wp E (App (Rec f x e1) e2) Q.
+  ▷ wp E (gsubst (gsubst e1 f (Rec f x e1)) x e2) Q ⊑ wp E (App (Rec f x e1) e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (App _ _)
+  intros <-%of_to_val; rewrite gsubst_correct (gsubst_correct _ _ (RecV _ _ _)).
+  rewrite -(wp_lift_pure_det_step (App _ _)
     (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
-    last by intros; inv_step; eauto.
+    intros; inv_step; eauto.
 Qed.
+Lemma wp_rec' E e1 f x erec e2 v Q :
+  e1 = Rec f x erec →
+  to_val e2 = Some v →
+  ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
+Proof. intros ->; apply wp_rec. Qed.
 
 Lemma wp_un_op E op l l' Q :
   un_op_eval op l = Some l' →
   ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
-    ?right_id //; last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Q :
@@ -104,54 +174,53 @@ Lemma wp_bin_op E op l1 l2 l' Q :
   ▷ Q (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Q.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
-    ?right_id //; last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If (Lit LitTrue) e1 e2) Q.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
-    ?right_id //; last by intros; inv_step; eauto.
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If (Lit LitFalse) e1 e2) Q.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
-    ?right_id //; last by intros; inv_step; eauto.
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v1 ⊑ wp E (Fst $ Pair e1 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v2 ⊑ wp E (Snd $ Pair e1 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e1 x1 v0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+  ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
-    ?right_id //; last by intros; inv_step; eauto.
+  intros <-%of_to_val; rewrite gsubst_correct.
+  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e2 x2 v0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+  ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
-    ?right_id //; last by intros; inv_step; eauto.
+  intros <-%of_to_val; rewrite gsubst_correct.
+  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 End lifting.

heap_lang/sugar.v

@@ -60,17 +60,20 @@ Implicit Types Q : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E x ef e v Q :
-  to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
-Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
+  to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
+Proof.
+  intros <-%of_to_val; rewrite -wp_rec ?to_of_val //.
+  by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty.
+Qed.
 
 Lemma wp_let E x e1 e2 v Q :
-  to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
+  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
 Proof. apply wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
 Proof.
   rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
-  by rewrite -wp_let //= ?subst_empty ?to_of_val.
+  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
 Qed.
 
 Lemma wp_le E (n1 n2 : nat) P Q :

heap_lang/tests.v

@@ -62,11 +62,11 @@ Module LiftingTests.
     λ: "x", if "x" ≤ '0 then '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Q :
-    (■ (n1 < n2) ∧ Q (LitV (pred n2))) ⊑ wp E (FindPred 'n2 'n1)%L Q.
+    (■ (n1 < n2) ∧ Q (LitV (n2 - 1))) ⊑ wp E (FindPred 'n2 'n1)%L Q.
   Proof.
     revert n1. apply löb_all_1=>n1.
     rewrite (commutative uPred_and (■ _)%I) associative; apply const_elim_r=>?.
-    rewrite -wp_rec //=.
+    rewrite -wp_rec' // =>-/=.
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Q _)).
     rewrite -!later_and; apply later_mono.
@@ -77,15 +77,15 @@ Module LiftingTests.
     - rewrite -wp_if_true.
       rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
-    - assert (n1 = pred n2) as -> by omega.
+    - assert (n1 = n2 - 1) as -> by omega.
       rewrite -wp_if_false.
       by rewrite -!later_intro -wp_value' // and_elim_r.
   Qed.
 
-  Lemma Pred_spec n E Q : ▷ Q (LitV (pred n)) ⊑ wp E (Pred 'n)%L Q.
+  Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
   Proof.
     rewrite -wp_lam //=.
-    rewrite -(wp_bindi (IfCtx _ _)).
+    rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_if_true.
       rewrite -!later_intro -wp_value' //=.

program_logic/auth.v

@@ -14,16 +14,12 @@ Section auth.
   (* TODO: Need this to be proven somewhere. *)
   (* FIXME ✓ binds too strong, I need parenthesis here. *)
   Hypothesis auth_valid :
-    forall a b, (✓(Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
-
-  (* FIXME how much would break if we had a global instance from ∅ to Inhabited? *)
-  Local Instance auth_inhabited : Inhabited A.
-  Proof. split. exact ∅. Qed.
+    forall a b, (✓ (Auth (Excl a) b) : iProp Λ (globalC Σ)) ⊑ (∃ b', a ≡ b ⋅ b').
 
   Definition auth_inv (γ : gname) : iProp Λ (globalC Σ) :=
-    (∃ a, own AuthI γ (●a) ★ φ a)%I.
-  Definition auth_own (γ : gname) (a : A) := own AuthI γ (◯a).
-  Definition auth_ctx (γ : gname) := inv N (auth_inv γ).
+    (∃ a, own AuthI γ (● a) ★ φ a)%I.
+  Definition auth_own (γ : gname) (a : A) : iProp Λ (globalC Σ) := own AuthI γ (◯ a).
+  Definition auth_ctx (γ : gname) : iProp Λ (globalC Σ) := inv N (auth_inv γ).
 
   Lemma auth_alloc a :
     ✓a → φ a ⊑ pvs N N (∃ γ, auth_ctx γ ∧ auth_own γ a).
@@ -58,30 +54,30 @@ Section auth.
     by rewrite sep_elim_l.
   Qed.
 
-  Context (L : LocalUpdate A) `{!LocalUpdateSpec L}.
-  Lemma auth_closing E a a' b γ :
-    L a = Some b → ✓(b ⋅ a') →
-    (▷φ (b ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
-      ⊑ pvs E E (▷auth_inv γ ★ auth_own γ b).
+  Lemma auth_closing E `{!LocalUpdate Lv L} a a' γ :
+    Lv a → ✓ (L a ⋅ a') →
+    (▷φ (L a ⋅ a') ★ own AuthI γ (● (a ⋅ a') ⋅ ◯ a))
+    ⊑ pvs E E (▷auth_inv γ ★ auth_own γ (L a)).
   Proof.
-    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (b ⋅ a')).
+    intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a ⋅ a')).
     rewrite later_sep [(_ ★ ▷φ _)%I]commutative -associative.
     rewrite -pvs_frame_l. apply sep_mono; first done.
-    rewrite -later_intro -own_op. apply own_update.
-    by apply (auth_local_update L).
+    rewrite -later_intro -own_op.
+    by apply own_update, (auth_local_update_l L).
   Qed.
 
   (* FIXME it should be enough to assume that A is all-timeless. *)
-  (* Notice how the user has t prove that `L a` equals `Some b` at
-     *all* step-indices, and similar that `b⋅a'` is valid at all
+  (* Notice how the user has to prove that `b⋅a'` is valid at all
      step-indices. This is because the side-conditions for frame-preserving
      updates have to be shown on the meta-level. *)
-  Lemma auth_pvs `{!∀ a : authRA A, Timeless a} E P (Q : A → iProp Λ (globalC Σ)) γ a :
+  (* TODO The form of the lemma, with a very specific post-condition, is not ideal. *)
+  Lemma auth_pvs `{!∀ a : authRA A, Timeless a}`{!LocalUpdate Lv L}
+        E P (Q : A → iProp Λ (globalC Σ)) γ a :
     nclose N ⊆ E →
     (auth_ctx γ ★ auth_own γ a ★ (∀ a', ▷φ (a ⋅ a') -★
           pvs (E ∖ nclose N) (E ∖ nclose N)
-            (∃ b, L a = Some b ★ ■(✓(b⋅a')) ★ ▷φ (b ⋅ a') ★ Q b)))
-      ⊑ pvs E E (∃ b, auth_own γ b ★ Q b).
+            (■(Lv a ∧ ✓(L a⋅a')) ★ ▷φ (L a ⋅ a') ★ Q (L a))))
+      ⊑ pvs E E (auth_own γ (L a) ★ Q (L a)).
   Proof.
     rewrite /auth_ctx=>HN.
     rewrite -[pvs E E _]pvs_open_close; last eassumption.
@@ -90,14 +86,11 @@ Section auth.
     rewrite auth_opened later_exist sep_exist_r. apply exist_elim=>a'.
     rewrite (forall_elim a'). rewrite [(▷_ ★ _)%I]commutative later_sep.
     rewrite associative wand_elim_l pvs_frame_r. apply pvs_strip_pvs.
-    rewrite sep_exist_r. apply exist_elim=>b.
     rewrite [(▷own _ _ _)%I]pvs_timeless pvs_frame_l. apply pvs_strip_pvs.
-    rewrite -!associative. apply const_elim_sep_l=>HL.
-    apply const_elim_sep_l=>Hv.
-    rewrite associative [(_ ★ Q b)%I]commutative -associative auth_closing //; [].
-    erewrite pvs_frame_l. apply pvs_mono. rewrite -(exist_intro b).
-    rewrite associative [(_ ★ Q b)%I]commutative associative.
+    rewrite -!associative. apply const_elim_sep_l=>-[HL Hv].
+    rewrite associative [(_ ★ Q _)%I]commutative -associative auth_closing //; [].
+    erewrite pvs_frame_l. apply pvs_mono.
+    rewrite associative [(_ ★ Q _)%I]commutative associative.
     apply sep_mono; last done. by rewrite commutative.
   Qed.
 End auth.
-