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 125 126 127 128 129 130 131 132 133 134
  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 
    eval Σ e  eval Σ (ESep (to_expr l) (to_expr k)).
  Proof.
    intros He%remove_all_permutation.
    by rewrite eval_flatten He fmap_app big_sep_app /= !eval_to_expr.
  Qed.
  Lemma split_r Σ e l k :
    remove_all l (flatten e) = Some k 
    eval Σ e  eval Σ (ESep (to_expr k) (to_expr l)).
  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.