Add class `HasLcIf` so that it becomes easier to write generic adequacy lemmas.

iris/base_logic/lib/fancy_updates.v

@@ -44,15 +44,15 @@ Definition invΣ : gFunctors :=
 Global Instance subG_invΣ {Σ} : subG invΣ Σ → invGpreS Σ.
 Proof. solve_inG. Qed.
 
-(** [HasLc] asserts that the fancy update is defined with support for later credits. *)
-Class HasLc (Σ : gFunctors) `{!invGS Σ} :=
-  { has_credits : invGS_use_credits = true }.
-Global Hint Mode HasLc - - : typeclass_instances.
-(** [HasNoLc] asserts that the fancy update is defined without support for later credits,
-    but in turn supports the plainly interaction laws [BiFUpdPlainly]. *)
-Class HasNoLc (Σ : gFunctors) `{!invGS Σ} :=
-  { has_no_credits : invGS_use_credits = false }.
-Global Hint Mode HasNoLc - - : typeclass_instances.
+(** [HasLc] asserts that the fancy update is defined with support for later
+credits, and [HasNoLc] asserts that the fancy update is defined without support
+for later credits, but in turn supports the plainly interaction laws
+[BiFUpdPlainly]. *)
+Class HasLcIf (Σ : gFunctors) (b : bool) `{!invGS Σ} :=
+  { has_credits : invGS_use_credits = b }.
+Global Hint Mode HasLcIf - - - : typeclass_instances.
+Notation HasLc Σ := (HasLcIf Σ true).
+Notation HasNoLc Σ := (HasLcIf Σ false).
 
 Local Definition uPred_fupd_def `{!invGS Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   wsat ∗ ownE E1 -∗ le_upd_if invGS_use_credits (◇ (wsat ∗ ownE E2 ∗ P)).
@@ -93,7 +93,7 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_unseal. by iIntros (E P) ">? [$ $] !> !>".
 Global Instance uPred_bi_fupd_plainly_no_lc `{!invGS Σ, !HasNoLc Σ} :
   BiFUpdPlainly (uPredI (iResUR Σ)).
 Proof.
-  split; rewrite uPred_fupd_unseal /uPred_fupd_def has_no_credits.
+  split; rewrite uPred_fupd_unseal /uPred_fupd_def has_credits.
   - iIntros (E P) "H [Hw HE]".
     iAssert (◇ ■ P)%I as "#>HP".
     { by iMod ("H" with "[$]") as "(_ & _ & HP)". }
@@ -226,7 +226,7 @@ Qed.
   on whether to use credits or not. *)
 Lemma step_fupdN_soundness_gen `{!invGpreS Σ} (φ : Prop)
     (use_credits : bool) (n m : nat) :
-  (∀ `{Hinv : invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+  (∀ `{Hinv : invGS Σ} `{Hc : !HasLcIf Σ use_credits},
     (if use_credits then £ m else True) ={⊤,∅}=∗ |={∅}▷=>^n ⌜φ⌝) →
   φ.
 Proof.

iris/program_logic/adequacy.v

@@ -129,7 +129,7 @@ End adequacy.
 
 Local Lemma wp_progress_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} es σ1 n κs t2 σ2 e2
         (num_laters_per_step : nat → nat)  :
-    (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+  (∀ `{Hinv : !invGS Σ} `{Hc : !HasLcIf Σ use_credits},
     ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
@@ -147,7 +147,7 @@ Proof.
   iIntros (Hwp ??).
   eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n) 0).
   iIntros (Hinv Hc) "_".
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)"; first done.
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
   iMod (@wptp_progress _ _
        (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
@@ -165,7 +165,7 @@ Qed.
 Lemma wp_strong_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s es σ1 n κs t2 σ2 φ
         (num_laters_per_step : nat → nat) :
   (* WP *)
-  (∀ `{Hinv : !invGS Σ} `{Hc : if use_credits then HasLc Σ else HasNoLc Σ},
+  (∀ `{Hinv : !invGS Σ} `{Hc : !HasLcIf Σ use_credits},
       ⊢ |={⊤}=> ∃
          (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
          (Φs : list (val Λ → iProp Σ))
@@ -204,7 +204,7 @@ Proof.
   iIntros (Hwp ?).
   eapply (step_fupdN_soundness_gen _ use_credits (steps_sum num_laters_per_step 0 n) 0).
   iIntros (Hinv Hc) "_". (* no credit generation for now *)
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iDestruct (big_sepL2_length with "Hwp") as %Hlen1.
   iMod (@wptp_strong_adequacy _ _
        (IrisG _ _ Hinv stateI fork_post num_laters_per_step state_interp_mono) _ []
@@ -226,7 +226,7 @@ Proof.
   eapply (wp_progress_gen use_credits);
     [ done | clear stateI Φ fork_post state_interp_mono Hlen1 Hlen3 | done|done].
   iIntros (??).
-  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)"; first done.
+  iMod Hwp as (stateI Φ fork_post state_interp_mono) "(Hσ & Hwp & Hφ)".
   iModIntro. iExists _, _, _, _. iFrame.
 Qed.
 
@@ -292,7 +292,7 @@ this specific proof term.
 *)
 (** Again, we first prove a lemma generic over the usage of credits. *)
 Lemma wp_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e σ φ :
-  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
+  (∀ `{Hinv : !invGS Σ} `{Hc : !HasLcIf Σ use_credits} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → iProp Σ)
          (fork_post : val Λ → iProp Σ),
@@ -305,7 +305,7 @@ Lemma wp_adequacy_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e σ φ :
 Proof.
   intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
   eapply (wp_strong_adequacy_gen use_credits Σ _); [ | done]=> ??.
-  iMod Hwp as (stateI fork_post) "[Hσ Hwp]"; first done.
+  iMod Hwp as (stateI fork_post) "[Hσ Hwp]".
   iExists (λ σ _ κs _, stateI σ κs), [(λ v, ⌜φ v⌝%I)], fork_post, _ => /=.
   iIntros "{$Hσ $Hwp} !>" (e2 t2' -> ? ?) "_ H _".
   iApply fupd_mask_intro_discard; [done|]. iSplit; [|done].
@@ -323,7 +323,7 @@ Global Arguments wp_adequacy_no_lc _ _ {_}.
 
 
 Lemma wp_invariance_gen (use_credits : bool) Σ Λ `{!invGpreS Σ} s e1 σ1 t2 σ2 φ :
-  (∀ `{Hinv : !invGS Σ} `{!if use_credits then HasLc Σ else HasNoLc Σ} κs,
+  (∀ `{Hinv : !invGS Σ} `{Hc : !HasLcIf Σ use_credits} κs,
      ⊢ |={⊤}=> ∃
          (stateI : state Λ → list (observation Λ) → nat → iProp Σ)
          (fork_post : val Λ → iProp Σ),