upred_tactics.v 11.2 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
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
  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)).
  Lemma eval_flatten Σ e : eval Σ e  eval_list Σ (flatten e).
  Proof.
    induction e as [| |e1 IH1 e2 IH2];
      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
  Qed.
  Lemma flatten_entails Σ e1 e2 :
    flatten e2 `contains` flatten e1  eval Σ e1  eval Σ e2.
  Proof.
    intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
  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
    | 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.
  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
    | 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
90
91
    eval Σ e1'  eval Σ e2'  eval Σ e1  eval Σ e2.
  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
103
104
105
106
107
108
  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.
  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.

109
110
  Lemma split_l Σ e ns e' :
    cancel ns e = Some e'  eval Σ e  (eval Σ (to_expr ns)  eval Σ e')%I.
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
116
  Lemma split_r Σ e ns e' :
    cancel ns e = Some e'  eval Σ e  (eval Σ e'  eval Σ (to_expr ns))%I.
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
135
136
137

  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 =>
138
139
140
141
142
143
144
        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
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
165
166
167
168
169
170
  uPred_reflection.quote;
  let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
  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
176
177
(** [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) :=
178
179
180
181
182
183
184
  close_uPreds Ps ltac:(fun Ps =>
    uPred_reflection.quote_l;
    let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
    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
191
192
193
194
195
      simpl).

Tactic Notation "to_back" open_constr(Ps) :=
  close_uPreds Ps ltac:(fun Ps =>
    uPred_reflection.quote_l;
    let Σ := match goal with |- uPred_reflection.eval ?Σ _  _ => Σ end in
    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
(** Assumes a goal of the shape P   Q. Alterantively, if Q
    is built of , ,  with  in all branches; that will work, too.
    Will turn this goal into P  Q and strip  in P below , , . *)
211
Ltac strip_later :=
212
  let rec strip :=
213
214
215
216
217
218
219
220
221
222
223
224
225
    lazymatch goal with
    | |- (_  _)   _  =>
      etrans; last (eapply equiv_entails_sym, later_sep);
      apply sep_mono; strip
    | |- (_  _)   _  =>
      etrans; last (eapply equiv_entails_sym, later_and);
      apply sep_mono; strip
    | |- (_  _)   _  =>
      etrans; last (eapply equiv_entails_sym, later_or);
      apply sep_mono; strip
    | |-  _   _ => apply later_mono; reflexivity
    | |- _   _ => apply later_intro; reflexivity
    end
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
  in let rec shape_Q :=
    lazymatch goal with
    | |- _  (_  _) =>
      (* Force the later on the LHS to be top-level, matching laters
         below  on the RHS *)
      etrans; first (apply equiv_entails, later_sep; reflexivity);
      (* Match the arm recursively *)
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
      etrans; first (apply equiv_entails, later_and; reflexivity);
      apply sep_mono; shape_Q
    | |- _  (_  _) =>
      etrans; first (apply equiv_entails, later_or; reflexivity);
      apply sep_mono; shape_Q
    | |- _   _ => apply later_mono; reflexivity
    (* We fail if we don't find laters in all branches. *)
    end
243
  in intros_revert ltac:(etrans; [|shape_Q];
244
245
246
247
248
                         etrans; last eapply later_mono; first solve [ strip ]).

(** Transforms a goal of the form  ..., ?0...  ?1  ?2
    into True  ..., ?0...  ?1  ?2, applies tac, and
    the moves all the assumptions back. *)
249
250
(* TODO: this name may be a big too general *)
Ltac revert_all :=
251
  lazymatch goal with
252
253
254
255
256
257
258
259
  | |-  _, _ =>
    let H := fresh in intro H; revert_all;
    (* TODO: Really, we should distinguish based on whether this is a
    dependent function type or not. Right now, we distinguish based
    on the sort of the argument, which is suboptimal. *)
    first [ apply (const_intro_impl _ _ _ H); clear H
          | revert H; apply forall_elim']
  | |- _  _ => apply impl_entails
260
261
262
263
264
265
266
267
  end.

(** This starts on a goal of the form  ..., ?0...  ?1  ?2.
   It applies löb where all the Coq assumptions have been turned into logical
   assumptions, then moves all the Coq assumptions back out to the context,
   applies [tac] on the goal (now of the form _  _), and then reverts the
   Coq assumption so that we end up with the same shape as where we started,
   but with an additional assumption -ed to the context *)
268
269
Ltac löb tac :=
  revert_all;
270
271
272
273
274
275
276
277
278
279
  (* Add a box *)
  etrans; last (eapply always_elim; reflexivity);
  (* We now have a goal for the form True  P, with the "original" conclusion
     being locked. *)
  apply löb_strong; etransitivity;
    first (apply equiv_entails, left_id, _; reflexivity);
  apply: always_intro;
  (* Now introduce again all the things that we reverted, and at the bottom,
     do the work *)
  let rec go :=
280
281
282
283
284
285
286
287
288
289
290
    lazymatch goal with
    | |- _  ( _, _) =>
      apply forall_intro; let H := fresh in intro H; go; revert H
    | |- _  ( _  _) =>
      apply impl_intro_l, const_elim_l; let H := fresh in intro H; go; revert H
    (* This is the "bottom" of the goal, where we see the impl introduced
       by uPred_revert_all as well as the  from löb_strong and the  we added. *)
    | |-   ?R  (?L  _) => apply impl_intro_l;
      trans (L    R)%I;
        [eapply equiv_entails, always_and_sep_r, _; reflexivity | tac]
    end
291
  in go.