proofmode_monpred.v 6.66 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1
From iris.proofmode Require Import tactics monpred.
2
From iris.base_logic.lib Require Import invariants.
3
Set Ltac Backtrace.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
4 5

Section tests.
6
  Context {I : biIndex} {PROP : sbi}.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
7 8 9 10
  Local Notation monPred := (monPred I PROP).
  Local Notation monPredI := (monPredI I PROP).
  Local Notation monPredSI := (monPredSI I PROP).
  Implicit Types P Q R : monPred.
11
  Implicit Types 𝓟 𝓠 𝓡 : PROP.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
  Implicit Types i j : I.

  Lemma test0 P : P - P.
  Proof. iIntros "$". Qed.

  Lemma test_iStartProof_1 P : P - P.
  Proof. iStartProof. iStartProof. iIntros "$". Qed.
  Lemma test_iStartProof_2 P : P - P.
  Proof. iStartProof monPred. iStartProof monPredI. iIntros "$". Qed.
  Lemma test_iStartProof_3 P : P - P.
  Proof. iStartProof monPredI. iStartProof monPredSI. iIntros "$". Qed.
  Lemma test_iStartProof_4 P : P - P.
  Proof. iStartProof monPredSI. iStartProof monPred. iIntros "$". Qed.
  Lemma test_iStartProof_5 P : P - P.
  Proof. iStartProof PROP. iIntros (i) "$". Qed.
  Lemma test_iStartProof_6 P : P  P.
  Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
  Lemma test_iStartProof_7 P : ((P  P)%I : monPredI).
  Proof. iStartProof PROP. done. Qed.

32 33
  Lemma test_intowand_1 P Q : (P - Q) - P - Q.
  Proof.
34 35
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
  Qed.
  Lemma test_intowand_2 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "[HP //]"). done.
  Qed.
  Lemma test_intowand_3 P Q : (P - Q) - P - Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
  Lemma test_intowand_4 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP". by iApply "HW".
  Qed.
  Lemma test_intowand_5 P Q : (P - Q) -  P -  Q.
  Proof.
    iStartProof PROP. iIntros (i) "HW". iIntros (j ->) "HP".
    iSpecialize ("HW" with "HP"). done.
  Qed.
56

57 58
  Lemma test_apply_in_elim (P : monPredI) (i : I) : monPred_in i -  P i   P.
  Proof. iIntros. by iApply monPred_in_elim. Qed.
59 60 61 62 63 64 65 66 67

  Lemma test_iStartProof_forall_1 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof PROP. iIntros (n i) "$".
  Qed.
  Lemma test_iStartProof_forall_2 (Φ : nat  monPredI) :  n, Φ n - Φ n.
  Proof.
    iStartProof. iIntros (n) "$".
  Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
68 69 70 71 72

  Lemma test_embed_wand (P Q : PROP) : (P - Q) - P - Q : monPred.
  Proof.
    iIntros "H HP". by iApply "H".
  Qed.
73

74
  Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P  Q).
75 76
  Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.

77
  Lemma test_objectively_absorbing P Q R `{!Absorbing P} :
78
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
79
  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
80

81
  Lemma test_objectively_affine P Q R `{!Affine R} :
82
    <obj> emp - <obj> P - <obj> Q - R - <obj> (P  Q).
83
  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
84

85 86 87 88
  Lemma test_iModIntro_embed P `{!Affine Q} 𝓟 𝓠 :
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -  𝓟  𝓠 .
  Proof. iIntros "#H1 _ H2 H3". iAlways. iFrame. Qed.

89
  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
90
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -   i, 𝓟  𝓠  Q i .
91
  Proof. iIntros "#H1 H2 H3 H4". iAlways. Show. iFrame. Qed.
92

93 94 95 96
  Lemma test_iModIntro_embed_nested P 𝓟 𝓠 :
     P - ⎡◇ 𝓟⎤ - ⎡◇ 𝓠⎤ -   (𝓟  𝓠) .
  Proof. iIntros "#H1 H2 H3". iModIntro  _ %I. by iSplitL "H2". Qed.

97 98
  Lemma test_into_wand_embed 𝓟 𝓠 :
    (𝓟 -  𝓠) 
99
    ⎡𝓟⎤ @{monPredI}  ⎡𝓠⎤.
100 101 102 103 104 105 106 107 108
  Proof.
    iIntros (HPQ) "HP".
    iMod (HPQ with "[-]") as "$"; last by auto.
    iAssumption.
  Qed.

  (* This is a hack to avoid avoid coq bug #5735: sections variables ignore hint
     modes. So we assume the instances in a way that cannot be used by type
     class resolution, and then separately declare the instance as such. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110
  Context (FU0 : BiFUpd PROP * unit).
  Instance FU : BiFUpd PROP := fst FU0.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
111 112 113

  Lemma test_apply_fupd_intro_mask E1 E2 P :
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  Proof. iIntros. by iApply @fupd_intro_mask. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
115 116
  Lemma test_apply_fupd_intro_mask_2 E1 E2 P :
    E2  E1  P - |={E1,E2}=> |={E2,E1}=> P.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  Proof. iIntros. iFrame. by iApply @fupd_intro_mask'. Qed.
118 119 120 121 122 123 124

  Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
    Q   P  Q  P  P.
  Proof.
    iIntros "[$ #HP]". iFrame "HP".
  Qed.

125
  Lemma test_iNext_Bi P :
126
     P @{monPredI}  P.
127 128 129
  Proof. iIntros "H". by iNext. Qed.

  (** Test monPred_at framing *)
130 131 132 133
  Lemma test_iFrame_monPred_at_wand (P Q : monPred) i :
    P i - (Q - P) i.
  Proof. iIntros "$". Show. Abort.

134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
  Program Definition monPred_id (R : monPred) : monPred :=
    MonPred (λ V, R V) _.
  Next Obligation. intros ? ???. eauto. Qed.

  Lemma test_iFrame_monPred_id (Q R : monPred) i :
    Q i  R i - (Q  monPred_id R) i.
  Proof.
    iIntros "(HQ & HR)". iFrame "HR". iAssumption.
  Qed.

  Lemma test_iFrame_rel P i j ij :
    IsBiIndexRel i ij  IsBiIndexRel j ij 
    P i - P j - P ij  P ij.
  Proof. iIntros (??) "HPi HPj". iFrame. Qed.

  Lemma test_iFrame_later_rel `{!BiAffine PROP} P i j :
    IsBiIndexRel i j 
     (P i) - ( P) j.
  Proof. iIntros (?) "?". iFrame. Qed.

  Lemma test_iFrame_laterN n P i :
    ^n (P i) - (^n P) i.
  Proof. iIntros "?". iFrame. Qed.

  Lemma test_iFrame_quantifiers P i :
    P i - ( _:(),  _:(), P) i.
  Proof. iIntros "?". iFrame. Show. iIntros ([]). iExists (). iEmpIntro. Qed.

  Lemma test_iFrame_embed (P : PROP) i :
    P - (embed (B:=monPredI) P) i.
  Proof. iIntros "$". Qed.

  (* Make sure search doesn't diverge on an evar *)
  Lemma test_iFrame_monPred_at_evar (P : monPred) i j :
    P i -  Q, (Q j).
  Proof. iIntros "HP". iExists _. Fail iFrame "HP". Abort.
170

171
End tests.
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195

Section tests_iprop.
  Context {I : biIndex} `{!invG Σ}.

  Local Notation monPred := (monPred I (iPropI Σ)).
  Implicit Types P : iProp Σ.

  Lemma test_iInv_0 N P:
    embed (B:=monPred) (inv N (<pers> P)) ={}=  ⎡▷ P.
  Proof.
    iIntros "#H".
    iInv N as "#H2". Show.
    iModIntro. iSplit=>//. iModIntro. iModIntro; auto.
  Qed.

  Lemma test_iInv_0_with_close N P:
    embed (B:=monPred) (inv N (<pers> P)) ={}= ⎡▷ P.
  Proof.
    iIntros "#H".
    iInv N as "#H2" "Hclose". Show.
    iMod ("Hclose" with "H2").
    iModIntro. iModIntro. by iNext.
  Qed.
End tests_iprop.