refl.v 14.1 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stbor.lang Require Import lang subst_map.
Ralf Jung's avatar
Ralf Jung committed
2
From stbor.sim Require Import refl_step simple tactics viewshift.
Ralf Jung's avatar
Ralf Jung committed
3 4 5

Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
6 7
(** Enable use of [Forall] in recursion. *)
Lemma Forall_id {A: Type} (P: A  Prop) (l: list A) :
Ralf Jung's avatar
Ralf Jung committed
8
  Forall id (fmap P l)  Forall P l.
Ralf Jung's avatar
Ralf Jung committed
9 10 11 12 13 14 15 16
Proof.
  induction l; simpl; first by eauto using Forall_nil.
  split; intros [??]%Forall_cons_1; apply Forall_cons; simpl; tauto.
Qed.

(** "Well-formed" code doen't contain literal
pointers, places or administrative operations (init_call/end_call).
Defined by recursion to make sure we don't miss a case. *)
Ralf Jung's avatar
Ralf Jung committed
17
Definition scalar_wf (a: scalar) : Prop :=
Ralf Jung's avatar
Ralf Jung committed
18 19 20 21 22 23 24 25
  match a with
  | ScPoison | ScInt _ | ScFnPtr _ => True
  | ScnPtr => False
  end.
Definition value_wf (v: value) : Prop := Forall scalar_wf v.
Fixpoint expr_wf (e: expr) : Prop :=
  match e with
  (* Structural cases. *)
26
  | Var _ | Alloc _ => True
Ralf Jung's avatar
Ralf Jung committed
27
  | Val v => value_wf v
Ralf Jung's avatar
Ralf Jung committed
28 29
  | Call f args => expr_wf f  Forall id (fmap expr_wf args)
  | Case e branches => expr_wf e  Forall id (fmap expr_wf branches)
30
  | Deref e _ | Ref e | Copy e =>
Ralf Jung's avatar
Ralf Jung committed
31 32 33 34 35 36
    expr_wf e
  | Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
    expr_wf e1  expr_wf e2
  (* Forbidden cases. *)
  | InitCall e | EndCall e => False
  | Place _ _ _ => False
37
  | Free _ | Retag _ _ => False (* TODO: We'd like to support deallocation and retag! *)
Ralf Jung's avatar
Ralf Jung committed
38
  end.
Ralf Jung's avatar
Ralf Jung committed
39 40 41
Definition prog_wf (prog: fn_env) :=
  has_main prog 
  map_Forall (λ _ f, expr_wf f.(fun_body)) prog.
Ralf Jung's avatar
Ralf Jung committed
42

Ralf Jung's avatar
Ralf Jung committed
43 44 45
Section sem.
Context (fs ft: fn_env) `{!sim_local_funs_lookup fs ft}.
Context (css cst: call_id_stack).
Ralf Jung's avatar
Ralf Jung committed
46

Ralf Jung's avatar
Ralf Jung committed
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
(** Well-formed two-substitutions. *)
Definition srel (r: resUR) (xs: gmap string (result * result)) : Prop :=
  map_Forall (λ _ '(rs, rt), rrel r rs rt) xs.

Lemma srel_persistent r xs :
  srel r xs  srel (core r) xs.
Proof.
  intros Hrel x [vs vt] Hlk. apply rrel_persistent.
  eapply (Hrel _ _ Hlk).
Qed.

Lemma srel_mono r1 r2 xs :
   r2  r1  r2 
  srel r1 xs  srel r2 xs.
Proof.
  intros Hval Hincl Hrel x [vs vt] Hlk. eapply rrel_mono; [done..|].
  eapply (Hrel _ _ Hlk).
Qed.

Ralf Jung's avatar
Ralf Jung committed
66 67
Lemma srel_core_mono r rf xs:
  srel r xs   rf  core r  rf  srel rf xs.
Ralf Jung's avatar
Ralf Jung committed
68
Proof.
Ralf Jung's avatar
Ralf Jung committed
69 70 71
  intros Hrel%srel_persistent ??. eapply srel_mono; done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
72 73 74 75 76 77
Lemma vrel_core_mono r rf v1 v2 :
  vrel r v1 v2   rf  core r  rf  vrel rf v1 v2.
Proof.
  intros Hrel%vrel_persistent ??. eapply vrel_mono; done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
78 79 80 81 82 83 84 85 86 87
Lemma rrel_core_mono r rf r1 r2 :
  rrel r r1 r2   rf  core r  rf  rrel rf r1 r2.
Proof.
  intros Hrel%rrel_persistent ??. eapply rrel_mono; done.
Qed.

Lemma arel_core_mono r rf a1 a2 :
  arel r a1 a2   rf  core r  rf  arel rf a1 a2.
Proof.
  intros Hrel%arel_persistent ??. eapply arel_mono; done.
Ralf Jung's avatar
Ralf Jung committed
88 89 90
Qed.

(** Hints. *)
Ralf Jung's avatar
Ralf Jung committed
91
Local Hint Extern 10 (srel _ _) => apply: srel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
92
Local Hint Extern 20 (srel _ _) => apply: srel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
93
Local Hint Extern 10 (rrel _ _ _) => apply: rrel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
94
Local Hint Extern 20 (rrel _ _ _) => apply: rrel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
95 96 97 98
Local Hint Extern 10 (vrel _ _ _) => apply: vrel_core_mono; first fast_done : core.
Local Hint Extern 20 (vrel _ _ _) => apply: vrel_mono; last fast_done : core.
Local Hint Extern 10 (Forall2 (arel _) _ _) => apply: vrel_core_mono; first fast_done : core.
Local Hint Extern 20 (Forall2 (arel _) _ _) => apply: vrel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
99
Local Hint Extern 10 (arel _ _ _) => apply: arel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
100
Local Hint Extern 20 (arel _ _ _) => apply: arel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
101
Local Hint Extern 50 (_  _) => solve_res : core.
Ralf Jung's avatar
Ralf Jung committed
102

Ralf Jung's avatar
Ralf Jung committed
103
(** We define a "semantic well-formedness", in some context. *)
Ralf Jung's avatar
Ralf Jung committed
104 105 106
Definition sem_steps := 10%nat.

Definition sem_post (r: resUR) (n: nat) rs css' rt cst': Prop :=
Ralf Jung's avatar
Ralf Jung committed
107
  n = sem_steps  css' = css  cst' = cst  rrel r rs rt.
Ralf Jung's avatar
Ralf Jung committed
108 109

Definition sem_wf (r: resUR) es et :=
110
   xs : gmap string (result * result),
Ralf Jung's avatar
Ralf Jung committed
111
    srel r xs 
Ralf Jung's avatar
Ralf Jung committed
112
    r ⊨ˢ{sem_steps,fs,ft}
113
      (subst_map (fst <$> xs) es, css)
Ralf Jung's avatar
Ralf Jung committed
114
    
115
      (subst_map (snd <$> xs) et, cst)
Ralf Jung's avatar
Ralf Jung committed
116 117 118 119 120 121 122 123 124 125 126 127
    : sem_post.

Lemma value_wf_soundness r v :
  value_wf v  vrel r v v.
Proof.
  intros Hwf. induction v.
  - constructor.
  - apply Forall_cons_1 in Hwf as [??]. constructor.
    + destruct a; done.
    + apply IHv. done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
Lemma sim_simple_call_args' r r' (el1 el2: list expr) (rs rt: result) Φ :
  Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} (e1, css)  (e2, cst) : sem_post) el1 el2 
  ( r' (vs vt: list result),
    Forall2 (rrel r') vs vt 
    core r  r' ⊨ˢ{sem_steps,fs,ft}
      (Call rs (of_result <$> vs), css)  (Call rt (of_result <$> vt), cst)
    : Φ ) 
   vs vt, Forall2 (rrel r') vs vt 
  core r  r' ⊨ˢ{sem_steps,fs,ft}
    (Call rs ((of_result <$> vs) ++ el1), css)  (Call rt ((of_result <$> vt) ++ el2), cst)
  : Φ.
Proof.
  intros He Hcont. revert r'. induction He; intros r'.
  { intros vs vt ?. rewrite !app_nil_r. eapply (Hcont _ vs vt). done. }
  clear Hcont. intros vs vt Hvst.
  eapply sim_simple_bind_call.
  rewrite cmra_core_dup -assoc.
  eapply sim_simple_frame_r.
  eapply sim_simple_post_mono, H.
  intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
  simplify_eq/=.
  rewrite !cons_middle !assoc.
  change [rt']%E with (of_result <$> [rt']).
  rewrite - !fmap_app. rewrite [r''  core r]comm -assoc=>Hval.
  eapply IHHe. eapply Forall2_app.
  - eapply Forall2_impl; first done. intros.
    eapply rrel_mono; last done; eauto using cmra_valid_included.
  - constructor; last done.
    eapply rrel_mono; last done; eauto using cmra_valid_included.
Qed.

Lemma sim_simple_call_args r r' (el1 el2: list expr) (rs rt: result) Φ :
  Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} (e1, css)  (e2, cst) : sem_post) el1 el2 
  ( r' (vs vt: list result),
    Forall2 (rrel r') vs vt 
    core r  r' ⊨ˢ{sem_steps,fs,ft}
      (Call rs (of_result <$> vs), css)  (Call rt (of_result <$> vt), cst)
    : Φ ) 
  core r  r' ⊨ˢ{sem_steps,fs,ft} (Call rs el1, css)  (Call rt el2, cst) : Φ.
Proof.
  intros He Hcont.
  eapply sim_simple_call_args' with (vs:=[]) (vt:=[]); auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
172
Lemma expr_wf_soundness r e :
Ralf Jung's avatar
Ralf Jung committed
173
  expr_wf e  sem_wf r e e.
Ralf Jung's avatar
Ralf Jung committed
174
Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
175
  revert r. induction e using expr_ind; simpl; intros r.
Ralf Jung's avatar
Ralf Jung committed
176
  - (* Value *)
Ralf Jung's avatar
Ralf Jung committed
177
    move=>Hwf _ _ /=.
Ralf Jung's avatar
Ralf Jung committed
178
    apply: sim_simple_result.
Ralf Jung's avatar
Ralf Jung committed
179
    do 3 (split; first done).
Ralf Jung's avatar
Ralf Jung committed
180 181
    apply value_wf_soundness. done.
  - (* Variable *)
Ralf Jung's avatar
Ralf Jung committed
182
    move=>_ xs Hxswf /=.
183 184 185
    rewrite !lookup_fmap. specialize (Hxswf x).
    destruct (xs !! x); simplify_eq/=.
    + destruct p as [rs rt].
Ralf Jung's avatar
Ralf Jung committed
186
      intros σs σt ??. apply: sim_body_result.
Ralf Jung's avatar
Ralf Jung committed
187
      do 3 (split; first done).
188
      eapply (Hxswf (rs, rt)). done.
Ralf Jung's avatar
Ralf Jung committed
189
    + simpl. apply sim_simple_var.
Ralf Jung's avatar
Ralf Jung committed
190
  - (* Call *)
Ralf Jung's avatar
Ralf Jung committed
191 192
    move=>[Hwf1 /Forall_id Hwf2] xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_frame_core.
Ralf Jung's avatar
Ralf Jung committed
193
    eapply sim_simple_post_mono, IHe; [|by auto..].
Ralf Jung's avatar
Ralf Jung committed
194
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval. simpl.
Ralf Jung's avatar
Ralf Jung committed
195 196 197 198 199
    eapply sim_simple_call_args.
    { induction Hwf2; simpl; first by auto.
      destruct (Forall_cons_1 _ _ _ H) as [IHx IHl]. constructor.
      - eapply IHx; auto. exact: srel_persistent.
      - eapply IHHwf2. done. }
Ralf Jung's avatar
Ralf Jung committed
200 201 202 203
    intros r'' rs' rt' Hrel'. simplify_eq/=.
    eapply sim_simple_valid_post.
    eapply sim_simple_call; [by auto..|].
    intros rret vs vt vls vlt ? ??? Hrel''. simplify_eq.
Ralf Jung's avatar
Ralf Jung committed
204
    apply: sim_simple_result=>Hval'.
Ralf Jung's avatar
Ralf Jung committed
205
    do 3 (split; first done). auto.
Ralf Jung's avatar
Ralf Jung committed
206 207
  - (* InitCall: can't happen *) done.
  - (* EndCall: can't happen *) done.
Ralf Jung's avatar
Ralf Jung committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  - (* Proj *)
    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe1; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
    intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
    simplify_eq/=. eapply sim_simple_proj; [done..|].
    intros vi vv idx ?? Hidx ?. simplify_eq.
    do 3 (split; first done).
    move:Hrel=>/= /Forall2_lookup=>Hrel.
    specialize (Hrel (Z.to_nat idx)).
    rewrite Hidx in Hrel. inversion Hrel. simplify_eq/=.
    constructor; last done. auto.
Ralf Jung's avatar
Ralf Jung committed
224 225 226 227 228 229 230 231 232 233 234 235
  - (* Conc *)
    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe1; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
    intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
    simplify_eq/=. eapply sim_simple_conc; [done..|].
    intros v1 v2 ??. simplify_eq/=.
    do 3 (split; first done). simpl.
Ralf Jung's avatar
Ralf Jung committed
236
    apply Forall2_app; auto.
Ralf Jung's avatar
Ralf Jung committed
237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
  - (* BinOp *)
    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe1; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
    intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
    simplify_eq/=. eapply sim_simple_bin_op; [done..|].
    intros v1 v2 s ? ?? Heval. simplify_eq/=.
    do 3 (split; first done). constructor; last done.
    assert (arel (core r  core r'  r'') v1 v1) as Hrel_v1.
    { apply Forall2_cons_inv in Hrel as [??]. auto. }
    inversion Heval; simpl; auto; []. do 2 (split; first done).
    simplify_eq/=. apply Hrel_v1.
  - (* Place: can't happen *) done.
Ralf Jung's avatar
Ralf Jung committed
254 255 256
  - (* Deref *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
Ralf Jung's avatar
Ralf Jung committed
257
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
Ralf Jung's avatar
Ralf Jung committed
258
    simplify_eq/=. apply: sim_simple_deref=>l t ?. simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
259
    do 3 (split; first done). done.
Ralf Jung's avatar
Ralf Jung committed
260 261 262
  - (* Ref *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
Ralf Jung's avatar
Ralf Jung committed
263 264 265
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
    simplify_eq/=. eapply sim_simple_ref=>l t ??. simplify_eq/=.
    do 3 (split; first done). apply Hrel.
Ralf Jung's avatar
Ralf Jung committed
266 267 268 269 270
  - (* Copy *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
    eapply sim_simple_valid_post.
271
    eapply sim_simple_copy_public; [by auto..|].
Ralf Jung's avatar
Ralf Jung committed
272 273 274 275 276 277 278 279 280 281 282
    intros r'' v1 v2 Hrel'' Hval. simplify_eq/=.
    do 3 (split; first done). auto.
  - (* Write *)
    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe1; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
    intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel' ?]%rrel_with_eq) Hval'.
283
    simplify_eq/=. eapply sim_simple_write_public; [auto..|].
Ralf Jung's avatar
Ralf Jung committed
284
    do 3 (split; first done). constructor; done.
Ralf Jung's avatar
Ralf Jung committed
285 286 287
  - (* Alloc *)
    move=>Hwf xs Hxswf /=.
    eapply sim_simple_valid_post.
288
    eapply sim_simple_alloc_public=>l tg /= Hval.
Ralf Jung's avatar
Ralf Jung committed
289 290 291
    do 3 (split; first done).
    simpl. split; last done. constructor; last done.
    eapply arel_mono, arel_ptr; auto.
Ralf Jung's avatar
Ralf Jung committed
292
  - (* Free: can't happen *) done.
293
  - (* Retag: can't happen *) done.
Ralf Jung's avatar
Ralf Jung committed
294
  - (* Let *)
Ralf Jung's avatar
Ralf Jung committed
295 296 297
    move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe1; [|by auto..].
Ralf Jung's avatar
Ralf Jung committed
298
    intros r' n' rs css' rt cst' (-> & -> & -> & Hrel) Hval. simpl.
Ralf Jung's avatar
Ralf Jung committed
299
    eapply sim_simple_let; [destruct rs, rt; by eauto..|].
300 301 302
    rewrite !subst'_subst_map.
    change rs with (fst (rs, rt)). change rt with (snd (rs, rt)) at 2.
    rewrite !binder_insert_map.
Ralf Jung's avatar
Ralf Jung committed
303
    eapply IHe2; [by auto..|].
Ralf Jung's avatar
Ralf Jung committed
304
    destruct b; first by auto. simpl.
Ralf Jung's avatar
Ralf Jung committed
305 306
    apply map_Forall_insert_2; first by auto.
    eapply srel_core_mono; eauto.
Ralf Jung's avatar
Ralf Jung committed
307 308 309 310 311 312 313 314 315 316 317 318 319
  - (* Case *)
    move=>[Hwf1 /Forall_id Hwf2] xs Hxs /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_frame_core.
    eapply sim_simple_post_mono, IHe; [|by auto..].
    intros r' n' rs css' rt cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq) Hval.
    simplify_eq/=. eapply sim_simple_case.
    { rewrite !fmap_length //. }
    intros es et ??. rewrite !list_lookup_fmap.
    destruct (el !! Z.to_nat i) eqn:Hlk; last done.
    intros. simplify_eq/=.
    eapply (Forall_lookup_1  _ _ _ _ H Hlk).
    + eapply (Forall_lookup_1  _ _ _ _ Hwf2 Hlk).
    + eauto.
Ralf Jung's avatar
Ralf Jung committed
320
Qed.
Ralf Jung's avatar
Ralf Jung committed
321 322 323

End sem.

Ralf Jung's avatar
Ralf Jung committed
324
Theorem sim_mod_fun_refl f :
Ralf Jung's avatar
Ralf Jung committed
325
  expr_wf f.(fun_body) 
Ralf Jung's avatar
Ralf Jung committed
326 327
  ⊨ᶠ f  f.
Proof.
Ralf Jung's avatar
Ralf Jung committed
328 329 330 331
  intros Hwf fs ft Hlk r es et.
  intros vs vt σs σt Hrel Hsubst1 Hsubst2. exists sem_steps.
  apply sim_body_init_call=>/=.
  set css := snc σs :: scs σs. set cst := snc σt :: scs σt. move=>Hstacks.
Ralf Jung's avatar
Ralf Jung committed
332 333 334
  eapply sim_body_viewshift.
  { eapply viewshift_frame_l. eapply vs_call_empty_public. }
  eapply sim_body_frame_r.
Ralf Jung's avatar
Ralf Jung committed
335 336
  eapply sim_local_body_post_mono with
    (Φ:=(λ r n vs' σs' vt' σt', sem_post css cst r n vs' σs'.(scs) vt' σt'.(scs))).
Ralf Jung's avatar
Ralf Jung committed
337
  { intros r' n' rs css' rt cst' (-> & Hcss & Hcst & Hrrel) Hval. simplify_eq.
Ralf Jung's avatar
Ralf Jung committed
338
    split.
Ralf Jung's avatar
Ralf Jung committed
339
    - eexists. split; first by rewrite Hcst.
Ralf Jung's avatar
Ralf Jung committed
340 341
      apply: res_end_call_sat; first done. exact: cmra_included_r.
    - eapply rrel_mono; [done| |done]. exact: cmra_included_l.
Ralf Jung's avatar
Ralf Jung committed
342
  }
343
  destruct (subst_l_map _ _ _ _ _ _ _ (rrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
344
  { clear -Hrel. induction Hrel; eauto using Forall2. }
Ralf Jung's avatar
Ralf Jung committed
345 346
  eapply sim_simplify, expr_wf_soundness; done.
Qed.
Ralf Jung's avatar
Ralf Jung committed
347

348 349
Print Assumptions sim_mod_fun_refl.

Ralf Jung's avatar
Ralf Jung committed
350
Lemma sim_mod_funs_refl prog :
Ralf Jung's avatar
Ralf Jung committed
351
  prog_wf prog 
Ralf Jung's avatar
Ralf Jung committed
352 353
  sim_mod_funs prog prog.
Proof.
Ralf Jung's avatar
Ralf Jung committed
354
  intros [_ WF]. induction prog using map_ind.
Ralf Jung's avatar
Ralf Jung committed
355
  { intros ??. rewrite lookup_empty. done. }
Ralf Jung's avatar
Ralf Jung committed
356 357 358 359
  apply sim_mod_funs_insert; first done.
  - apply sim_mod_fun_refl. eapply WF. erewrite lookup_insert. done.
  - apply IHprog. eapply map_Forall_insert_12; done.
Qed.