Merge branch 'master' into gen_proofmode

opam

@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.7.dev" & < "8.8~" }
-  "coq-stdpp" { (= "dev.2017-11-12.2") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
 ]

theories/algebra/ofe.v

@@ -616,9 +616,9 @@ Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
 Instance: Params (@ccompose) 3.
 Infix "◎" := ccompose (at level 40, left associativity).
-Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
-  f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2.
-Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
+Global Instance ccompose_ne {A B C} :
+  NonExpansive2 (@ccompose A B C).
+Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
 
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
@@ -1057,6 +1057,7 @@ Record later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
+Instance: Params (@Next) 1.
 
 Section later.
   Context {A : ofeT}.
@@ -1096,8 +1097,7 @@ Section later.
 
   (* f is contractive iff it can factor into `Next` and a non-expansive function. *)
   Lemma contractive_alt {B : ofeT} (f : A → B) :
-    Contractive f ↔ ∃ g : later A → B,
-      (NonExpansive g) ∧ (∀ x, f x ≡ g (Next x)).
+    Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
   Proof.
     split.
     - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.

theories/algebra/sts.v

@@ -79,7 +79,7 @@ Qed.
 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
 Proof.
   intros S1 S2 HS T1 T2 HT. rewrite /up_set.
-  f_equiv=> // s1 s2 Hs. by apply up_preserving.
+  f_equiv=> // s1 s2. by apply up_preserving.
 Qed.
 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.

theories/base_logic/lib/saved_prop.v

 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
 From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
-  saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
-Definition savedPropΣ (F : cFunctor) : gFunctors :=
-  #[ GFunctor (agreeRF (▶ F)) ].
+(* "Saved anything" -- this can give you saved propositions, saved predicates,
+   saved whatever-you-like. *)
 
-Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
+Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
+  saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+  #[ GFunctor (agreeRF F) ].
+
+Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
+  subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
-Definition saved_prop_own `{savedPropG Σ F}
+Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
-  own γ (to_agree $ Next (cFunctor_map F (iProp_fold, iProp_unfold) x)).
-Typeclasses Opaque saved_prop_own.
-Instance: Params (@saved_prop_own) 3.
+  own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
+Typeclasses Opaque saved_anything_own.
+Instance: Params (@saved_anything_own) 4.
 
-Section saved_prop.
-  Context `{savedPropG Σ F}.
+Section saved_anything.
+  Context `{savedAnythingG Σ F}.
   Implicit Types x y : F (iProp Σ).
   Implicit Types γ : gname.
 
-  Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
-  Proof. rewrite /saved_prop_own; apply _. Qed.
+  Global Instance saved_anything_persistent γ x :
+    Persistent (saved_anything_own γ x).
+  Proof. rewrite /saved_anything_own; apply _. Qed.
+
+  Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
+  Proof. solve_proper. Qed.
+  Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
+  Proof. solve_proper. Qed.
 
-  Lemma saved_prop_alloc_strong x (G : gset gname) :
-    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc_strong x (G : gset gname) :
+    (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.
 
-  Lemma saved_prop_alloc x : (|==> ∃ γ, saved_prop_own γ x)%I.
+  Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
   Proof. by apply own_alloc. Qed.
 
-  Lemma saved_prop_agree γ x y :
-    saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
+  Lemma saved_anything_agree γ x y :
+    saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
   Proof.
-    apply wand_intro_r.
-    rewrite /saved_prop_own -own_op own_valid agree_validI agree_equivI.
-    rewrite later_equivI.
+    iIntros "Hx Hy". rewrite /saved_anything_own.
+    iDestruct (own_valid_2 with "Hx Hy") as "Hv".
+    rewrite agree_validI agree_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
+    rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
   Qed.
-End saved_prop.
+End saved_anything.
+
+(** Provide specialized versions of this for convenience. **)
+
+(* Saved propositions. *)
+Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
+Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
+
+Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+  saved_anything_own (F := ▶ ∙) γ (Next P).
+
+Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+  Contractive (saved_prop_own γ).
+Proof. solve_contractive. Qed.
+
+Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
+  (|==> ∃ γ, saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
+  saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
+Proof.
+  iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
+Qed.
+
+(* Saved predicates. *)
+Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
+Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
+
+Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+  saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
+
+Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
+  Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
+Proof.
+  solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
+Qed.
+
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) :
+  (|==> ∃ γ, saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+(* We put the `x` on the outside to make this lemma easier to apply. *)
+Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+  saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
+Proof.
+  iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
+  iDestruct (ofe_funC_equivI (CofeMor Next ∘ Φ) (CofeMor Next ∘ Ψ)) as "[FE _]".
+  simpl. iApply ("FE" with "[-]").
+  iApply (saved_anything_agree with "HΦ HΨ").
+Qed.

theories/base_logic/lib/wsat.v

@@ -22,6 +22,7 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (◯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
+Instance: Params (@invariant_unfold) 1.
 Instance: Params (@ownI) 3.
 
 Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=

theories/heap_lang/lib/spin_lock.v

@@ -49,7 +49,7 @@ Section proof.
     {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
   Proof.
     iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
-    wp_seq. wp_alloc l as "Hl".
+    wp_lam. wp_alloc l as "Hl".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
     iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
     { iIntros "!>". iExists false. by iFrame. }

theories/proofmode/base.v

@@ -83,3 +83,7 @@ Qed.
 
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
+
+Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+  match mx with Some x => f x | None => None end.
+Arguments option_bind _ _ _ !_ /.

theories/proofmode/coq_tactics.v

@@ -58,7 +58,7 @@ Definition envs_lookup_delete {PROP} (i : ident)
   let (Γp,Γs) := Δ in
   match env_lookup_delete i Γp with
   | Some (P,Γp') => Some (true, P, Envs Γp' Γs)
-  | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
+  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
   end.
 
 Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : bool)
@@ -66,9 +66,9 @@ Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : b
   match js with
   | [] => Some (true, [], Δ)
   | j :: js =>
-     '(p,P,Δ') ← envs_lookup_delete j Δ;
-     let Δ' := if p then (if remove_persistent then Δ' else Δ) else Δ' in
-     '(q,Hs,Δ'') ← envs_lookup_delete_list js remove_persistent Δ';
+     ''(p,P,Δ') ← envs_lookup_delete j Δ;
+     let Δ' := if p : bool then (if remove_persistent then Δ' else Δ) else Δ' in
+     ''(q,Hs,Δ'') ← envs_lookup_delete_list js remove_persistent Δ';
      Some (p && q, P :: Hs, Δ'')
   end.
 
@@ -112,16 +112,15 @@ Fixpoint envs_split_go {PROP}
   match js with
   | [] => Some (Δ1, Δ2)
   | j :: js =>
-     '(p,P,Δ1') ← envs_lookup_delete j Δ1;
-     if p then envs_split_go js Δ1 Δ2 else
+     ''(p,P,Δ1') ← envs_lookup_delete j Δ1;
+     if p : bool then envs_split_go js Δ1 Δ2 else
      envs_split_go js Δ1' (envs_snoc Δ2 false j P)
   end.
 (* if [d = Right] then [result = (remaining hyps, hyps named js)] and
    if [d = Left] then [result = (hyps named js, remaining hyps)] *)
-
 Definition envs_split {PROP} (d : direction)
     (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
-  '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
+  ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
 (* Coq versions of the tactics *)
@@ -328,7 +327,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_singleton_sound'//. Q
 
 Lemma envs_lookup_envs_clear_spatial Δ j :
   envs_lookup j (envs_clear_spatial Δ)
-  = '(p,P) ← envs_lookup j Δ; if p then Some (p,P) else None.
+  = ''(p,P) ← envs_lookup j Δ; if p : bool then Some (p,P) else None.
 Proof.
   rewrite /envs_lookup /envs_clear_spatial.
   destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
@@ -400,7 +399,7 @@ Proof.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
   { intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
-  destruct d; simplify_eq; solve_sep_entails.
+  destruct d; simplify_eq/=; solve_sep_entails.
 Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
@@ -734,7 +733,7 @@ Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand q false R P1 P2 →
   ElimModal P1' P1 Q Q →
-  ('(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
+  (''(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
   envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.

theories/proofmode/environments.v

@@ -17,11 +17,9 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   end.
 
 Module env_notations.
-  Notation "x ← y ; z" := (match y with Some x => z | None => None end).
-  Notation "' ( x1 , x2 ) ← y ; z" :=
-    (match y with Some (x1,x2) => z | None => None end).
-  Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
-    (match y with Some (x1,x2,x3) => z | None => None end).
+  Notation "y ≫= f" := (option_bind f y).
+  Notation "x ← y ; z" := (y ≫= λ x, z).
+  Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
 End env_notations.
 Import env_notations.
@@ -68,7 +66,7 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
   | Enil => None
   | Esnoc Γ j x =>
      if ident_beq i j then Some (x,Γ)
-     else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
+     else ''(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
 Definition env_is_singleton {A} (Γ : env A) : bool :=
@@ -101,6 +99,8 @@ Ltac simplify :=
   | _ => progress simplify_eq/=
   | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
   | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
+  | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
+  | |- context [option_bind _ ?x] => destruct x eqn:?
   | _ => case_match
   end.
 

theories/proofmode/intro_patterns.v

@@ -39,9 +39,9 @@ Fixpoint close_list (k : stack)
   | SList :: k => Some (SPat (IList (ps :: pss)) :: k)
   | SPat pat :: k => close_list k (pat :: ps) pss
   | SAlwaysElim :: k =>
-     '(p,ps) ← maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
+     ''(p,ps) ← maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
   | SModalElim :: k =>
-     '(p,ps) ← maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
+     ''(p,ps) ← maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
   | SBar :: k => close_list k [] (ps :: pss)
   | _ => None
   end.
@@ -114,8 +114,8 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
   match k with
   | [] => Some ps
   | SPat pat :: k => close k (pat :: ps)
-  | SAlwaysElim :: k => '(p,ps) ← maybe2 (::) ps; close k (IAlwaysElim p :: ps)
-  | SModalElim :: k => '(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
+  | SAlwaysElim :: k => ''(p,ps) ← maybe2 (::) ps; close k (IAlwaysElim p :: ps)
+  | SModalElim :: k => ''(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
   | _ => None
   end.
 

theories/proofmode/tactics.v

@@ -8,6 +8,7 @@ Set Default Proof Using "Type".
 Export ident.
 
 Declare Reduction env_cbv := cbv [
+  option_bind
   beq ascii_beq string_beq positive_beq ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_persistent env_spatial env_spatial_is_nil envs_dom