refl.v 13.7 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
  match a with
  | ScPoison | ScInt _ | ScFnPtr _ => True
Ralf Jung's avatar
Ralf Jung committed
20
  | ScnPtr => False (* literal pointers *)
Ralf Jung's avatar
Ralf Jung committed
21 22 23 24 25
  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)
Ralf Jung's avatar
Ralf Jung committed
30
  | Deref e _ | Ref e | Copy e | Free e | Retag e _ =>
Ralf Jung's avatar
Ralf Jung committed
31 32 33 34
    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. *)
Ralf Jung's avatar
Ralf Jung committed
35 36
  | InitCall e | EndCall e => False (* administrative *)
  | Place _ _ _ => False (* literal pointers *)
Ralf Jung's avatar
Ralf Jung committed
37
  end.
Ralf Jung's avatar
Ralf Jung committed
38 39 40
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
41

Ralf Jung's avatar
Ralf Jung committed
42 43
Section sem.
Context (fs ft: fn_env) `{!sim_local_funs_lookup fs ft}.
Ralf Jung's avatar
Ralf Jung committed
44

Ralf Jung's avatar
Ralf Jung committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
(** 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
64 65
Lemma srel_core_mono r rf xs:
  srel r xs   rf  core r  rf  srel rf xs.
Ralf Jung's avatar
Ralf Jung committed
66
Proof.
Ralf Jung's avatar
Ralf Jung committed
67 68 69
  intros Hrel%srel_persistent ??. eapply srel_mono; done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
70 71 72 73 74 75
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
76 77 78 79 80 81 82 83 84 85
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
86 87 88
Qed.

(** Hints. *)
Ralf Jung's avatar
Ralf Jung committed
89
Local Hint Extern 10 (srel _ _) => apply: srel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
90
Local Hint Extern 20 (srel _ _) => apply: srel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
91
Local Hint Extern 10 (rrel _ _ _) => apply: rrel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
92
Local Hint Extern 20 (rrel _ _ _) => apply: rrel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
93 94 95 96
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
97
Local Hint Extern 10 (arel _ _ _) => apply: arel_core_mono; first fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
98
Local Hint Extern 20 (arel _ _ _) => apply: arel_mono; last fast_done : core.
Ralf Jung's avatar
Ralf Jung committed
99
Local Hint Extern 50 (_  _) => solve_res : core.
Ralf Jung's avatar
Ralf Jung committed
100

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

104 105
Definition sem_post (r: resUR) (n: nat) rs rt: Prop :=
  n = sem_steps  rrel r rs rt.
Ralf Jung's avatar
Ralf Jung committed
106 107

Definition sem_wf (r: resUR) es et :=
108
   xs : gmap string (result * result),
Ralf Jung's avatar
Ralf Jung committed
109
    srel r xs 
Ralf Jung's avatar
Ralf Jung committed
110
    r ⊨ˢ{sem_steps,fs,ft}
111
      subst_map (fst <$> xs) es
Ralf Jung's avatar
Ralf Jung committed
112
    
113
      subst_map (snd <$> xs) et
Ralf Jung's avatar
Ralf Jung committed
114 115 116 117 118 119 120 121 122 123 124 125
    : 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
126
Lemma sim_simple_call_args' r r' (el1 el2: list expr) (rs rt: result) Φ :
127
  Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} e1  e2 : sem_post) el1 el2 
Ralf Jung's avatar
Ralf Jung committed
128 129 130
  ( r' (vs vt: list result),
    Forall2 (rrel r') vs vt 
    core r  r' ⊨ˢ{sem_steps,fs,ft}
131
      Call rs (of_result <$> vs)  Call rt (of_result <$> vt)
Ralf Jung's avatar
Ralf Jung committed
132 133 134
    : Φ ) 
   vs vt, Forall2 (rrel r') vs vt 
  core r  r' ⊨ˢ{sem_steps,fs,ft}
135
    Call rs ((of_result <$> vs) ++ el1)  Call rt ((of_result <$> vt) ++ el2)
Ralf Jung's avatar
Ralf Jung committed
136 137 138 139 140 141 142 143 144
  : Φ.
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.
145
  intros r'' n' rs' rt' (-> & [Hrel ?]%rrel_with_eq).
Ralf Jung's avatar
Ralf Jung committed
146 147 148 149 150 151 152 153 154 155 156 157
  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) Φ :
158
  Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} e1  e2 : sem_post) el1 el2 
Ralf Jung's avatar
Ralf Jung committed
159 160 161
  ( r' (vs vt: list result),
    Forall2 (rrel r') vs vt 
    core r  r' ⊨ˢ{sem_steps,fs,ft}
162
      Call rs (of_result <$> vs)  Call rt (of_result <$> vt)
Ralf Jung's avatar
Ralf Jung committed
163
    : Φ ) 
164
  core r  r' ⊨ˢ{sem_steps,fs,ft} Call rs el1  Call rt el2 : Φ.
Ralf Jung's avatar
Ralf Jung committed
165 166 167 168 169
Proof.
  intros He Hcont.
  eapply sim_simple_call_args' with (vs:=[]) (vt:=[]); auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
170
Lemma expr_wf_soundness r e :
Ralf Jung's avatar
Ralf Jung committed
171
  expr_wf e  sem_wf r e e.
Ralf Jung's avatar
Ralf Jung committed
172
Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
173
  revert r. induction e using expr_ind; simpl; intros r.
Ralf Jung's avatar
Ralf Jung committed
174
  - (* Value *)
Ralf Jung's avatar
Ralf Jung committed
175
    move=>Hwf _ _ /=.
Ralf Jung's avatar
Ralf Jung committed
176
    apply: sim_simple_result.
177
    split; first done.
Ralf Jung's avatar
Ralf Jung committed
178 179
    apply value_wf_soundness. done.
  - (* Variable *)
Ralf Jung's avatar
Ralf Jung committed
180
    move=>_ xs Hxswf /=.
181 182
    rewrite !lookup_fmap. specialize (Hxswf x).
    destruct (xs !! x); simplify_eq/=.
183 184
    + destruct p as [rs rt]. apply: sim_simple_result.
      split; first done. eapply (Hxswf (rs, rt)). done.
Ralf Jung's avatar
Ralf Jung committed
185
    + simpl. apply sim_simple_var.
Ralf Jung's avatar
Ralf Jung committed
186
  - (* Call *)
Ralf Jung's avatar
Ralf Jung committed
187 188
    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
189
    eapply sim_simple_post_mono, IHe; [|by auto..].
190
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval. simpl.
Ralf Jung's avatar
Ralf Jung committed
191 192 193 194 195
    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
196 197 198 199
    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
200
    apply: sim_simple_result=>Hval'.
201
    split; first done. auto.
Ralf Jung's avatar
Ralf Jung committed
202 203
  - (* InitCall: can't happen *) done.
  - (* EndCall: can't happen *) done.
Ralf Jung's avatar
Ralf Jung committed
204 205 206 207
  - (* 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..].
208
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval.
Ralf Jung's avatar
Ralf Jung committed
209 210 211
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
212
    intros r'' n' rs' rt' (-> & [Hrel' ?]%rrel_with_eq) Hval'.
Ralf Jung's avatar
Ralf Jung committed
213 214
    simplify_eq/=. eapply sim_simple_proj; [done..|].
    intros vi vv idx ?? Hidx ?. simplify_eq.
215
    split; first done.
Ralf Jung's avatar
Ralf Jung committed
216 217 218 219
    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
220 221 222 223
  - (* 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..].
224
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval.
Ralf Jung's avatar
Ralf Jung committed
225 226 227
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
228
    intros r'' n' rs' rt' (-> & [Hrel' ?]%rrel_with_eq) Hval'.
Ralf Jung's avatar
Ralf Jung committed
229 230
    simplify_eq/=. eapply sim_simple_conc; [done..|].
    intros v1 v2 ??. simplify_eq/=.
231
    split; first done. simpl.
Ralf Jung's avatar
Ralf Jung committed
232
    apply Forall2_app; auto.
Ralf Jung's avatar
Ralf Jung committed
233 234 235 236
  - (* 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..].
237
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval.
Ralf Jung's avatar
Ralf Jung committed
238 239 240
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
241
    intros r'' n' rs' rt' (-> & [Hrel' ?]%rrel_with_eq) Hval'.
Ralf Jung's avatar
Ralf Jung committed
242 243
    simplify_eq/=. eapply sim_simple_bin_op; [done..|].
    intros v1 v2 s ? ?? Heval. simplify_eq/=.
244
    split; first done. constructor; last done.
Ralf Jung's avatar
Ralf Jung committed
245 246 247 248 249
    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
250 251 252
  - (* Deref *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
253
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq).
Ralf Jung's avatar
Ralf Jung committed
254
    simplify_eq/=. apply: sim_simple_deref=>l t ?. simplify_eq/=.
255
    split; first done. done.
Ralf Jung's avatar
Ralf Jung committed
256 257 258
  - (* Ref *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
259
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq).
Ralf Jung's avatar
Ralf Jung committed
260
    simplify_eq/=. eapply sim_simple_ref=>l t ??. simplify_eq/=.
261
    split; first done. apply Hrel.
Ralf Jung's avatar
Ralf Jung committed
262 263 264
  - (* Copy *)
    move=>Hwf xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
265
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq).
Ralf Jung's avatar
Ralf Jung committed
266
    eapply sim_simple_valid_post.
267
    eapply sim_simple_copy_public; [by auto..|].
Ralf Jung's avatar
Ralf Jung committed
268
    intros r'' v1 v2 Hrel'' Hval. simplify_eq/=.
269
    split; first done. auto.
Ralf Jung's avatar
Ralf Jung committed
270 271 272 273
  - (* 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..].
274
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval.
Ralf Jung's avatar
Ralf Jung committed
275 276 277
    simplify_eq/=. sim_bind (subst_map _ e2) (subst_map _ e2).
    eapply sim_simple_frame_more_core.
    eapply sim_simple_post_mono, IHe2; [|by auto..].
278
    intros r'' n' rs' rt' (-> & [Hrel' ?]%rrel_with_eq) Hval'.
279
    simplify_eq/=. eapply sim_simple_write_public; [auto..|].
280
    split; first done. constructor; done.
Ralf Jung's avatar
Ralf Jung committed
281 282 283
  - (* Alloc *)
    move=>Hwf xs Hxswf /=.
    eapply sim_simple_valid_post.
284
    eapply sim_simple_alloc_public=>l tg /= Hval.
285
    split; first done.
Ralf Jung's avatar
Ralf Jung committed
286 287
    simpl. split; last done. constructor; last done.
    eapply arel_mono, arel_ptr; auto.
Hai Dang's avatar
Hai Dang committed
288 289 290 291 292
  - (* Free *)
    move=>Hwf xs Hxswf /=.
    sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
    intros r' n' rs rt (-> & Hrel). simpl.
Hai Dang's avatar
Hai Dang committed
293
    apply: sim_simple_free_public; eauto.
Ralf Jung's avatar
Ralf Jung committed
294 295 296 297 298 299 300
    split; first done. constructor; done.
  - (* Retag *)
    move=>Hwf xs Hxswf /=.
    sim_bind (subst_map _ e) (subst_map _ e).
    eapply sim_simple_post_mono, IHe; [|by auto..].
    intros r' n' rs rt (-> & Hrel). simpl.
    eapply sim_simple_retag_public; eauto.
Hai Dang's avatar
Hai Dang committed
301
    split; first done. constructor; done.
Ralf Jung's avatar
Ralf Jung committed
302
  - (* Let *)
Ralf Jung's avatar
Ralf Jung committed
303 304 305
    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..].
306
    intros r' n' rs rt (-> & Hrel) Hval. simpl.
Ralf Jung's avatar
Ralf Jung committed
307
    eapply sim_simple_let; [destruct rs, rt; by eauto..|].
308 309 310
    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
311
    eapply IHe2; [by auto..|].
Ralf Jung's avatar
Ralf Jung committed
312
    destruct b; first by auto. simpl.
Ralf Jung's avatar
Ralf Jung committed
313 314
    apply map_Forall_insert_2; first by auto.
    eapply srel_core_mono; eauto.
Ralf Jung's avatar
Ralf Jung committed
315 316 317 318
  - (* 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..].
319
    intros r' n' rs rt (-> & [Hrel ?]%rrel_with_eq) Hval.
Ralf Jung's avatar
Ralf Jung committed
320 321 322 323 324 325 326 327
    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
328
Qed.
Ralf Jung's avatar
Ralf Jung committed
329 330 331

End sem.

Ralf Jung's avatar
Ralf Jung committed
332
Theorem sim_mod_fun_refl f :
Ralf Jung's avatar
Ralf Jung committed
333
  expr_wf f.(fun_body) 
Ralf Jung's avatar
Ralf Jung committed
334 335
  ⊨ᶠ f  f.
Proof.
336 337
  intros Hwf. eapply (sim_fun_simple sem_steps); first done.
  intros fs ft r es et vs vt c Hlk Hrel Hsubst1 Hsubst2.
Hai Dang's avatar
Hai Dang committed
338 339
  (* eapply sim_simple_viewshift.
  { eapply viewshift_frame_l. eapply vs_call_empty_public. } *)
340
  eapply sim_simple_frame_r.
341
  destruct (subst_l_map _ _ _ _ _ _ _ (rrel r) Hsubst1 Hsubst2) as (map & -> & -> & Hmap).
342
  { clear -Hrel. induction Hrel; eauto using Forall2. }
343 344 345 346
  eapply sim_simple_post_mono; last exact: expr_wf_soundness.
  intros rr n rs rt [??] Hval. split.
  - solve_res.
  - eapply rrel_mono; [done| |done]. solve_res.
Ralf Jung's avatar
Ralf Jung committed
347
Qed.
Ralf Jung's avatar
Ralf Jung committed
348

349 350
Print Assumptions sim_mod_fun_refl.

Ralf Jung's avatar
Ralf Jung committed
351
Lemma sim_mod_funs_refl prog :
Ralf Jung's avatar
Ralf Jung committed
352
  prog_wf prog 
Ralf Jung's avatar
Ralf Jung committed
353 354
  sim_mod_funs prog prog.
Proof.
Ralf Jung's avatar
Ralf Jung committed
355
  intros [_ WF]. induction prog using map_ind.
Ralf Jung's avatar
Ralf Jung committed
356
  { intros ??. rewrite lookup_empty. done. }
Ralf Jung's avatar
Ralf Jung committed
357 358 359 360
  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.