upred_tactics.v 9.69 KB
Newer Older
1
2
From iris.algebra Require Export upred.
From iris.algebra Require Export upred_big_op.
3
Import uPred.
4

5
Module uPred_reflection. Section uPred_reflection.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
  Context {M : cmraT}.

  Inductive expr :=
    | ETrue : expr
    | EVar : nat  expr
    | ESep : expr  expr  expr.
  Fixpoint eval (Σ : list (uPred M)) (e : expr) : uPred M :=
    match e with
    | ETrue => True
    | EVar n => from_option True%I (Σ !! n)
    | ESep e1 e2 => eval Σ e1  eval Σ e2
    end.
  Fixpoint flatten (e : expr) : list nat :=
    match e with
    | ETrue => []
    | EVar n => [n]
    | ESep e1 e2 => flatten e1 ++ flatten e2
    end.

  Notation eval_list Σ l :=
    (uPred_big_sep ((λ n, from_option True%I (Σ !! n)) <$> l)).
27
  Lemma eval_flatten Σ e : eval Σ e  eval_list Σ (flatten e).
28
29
30
31
32
  Proof.
    induction e as [| |e1 IH1 e2 IH2];
      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
  Qed.
  Lemma flatten_entails Σ e1 e2 :
33
    flatten e2 `contains` flatten e1  eval Σ e1  eval Σ e2.
34
35
36
37
  Proof.
    intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
  Qed.
  Lemma flatten_equiv Σ e1 e2 :
38
    flatten e2  flatten e1  eval Σ e1  eval Σ e2.
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
  Proof. intros He. by rewrite !eval_flatten He. Qed.

  Fixpoint prune (e : expr) : expr :=
    match e with
    | ETrue => ETrue
    | EVar n => EVar n
    | ESep e1 e2 =>
       match prune e1, prune e2 with
       | ETrue, e2' => e2'
       | e1', ETrue => 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.
57
  Lemma prune_correct Σ e : eval Σ (prune e)  eval Σ e.
58
59
60
61
62
63
64
65
66
67
68
69
  Proof. by rewrite !eval_flatten flatten_prune. Qed.

  Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
    match e with
    | ETrue => None
    | EVar n' => if decide (n = n') then Some ETrue 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.
70
71
  Definition cancel (ns : list nat) (e: expr) : option expr :=
    prune <$> fold_right (mbind  cancel_go) (Some e) ns.
72
73
74
75
76
  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.
77
78
    - by rewrite IH1 //.
    - by rewrite IH2 // Permutation_middle.
79
  Qed.
80
81
  Lemma flatten_cancel e e' ns :
    cancel ns e = Some e'  flatten e  ns ++ flatten e'.
82
  Proof.
83
84
85
    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.
86
  Qed.
87
88
  Lemma cancel_entails Σ e1 e2 e1' e2' ns :
    cancel ns e1 = Some e1'  cancel ns e2 = Some e2' 
89
    eval Σ e1'  eval Σ e2'  eval Σ e1  eval Σ e2.
90
91
  Proof.
    intros ??. rewrite !eval_flatten.
92
    rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
93
    rewrite !fmap_app !big_sep_app. apply sep_mono_r.
94
95
  Qed.

96
97
98
99
100
101
102
  Fixpoint to_expr (l : list nat) : expr :=
    match l with
    | [] => ETrue
    | [n] => EVar n
    | n :: l => ESep (EVar n) (to_expr l)
    end.
  Arguments to_expr !_ / : simpl nomatch.
103
  Lemma eval_to_expr Σ l : eval Σ (to_expr l)  eval_list Σ l.
104
105
106
107
108
  Proof.
    induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
    by rewrite IH.
  Qed.

109
  Lemma split_l Σ e ns e' :
110
    cancel ns e = Some e'  eval Σ e  (eval Σ (to_expr ns)  eval Σ e').
111
  Proof.
112
113
    intros He%flatten_cancel.
    by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
114
  Qed.
115
  Lemma split_r Σ e ns e' :
116
    cancel ns e = Some e'  eval Σ e  (eval Σ e'  eval Σ (to_expr ns)).
117
118
  Proof. intros. rewrite /= comm. by apply split_l. Qed.

119
120
121
122
123
124
  Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
  Global Instance quote_True Σ : Quote Σ Σ True ETrue.
  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) (ESep e1 e2).
125
126
127
128
129
130

  Class QuoteArgs (Σ: list (uPred M)) (Ps: list (uPred M)) (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).
131
  End uPred_reflection.
132
133
134

  Ltac quote :=
    match goal with
135
    | |- ?P1  ?P2 =>
136
137
      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
      lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
138
        change (eval Σ3 e1  eval Σ3 e2) end end
139
140
141
    end.
  Ltac quote_l :=
    match goal with
142
    | |- ?P1  ?P2 =>
143
      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
144
        change (eval Σ2 e1  P2) end
145
    end.
146
End uPred_reflection.
147

148
Tactic Notation "solve_sep_entails" :=
149
  uPred_reflection.quote; apply uPred_reflection.flatten_entails;
150
151
  apply (bool_decide_unpack _); vm_compute; exact Logic.I.

152
153
154
155
156
157
158
159
160
161
162
Ltac close_uPreds Ps tac :=
  let M := match goal with |- @uPred_entails ?M _ _ => M 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 (uPred M)) end;
  go Ps (@nil (uPred M)).

163
Tactic Notation "cancel" constr(Ps) :=
164
  uPred_reflection.quote;
165
  let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
166
167
168
169
170
  let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
             | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
             end in
  eapply uPred_reflection.cancel_entails with (ns:=ns');
    [cbv; reflexivity|cbv; reflexivity|simpl].
171
172

Tactic Notation "ecancel" open_constr(Ps) :=
173
  close_uPreds Ps ltac:(fun Qs => cancel Qs).
174

175
(** [to_front [P1, P2, ..]] rewrites in the premise of ⊢ such that
176
177
    the assumptions P1, P2, ... appear at the front, in that order. *)
Tactic Notation "to_front" open_constr(Ps) :=
178
179
  close_uPreds Ps ltac:(fun Ps =>
    uPred_reflection.quote_l;
180
    let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
181
182
183
184
    let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
               | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
               end in
    eapply entails_equiv_l;
185
      first (apply uPred_reflection.split_l with (ns:=ns'); cbv; reflexivity);
186
187
188
189
190
      simpl).

Tactic Notation "to_back" open_constr(Ps) :=
  close_uPreds Ps ltac:(fun Ps =>
    uPred_reflection.quote_l;
191
    let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
192
193
194
195
    let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
               | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
               end in
    eapply entails_equiv_l;
196
      first (apply uPred_reflection.split_r with (ns:=ns'); cbv; reflexivity);
197
      simpl).
198
199
200
201
202
203

(** [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) :=
204
  to_back Ps; apply sep_mono.
205
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
206
  to_front Ps; apply sep_mono.
207

208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
Class StripLaterR {M} (P Q : uPred M) := strip_later_r : P   Q.
Arguments strip_later_r {_} _ _ {_}.
Class StripLaterL {M} (P Q : uPred M) := strip_later_l :  Q  P.
Arguments strip_later_l {_} _ _ {_}.

Section strip_later.
Context {M : cmraT}.
Implicit Types P Q : uPred M. 

Global Instance strip_later_r_fallthrough P : StripLaterR P P | 1000.
Proof. apply later_intro. Qed.
Global Instance strip_later_r_later P : StripLaterR ( P) P.
Proof. done. Qed.
Global Instance strip_later_r_and P1 P2 Q1 Q2 :
  StripLaterR P1 Q1  StripLaterR P2 Q2  StripLaterR (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance strip_later_r_or P1 P2 Q1 Q2 :
  StripLaterR P1 Q1  StripLaterR P2 Q2  StripLaterR (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance strip_later_r_sep P1 P2 Q1 Q2 :
  StripLaterR P1 Q1  StripLaterR P2 Q2  StripLaterR (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.

Global Instance strip_later_l_later P : StripLaterL ( P) P.
Proof. done. Qed.
Global Instance strip_later_l_and P1 P2 Q1 Q2 :
  StripLaterL P1 Q1  StripLaterL P2 Q2  StripLaterL (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance strip_later_l_or P1 P2 Q1 Q2 :
  StripLaterL P1 Q1  StripLaterL P2 Q2  StripLaterL (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance strip_later_l_sep P1 P2 Q1 Q2 :
  StripLaterL P1 Q1  StripLaterL P2 Q2  StripLaterL (P1  P2) (Q1  Q2).
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
End strip_later.

244
(** Assumes a goal of the shape P ⊢ ▷ Q. Alterantively, if Q
245
    is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
246
    Will turn this goal into P ⊢ Q and strip ▷ in P below ★, ∧, ∨. *)
247
Ltac strip_later :=
248
249
250
  intros_revert ltac:(
    etrans; [apply: strip_later_r|];
    etrans; [|apply: strip_later_l]; apply later_mono).