proofmode_monpred.v 6 KB
Newer Older
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
1
2
3
From iris.proofmode Require Import tactics monpred.

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

30
31
  Lemma test_intowand_1 P Q : (P - Q) - P - Q.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
32
33
    iStartProof PROP. iIntros (i) "HW". Show.
    iIntros (j ->) "HP". Show. by iApply "HW".
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
  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.
54

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

  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
66
67
68
69
70

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

Robbert Krebbers's avatar
Robbert Krebbers committed
72
  Lemma test_objectively P Q : <obj> emp - <obj> P - <obj> Q - <obj> (P  Q).
73
74
  Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.

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

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

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

87
  Lemma test_iModIntro_embed_objective P `{!Objective Q} 𝓟 𝓠 :
88
     P - Q - ⎡𝓟⎤ - ⎡𝓠⎤ -   i, 𝓟  𝓠  Q i .
Ralf Jung's avatar
Ralf Jung committed
89
  Proof. iIntros "#H1 H2 H3 H4". iAlways. Show. iFrame. Qed.
90

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

95
96
  Lemma test_into_wand_embed 𝓟 𝓠 :
    (𝓟 -  𝓠) 
Ralf Jung's avatar
Ralf Jung committed
97
    ⎡𝓟⎤ @{monPredI}  ⎡𝓠⎤.
98
99
100
101
102
103
104
105
106
  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
107
108
  Context (FU0 : BiFUpd PROP * unit).
  Instance FU : BiFUpd PROP := fst FU0.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
109
110
111

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

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

123
124
125
126
127
  Lemma test_iNext_Bi P :
    @bi_entails monPredI ( P) ( P).
  Proof. iIntros "H". by iNext. Qed.

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

132
133
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
  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.
168

169
End tests.