Merge branch 'ralf/tc-weakestpre' into 'master'

don't tie bi.weakestpre to program_logic.language (full TC approach)

Closes #408

See merge request iris/iris!656

CHANGELOG.md

@@ -46,6 +46,11 @@ Coq 8.11 is no longer supported in this version of Iris.
   `big_sep{L,L2,M,M2,S}_intro`, and `big_orL_lookup` → `big_orL_intro`.
 * Rename `bupd_forall` to `bupd_plain_forall`, and add
   `{bupd,fupd}_{and,or,forall,exist}`.
+* Decouple `Wp` and `Twp` typeclasses from the `program_logic.language`
+  interface. The typeclasses are now parameterized over an expression and a
+  value type, instead of a language. This requires extra type annotations or
+  explicit coercions in a few cases, in particular `WP v {{ Φ }}` must now be
+  written `WP (of_val v) {{ Φ }}`.
 
 **Changes in `proofmode`:**
 

iris/bi/weakestpre.v

+(** Shared notation file for WP connectives. *)
+
 From stdpp Require Export coPset.
 From iris.bi Require Import interface derived_connectives.
-From iris.program_logic Require Import language.
 From iris.prelude Require Import options.
 
+Declare Scope expr_scope.
+Delimit Scope expr_scope with E.
+
+Declare Scope val_scope.
+Delimit Scope val_scope with V.
+
 Inductive stuckness := NotStuck | MaybeStuck.
 
 Definition stuckness_leb (s1 s2 : stuckness) : bool :=
@@ -14,9 +21,6 @@ Global Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
 Global Instance stuckness_le_po : PreOrder stuckness_le.
 Proof. split; by repeat intros []. Qed.
 
-Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
-  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
-
 (** Weakest preconditions [WP e @ s ; E {{ Φ }}] have an additional argument [s]
 of arbitrary type [A], that can be chosen by the one instantiating the [Wp] type
 class. This argument can be used for e.g. the stuckness bit (as in Iris) or
@@ -28,15 +32,15 @@ and [s] to be [NotStuck] or [MaybeStuck].  This will fail to typecheck if [A] is
 not [stuckness].  If we ever want to use the notation [WP e @ E {{ Φ }}] with a
 different [A], the plan is to generalize the notation to use [Inhabited] instead
 to pick a default value depending on [A]. *)
-Class Wp (Λ : language) (PROP A : Type) :=
-  wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Global Arguments wp {_ _ _ _} _ _ _%E _%I.
-Global Instance: Params (@wp) 7 := {}.
-
-Class Twp (Λ : language) (PROP A : Type) :=
-  twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
-Global Arguments twp {_ _ _ _} _ _ _%E _%I.
-Global Instance: Params (@twp) 7 := {}.
+Class Wp (PROP EXPR VAL A : Type) :=
+  wp : A → coPset → EXPR → (VAL → PROP) → PROP.
+Global Arguments wp {_ _ _ _ _} _ _ _%E _%I.
+Global Instance: Params (@wp) 8 := {}.
+
+Class Twp (PROP EXPR VAL A : Type) :=
+  twp : A → coPset → EXPR → (VAL → PROP) → PROP.
+Global Arguments twp {_ _ _ _ _} _ _ _%E _%I.
+Global Instance: Params (@twp) 8 := {}.
 
 (** Notations for partial weakest preconditions *)
 (** Notations without binder -- only parsing because they overlap with the

iris/program_logic/language.v

 From iris.algebra Require Export ofe.
+From iris.bi Require Export weakestpre.
 From iris.prelude Require Import options.
 
 Section language_mixin.
@@ -28,12 +29,7 @@ Structure language := Language {
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 
-Declare Scope expr_scope.
-Delimit Scope expr_scope with E.
 Bind Scope expr_scope with expr.
-
-Declare Scope val_scope.
-Delimit Scope val_scope with V.
 Bind Scope val_scope with val.
 
 Global Arguments Language {_ _ _ _ _ _ _} _.
@@ -63,6 +59,9 @@ Proof. constructor; naive_solver. Qed.
 
 Inductive atomicity := StronglyAtomic | WeaklyAtomic.
 
+Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.

iris/program_logic/total_weakestpre.v

@@ -57,7 +57,7 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{!irisGS Λ Σ} : Twp Λ (iProp Σ) stuckness
+Definition twp_def `{!irisGS Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
   := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
 Definition twp' := twp_aux.(unseal).

iris/program_logic/weakestpre.v

@@ -73,7 +73,7 @@ Proof.
   - by rewrite -IH.
 Qed.
 
-Definition wp_def `{!irisGS Λ Σ} : Wp Λ (iProp Σ) stuckness :=
+Definition wp_def `{!irisGS Λ Σ} : Wp (iProp Σ) (expr Λ) (val Λ) stuckness :=
   λ s : stuckness, fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
 Definition wp' := wp_aux.(unseal).

tests/heap_lang.v

@@ -176,9 +176,9 @@ Section tests.
   Proof. Fail wp_store. Abort.
 
   Check "(t)wp_bind_fail".
-  Lemma wp_bind_fail : ⊢ WP #() {{ v, True }}.
+  Lemma wp_bind_fail : ⊢ WP of_val #() {{ v, True }}.
   Proof. Fail wp_bind (!_)%E. Abort.
-  Lemma twp_bind_fail : ⊢ WP #() [{ v, True }].
+  Lemma twp_bind_fail : ⊢ WP of_val #() [{ v, True }].
   Proof. Fail wp_bind (!_)%E. Abort.
 
   Lemma wp_apply_evar e P :
@@ -186,10 +186,10 @@ Section tests.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
   Lemma wp_pures_val (b : bool) :
-    ⊢ WP #b {{ _, True }}.
+    ⊢ WP of_val #b {{ _, True }}.
   Proof. wp_pures. done. Qed.
   Lemma twp_pures_val (b : bool) :
-    ⊢ WP #b [{ _, True }].
+    ⊢ WP of_val #b [{ _, True }].
   Proof. wp_pures. done. Qed.
 
   Lemma wp_cmpxchg l v :
@@ -315,14 +315,14 @@ Section tests.
 
   Check "test_wp_finish_fupd".
   Lemma test_wp_finish_fupd (v : val) :
-    ⊢ WP v {{ v, |={⊤}=> True }}.
+    ⊢ WP of_val v {{ v, |={⊤}=> True }}.
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.
 
   Check "test_twp_finish_fupd".
   Lemma test_twp_finish_fupd (v : val) :
-    ⊢ WP v [{ v, |={⊤}=> True }].
+    ⊢ WP of_val v [{ v, |={⊤}=> True }].
   Proof.
     wp_pures. Show. (* No second fupd was added. *)
   Abort.

tests/one_shot.v

@@ -46,7 +46,9 @@ Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
 Lemma wp_one_shot (Φ : val → iProp Σ) :
   (∀ f1 f2 : val,
     (∀ n : Z, □ WP f1 #n {{ w, ⌜w = #true⌝ ∨ ⌜w = #false⌝ }}) ∗
-    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (of_val g) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+      (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+         so that we can add a type annotation at the [g] binder here. *)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.

tests/one_shot_once.v

@@ -60,7 +60,9 @@ Qed.
 Lemma wp_one_shot (Φ : val → iProp Σ) :
   (∀ (f1 f2 : val) (T : iProp Σ), T ∗
     □ (∀ n : Z, T -∗ WP f1 #n {{ w, True }}) ∗
-    □ WP f2 #() {{ g, □ WP g #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+    □ WP f2 #() {{ g, □ WP (of_val g) #() {{ _, True }} }} -∗ Φ (f1,f2)%V)
+      (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+         so that we can add a type annotation at the [g] binder here. *)
   ⊢ WP one_shot_example #() {{ Φ }}.
 Proof.
   iIntros "Hf /=". pose proof (nroot .@ "N") as N.