upred_tactics.v 11.8 KB
Newer Older
1
2
From algebra Require Export upred.
From 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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
  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.

  Fixpoint remove_all (l k : list nat) : option (list nat) :=
    match l with
    | [] => Some k
    | n :: l => '(i,_)  list_find (n =) k; remove_all l (delete i k)
    end.

  Lemma remove_all_permutation l k k' : remove_all l k = Some k'  k  l ++ k'.
  Proof.
    revert k k'; induction l as [|n l IH]; simpl; intros k k' Hk.
    { by simplify_eq. }
    destruct (list_find _ _) as [[i ?]|] eqn:?Hk'; simplify_eq/=.
    move: Hk'; intros [? <-]%list_find_Some.
    rewrite -(IH (delete i k) k') // -delete_Permutation //.
  Qed.
  Lemma split_l Σ e l k :
    remove_all l (flatten e) = Some k 
125
    eval Σ e  (eval Σ (to_expr l)  eval Σ (to_expr k))%I.
126
127
  Proof.
    intros He%remove_all_permutation.
128
    by rewrite eval_flatten He fmap_app big_sep_app !eval_to_expr.
129
130
131
  Qed.
  Lemma split_r Σ e l k :
    remove_all l (flatten e) = Some k 
132
    eval Σ e  (eval Σ (to_expr k)  eval Σ (to_expr l))%I.
133
134
  Proof. intros. rewrite /= comm. by apply split_l. Qed.

135
136
137
138
139
140
  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).
141
142
143
144
145
146

  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).
147
  End uPred_reflection.
148
149
150
151
152
153

  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 =>
154
155
156
157
158
159
160
        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
161
    end.
162
End uPred_reflection.
163

164
Tactic Notation "solve_sep_entails" :=
165
  uPred_reflection.quote; apply uPred_reflection.flatten_entails;
166
167
  apply (bool_decide_unpack _); vm_compute; exact Logic.I.

168
169
170
171
172
173
174
175
176
177
178
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)).

179
Tactic Notation "cancel" constr(Ps) :=
180
181
182
183
184
185
186
  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].
187
188

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

191
192
193
(** [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) :=
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
  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;
      first (apply uPred_reflection.split_l with (l:=ns'); cbv; reflexivity);
      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;
      first (apply uPred_reflection.split_r with (l:=ns'); cbv; reflexivity);
      simpl).
214
215
216
217
218
219

(** [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) :=
220
  to_back Ps; apply sep_mono.
221
Tactic Notation "sep_split" "left:" open_constr(Ps) :=
222
  to_front Ps; apply sep_mono.
223

224
225
226
(** 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 ★, ∧, ∨. *)
227
Ltac strip_later :=
228
  let rec strip :=
229
230
231
232
233
234
235
236
237
238
239
240
241
    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
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
  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
259
  in intros_revert ltac:(etrans; [|shape_Q];
260
261
262
263
264
                         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. *)
265
266
(* TODO: this name may be a big too general *)
Ltac revert_all :=
267
  lazymatch goal with
268
269
270
271
272
273
274
275
  | |-  _, _ =>
    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
276
277
278
279
280
281
282
283
  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 *)
284
285
Ltac löb tac :=
  revert_all;
286
287
288
289
290
291
292
293
294
295
  (* 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 :=
296
297
298
299
300
301
302
303
304
305
306
    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
307
  in go.