tests/proofmode.v

@@ -44,10 +44,10 @@ Proof.
   (* To test destruct: can also be part of the intro-pattern *)
   iDestruct "foo" as "[_ meh]".
   repeat iSplit; [|by iLeft|iIntros "#[]"].
-  iFrame "H2".
+  iFrame "H2". (* also simplifies the [∧ False] and [∨ False] *)
   (* split takes a list of hypotheses just for the LHS *)
   iSplitL "H3".
-  - iFrame "H3". iRight. auto.
+  - by iFrame "H3".
   - iSplitL "HQ"; first iAssumption. by iSplitL "H1".
 Qed.
 
@@ -654,6 +654,15 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
 Lemma test_iFrame_conjunction_2 P Q :
   P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
 Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Check "test_iFrame_conjunction_3".
+Lemma test_iFrame_conjunction_3 P Q `{!Absorbing Q} :
+  P -∗ Q -∗ ((P ∗ False) ∧ Q).
+Proof.
+  iIntros "HP HQ".
+  iFrame "HP".
+  (* [iFrame] should simplify [False ∧ Q] to just [False]. *)
+  Show.
+Abort.
 
 Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
 Proof. iIntros "H1 H2". by iFrame "H1". Qed.
@@ -707,6 +716,16 @@ Proof.
   is not simplified to [emp]. *)
   iExists 0. auto.
 Qed.
+Check "test_iFrame_or_3".
+Lemma test_iFrame_or_3 P1 P2 P3 :
+  P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ (False ∗ P3)).
+Proof.
+  iIntros "($ & $ & $)".
+  Show. (* After framing [P3], the disjunction becomes [⌜x = 0⌝ ∨ False].
+  The simplification of disjunctions by [iFrame] will now get rid of the
+  [∨ False], to just [⌜x = 0⌝] *)
+  by iExists 0.
+Qed.
 Check "test_iFrame_or_affine_1".
 Lemma test_iFrame_or_affine_1 `{!BiAffine PROP} P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∗ ⌜x = 0⌝) ∨ P3).

tests/proofmode_iris.ref

@@ -134,6 +134,18 @@ The command has indeed failed with message:
 Tactic failure: iInv: invariant nroot not found.
 The command has indeed failed with message:
 Tactic failure: iInv: invariant "H2" not found.
+"test_iInv_accessor_variable"
+     : string
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
+The command has indeed failed with message:
+The command has not failed!
+The command has indeed failed with message:
+Tactic failure: iExistDestruct: cannot destruct (Φ H1).
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
+The command has indeed failed with message:
+Tactic failure: Missing intro pattern for accessor variable.
 "test_frac_split_combine"
      : string
 1 goal
@@ -201,6 +213,23 @@ goal 2 is:
  "Hlc2" : £ m
  --------------------------------------∗
  £ m
+"test_iCombine_mapsto_no_beta"
+     : string
+1 goal
+  
+  hlc : has_lc
+  Σ : gFunctors
+  invGS_gen0 : invGS_gen hlc Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  ghost_varG0 : ghost_varG Σ nat
+  l : gname
+  v : nat
+  q1, q2 : Qp
+  ============================
+  "H" : ghost_var l (q1 + q2) v
+  --------------------------------------∗
+  ghost_var l (q1 + q2) v
 "test_iInv"
      : string
 1 goal

tests/proofmode_iris.v

 From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
-From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants ghost_var.
 From iris.prelude Require Import options.
 
 Unset Mangle Names.
+Set Default Proof Using "Type*".
 
 Section base_logic_tests.
   Context {M : ucmra}.
@@ -233,6 +234,37 @@ Section iris_tests.
     eauto.
   Qed.
 
+  (* Test [iInv] with accessor variables. *)
+  Section iInv_accessor_variables.
+    (** We consider a kind of invariant that does not take a proposition, but
+    a predicate. The invariant accessor gives the predicate existentially. *)
+    Context (INV : (bool → iProp Σ) → iProp Σ).
+    Context `{!∀ Φ,
+      IntoAcc (INV Φ) True True (fupd ⊤ ∅) (fupd ∅ ⊤) Φ Φ (λ b, Some (INV Φ))}.
+
+    Check "test_iInv_accessor_variable".
+    Lemma test_iInv_accessor_variable Φ : INV Φ ={⊤}=∗ INV Φ.
+    Proof.
+      iIntros "HINV".
+      (* There are 4 variants of [iInv] that we have to test *)
+      (* No selection pattern, no closing view shift *)
+      Fail iInv "HINV" as "HINVinner".
+      iInv "HINV" as (b) "HINVinner"; rename b into b_exists. Undo.
+      (* Both sel.pattern and closing view shift *)
+      (* FIXME this one is broken: no proper error message without a pattern for
+      the accessor variable, and an error when the pattern is given *)
+      Fail Fail iInv "HINV" with "[//]" as "HINVinner" "Hclose".
+      Fail iInv "HINV" with "[//]" as (b) "HINVinner" "Hclose"; rename b into b_exists.
+      (* Sel.pattern but no closing view shift *)
+      Fail iInv "HINV" with "[//]" as "HINVinner".
+      iInv "HINV" with "[//]" as (b) "HINVinner"; rename b into b_exists. Undo.
+      (* Closing view shift, no selection pattern *)
+      Fail iInv "HINV" as "HINVinner" "Hclose".
+      iInv "HINV" as (b) "HINVinner" "Hclose"; rename b into b_exists.
+      by iApply "Hclose".
+    Qed.
+  End iInv_accessor_variables.
+
   Theorem test_iApply_inG `{!inG Σ A} γ (x x' : A) :
     x' ≼ x →
     own γ x -∗ own γ x'.
@@ -263,6 +295,14 @@ Section iris_tests.
   Check "lc_iSplit_lc".
   Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
   Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
+
+  (** Make sure [iCombine] doesn't leave behind beta redexes. *)
+  Check "test_iCombine_mapsto_no_beta".
+  Lemma test_iCombine_ghost_var_no_beta `{!ghost_varG Σ nat} l (v : nat) q1 q2 :
+    ghost_var l q1 v -∗ ghost_var l q2 v -∗ ghost_var l (q1+q2) v.
+  Proof.
+    iIntros "H1 H2". iCombine "H1 H2" as "H". Show. done.
+  Qed.
 End iris_tests.
 
 Section monpred_tests.