-
Notifications
You must be signed in to change notification settings - Fork 5
/
tactics.v
214 lines (194 loc) · 7.79 KB
/
tactics.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
From stdpp Require Import gmap.
From iris.bi Require Export bi.
Set Default Proof Using "Type".
Import bi.
Module bi_reflection. Section bi_reflection.
Context {PROP : bi}.
Inductive expr :=
| EEmp : expr
| EVar : nat → expr
| ESep : expr → expr → expr.
Fixpoint eval (Σ : list PROP) (e : expr) : PROP :=
match e with
| EEmp => emp
| EVar n => default emp (Σ !! n)
| ESep e1 e2 => eval Σ e1 ∗ eval Σ e2
end%I.
Fixpoint flatten (e : expr) : list nat :=
match e with
| EEmp => []
| EVar n => [n]
| ESep e1 e2 => flatten e1 ++ flatten e2
end.
Notation eval_list Σ l := ([∗ list] n ∈ l, default emp (Σ !! n))%I.
Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
Proof.
induction e as [| |e1 IH1 e2 IH2];
rewrite /= ?right_id ?big_opL_app ?IH1 ?IH2 //.
Qed.
(* Can be related to the RHS being affine *)
Lemma flatten_entails `{BiAffine PROP} Σ e1 e2 :
flatten e2 ⊆+ flatten e1 → eval Σ e1 ⊢ eval Σ e2.
Proof. intros. rewrite !eval_flatten. by apply big_sepL_submseteq. Qed.
Lemma flatten_equiv Σ e1 e2 :
flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
Proof. intros He. by rewrite !eval_flatten He. Qed.
Fixpoint prune (e : expr) : expr :=
match e with
| EEmp => EEmp
| EVar n => EVar n
| ESep e1 e2 =>
match prune e1, prune e2 with
| EEmp, e2' => e2'
| e1', EEmp => e1'
| e1', e2' => ESep e1' e2'
end
end.
Lemma flatten_prune e : flatten (prune e) = flatten e.
Proof.
induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
Qed.
Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
Proof. by rewrite !eval_flatten flatten_prune. Qed.
Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
match e with
| EEmp => None
| EVar n' => if decide (n = n') then Some EEmp else None
| ESep e1 e2 =>
match cancel_go n e1 with
| Some e1' => Some (ESep e1' e2)
| None => ESep e1 <$> cancel_go n e2
end
end.
Definition cancel (ns : list nat) (e: expr) : option expr :=
prune <$> fold_right (mbind ∘ cancel_go) (Some e) ns.
Lemma flatten_cancel_go e e' n :
cancel_go n e = Some e' → flatten e ≡ₚ n :: flatten e'.
Proof.
revert e'; induction e as [| |e1 IH1 e2 IH2]; intros;
repeat (simplify_option_eq || case_match); auto.
- by rewrite IH1 //.
- by rewrite IH2 // Permutation_middle.
Qed.
Lemma flatten_cancel e e' ns :
cancel ns e = Some e' → flatten e ≡ₚ ns ++ flatten e'.
Proof.
rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune.
revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
rewrite Permutation_middle -flatten_cancel_go //; eauto.
Qed.
Lemma cancel_entails Σ e1 e2 e1' e2' ns :
cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
(eval Σ e1' ⊢ eval Σ e2') → eval Σ e1 ⊢ eval Σ e2.
Proof.
intros ??. rewrite !eval_flatten.
rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
rewrite !big_opL_app. apply sep_mono_r.
Qed.
Fixpoint to_expr (l : list nat) : expr :=
match l with
| [] => EEmp
| [n] => EVar n
| n :: l => ESep (EVar n) (to_expr l)
end.
Arguments to_expr !_ / : simpl nomatch.
Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
Proof.
induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
by rewrite IH.
Qed.
Lemma split_l Σ e ns e' :
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ∗ eval Σ e').
Proof.
intros He%flatten_cancel.
by rewrite eval_flatten He big_opL_app eval_to_expr eval_flatten.
Qed.
Lemma split_r Σ e ns e' :
cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ∗ eval Σ (to_expr ns)).
Proof. intros. rewrite /= comm. by apply split_l. Qed.
Class Quote (Σ1 Σ2 : list PROP) (P : PROP) (e : expr) := {}.
Global Instance quote_True Σ : Quote Σ Σ emp%I EEmp.
Global Instance quote_var Σ1 Σ2 P i:
rlist.QuoteLookup Σ1 Σ2 P i → Quote Σ1 Σ2 P (EVar i) | 1000.
Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 :
Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ∗ P2)%I (ESep e1 e2).
Class QuoteArgs (Σ : list PROP) (Ps : list PROP) (ns : list nat) := {}.
Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil.
Global Instance quote_args_cons Σ Ps P ns n :
rlist.QuoteLookup Σ Σ P n →
QuoteArgs Σ Ps ns → QuoteArgs Σ (P :: Ps) (n :: ns).
End bi_reflection.
Ltac quote :=
match goal with
| |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
change (eval Σ3 e1 ⊢ eval Σ3 e2) end end
end.
Ltac quote_l :=
match goal with
| |- ?P1 ⊢ ?P2 =>
lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
change (eval Σ2 e1 ⊢ P2) end
end.
End bi_reflection.
Tactic Notation "solve_sep_entails" :=
bi_reflection.quote;
first
[apply bi_reflection.flatten_entails (* for affine BIs *)
|apply equiv_entails, bi_reflection.flatten_equiv (* for other BIs *) ];
apply (bool_decide_unpack _); vm_compute; exact Logic.I.
Tactic Notation "solve_sep_equiv" :=
bi_reflection.quote; apply bi_reflection.flatten_equiv;
apply (bool_decide_unpack _); vm_compute; exact Logic.I.
Ltac close_uPreds Ps tac :=
let PROP := match goal with |- @bi_entails ?PROP _ _ => PROP end in
let rec go Ps Qs :=
lazymatch Ps with
| [] => let Qs' := eval cbv [reverse rev_append] in (reverse Qs) in tac Qs'
| ?P :: ?Ps => find_pat P ltac:(fun Q => go Ps (Q :: Qs))
end in
(* avoid evars in case Ps = @nil ?A *)
try match Ps with [] => unify Ps (@nil PROP) end;
go Ps (@nil PROP).
Tactic Notation "cancel" constr(Ps) :=
bi_reflection.quote;
let Σ := match goal with |- bi_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : bi_reflection.QuoteArgs Σ Ps _) with
| bi_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply bi_reflection.cancel_entails with (ns:=ns');
[cbv; reflexivity|cbv; reflexivity|simpl].
Tactic Notation "ecancel" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Qs => cancel Qs).
(** [to_front [P1, P2, ..]] rewrites in the premise of ⊢ such that
the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
bi_reflection.quote_l;
let Σ := match goal with |- bi_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : bi_reflection.QuoteArgs Σ Ps _) with
| bi_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply entails_equiv_l;
first (apply bi_reflection.split_l with (ns:=ns'); cbv; reflexivity);
simpl).
Tactic Notation "to_back" open_constr(Ps) :=
close_uPreds Ps ltac:(fun Ps =>
bi_reflection.quote_l;
let Σ := match goal with |- bi_reflection.eval ?Σ _ ⊢ _ => Σ end in
let ns' := lazymatch type of (_ : bi_reflection.QuoteArgs Σ Ps _) with
| bi_reflection.QuoteArgs _ _ ?ns' => ns'
end in
eapply entails_equiv_l;
first (apply bi_reflection.split_r with (ns:=ns'); cbv; reflexivity);
simpl).
(** [sep_split] is used to introduce a (∗).
Use [sep_split left: [P1, P2, ...]] to define which assertions will be
taken to the left; the rest will be available on the right.
[sep_split right: [P1, P2, ...]] works the other way around. *)
Tactic Notation "sep_split" "right:" open_constr(Ps) :=
to_back Ps; apply sep_mono.
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
to_front Ps; apply sep_mono.