upred_tactics.v 10.3 KB
Newer Older
1
From iris.prelude Require Import gmap.
2 3
From iris.algebra Require Export upred.
From iris.algebra Require Export upred_big_op.
4
Import uPred.
5

6
Module uPred_reflection. Section uPred_reflection.
7
  Context {M : ucmraT}.
8 9 10 11 12 13 14 15

  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
16
    | EVar n => from_option id True%I (Σ !! n)
17 18 19 20 21 22 23 24 25
    | 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.

26
  Notation eval_list Σ l := ([] ((λ n, from_option id True%I (Σ !! n)) <$> l))%I.
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
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.
214
Context {M : ucmraT}.
215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
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.

231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
Global Instance strip_later_r_big_sepM `{Countable K} {A}
    (Φ Ψ : K  A  uPred M) (m : gmap K A) :
  ( x k, StripLaterR (Φ k x) (Ψ k x)) 
  StripLaterR ([ map] k  x  m, Φ k x) ([ map] k  x  m, Ψ k x).
Proof.
  rewrite /StripLaterR=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
Qed.
Global Instance strip_later_r_big_sepS `{Countable A}
    (Φ Ψ : A  uPred M) (X : gset A) :
  ( x, StripLaterR (Φ x) (Ψ x)) 
  StripLaterR ([ set] x  X, Φ x) ([ set] x  X, Ψ x).
Proof.
  rewrite /StripLaterR=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
Qed.

246 247 248 249 250 251 252 253 254 255 256 257 258
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.

259
(** Assumes a goal of the shape P ⊢ ▷ Q. Alterantively, if Q
260
    is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
261
    Will turn this goal into P ⊢ Q and strip ▷ in P below ★, ∧, ∨. *)
262
Ltac strip_later :=
263 264 265
  intros_revert ltac:(
    etrans; [apply: strip_later_r|];
    etrans; [|apply: strip_later_l]; apply later_mono).