iris_wp.v 43.1 KB
Newer Older
1 2
Require Import ssreflect.
Require Import world_prop core_lang lang masks iris_vs.
3
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
4

Ralf Jung's avatar
Ralf Jung committed
5
Module IrisWP (RL : PCM_T) (C : CORE_LANG).
6
  Module Export L  := Lang C.
Ralf Jung's avatar
Ralf Jung committed
7
  Module Export VS := IrisVS RL C.
8

9 10 11
  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

Filip Sieczkowski's avatar
Filip Sieczkowski committed
12 13 14 15 16 17 18 19 20
  Section HoareTriples.
  (* Quadruples, really *)
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.

    Global Instance expr_type : Setoid expr := discreteType.
    Global Instance expr_metr : metric expr := discreteMetric.
21 22 23 24 25
    Global Instance expr_cmetr : cmetric expr := discreteCMetric.
    Instance LP_isval : LimitPreserving is_value.
    Proof.
      intros σ σc HC; apply HC.
    Qed.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
26

27 28 29 30 31 32 33
    (* We use this type quite a bit, so give it and its instances names *)
    Definition vPred := value -n> Props.
    Global Instance vPred_type  : Setoid vPred  := _.
    Global Instance vPred_metr  : metric vPred  := _.
    Global Instance vPred_cmetr : cmetric vPred := _.

    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : res).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
34 35 36

    Local Obligation Tactic := intros; eauto with typeclass_instances.

37 38 39 40 41
    Definition safeExpr e σ :=
      is_value e \/
         (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
         (exists e' K, e = K [[ fork e' ]]).

42
    Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
Ralf Jung's avatar
Ralf Jung committed
43 44
      forall w' k rf mf σ (HSw : w  w') (HLt : k < n) (HD : mf # m)
             (HE : wsat σ (m  mf) (Some r · rf) w' @ S k),
Filip Sieczkowski's avatar
Filip Sieczkowski committed
45
        (forall (HV : is_value e),
Ralf Jung's avatar
Ralf Jung committed
46 47
         exists w'' r', w'  w'' /\ φ (exist _ e HV) w'' (S k) r'
                           /\ wsat σ (m  mf) (Some r' · rf) w'' @ S k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
48 49
        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                (HStep : prim_step (ei, σ) (ei', σ')),
Ralf Jung's avatar
Ralf Jung committed
50 51
         exists w'' r', w'  w'' /\ WP (K [[ ei' ]]) φ w'' k r'
                           /\ wsat σ' (m  mf) (Some r' · rf) w'' @ k) /\
52
        (forall e' K (HDec : e = K [[ fork e' ]]),
Ralf Jung's avatar
Ralf Jung committed
53
         exists w'' rfk rret, w'  w''
54 55
                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                 /\ WP e' (umconst ) w'' k rfk
Ralf Jung's avatar
Ralf Jung committed
56
                                 /\ wsat σ (m  mf) (Some rfk · Some rret · rf) w'' @ k) /\
57
        (forall HSafe : safe = true, safeExpr e σ).
58

59 60
    (* Define the function wp will be a fixed-point of *)
    Program Definition wpF safe m : (expr -n> vPred -n> Props) -n> (expr -n> vPred -n> Props) :=
61
      n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP safe m WP e φ w) _)])])])].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
62
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
63
      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
64
      rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
Ralf Jung's avatar
Ralf Jung committed
65
      specialize (Hp w' k (Some rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
66 67
      [| now eauto with arith | ..]; try assumption; [].      
      split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
68
      - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
69
        rewrite ->assoc, (comm (Some r1')) in HE'.
70
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
71
          [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
Ralf Jung's avatar
Ralf Jung committed
72
        exists w'' r2'; split; [assumption | split; [| assumption] ].
73
        eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
74
      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
75
        rewrite ->assoc, (comm (Some r1')) in HE'.
Ralf Jung's avatar
Ralf Jung committed
76
        destruct k as [| k]; [exists w'' r1'; simpl wsat; tauto |].
77
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
78
          [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
Ralf Jung's avatar
Ralf Jung committed
79
        exists w'' r2'; split; [assumption | split; [| assumption] ].
80
        eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
81 82
      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
        destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
83
        rewrite ->assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
84
        destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
85
          [| apply wsat_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
Ralf Jung's avatar
Ralf Jung committed
86
        exists w'' rfk rret2; repeat (split; try assumption); [].
87
        eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
88
      - auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
89 90 91 92
    Qed.
    Next Obligation.
      intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
      - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
93
        edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
94
        [eapply wsat_dist, HE; [eassumption | now eauto with arith] |].
95
        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
96
        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
97 98
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
99
          exists (extend w1'' w2') r'; split; [assumption |].
100
          split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
101
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
102
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
103 104
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
105
          exists (extend w1'' w2') r'; split; [assumption |].
106
          split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
107
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
108
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
109 110
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
111
          exists (extend w1'' w2') rfk rret; split; [assumption |].
112
          split; [| split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ] ];
113
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
114
        + auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
115
      - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
116
        edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
117
        [eapply wsat_dist, HE; [eassumption | now eauto with arith] |].
118
        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
119
        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
120 121
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
122
          exists (extend w1'' w2') r'; split; [assumption |].
123
          split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
124
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
125
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
126 127
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
128
          exists (extend w1'' w2') r'; split; [assumption |].
129
          split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
130
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
131
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
132 133
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
Ralf Jung's avatar
Ralf Jung committed
134
          exists (extend w1'' w2') rfk rret; split; [assumption |].
135
          split; [| split; [| eapply wsat_dist, HE'; [eassumption | now eauto with arith] ] ];
136
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
137
        + auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
138 139 140 141 142 143 144
    Qed.
    Next Obligation.
      intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
      etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
145 146
      split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
      - split; [| split; [| split] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
147 148
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
149
          apply EQφ, Hφ; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
150 151
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
152
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
153 154
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret ; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
155
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
156 157
        + auto.
      - split; [| split; [| split] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
158 159
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
160
          apply EQφ, Hφ; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
161 162
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
163
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
164 165
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
166
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
167
        + auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
168 169 170 171 172 173 174
    Qed.
    Next Obligation.
      intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
      simpl in EQe; subst e2; reflexivity.
    Qed.
    Next Obligation.
      intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
175 176
      split; intros Hp w'; intros; edestruct Hp as [HF [HS [HV HS'] ] ]; try eassumption; [|].
      - split; [assumption | split; [| split]; intros].
Ralf Jung's avatar
Ralf Jung committed
177 178
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
179
          eapply (EQWP _ _ _), HWP; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
180 181
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret; split; [assumption |].
182
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
183 184
        + auto.
      - split; [assumption | split; [| split]; intros].
Ralf Jung's avatar
Ralf Jung committed
185 186
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
187
          eapply (EQWP _ _ _), HWP; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
188 189
        + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret; split; [assumption |].
190
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
191
        + auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
192 193
    Qed.

194
    Instance contr_wpF safe m : contractive (wpF safe m).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
195 196
    Proof.
      intros n WP1 WP2 EQWP e φ w k r HLt.
197 198
      split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
      - split; [assumption | split; [| split]; intros].
Ralf Jung's avatar
Ralf Jung committed
199 200
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
201
          eapply EQWP, HWP; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
202 203
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret; split; [assumption |].
204
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
205 206
        + auto.
      - split; [assumption | split; [| split]; intros].
Ralf Jung's avatar
Ralf Jung committed
207 208
        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
          exists w'' r'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
209
          eapply EQWP, HWP; now eauto with arith.
Ralf Jung's avatar
Ralf Jung committed
210 211
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
          exists w'' rfk rret; split; [assumption |].
212
          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
213
        + auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
214 215
    Qed.

216
    Definition wp safe m : expr -n> vPred -n> Props :=
217
      fixp (wpF safe m) (umconst (umconst )).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
218

219 220 221 222 223 224 225 226
    Lemma unfold_wp safe m :
      wp safe m == (wpF safe m) (wp safe m).
    Proof.
      unfold wp; apply fixp_eq.
    Qed.

    Opaque wp.

227
    Definition ht safe m P e φ :=  (P  wp safe m e φ).
228

Filip Sieczkowski's avatar
Filip Sieczkowski committed
229
  End HoareTriples.
230

231
  Section Adequacy.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
232 233 234 235 236 237
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.
    Local Open Scope list_scope.

238
    (* weakest-pre for a threadpool *)
239 240 241 242 243 244
    Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> list vPred -> Prop :=
    | wp_emp : wptp safe m w n nil nil nil
    | wp_cons e φ r tp rs φs
              (WPE  : wp safe m e φ w n r)
              (WPTP : wptp safe m w n tp rs φs) :
        wptp safe m w n (e :: tp) (r :: rs) (φ :: φs).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
245

246
    (* Trivial lemmas about split over append *)
247 248 249 250
    Lemma wptp_app safe m w n tp1 tp2 rs1 rs2 φs1 φs2
          (HW1 : wptp safe m w n tp1 rs1 φs1)
          (HW2 : wptp safe m w n tp2 rs2 φs2) :
      wptp safe m w n (tp1 ++ tp2) (rs1 ++ rs2) (φs1 ++ φs2).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
251 252 253 254
    Proof.
      induction HW1; [| constructor]; now trivial.
    Qed.

255 256 257
    Lemma wptp_app_tp safe m w n t1 t2 rs φs
          (HW : wptp safe m w n (t1 ++ t2) rs φs) :
      exists rs1 rs2 φs1 φs2, rs1 ++ rs2 = rs /\ φs1 ++ φs2 = φs /\ wptp safe m w n t1 rs1 φs1 /\ wptp safe m w n t2 rs2 φs2.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
258
    Proof.
259 260 261 262 263
      revert rs φs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
      - do 4 eexists. split; [|split; [|split; now econstructor] ]; reflexivity.
      - do 4 eexists. split; [|split; [|split; now eauto using wptp] ]; reflexivity.
      - apply IHt1 in WPTP; destruct WPTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [WP1 WP2] ] ] ] ] ] ]; clear IHt1.
        exists (r :: rs1) rs2 (φ :: φs1) φs2; simpl; subst; now auto using wptp.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
264 265
    Qed.

266
    (* Closure under future worlds and smaller steps *)
267
    Lemma wptp_closure safe m (w1 w2 : Wld) n1 n2 tp rs φs
268
          (HSW : w1  w2) (HLe : n2 <= n1)
269 270
          (HW : wptp safe m w1 n1 tp rs φs) :
      wptp safe m w2 n2 tp rs φs.
271 272 273 274 275 276
    Proof.
      induction HW; constructor; [| assumption].
      eapply uni_pred; [eassumption | reflexivity |].
      rewrite <- HSW; assumption.
    Qed.

277 278 279 280 281 282
    Lemma preserve_wptp safe m n k tp tp' σ σ' w rs φs
          (HSN  : stepn n (tp, σ) (tp', σ'))
          (HWTP : wptp safe m w (n + S k) tp rs φs)
          (HE   : wsat σ m (comp_list rs) w @ n + S k) :
      exists w' rs' φs',
        w  w' /\ wptp safe m w' (S k) tp' rs' (φs ++ φs') /\ wsat σ' m (comp_list rs') w' @ S k.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
283
    Proof.
284 285 286 287 288
      revert tp σ w rs  φs HSN HWTP HE. induction n; intros; inversion HSN; subst; clear HSN.
      (* no step is taken *)
      { exists w rs (@nil vPred). split; [reflexivity|]. split.
        - rewrite List.app_nil_r. assumption.
        - assumption.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
289
      }
290
      inversion HS; subst; clear HS.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
291
      (* atomic step *)
292 293 294 295 296 297 298 299 300 301 302 303 304
      { inversion H0; subst; clear H0.
        apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
        inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
        edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [HS _] ];
          [reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
        + eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
          rewrite !comp_list_app; simpl comp_list; unfold equiv.
          rewrite ->assoc, (comm (Some r)), <- assoc. reflexivity.       
        + edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
          [reflexivity | eassumption | clear WPE HS].
          setoid_rewrite HSW. eapply IHn; clear IHn.
          * eassumption.
          * apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
305
            constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
306 307 308
          * eapply wsat_equiv, HE'; [now erewrite mask_emp_union| |reflexivity].
            rewrite !comp_list_app; simpl comp_list; unfold equiv.
            rewrite ->2!assoc, (comm (Some r')). reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
309 310
      }
      (* fork *)
311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333
      inversion H; subst; clear H.
      apply wptp_app_tp in HWTP; destruct HWTP as [rs1 [rs2 [φs1 [φs2 [EQrs [EQφs [HWTP1 HWTP2] ] ] ] ] ] ].
      inversion HWTP2; subst; clear HWTP2; rewrite ->unfold_wp in WPE.
      edestruct (WPE w (n + S k) (comp_list (rs1 ++ rs0))) as [_ [_ [HF _] ] ];
        [reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
      + eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
        rewrite !comp_list_app; simpl comp_list; unfold equiv.
        rewrite ->assoc, (comm (Some r)), <- assoc. reflexivity.
      + specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
        setoid_rewrite HSW. edestruct IHn as [w'' [rs'' [φs'' [HSW'' [HSWTP'' HSE''] ] ] ] ]; first eassumption; first 2 last.
        * exists w'' rs'' ([umconst ] ++ φs''). split; [eassumption|].
          rewrite List.app_assoc. split; eassumption.
        * rewrite -List.app_assoc. apply wptp_app; [eapply wptp_closure, HWTP1; [assumption | now auto with arith] |].
          constructor; [eassumption|].
          apply wptp_app; [eapply wptp_closure, WPTP; [assumption | now auto with arith] |].
          constructor; [|now constructor]. eassumption.
        * eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
          rewrite comp_list_app. simpl comp_list. rewrite !comp_list_app. simpl comp_list.
          rewrite (comm _ 1). erewrite pcm_op_unit by apply _. unfold equiv.
          rewrite (comm _ (Some rfk)). rewrite ->!assoc. apply pcm_op_equiv;[|reflexivity]. unfold equiv.
          rewrite <-assoc, (comm (Some rret)), comm. reflexivity.
    Qed.

334
    Lemma adequacy_ht {safe m e p φ n k tp' σ σ' w r}
335
            (HT  : valid (ht safe m p e φ))
336
            (HSN : stepn n ([e], σ) (tp', σ'))
Filip Sieczkowski's avatar
Filip Sieczkowski committed
337
            (HP  : p w (n + S k) r)
Ralf Jung's avatar
Ralf Jung committed
338
            (HE  : wsat σ m (Some r) w @ n + S k) :
339 340
      exists w' rs' φs',
        w  w' /\ wptp safe m w' (S k) tp' rs' (φ :: φs') /\ wsat σ' m (comp_list rs') w' @ S k.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
341
    Proof.
342 343 344 345
      edestruct preserve_wptp with (rs:=[r]) as [w' [rs' [φs' [HSW' [HSWTP' HSWS'] ] ] ] ]; [eassumption | | simpl comp_list; erewrite comm, pcm_op_unit by apply _; eassumption | clear HT HSN HP HE].
      - specialize (HT w (n + S k) r). apply HT in HP; try reflexivity; [|now apply unit_min].
        econstructor; [|now econstructor]. eassumption.
      - exists w' rs' φs'. now auto.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
346 347
    Qed.

348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
    (** This is a (relatively) generic adequacy statement for triples about an entire program: They always execute to a "good" threadpool. It does not expect the program to execute to termination.  *)
    Theorem adequacy_glob safe m e φ tp' σ σ' k'
            (HT  : valid (ht safe m (ownS σ) e φ))
            (HSN : steps ([e], σ) (tp', σ')):
      exists w' rs' φs',
        wptp safe m w' (S k') tp' rs' (φ :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
    Proof.
      destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
      edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=(ex_own _ σ, pcm_unit _)) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
      - exists (pcm_unit _); now rewrite ->pcm_op_unit by apply _.
      - hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=res)). split.
        + assert (HS : Some (ex_own _ σ, pcm_unit _) · 1 = Some (ex_own _ σ, pcm_unit _));
          [| now setoid_rewrite HS].
          eapply ores_equiv_eq; now erewrite comm, pcm_op_unit by apply _.
        + intros i _; split; [reflexivity |].
          intros _ _ [].
      - do 3 eexists. split; [eassumption|]. assumption.
    Qed.
      
367
    Program Definition cons_pred (φ : value -=> Prop): vPred :=
368 369 370 371 372 373 374 375 376 377
      n[(fun v => pcmconst (mkUPred (fun n r => φ v) _))].
    Next Obligation.
      firstorder.
    Qed.
    Next Obligation.
      intros x y H_xy P m r. simpl in H_xy. destruct n.
      - intros LEZ. exfalso. omega.
      - intros _. simpl. assert(H_xy': equiv x y) by assumption. rewrite H_xy'. tauto.
    Qed.

378 379
    (* Adequacy as stated in the paper: for observations of the return value, after termination *)
    Theorem adequacy_obs safe m e (φ : value -=> Prop) e' tp' σ σ'
380
            (HT  : valid (ht safe m (ownS σ) e (cons_pred φ)))
381
            (HSN : steps ([e], σ) (e' :: tp', σ'))
382 383 384
            (HV : is_value e') :
        φ (exist _ e' HV).
    Proof.
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
      edestruct adequacy_glob as [w' [rs' [φs' [HSWTP HWS] ] ] ]; try eassumption.
      inversion HSWTP; subst; clear HSWTP WPTP.
      rewrite ->unfold_wp in WPE.
      edestruct (WPE w' O) as [HVal _];
        [reflexivity | unfold lt; reflexivity | now apply mask_emp_disjoint | rewrite mask_emp_union; eassumption |].
      fold comp_list in HVal.
      specialize (HVal HV); destruct HVal as [w'' [r'' [HSW'' [Hφ'' HE''] ] ] ].
      destruct (Some r'' · comp_list rs) as [r''' |] eqn: EQr.
      + assumption.
      + exfalso. eapply wsat_not_empty, HE''. reflexivity.
    Qed.

    (* Adequacy for safe triples *)
    Theorem adequacy_safe m e (φ : vPred) tp' σ σ' e'
            (HT  : valid (ht true m (ownS σ) e φ))
            (HSN : steps ([e], σ) (tp', σ'))
            (HE  : e'  tp'):
      safeExpr e' σ'.
    Proof.
      edestruct adequacy_glob as [w' [rs' [φs' [HSWTP HWS] ] ] ]; try eassumption.
      destruct (List.in_split _ _ HE) as [tp1 [tp2 HTP] ]. clear HE. subst tp'.
      apply wptp_app_tp in HSWTP; destruct HSWTP as [rs1 [rs2 [_ [φs2 [EQrs [_ [_ HWTP2] ] ] ] ] ] ].
      inversion HWTP2; subst; clear HWTP2 WPTP.
      rewrite ->unfold_wp in WPE.
      edestruct (WPE w' O) as [_ [_ [_ HSafe] ] ];
        [reflexivity | unfold lt; reflexivity | now apply mask_emp_disjoint | |].
      - rewrite mask_emp_union.
        eapply wsat_equiv, HWS; try reflexivity.
        rewrite comp_list_app. simpl comp_list.
        rewrite ->(assoc (comp_list rs1)), ->(comm (comp_list rs1) (Some r)), <-assoc. reflexivity.
      - apply HSafe. reflexivity.
416 417
    Qed.

418
  End Adequacy.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
419

420 421 422 423 424 425 426 427
  Section HoareTripleProperties.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.

    Existing Instance LP_isval.

428
    Implicit Types (P Q R : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (φ : vPred) (r : res).
429 430

    (** Ret **)
431
    Program Definition eqV v : vPred :=
432 433 434 435 436 437
      n[(fun v' : value => v === v')].
    Next Obligation.
      intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
      split; congruence.
    Qed.

438 439
    Lemma htRet e (HV : is_value e) safe m :
      valid (ht safe m  e (eqV (exist _ e HV))).
440
    Proof.
441
      intros w' nn rr w _ n r' _ _ _; clear w' nn rr.
442
      rewrite unfold_wp; intros w'; intros; split; [| split; [| split] ]; intros.
Ralf Jung's avatar
Ralf Jung committed
443
      - exists w' r'; split; [reflexivity | split; [| assumption] ].
444
        simpl; reflexivity.
445 446
      - contradiction (values_stuck _ HV _ _ HDec).
        repeat eexists; eassumption.
447 448 449
      - subst e; assert (HT := fill_value _ _ HV); subst K.
        revert HV; rewrite fill_empty; intros.
        contradiction (fork_not_value _ HV).
450
      - unfold safeExpr. auto.
451 452
    Qed.

453
    Lemma wpO safe m e φ w r : wp safe m e φ w O r.
454
    Proof.
455
      rewrite unfold_wp; intros w'; intros; now inversion HLt.
456
    Qed.
457 458

    (** Bind **)
459 460 461 462

    (** Quantification in the logic works over nonexpansive maps, so
        we need to show that plugging the value into the postcondition
        and context is nonexpansive. *)
463 464
    Program Definition plugV safe m φ φ' K :=
      n[(fun v : value => ht safe m (φ v) (K [[` v]]) φ')].
465 466 467 468 469 470 471 472
    Next Obligation.
      intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
      eapply (impl_dist (ComplBI := Props_BI)).
      - apply φ; assumption.
      - destruct n as [| n]; [apply dist_bound | simpl in EQv].
        rewrite EQv; reflexivity.
    Qed.

473 474
    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.

475 476
    Lemma htBind P φ φ' K e safe m :
      ht safe m P e φ  all (plugV safe m φ φ' K)  ht safe m P (K [[ e ]]) φ'.
477 478
    Proof.
      intros wz nz rz [He HK] w HSw n r HLe _ HP.
479 480
      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
      rewrite ->HSw, <- HLe in HK; clear wz nz HSw HLe HP.
481
      revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
482
      rewrite ->unfold_wp in He; rewrite unfold_wp.
483 484
      destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
      - intros w'; intros; edestruct He as [HV _]; try eassumption; [].
Ralf Jung's avatar
Ralf Jung committed
485
        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
486 487
        (* Fold the goal back into a wp *)
        setoid_rewrite HSw'.
488
        assert (HT : wp safe m (K [[ e ]]) φ' w'' (S k) r');
489
          [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
490 491 492
        clear HE; specialize (HK (exist _ e HVal)).
        do 30 red in HK; unfold proj1_sig in HK.
        apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
493
      - intros w'; intros; edestruct He as [_ [HS [HF HS'] ] ]; try eassumption; [].
494
        split; [intros HVal; contradiction HNVal; assert (HT := fill_value _ _ HVal);
495
                subst K; rewrite fill_empty in HVal; assumption | split; [| split]; intros].
496 497
        + clear He HF HE; edestruct step_by_value as [K' EQK];
          [eassumption | repeat eexists; eassumption | eassumption |].
498
          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
Ralf Jung's avatar
Ralf Jung committed
499
          edestruct HS as [w'' [r' [HSw' [He HE] ] ] ]; try eassumption; [].
500
          subst e; clear HStep HS.
Ralf Jung's avatar
Ralf Jung committed
501
          do 2 eexists; split; [eassumption | split; [| eassumption] ].
502
          rewrite <- fill_comp. apply IH; try assumption; [].
503 504 505
          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
        + clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
Ralf Jung's avatar
Ralf Jung committed
506
          edestruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE] ] ] ] ] ];
507
            try eassumption; []; subst e; clear HF.
Ralf Jung's avatar
Ralf Jung committed
508
          do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
509 510
          rewrite <- fill_comp; apply IH; try assumption; [].
          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
511 512 513 514 515 516 517
        + clear IH He HS HE HF; specialize (HS' HSafe); clear HSafe.
          destruct HS' as [HV | [HS | HF] ].
          { contradiction. }
          { right; left; destruct HS as [σ' [ei [ei' [K0 [HE HS] ] ] ] ].
            exists σ' ei ei' (K  K0); rewrite -> HE, fill_comp. auto. }
          { right; right; destruct HF as [e' [K0 HE] ].
            exists e' (K  K0). rewrite -> HE, fill_comp. auto. }
518
    Qed.
519 520 521

    (** Consequence **)

522 523 524
    (** Much like in the case of the plugging, we need to show that
        the map from a value to a view shift between the applied
        postconditions is nonexpansive *)
525 526 527 528
    Program Definition vsLift m1 m2 φ φ' :=
      n[(fun v => vs m1 m2 (φ v) (φ' v))].
    Next Obligation.
      intros v1 v2 EQv; unfold vs.
529
      rewrite ->EQv; reflexivity.
530 531
    Qed.

532 533
    Lemma htCons P P' φ φ' safe m e :
      vs m m P P'  ht safe m P' e φ'  all (vsLift m m φ' φ)  ht safe m P e φ.
534 535
    Proof.
      intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
536
      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
537
      rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
Ralf Jung's avatar
Ralf Jung committed
538
      intros w'; intros; edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
539
      clear HP HE; rewrite ->HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
540
      setoid_rewrite HSw'.
541
      assert (HT : wp safe m e φ w'' (S k) r');
542 543
        [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
      unfold lt in HLt; rewrite ->HSw, HSw', <- HLt in Hφ; clear - He Hφ.
544 545 546 547
      (* Second phase of the proof: got rid of the preconditions,
         now induction takes care of the evaluation. *)
      rename r' into r; rename w'' into w.
      revert w r e He Hφ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
548
      rename H into IH; intros; rewrite ->unfold_wp; rewrite ->unfold_wp in He.
549 550
      intros w'; intros; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
      split; [intros HVal; clear HS HF IH HS' | split; intros; [clear HV HF HS' | split; [intros; clear HV HS HS' | clear HV HS HF ] ] ].
Ralf Jung's avatar
Ralf Jung committed
551
      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ' HE] ] ] ].
552
        eapply Hφ in Hφ'; [| etransitivity; eassumption | apply HLt | apply unit_min].
Ralf Jung's avatar
Ralf Jung committed
553
        clear w n HSw Hφ HLt; edestruct Hφ' as [w [r'' [HSw [Hφ HE'] ] ] ];
554
        [reflexivity | apply le_n | rewrite mask_union_idem; eassumption | eassumption |].
Ralf Jung's avatar
Ralf Jung committed
555 556
        exists w r''; split; [etransitivity; eassumption | split; assumption].
      - clear HE He; edestruct HS as [w'' [r' [HSw' [He HE] ] ] ];
557
        try eassumption; clear HS.
Ralf Jung's avatar
Ralf Jung committed
558
        do 2 eexists; split; [eassumption | split; [| eassumption] ].
559
        apply IH; try assumption; [].
560
        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
Ralf Jung's avatar
Ralf Jung committed
561 562
      - clear HE He; edestruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]; [eassumption |].
        clear HF; do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
563
        apply IH; try assumption; [].
564
        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply Hφ.
565
      - assumption.
566
    Qed.
567

568
    Lemma htACons safe m m' e P P' φ φ'
569
          (HAt   : atomic e)
570
          (HSub  : m'  m) :
571
      vs m m' P P'  ht safe m' P' e φ'  all (vsLift m' m φ' φ)  ht safe m P e φ.
572 573
    Proof.
      intros wz nz rz [ [HP He] Hφ] w HSw n r HLe _ Hp.
574
      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
575
      split; [intros HV; contradiction (atomic_not_value e) |].
Ralf Jung's avatar
Ralf Jung committed
576
      edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
577 578 579
      { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
        destruct Hmm'; [| apply HSub]; assumption.
      }
580 581
      split; [| split; [intros; subst; contradiction (fork_not_atomic K e') |] ].
      - intros; rewrite <- HLe, HSw in He, Hφ; clear wz nz HSw HLe Hp.
582 583 584 585
        clear HE; rewrite ->HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
        unfold lt in HLt; rewrite ->HSw0, <- HLt in Hφ; clear w n HSw0 HLt Hp'.
        rewrite ->unfold_wp in He; edestruct He as [_ [HS _] ];
          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
Ralf Jung's avatar
Ralf Jung committed
586 587
        edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
        destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
588 589 590
        assert (HNV : ~ is_value ei)
          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
591
        rewrite ->fill_empty in *; rename ei into e.
592 593
        setoid_rewrite HSw'; setoid_rewrite HSw.
        assert (HVal := atomic_step _ _ _ _ HAt HStep).
594 595 596
        rewrite ->HSw', HSw in Hφ; clear - HE He' Hφ HSub HVal HD.
        rewrite ->unfold_wp in He'; edestruct He' as [HV _];
        [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
Ralf Jung's avatar
Ralf Jung committed
597
        clear HE He'; specialize (HV HVal); destruct HV as [w' [r [HSw [Hφ' HE] ] ] ].
598
        eapply Hφ in Hφ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
Ralf Jung's avatar
Ralf Jung committed
599
        clear Hφ; edestruct Hφ' as [w'' [r' [HSw' [Hφ HE'] ] ] ];
600 601 602 603
          [reflexivity | apply le_n | | eassumption |].
        { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
          destruct Hmm'; [apply HSub |]; assumption.
        }