proofmode.v 5.97 KB
Newer Older
1
From iris_c.c_translation Require Export translation.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris_c.vcgen Require Import vcgen denv reification.
3 4
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
5

Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
Class IntoDEnv `{amonadG Σ} (E E' : known_locs) (Γin Γout : env (iProp Σ)) (m : denv) := {
  into_denv : [] Γin  [] Γout  denv_interp E' m;
  into_denv_env_wf : env_wf Γin  env_wf Γout;
  into_denv_env_lookup i : Γin !! i = None  Γout !! i = None;
  into_denv_wf : denv_wf E' m;
  into_denv_mono : E `prefix_of` E';
}.

Class PropIntoDEnv `{amonadG Σ} (E E' : known_locs) (Pin Pout : iProp Σ) (m1 m2 : denv) := {
  prop_into_denv : denv_wf E m1  Pin  denv_interp E m1  Pout  denv_interp E' m2;
  prop_into_denv_wf : denv_wf E m1  denv_wf E' m2;
  prop_into_denv_mono : E `prefix_of` E';
}.
Arguments PropIntoDEnv {_ _} _ _ _%I _%I _.

21
Section tactics.
22
  Context `{amonadG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26 27 28 29 30 31
  Implicit Types P Q : iProp Σ.
  Hint Extern 0 (0 < _)%Q => apply Qp_prf.
  Hint Extern 2 (_ `prefix_of` _) => etrans; [eassumption|].

  Global Instance prop_into_denv_default E P m : PropIntoDEnv E E P P m m | 100.
  Proof. by split. Qed.
  Global Instance prop_into_denv_mapsto E E' E'' cl i lv q v dv m :
    LocLookup E E' cl i  IntoDVal E' E'' v dv 
    PropIntoDEnv E E'' (cl C[lv]{q} v) emp m (denv_insert i lv q dv m).
32
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36 37 38 39
    intros [??] [-> ? HE']. split; last by etrans.
    - iIntros (?) "[??]". iSplit=> //.
      iApply denv_insert_interp; eauto using denv_wf_mono.
      rewrite Q_to_of_Qp -(denv_interp_mono E); eauto.
      rewrite /dloc_var_interp (prefix_lookup E' _ _ cl) //=. iFrame.
    - intros. eapply denv_wf_insert; eauto using denv_wf_mono.
      rewrite /dloc_var_wf (prefix_lookup E' _ _ cl) //=.
40
  Qed.
41 42 43
  (* Not an instance, due to the IntoSep, this rule will loop if Pin can be
  split infinitely many times *)
  Lemma prop_into_denv_sep_aux E E' E'' Pin Pin1 Pin2 Pout1 Pout2 Pout m1 m2 m3 :
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47 48
    IntoSep Pin Pin1 Pin2 
    PropIntoDEnv E E' Pin1 Pout1 m1 m2 
    PropIntoDEnv E' E'' Pin2 Pout2 m2 m3 
    MakeSep Pout1 Pout2 Pout 
    PropIntoDEnv E E'' Pin Pout m1 m3.
49
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53
    rewrite /IntoSep /MakeSep. intros HP [HP1 ??] [HP2 ??] HPout.
    split; [|eauto|by etrans].
    intros. rewrite HP (comm _ Pin1) -assoc HP1 // assoc.
    rewrite (comm _ Pin2) -assoc HP2; last by eauto. by rewrite assoc -HPout.
54
  Qed.
55 56 57 58 59 60 61 62 63 64 65 66 67
  Global Instance prop_into_denv_sep E E' E'' Pin1 Pin2 Pout1 Pout2 Pout m1 m2 m3 :
    PropIntoDEnv E E' Pin1 Pout1 m1 m2 
    PropIntoDEnv E' E'' Pin2 Pout2 m2 m3 
    MakeSep Pout1 Pout2 Pout 
    PropIntoDEnv E E'' (Pin1  Pin2) Pout m1 m3.
  Proof. apply prop_into_denv_sep_aux, _. Qed.
  Global Instance prop_into_denv_mapsto_list E E' E'' q cl vs v vs' Pout1 Pout2 Pout m1 m2 m3 :
    IsCons vs v vs' 
    PropIntoDEnv E E' (cl C{q} v) Pout1 m1 m2 
    PropIntoDEnv E' E'' ((cl + 1) C{q} vs') Pout2 m2 m3 
    MakeSep Pout1 Pout2 Pout 
    PropIntoDEnv E E'' (cl C{q} vs) Pout m1 m3.
  Proof. intros ?. apply prop_into_denv_sep_aux, _. Qed.
68

Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71 72 73 74 75
  Global Instance into_denv_nil E : IntoDEnv E E Enil Enil nil.
  Proof. split; unfold denv_interp; eauto. Qed.
  Global Instance into_denv_snoc E E' E'' Γin Γout Γout' i Pin Pout m1 m2 :
    IntoDEnv E E' Γin Γout m1 
    PropIntoDEnv E' E'' Pin Pout m1 m2 
    TCIf (TCEq Pout emp)%I (TCEq Γout Γout') (TCEq Γout' (Esnoc Γout i Pout)) 
    IntoDEnv E E'' (Esnoc Γin i Pin) Γout' m2.
76
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82 83 84 85
    intros [HΓ ????] [HP ??] [-> ->| ->].
    - split; simpl; eauto.
      + by rewrite HΓ assoc (comm _ Pin) -assoc HP // left_id.
      + inversion_clear 1; eauto.
      + intros j. destruct (ident_beq_reflect j i) as [->|]; by eauto.
    - split; simpl; eauto.
      + by rewrite HΓ assoc (comm _ Pin) -assoc HP // assoc (comm _ Pout).
      + inversion_clear 1; constructor; eauto.
      + intros j. destruct (ident_beq_reflect j i) as [->|]; by eauto.
86 87
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90 91 92 93
  Lemma tac_vcg E1 E2 Γp Γs_in Γs_out m c e de R Φ :
    IntoDEnv [] E1 Γs_in Γs_out m 
    IntoDCExpr E1 E2 e de 
    envs_entails (Envs Γp Γs_out c) (vcg_wp_while E2 (dcexpr_size de) m de R
      (λ E3 m dv, wand_denv_interp E3 m (Φ (dval_interp E3 dv)))) 
    envs_entails (Envs Γp Γs_in c) (AWP e @ R {{ Φ }}).
94
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97 98 99 100 101 102 103 104 105 106
    intros [HΓ ????] [-> ??]; rewrite !envs_entails_eq /= /of_envs.
    iIntros (Hentails) "(Hwf & #HΓp & HΓs)".
    iDestruct "Hwf" as %Hwf; inversion_clear Hwf; simpl in *.
    iDestruct (HΓ with "HΓs") as "[HΓs Hm]".
    iDestruct (Hentails with "[$HΓs $HΓp]") as "HΓs".
    { iPureIntro; constructor; naive_solver. }
    iApply (awp_wand with "[-]").
    { iApply (vcg_wp_while_correct with "[Hm] HΓs"); eauto using denv_wf_mono.
      iApply (denv_interp_mono with "Hm"); eauto. }
    rewrite /vcg_wp_continuation. iIntros (v) "H".
    iDestruct "H" as (E3 dv m' -> ???) "[Hm HΦ]".
    by iApply (wand_denv_interp_spec with "HΦ").
107 108
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
109 110 111 112 113
  Lemma tac_vcg_continue E1 E2 E3 Γp Γs_in Γs_out m c v dv Φ :
    IntoDEnv E1 E2 Γs_in Γs_out m 
    IntoDVal E2 E3 v dv 
    envs_entails (Envs Γp Γs_out c) (Φ E3 m dv) 
    envs_entails (Envs Γp Γs_in c) (vcg_wp_continuation E1 Φ v).
Robbert Krebbers's avatar
Robbert Krebbers committed
114
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116 117 118 119 120 121 122
    intros [HΓ ????] [-> ??]; rewrite !envs_entails_eq /= /of_envs.
    iIntros (Hentails) "(Hwf & #HΓp & HΓs)".
    iDestruct "Hwf" as %Hwf; inversion_clear Hwf; simpl in *.
    iDestruct (HΓ with "HΓs") as "[HΓs Hm]".
    iDestruct (Hentails with "[$HΓs $HΓp]") as "HΓs".
    { iPureIntro; constructor; naive_solver. }
    iExists E3, dv, m. repeat (iSplit; first by eauto using denv_wf_mono).
    iFrame "HΓs". iApply (denv_interp_mono with "Hm"); eauto.
123
  Qed.
124
End tactics.
125

Robbert Krebbers's avatar
Robbert Krebbers committed
126
(* Make sure users do not see auxiliary junk *)
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Arguments vcg_wp_continuation {_ _ _ _}.
128

Robbert Krebbers's avatar
Robbert Krebbers committed
129
Ltac vcg :=
130
  iStartProof;
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133 134
  eapply tac_vcg;
    [iSolveTC (* Reify the context *)
    |iSolveTC (* Reify the expression *)
    |simpl].
135 136

Ltac vcg_continue :=
137
  iStartProof;
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140 141
  eapply tac_vcg_continue;
    [iSolveTC (* Reify the context *)
    |iSolveTC (* Reify the expression *)
    |simpl].