Typing.v 40.4 KB
Newer Older
1
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets.
2
Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs Daisy.Infra.RationalSimps.
3
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
4

5
Fixpoint typeExpression (V:Type) (defVars:nat -> option mType) (e:exp V) : option mType :=
6
  match e with
7
  | Var _ v => defVars v
8
  | Const m n => Some m
9
  | Unop u e1 => typeExpression defVars e1
10
  | Binop b e1 e2 =>
11
12
    let tm1 := typeExpression defVars e1 in
    let tm2 := typeExpression defVars e2 in
13
14
15
16
17
    match tm1, tm2 with
    | Some m1, Some m2 => Some (computeJoin m1 m2)
    | _, _=> None
    end
  | Downcast m e1 =>
18
    let tm1 := typeExpression defVars e1 in
19
20
21
22
23
24
    match tm1 with
    |Some m1 => if (isMorePrecise m1 m) then Some m else None
    |_ => None
    end
  end.

25
Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mType :=
26
  match e with
27
  | Var _ v => if expEqBool e e' then defVars v else None
28
  | Const m n => if expEqBool e e' then Some m else None
29
30
  | Unop u e1 => if expEqBool e e' then typeExpression defVars e else typeMap defVars e1 e'
  | Binop b e1 e2 => if expEqBool e e' then typeExpression defVars e
31
                    else
32
33
34
35
36
                      match (typeMap defVars e1 e'), (typeMap defVars e2 e')  with
                      | Some m1, Some m2 => if (mTypeEqBool m1 m2) then Some m1 else None
                      | Some m1, None => Some m1
                      | None, Some m2 => Some m2
                      | None, None => None
37
                      end
38
  | Downcast m e1 => if expEqBool e e' then typeExpression defVars (Downcast m e1) else typeMap defVars e1 e'
39
40
  end.

41
42
(* todo: need both variable assignment in vartype and the map? *)
Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType :=
43
  match f with
44
  |Let m n e c => match typeExpression defVars e with
45
                 |Some m' => if mTypeEqBool m m' then typeCmd defVars (*(fun f => if (n =? f) then Some m else defVars f)*) c
46
47
48
                            else None
                 |None => None
                 end
49
  |Ret e => typeExpression defVars e 
50
51
  end.

52
Fixpoint typeMapCmd (defVars:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType :=
53
  match f with
54
  |Let m n e c => if expEqBool f' (Var Q n) then
55
56
57
58
                   match defVars n with
                   | Some m' => if mTypeEqBool m m' then Some m else None
                   | None => None
                   end
59
                  else
60
61
                    let te := typeMap defVars e in
                    let tc := typeMapCmd defVars c in
62
63
64
65
66
67
                    match (te f'), (tc f') with
                    |Some m1, Some m2 => if mTypeEqBool m1 m2 then Some m1 else None
                    |Some m1, None => Some m1
                    |None, Some m2 => Some m2
                    |None, None => None
                    end
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
  |Ret e => (typeMap defVars e) f'
  end.

Fixpoint typeCheck (e:exp Q) (defVars:nat -> option mType) (tMap: exp Q -> option mType) : bool :=
  match e with
  | Var _ v => match tMap e, defVars v with
              | Some m, Some m' => mTypeEqBool m m'
              | _, _ => false
             end
  | Const m n => match tMap e with
               | Some m' => mTypeEqBool m m'
               | None => false
               end
  | Unop u e1 => match tMap e with
                | Some m => match tMap e1 with
                           | Some m' => mTypeEqBool m m' && typeCheck e1 defVars tMap
                           | None => false
                           end
                | None => false
                end
  | Binop b e1 e2 => match tMap e, tMap e1, tMap e2 with
                    | Some m, Some m1, Some m2 =>
                      mTypeEqBool m (computeJoin m1 m2)
                                  && typeCheck e1 defVars tMap
                                  && typeCheck e2 defVars tMap
                    | _, _, _ => false
                    end
  | Downcast m e1 => match tMap e, tMap e1 with
                    | Some m', Some m1 => mTypeEqBool m m' && isMorePrecise m1 m && typeCheck e1 defVars tMap
                    | _, _ => false
                    end
99
100
  end.

101
102
103
Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> option mType) : bool :=
  match c with
  | Let m x e g => match tMap (Var Q x), tMap e with
104
                  | Some mx, Some me => (mTypeEqBool mx m) && (mTypeEqBool mx me) && typeCheck e defVars tMap && typeCheckCmd g defVars tMap
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
                  | _, _ => false
                  end
  | Ret e => typeCheck e defVars tMap
  end.

Lemma eqTypeExpression e m defVars:
  typeMap defVars e e = Some m <-> typeExpression defVars e = Some m.
Proof.
  revert m defVars; induction e; intros.
  - split; intros.
    + simpl in *.
      rewrite <- beq_nat_refl in H; simpl in H; auto.
    + simpl in *.
      rewrite <- beq_nat_refl; simpl; auto.
  - split; intros; simpl in *.
    + rewrite mTypeEqBool_refl,Qeq_bool_refl in H; simpl in H; auto.
    + rewrite mTypeEqBool_refl,Qeq_bool_refl; simpl; auto.
  - split; intros; simpl in *.
    + rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto.
    + rewrite unopEqBool_refl,expEqBool_refl; simpl; auto.
  - split; intros; simpl in *.
    + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto.
    + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl; simpl; auto.
  - split; intros; simpl in *.
    + rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto.
    + rewrite mTypeEqBool_refl,expEqBool_refl; simpl; auto.
Qed.

Definition Gamma_stronger (Gamma1 Gamma2: exp Q -> option mType):=
  (forall e m, Gamma1 e = Some m -> Gamma2 e = Some m).

Lemma Gamma_stronger_trans Gamma1 Gamma2 Gamma3 :
  Gamma_stronger Gamma1 Gamma2 ->
  Gamma_stronger Gamma2 Gamma3 ->
  Gamma_stronger Gamma1 Gamma3.
Proof.
  intros g12 g23 e m hyp.
  unfold Gamma_stronger in g12,g23.
  apply g23; apply g12; auto.
Qed.
='s avatar
= committed
145
146
  

147
148
149
150
Lemma Gamma_strengthening e Gamma1 Gamma2 defVars:
  Gamma_stronger Gamma1 Gamma2 ->
  typeCheck e defVars Gamma1 = true ->
  typeCheck e defVars Gamma2 = true.
151
Proof.
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
  revert Gamma1 Gamma2; induction e; intros.
  - simpl in *.
    case_eq (Gamma1 (Var Q n)); intros; rewrite H1 in H0; [ | inversion H0 ].
    specialize (H _ _ H1); rewrite H.
    auto.
  - simpl in *.
    case_eq (Gamma1 (Const m v)); intros; rewrite H1 in H0; [ | inversion H0 ].
    specialize (H _ _ H1); rewrite H.
    auto.
  - simpl in *.
    case_eq (Gamma1 (Unop u e)); intros; rewrite H1 in H0; [ | inversion H0 ].
    rewrite (H _ _ H1). 
    case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ].
    apply andb_true_iff in H0; destruct H0.
    apply EquivEqBoolEq in H0; subst.
    rewrite (H _ _ H2).
    rewrite mTypeEqBool_refl; simpl.
    eapply IHe; eauto.
  - simpl in *.
    case_eq (Gamma1 (Binop b e1 e2)); intros; rewrite H1 in H0; [ | inversion H0 ].
    case_eq (Gamma1 e1); intros; rewrite H2 in H0; [ | inversion H0 ].
    case_eq (Gamma1 e2); intros; rewrite H3 in H0; [ | inversion H0 ].
    rewrite (H _ _ H1), (H _ _ H2), (H _ _ H3).
    andb_to_prop H0.
    rewrite L0; simpl.
    apply andb_true_iff; split.
    + eapply IHe1; eauto.
    + eapply IHe2; eauto.
  - simpl in *.
    case_eq (Gamma1 (Downcast m e)); intros; rewrite H1 in H0; [ | inversion H0 ].
    case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ].
    rewrite (H _ _ H1), (H _ _ H2).
    andb_to_prop H0.
    rewrite L0, R0; simpl.
    eapply IHe; eauto.
187
188
Qed.

189
190
191
192
193
194
195
196
197
198
199
200
201
(* Lemma typeMapUnopUnfolding u e e0 defVars m0: *)
(*   typeMap defVars (Unop u e) e0 = Some m0 -> *)
(*   expEqBool (Unop u e) e0 = false -> *)
(*   typeMap defVars e e0 = Some m0. *)
(* Proof. *)
(*   revert e e0 m0; destruct e0; intros. *)
(*   - simpl in H; auto. *)
(*   - simpl in H; auto. *)
(*   - simpl in H, H0; rewrite H0 in H; auto. *)
(*   - simpl in H; auto. *)
(*   - simpl in H; auto. *)
(* Qed. *)

='s avatar
= committed
202

203
204
205
206
207
208
209
210
211
212
(* Lemma typeCheckLeftUnfolding Gamma u e defVars: *)
(*   typeCheck (Unop u e) defVars Gamma = true -> *)
(*   typeCheck e defVars Gamma = true. *)
(* Proof. *)
(*   intros tc_u. *)
(*   simpl in *. *)
(*   case_eq (Gamma (Unop u e)); intros; rewrite H in tc_u; [ | inversion tc_u ]. *)
(*   case_eq (Gamma e); intros; rewrite H0 in tc_u; [ | inversion tc_u ]. *)
(*   apply andb_true_iff in tc_u; destruct tc_u; auto. *)
(* Qed. *)
='s avatar
= committed
213

214

215
216
217
218
219
220
221
222
223
(* Lemma typeMapUnopStrenghtening u defVars e: *)
(*   Gamma_stronger (typeMap defVars e) (typeMap defVars (Unop u e)). *)
(* Proof. *)
(*   intros e0 m0 hyp. *)
(*   simpl. *)
(*   assert (expEqBool (Unop u e) e0 = false) by admit. *)
(*   simpl in H; rewrite H. *)
(*   auto. *)
(* Admitted. *)
='s avatar
= committed
224
  
225

226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
(* Lemma typeMapBinopStrengthening_l b defVars e1 e2: *)
(*   Gamma_stronger (typeMap defVars e1) (typeMap defVars (Binop b e1 e2)). *)
(* Proof. *)
(*   intros e0 m0 hyp. *)
(*   simpl. *)
(*   (*case_eq (expEqBool (Binop b e1 e2) e0); intros; simpl in H; rewrite H.*) *)
(*   assert (expEqBool (Binop b e1 e2) e0 = false) by admit. *)
(*   simpl in H; rewrite H, hyp; auto. *)
(* Admitted. *)


(* Lemma typeMapBinopStrengthening_r b defVars e1 e2: *)
(*   Gamma_stronger (typeMap defVars e2) (typeMap defVars (Binop b e1 e2)). *)
(* Proof. *)
(*   intros e0 m0 hyp. *)
(*   simpl. *)
(*   (*case_eq (expEqBool (Binop b e1 e2) e0); intros; simpl in H; rewrite H.*) *)
(*   assert (expEqBool (Binop b e1 e2) e0 = false) by admit. *)
(*   simpl in H; rewrite H, hyp; auto. *)
(* Admitted. *)

247

248
249
250
251
252
Theorem typingSoundnessExp e defVars E:
  forall v m Gamma,
    typeCheck e defVars Gamma = true ->
    eval_exp E defVars (toRExp e) v m ->
    Gamma e = Some m.
253
Proof.
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
  revert e; induction e; intros * (*gamma_def*) typechecks evals.
  - simpl in typechecks.
    inversion evals; subst.
    rewrite H0 in typechecks.
    case_eq (Gamma (Var Q n)); intros; rewrite H in typechecks; [ | inversion typechecks ].
    apply EquivEqBoolEq in typechecks; subst; auto.
  - simpl in typechecks.
    inversion evals; subst.
    case_eq (Gamma (Const m0 v)); intros; rewrite H in typechecks; [ | inversion typechecks ].
    apply EquivEqBoolEq in typechecks; subst; auto.
  - simpl in typechecks.
    case_eq (Gamma (Unop u e)); intros; rewrite H in typechecks; [ | inversion typechecks ].
    case_eq (Gamma e); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
    apply andb_true_iff in typechecks; destruct typechecks.
    apply EquivEqBoolEq in H1; subst.
    inversion evals; subst.
    + rewrite <- H0.
      eapply IHe; eauto.
    + rewrite <- H0.
      eapply IHe; eauto.
  - inversion evals; subst.
    simpl in typechecks.
    case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in typechecks; [ | inversion typechecks ].
    case_eq (Gamma e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
    case_eq (Gamma e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ].
    andb_to_prop typechecks.
    apply EquivEqBoolEq in L0; subst.
    assert (Gamma e1 = Some m1) by (eapply IHe1; eauto).
    assert (Gamma e2 = Some m2) by (eapply IHe2; eauto).
    rewrite H0 in H4. rewrite H1 in H5.
    inversion H4; inversion H5; subst; auto.
  - simpl in typechecks.
    case_eq (Gamma (Downcast m e)); intros; rewrite H in typechecks; [ | inversion typechecks ].
    case_eq (Gamma e); intros; rewrite H0 in typechecks; [ | inversion typechecks ].
    andb_to_prop typechecks.
    apply EquivEqBoolEq in L0; subst.
    inversion evals; subst.
291
292
293
    auto.
Qed.

294
295
296
297
Theorem typingSoundnessCmd c defVars E v m Gamma:
  typeCheckCmd c defVars Gamma = true ->
  bstep (toRCmd c) E defVars v m ->
  (*(typeMapCmd defVars c)*) Gamma (getRetExp c) = Some m.
298
Proof.
299
  revert E defVars; induction c; intros * tc bc.
300
301
302
303
  - simpl in tc.
    case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ].
    case_eq (Gamma e); intros; rewrite H0 in tc; [ | inversion tc ].
    andb_to_prop tc.
304
    apply EquivEqBoolEq in L; apply EquivEqBoolEq in R1; subst.
305
    simpl.
306
307
308
309
310
    inversion bc; subst.
    eapply IHc; eauto.
  - simpl in *.
    inversion bc; subst.
    eapply typingSoundnessExp; eauto.
311
Qed.
312

313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
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
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
Lemma stupidlemma e defVars Gamma:
  typeCheck e defVars Gamma = true ->
  exists m, Gamma e = Some m.
Proof.
  destruct e; intros * tc.
  - simpl in *.
    case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ].
    eauto.
  - simpl in *.
    case_eq (Gamma (Const m q)); intros; rewrite H in tc; [ | inversion tc ].
    eauto.
  - simpl in *.
    case_eq (Gamma (Unop u e)); intros; rewrite H in tc; [ | inversion tc ].
    eauto.
  - simpl in *; 
    case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
  - simpl in *; 
      case_eq (Gamma (Downcast m e)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
Qed.

Fixpoint defVarsWellDefined (e:exp Q) (defVars:nat -> option mType) : bool :=
  NatSet.for_all (fun v => match defVars v with | Some m => true | _ => false end) (usedVars e).

Fixpoint defVarsWellDefinedCmd c defVars : bool :=
  match c with
  | Let m x e g => match defVars x with
                  | Some m' => mTypeEqBool m m' && defVarsWellDefined e defVars && defVarsWellDefinedCmd g defVars
                  | _ => false
                  end
  | Ret e => defVarsWellDefined e defVars
  end.

(* Theorem typeExpressionChecks e defVars: *)
(*   defVarsWellDefined e defVars = true -> *)
(*   typeCheck e defVars (fun e => typeExpression defVars e) = true. *)
(* Proof. *)
(*   intros defVars_wd. induction e. *)
(*   - simpl in *. *)
(*     apply NatSet.for_all_spec in defVars_wd; try auto. *)
(*     Focus 2. intros a b c; rewrite c; auto. *)
(*     specialize (defVars_wd n). *)
(*     rewrite NatSet.singleton_spec in defVars_wd. *)
(*     assert (n = n) by auto; specialize (defVars_wd H). *)
(*     case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *)
(*     rewrite mTypeEqBool_refl; auto. *)
(*   - simpl. *)
(*     rewrite mTypeEqBool_refl; auto. *)
(*   - simpl in *. *)
(*     assert (defVarsWellDefined e defVars = true) by admit. *)
(*     specialize (IHe H). *)
(*     pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *)
(*     rewrite type_e, mTypeEqBool_refl; simpl. *)
(*     auto. *)
(*   - simpl in *. *)
(*     assert (defVarsWellDefined e1 defVars = true) by admit. *)
(*     specialize (IHe1 H). *)
(*     assert (defVarsWellDefined e2 defVars = true) by admit. *)
(*     specialize (IHe2 H0). *)
(*     pose proof (stupidlemma _ _ _ IHe1) as [me1 type_e1]. *)
(*     pose proof (stupidlemma _ _ _ IHe2) as [me2 type_e2]. *)
(*     rewrite type_e1,type_e2,mTypeEqBool_refl; simpl; auto. *)
(*     rewrite IHe1, IHe2; auto. *)
(*   -  *)
(*     unfold typeCheck. *)
    

(*     simpl in *. *)
(*     assert (defVarsWellDefined e defVars = true) by admit. *)
(*     specialize (IHe H). *)
(*     pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *)
(*     rewrite type_e. *)
(*     assert (typeExpression defVars (Downcast m e) = Some m). *)
(*     { simpl; rewrite type_e. *)

    

  
(* Theorem typeMapChecks e defVars: *)
(*   defVarsWellDefined e defVars = true ->  *)
(*   (*(forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) ->*) *)
(*   typeCheck e defVars (typeMap defVars e) = true. *)
(* Proof. *)
(*   intros defVars_wd; induction e; intros. *)
(*   - simpl in *; rewrite <- beq_nat_refl. *)
(*     rewrite NatSet.for_all_spec in defVars_wd. *)
(*     + unfold NatSet.For_all in defVars_wd. *)
(*       specialize (defVars_wd n). *)
(*       rewrite NatSet.singleton_spec in defVars_wd. *)
(*       assert (n = n) by auto; specialize (defVars_wd H). *)
(*       case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *)
(*       rewrite mTypeEqBool_refl; auto. *)
(*     + intros a b hyp; rewrite hyp; auto. *)
(*   - simpl in *. *)
(*     rewrite mTypeEqBool_refl, Qeq_bool_refl; simpl. *)
(*     rewrite mTypeEqBool_refl; auto. *)
(*   - simpl. *)
(*     rewrite unopEqBool_refl, expEqBool_refl; simpl. *)
(*     assert (defVarsWellDefined e defVars = true) by admit. *)
(*     specialize (IHe H). *)
(*     pose proof (stupidlemma _ _ _ IHe) as [m type_e]. *)
(*     apply  eqTypeExpression in type_e. *)
(*     rewrite type_e. *)
(*     case_eq (expEqBool (Unop u e) e); intros; simpl in H0; rewrite H0. *)
(*     + admit. *)
(*     + apply eqTypeExpression in type_e; rewrite type_e. *)
(*       rewrite mTypeEqBool_refl; simpl. *)
(*       eapply Gamma_strengthening. *)
(*       Focus 2. eapply IHe. *)
(*       intros e0 m0 type_e0. *)
(*       case_eq (expEqBool (Unop u e) e0); intros; simpl in H1; rewrite H1. *)
(*       * admit. *)
(*       * auto. *)
(*   - unfold typeCheck. *)
(*     assert (defVarsWellDefined e1 defVars = true) by admit. *)
(*     assert (defVarsWellDefined e2 defVars = true) by admit. *)
(*     specialize (IHe1 H). *)
(*     specialize (IHe2 H0). *)
(*     pose proof (stupidlemma _ _ _ IHe1) as [m1 tMap_e1]. *)
(*     pose proof (stupidlemma _ _ _ IHe2) as [m2 tMap_e2]. *)
(*     assert (typeMap defVars (Binop b e1 e2) (Binop b e1 e2) = Some (computeJoin m1 m2)) as tMap_binop. *)
(*     { simpl; rewrite binopEqBool_refl,?expEqBool_refl; simpl. *)
(*       rewrite eqTypeExpression in tMap_e1, tMap_e2. *)
(*       rewrite tMap_e1, tMap_e2. *)
(*       auto. } *)
(*     rewrite tMap_binop. *)
(*     assert (typeMap defVars (Binop b e1 e2) e1 = Some m1). *)
(*     { simpl.  *)
(*       assert (expEqBool (Binop b e1 e2) e1 = false) by admit; simpl in H1; rewrite H1. *)
(*       rewrite tMap_e1. *)
(* Admitted. *)


(* Theorem typeMapCmdChecks c defVars: *)
(*   defVarsWellDefinedCmd c defVars = true -> *)
(*   typeCheckCmd c defVars (typeMapCmd defVars c) = true. *)
(* Proof. *)
(*   intros defVars_wd; induction c; intros. *)
(*   - unfold typeCheckCmd. *)
(*     assert (typeMapCmd defVars (Let m n e c) (Var Q n) = Some m). *)
(*     { unfold typeMapCmd.  simpl; rewrite <- beq_nat_refl.  *)
(*       simpl in defVars_wd. *)
(*       case_eq (defVars n); intros; rewrite H in defVars_wd; [ | inversion defVars_wd ]. *)
(*       andb_to_prop defVars_wd. *)
(*       rewrite L0; simpl; auto. } *)
(*     rewrite H. *)
(*     assert (typeMapCmd defVars (Let m n e c) e = Some m). *)
(*     { simpl. *)
(*       case_eq (expEqBool e (Var Q n)); intros. *)
(*       - admit. *)
(*       -  *)
(* Admitted. *)


        
  
(* Theorem typeMapChecks2 e defVars Gamma: *)
(*   (forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) -> *)
(*   Gamma_stronger (typeMap defVars e) Gamma -> *)
(*   typeCheck e defVars Gamma = true. *)
(* Proof. *)
(*   intros defVars_wd gamma_st. *)
(*   induction e; intros. *)
(*   - simpl. *)
(*     unfold Gamma_stronger in gamma_st. *)
(*     specialize (gamma_st (Var Q n)); simpl in gamma_st. *)
(*     rewrite <- beq_nat_refl in gamma_st. *)
(*     simpl in defVars_wd. *)
(*     specialize (defVars_wd n). *)
(*     rewrite NatSet.singleton_spec in defVars_wd. *)
(*     assert (n = n) by auto. *)
(*     specialize (defVars_wd H). *)
(*     destruct defVars_wd as [m defVars_wd]. *)
(*     rewrite defVars_wd. *)
(*     specialize (gamma_st _ defVars_wd). *)
(*     rewrite gamma_st. *)
(*     apply mTypeEqBool_refl. *)
(*   - simpl. *)
(*     unfold Gamma_stronger in gamma_st. *)
(*     specialize (gamma_st (Const m v)); simpl in gamma_st.     *)
(*     rewrite mTypeEqBool_refl, Qeq_bool_refl in gamma_st; simpl in gamma_st. *)
(*     specialize (gamma_st m). *)
(*     assert (Some m = Some m) by auto. *)
(*     rewrite (gamma_st H). *)
(*     rewrite mTypeEqBool_refl; auto. *)
(*   - simpl. *)
(*     simpl in defVars_wd. *)
(*     specialize (IHe defVars_wd). *)
(*     assert (Gamma_stronger (typeMap defVars e) Gamma). *)
(*     {  *)
(*       eapply Gamma_stronger_trans; eauto. *)
(*       intros e0 m0 typemap_e. *)
(*       simpl. *)
(*       case_eq (expEqBool (Unop u e) e0); intros; simpl in H; rewrite H. *)
(*       + admit.  *)
(*       + auto. } *)
(*     specialize (IHe H); rewrite IHe; simpl. *)
(*     unfold Gamma_stronger in gamma_st. *)
(*     specialize (gamma_st (Unop u e)); simpl in gamma_st. *)
(*     rewrite unopEqBool_refl, expEqBool_refl in gamma_st; simpl in gamma_st. *)
(*     unfold Gamma_stronger in H. *)
(*     pose proof (stupidlemma _ _  _ IHe) as [m type_e]. *)
(*     rewrite type_e. *)
(*     apply  eqTypeExpression in type_e. *)
(*     rewrite type_e. *)
(*     case_eq (expEqBool (Unop u e) e); intros; simpl in H; rewrite H. *)
(*     + admit. *)
(*     + apply eqTypeExpression in type_e; rewrite type_e. *)
(*       rewrite mTypeEqBool_refl; simpl. *)



    


527
528
529
(* Lemma typeMapVarDet e m m' v: *)
(*   typeMap e (Var Q m v) = Some m' -> *)
(*   m = m'. *)
='s avatar
= committed
530
(* Proof. *)
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
(*   revert e; induction e; intros. *)
(*   - simpl in H. *)
(*     case_eq (mTypeEqBool m0 m && (n =? v)); intros; rewrite H0 in H. *)
(*     apply andb_true_iff in H0; destruct H0. *)
(*     inversion H; subst. *)
(*     apply EquivEqBoolEq in H0; subst; auto. *)
(*     inversion H. *)
(*   - simpl in H. inversion H. *)
(*   - simpl in H. apply IHe; auto. *)
(*   - simpl in H. *)
(*     case_eq (typeMap e1 (Var Q m v)); intros; rewrite H0 in H. *)
(*     + inversion H; subst. *)
(*       apply IHe1; auto. *)
(*     + apply IHe2; auto. *)
(*   - simpl in H. apply IHe; auto. *)
='s avatar
= committed
546
(* Qed. *)
547

548
549
550
(* Lemma typeGivesTypeMap e m : *)
(*   typeExpression e  = Some m -> *)
(*   typeMap e e = Some m. *)
='s avatar
= committed
551
(* Proof. *)
552
553
554
555
556
557
558
559
560
561
562
563
(*   intros; induction e; simpl in *; auto. *)
(*   - rewrite mTypeEqBool_refl, <- beq_nat_refl; simpl; auto.  *)
(*   - rewrite mTypeEqBool_refl. *)
(*     assert (Qeq_bool v v = true) by (apply Qeq_bool_iff; lra). *)
(*     rewrite H0; simpl; auto. *)
(*   - assert (unopEqBool u u = true) by (destruct u; auto). *)
(*     rewrite H0, expEqBool_refl; simpl; auto. *)
(*   - pose proof (expEqBool_refl (Binop b e1 e2)). *)
(*     simpl in H0; rewrite H0. *)
(*     auto. *)
(*   - rewrite mTypeEqBool_refl,expEqBool_refl. *)
(*     simpl; auto. *)
='s avatar
= committed
564
(* Qed. *)
565

566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
(* Lemma typeMap_gives_type: *)
(*   forall e m, *)
(*     typeMap e e = Some m -> *)
(*     typeExpression e = Some m. *)
(* Proof. *)
(*   intros e; induction e; intros; simpl in *; try auto. *)
(*   - rewrite mTypeEqBool_refl in H. *)
(*     rewrite <- beq_nat_refl in H. simpl in *. auto. *)
(*   - assert (Qeq_bool v v = true) as Qeq_bool_refl by (apply Qeq_bool_iff; lra). *)
(*     rewrite Qeq_bool_refl,mTypeEqBool_refl in H. *)
(*     simpl in H; auto. *)
(*   - assert (unopEqBool u u = true) as unopEqBool_refl by (destruct u; auto). *)
(*     rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(*   - assert (binopEqBool b b = true) as binopEqBool_refl by (destruct b; auto). *)
(*     rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(*   - rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto. *)
(* Qed. *)
583

584
585
(* Lemma unop_neq u e: *)
(*   expEqBool (Unop u e) e = true -> False . *)
='s avatar
= committed
586
(* Proof. *)
587
588
589
590
591
(*   induction e; intros; simpl in *; try congruence. *)
(*   case_eq ( unopEqBool u u0); intros; rewrite H0 in *; simpl in *; try congruence. *)
(*   apply IHe. *)
(*   assert (u = u0) by (destruct u; destruct u0; cbv in H0; inversion H0; auto). *)
(*   subst. auto. *)
='s avatar
= committed
592
(* Qed. *)
593

594
595
596
597
598
599
600
601
602
603
604
(* Lemma t e u m: *)
(*   typeMap e e = Some m -> *)
(*   typeMap (Unop u e) e = Some m. *)
(* Proof. *)
(*   intros. *)
(*   simpl. destruct e; try auto. *)
(*   case_eq (expEqBool (Unop u0 e) e); intros case_exp. *)
(*   - exfalso. eapply unop_neq; eauto.  *)
(*   - rewrite andb_false_r. *)
(*     assumption. *)
(* Qed. *)
605

606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
(* Inductive validType (Gamma:exp Q -> option mType) : exp Q -> mType -> Prop := *)
(* |tVar m v: *)
(*    Gamma (Var Q m v) = Some m -> validType Gamma (Var Q m v) m *)
(* |tConst m n: *)
(*    Gamma (Const m n) = Some m -> validType Gamma (Const m n) m *)
(* |tUnop u e1 m: *)
(*    validType Gamma e1 m -> *)
(*    Gamma (Unop u e1) = Some m -> *)
(*    validType Gamma (Unop u e1) m *)
(* |tBinop b e1 e2 m m1 m2: *)
(*    validType Gamma e1 m1 -> *)
(*    validType Gamma e2 m2 -> *)
(*    m = computeJoin m1 m2 -> *)
(*    Gamma (Binop b e1 e2) = Some m -> *)
(*    validType Gamma (Binop b e1 e2) m *)
(* |tDowncast m e1 m1: *)
(*    validType Gamma e1 m1 -> *)
(*    isMorePrecise m1 m = true -> *)
(*    Gamma (Downcast m e1) = Some m -> *)
(*    validType Gamma (Downcast m e1) m. *)
   
(* Lemma valid_typing e m: *)
(*   typeExpression e = Some m -> *)
(*   validType (fun e => typeExpression e) e m. *)
='s avatar
= committed
630
(* Proof. *)
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
(*   revert m; induction e; intros; simpl in *. *)
(*   - inversion H; constructor; auto. *)
(*   - inversion H; constructor; auto. *)
(*   - constructor; simpl; auto. *)
(*   - case_eq (typeExpression e1); intros; rewrite H0 in H; [ | inversion H ]. *)
(*     case_eq (typeExpression e2); intros; rewrite H1 in H; inversion H; subst. *)
(*     specialize (IHe1 _ H0). specialize (IHe2 _ H1). *)
(*     econstructor; try eauto. *)
(*     simpl; rewrite H0, H1; auto. *)
(*   - case_eq (typeExpression e); intros; rewrite H0 in H; [| inversion H]. *)
(*     case_eq (isMorePrecise m1 m); intros; rewrite H1 in H; [| inversion H]. *)
(*     inversion H; subst. *)
(*     econstructor; try eauto. *)
(*     simpl; rewrite H0,H1; auto. *)
(* Qed. *)
646

647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662

(* Inductive validTypeCmd (Gamma:exp Q -> option mType) : cmd Q -> mType -> Prop := *)
(* |tRet m e: *)
(*    validType Gamma e m -> validTypeCmd Gamma (Ret e) m *)
(* |tLet m x e c mc: *)
(*    validType Gamma e m -> *)
(*    validType Gamma (Var Q m x) m -> *)
(*    validTypeCmd Gamma c mc -> *)
(*    validTypeCmd Gamma (Let m x e c) mc. *)

  

(* Lemma Gamma_strengthening e m Gamma1 Gamma2: *)
(*   (forall e m, Gamma1 e = Some m -> Gamma2 e = Some m ) -> *)
(*   validType Gamma1 e m -> *)
(*   validType Gamma2 e m. *)
='s avatar
= committed
663
(* Proof. *)
664
665
666
667
668
(*   revert Gamma1 Gamma2 m; induction e; *)
(*     intros; *)
(*     inversion H0; subst; *)
(*       econstructor; eauto. *)
(* Qed. *)
669

670
671
672
673
674
675
676
677
678
679
680
(* Definition GammaStronger (Gamma1 Gamma2:exp Q -> option mType):= *)
(*   forall e m, Gamma1 e = Some m -> Gamma2 e = Some m. *)



(* Lemma binop_neq_l b e1 e2: *)
(*   expEqBool (Binop b e1 e2) e1 = false. *)
(* Admitted. *)
  
(* Lemma binop_neq_r b e1 e2: *)
(*   expEqBool (Binop b e1 e2) e2 = false. *)
='s avatar
= committed
681
(* Admitted. *)
682

683
684
(* Lemma downcast_neq m e: *)
(*   expEqBool (Downcast m e) e = false. *)
='s avatar
= committed
685
(* Admitted. *)
686

687
688
689
(* Lemma typeExpressionIsSound E e v m: *)
(*   eval_exp E (toRExp e) v m -> *)
(*   typeExpression e = Some m. *)
='s avatar
= committed
690
(* Proof. *)
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
(*   revert v m; induction e; intros * eval_e. *)
(*   - simpl.  inversion eval_e; subst; auto. *)
(*   - simpl. inversion eval_e; subst; auto. *)
(*   - simpl. *)
(*     inversion eval_e; subst. *)
(*     + eapply IHe; eauto. *)
(*     + eapply IHe; eauto. *)
(*   - simpl. *)
(*     inversion eval_e; subst. *)
(*     specialize (IHe1 _ _ H3). *)
(*     specialize (IHe2 _ _ H6). *)
(*     rewrite IHe1, IHe2. *)
(*     auto. *)
(*   - inversion eval_e; subst; simpl. *)
(*     specialize (IHe _ _ H5); rewrite IHe. *)
(*     rewrite H1; auto. *)
(* Qed. *)
    

710

711
712
(* Lemma validTypeMap e m vF E2: *)
(*   eval_exp E2 (toRExp e) vF m ->  validType (typeMap e) e m. *)
='s avatar
= committed
713
(* Proof. *)
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
(*   revert m vF; induction e; intros * eval_e. *)
(*   - inversion eval_e; subst. *)
(*     econstructor; eauto. *)
(*     unfold typeMap; rewrite expEqBool_refl; auto. *)
(*   - inversion eval_e; subst. *)
(*     econstructor; eauto. *)
(*     unfold typeMap; rewrite expEqBool_refl; auto. *)
(*   - inversion eval_e; subst. *)
(*     + specialize (IHe _ _ H3). *)
(*       econstructor; eauto.  *)
(*       * eapply Gamma_strengthening; auto. *)
(*         Focus 2. eauto. *)
(*         intros. unfold typeMap. *)
(*         assert (expEqBool (Unop Neg e) e0 = false) by admit. *)
(*         rewrite H0; auto. *)
(*       * simpl; rewrite expEqBool_refl. *)
(*         eapply typeExpressionIsSound; eauto. *)
(*     + specialize (IHe _ _ H4). *)
(*       econstructor; eauto. *)
(*       * eapply Gamma_strengthening; auto. *)
(*         Focus 2. eauto. *)
(*         intros. unfold typeMap. *)
(*         assert (expEqBool (Unop Inv e) e0= false) by admit. *)
(*         rewrite H0; auto. *)
(*       * simpl; rewrite expEqBool_refl. *)
(*         eapply typeExpressionIsSound; eauto. *)
(*   - inversion eval_e; subst. *)
(*     econstructor; eauto. *)
(*     + specialize (IHe1 _ _ H3). *)
(*       eapply Gamma_strengthening. *)
(*       Focus 2. eapply IHe1. *)
(*       intros. unfold typeMap.  *)
(*       assert (expEqBool (Binop b e1 e2) e = false) by admit. *)
(*       rewrite H0. *)
(*       unfold typeMap in H; rewrite H. *)
(*       auto. *)
(*     + specialize (IHe2 _ _ H6). *)
(*       eapply Gamma_strengthening. *)
(*       Focus 2. eapply IHe2. *)
(*       intros. unfold typeMap.  *)
(*       assert (expEqBool (Binop b e1 e2) e = false) by admit. *)
(*       rewrite H0. *)
(*       unfold typeMap in H; rewrite H. *)
(*       case_eq (typeMap e1 e); intros; unfold typeMap in H1; rewrite H1. *)
(*       * (* todo: need to change typeMap *) admit. *)
(*       * auto. *)
(*     + unfold typeMap; rewrite expEqBool_refl. *)
(*         eapply typeExpressionIsSound; eauto. *)
(*   - inversion eval_e; subst. *)
(*     econstructor; eauto. *)
(*     + eapply Gamma_strengthening. *)
(*       Focus 2. eapply IHe; eauto. *)
(*       intros. unfold typeMap. *)
(*       assert (expEqBool (Downcast m0 e) e0 = false) by admit. *)
(*       rewrite H0. *)
(*       unfold typeMap in H. auto. *)
(*     + unfold typeMap; rewrite expEqBool_refl. *)
(*       eapply typeExpressionIsSound; eauto. *)
='s avatar
= committed
772
(* Admitted. *)
773

774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
(* Lemma typeCmdIsSound f E v m cont: *)
(*   bstep (toRCmd f) E v m -> typeCmd f cont  = Some m. *)
(* Proof. *)
(*   revert cont E v m; induction f; intros. *)
(*   - inversion H; subst. *)
(*     specialize (IHf (fun n' => if n =? n' then Some m else cont n') _ _ _ H8). *)
(*     simpl. *)
(*     pose proof (typeExpressionIsSound _ H7) as t_e; rewrite t_e. *)
(*     rewrite mTypeEqBool_refl. *)
(*     rewrite IHf. *)
(*     auto. *)
(*   - simpl. *)
(*     inversion H; subst. *)
(*     eapply typeExpressionIsSound; eauto. *)
(* Qed. *)
    
(* Lemma typeMapCmdValid f E v m: *)
(*   bstep (toRCmd f) E v m -> validTypeCmd (typeMapCmd f) f m. *)
='s avatar
= committed
792
(* Proof. *)
793
794
795
796
797
798
799
800
801
802
803
(*   revert E v m; induction f; intros * bstep_f. *)
(*   - inversion bstep_f; subst. *)
(*     econstructor; eauto. *)
(*     + pose proof (validTypeMap _ H6). *)
(*       eapply Gamma_strengthening. *)
(*       Focus 2. eapply H. *)
(*       intros.  simpl. rewrite H0. *)
(*       case_eq (expEqBool e0 (Var Q m n)); intros eq_e_varn. *)
(*       * admit. *)
(*       * admit. *)
(*     + econstructor; eauto. *)
='s avatar
= committed
804
(* Admitted. *)
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004

(* (* Fixpoint isSubExpression (e':exp Q) (e:exp Q) := *) *)
(* (*   orb (expEqBool e e') *) *)
(* (*       (match e with *) *)
(* (*        |Var _ _ _ => false *) *)
(* (*        |Const _ _ => false  *) *)
(* (*        |Unop o1 e1 => isSubExpression e' e1 *) *)
(* (*        |Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2) *) *)
(* (*        |Downcast m e1 => isSubExpression e' e1 *) *)
(* (*        end). *) *)

(* (* Lemma eqImpliesSub e e': *) *)
(* (*   expEqBool e' e = true -> isSubExpression e e' = true. *) *)
(* (* Proof. *) *)
(* (*   revert e e'; destruct e'; intros; simpl in *; rewrite H; auto. *) *)
(* (* Qed. *) *)

(* (* Lemma typeMapSubExpr e e' m: *) *)
(* (*   typeMap e e' = Some m -> isSubExpression e' e = true. *) *)
(* (* Proof. *) *)
(* (*   revert e e' m; induction e; intros. *) *)
(* (*   - unfold typeMap in H. *) *)
(* (*     case_eq (expEqBool (Var Q m n) e'); intros; rewrite H0 in H; inversion H; subst. *) *)
(* (*     apply eqImpliesSub; auto. *) *)
(* (*   - unfold typeMap in H. *) *)
(* (*     case_eq (expEqBool (Const m v) e'); intros hyp_if; rewrite hyp_if in H; inversion H; subst. *) *)
(* (*     apply eqImpliesSub; auto. *) *)
(* (*   - unfold typeMap in H. *) *)
(* (*     case_eq (expEqBool (Unop u e) e'); intros hyp_if; rewrite hyp_if in H.  *) *)
(* (*     + apply eqImpliesSub; auto. *) *)
(* (*     + specialize (IHe _ _ H). *) *)
(* (*       simpl. *) *)
(* (*       rewrite IHe; auto; apply orb_true_r. *) *)
(* (*   - unfold typeMap in H. *) *)
(* (*     case_eq (expEqBool (Binop b e1 e2) e'); intros hyp_if; rewrite hyp_if in H. *) *)
(* (*     + apply eqImpliesSub; auto. *) *)
(* (*     + case_eq (typeMap e1 e'); intros; unfold typeMap in H0; rewrite H0 in H. *) *)
(* (*       * inversion H; subst. *) *)
(* (*         specialize (IHe1 _ _ H0). *) *)
(* (*         simpl; rewrite IHe1; simpl; apply orb_true_r. *) *)
(* (*       * case_eq (typeMap e2 e'); intros; unfold typeMap in H1; rewrite H1 in H. *) *)
(* (*         { inversion H; subst. *) *)
(* (*           specialize (IHe2 _ _ H1). *) *)
(* (*           simpl; rewrite IHe2; repeat rewrite orb_true_r; auto. } *) *)
(* (*         { inversion H. } *) *)
(* (*   - unfold typeMap in H. *) *)
(* (*     case_eq (expEqBool (Downcast m e) e'); intros hyp_if; rewrite hyp_if in H.  *) *)
(* (*     + apply eqImpliesSub; auto. *) *)
(* (*     + specialize (IHe _ _ H). *) *)
(* (*       simpl. *) *)
(* (*       rewrite IHe; auto; apply orb_true_r. *) *)
(* (* Qed. *) *)


(* (* Lemma rewriteEqInSub e e' f: *) *)
(* (*   expEqBool e e' = true -> *) *)
(* (*   isSubExpression e f = true -> *) *)
(* (*   isSubExpression e' f = true. *) *)
(* (* Proof. *) *)
(* (*   induction f; intros. *) *)
(* (*   - unfold isSubExpression in *. *) *)
(* (*     rewrite orb_false_r in *. *) *)
(* (*     eapply expEqBool_trans; eauto. *) *)
(* (*   - unfold isSubExpression in *. *) *)
(* (*     rewrite orb_false_r in *. *) *)
(* (*     eapply expEqBool_trans; eauto. *) *)
(* (*   - unfold isSubExpression in *. *) *)
(* (*     case_eq (expEqBool (Unop u f) e); intros; rewrite H1 in H0. *) *)
(* (*     + pose proof (expEqBool_trans _ _ _ H1 H); rewrite H2. *) *)
(* (*       simpl; auto. *) *)
(* (*     + simpl in H0. *) *)
(* (*       apply orb_true_iff; right. *) *)
(* (*       eapply IHf; eauto. *) *)
(* (*   - unfold isSubExpression in *. *) *)
(* (*     case_eq (expEqBool (Binop b f1 f2) e); intros; rewrite H1 in H0. *) *)
(* (*     + apply orb_true_iff; left. *) *)
(* (*       eapply expEqBool_trans; eauto. *) *)
(* (*     + apply orb_true_iff; right. *) *)
(* (*       simpl in H0. *) *)
(* (*       case_eq (isSubExpression e f1); intros; unfold isSubExpression in H2; rewrite H2 in H0. *) *)
(* (*       * apply orb_true_iff; left. *) *)
(* (*         clear H0. *) *)
(* (*         clear IHf2. *) *)
(* (*         eapply IHf1; eauto. *) *)
(* (*       * simpl in H0. *) *)
(* (*         apply orb_true_iff; right. *) *)
(* (*         eapply IHf2; eauto. *) *)
(* (*   - unfold isSubExpression in *. *) *)
(* (*     case_eq (expEqBool (Downcast m f) e); intros; rewrite H1 in H0. *) *)
(* (*     + apply orb_true_iff; left. *) *)
(* (*       eapply expEqBool_trans; eauto. *) *)
(* (*     + apply orb_true_iff; right. *) *)
(* (*       eapply IHf; eauto. *) *)
(* (* Qed. *) *)


(* (* Lemma subExpr_antisym e f: *) *)
(* (*   isSubExpression e f = true -> *) *)
(* (*   isSubExpression f e = true -> *) *)
(* (*   expEqBool e f = true. *) *)
(* (* Proof. *) *)
(* (* Admitted. *) *)

    
(* (* Lemma subExprNotUnop u e: *) *)
(* (*   isSubExpression (Unop u e) e = false. *) *)
(* (* Proof. *) *)
(* (*   revert u e; induction e.   *) *)
(* (*   - simpl; auto. *) *)
(* (*   - simpl; auto. *) *)
(* (*   - simpl. *) *)
(* (*     intros. *) *)
(* (*     rewrite expEqBool_sym,unop_neq. *) *)
(* (*     rewrite andb_false_r; simpl. *) *)
    
(* (* Admitted. *) *)

(* (* Lemma equal_typing e e1 e2 m: *) *)
(* (*   expEqBool e1 e2 = true -> *) *)
(* (*   typeMap e e1 = Some m -> *) *)
(* (*   typeMap e e2 = Some m. *) *)
(* (*   revert e1 e2 m; induction e; intros *; intros eqExp type_e1. *) *)
(* (*   - simpl in *. destruct e1; try congruence. *) *)
(* (*     case_eq (mTypeEqBool m m1 && (n =? n0)); intros case_types; *) *)
(* (*       rewrite case_types in *; try congruence. *) *)
(* (*     destruct e2; simpl in *; try congruence. *) *)
(* (*     admit. *) *)
(* (*   - admit. *) *)
(* (*   - simpl in *. *) *)
(* (*     destruct e1; destruct e2; simpl in *; try congruence; simpl in *. *) *)
(* (*     + eapply IHe; eauto. *) *)
(* (*       simpl; auto. *) *)
(* (*     + eapply IHe; eauto. *) *)
(* (*       simpl; auto. *) *)
(* (*     + admit. *) *)
(* (*     + eapply IHe; eauto. *) *)
(* (*       simpl; auto. *) *)
(* (*     + eapply IHe; eauto. *) *)
(* (*       simpl; auto. *) *)
(* (*   - simpl in *. *) *)
(* (*     destruct e0; destruct e3; simpl in *; try congruence; simpl in *. *) *)
(* (*     + admit. *) *)
(* (*     + admit. *) *)
(* (*     + admit. *) *)
(* (*     + admit. *) *)
(* (*     + admit. *) *)
(* (*   - admit. *) *)
(* (* Admitted. *) *)

(* (* Lemma unopTypeMapStrenghtening u e e0 m: *) *)
(* (*   typeMap e e0 = Some m -> typeMap (Unop u e) e0 = Some m. *) *)
(* (* Proof. *) *)
(* (*   intros. *) *)
(* (*   induction e0; destruct e0; simpl in *; try auto; try congruence. *) *)
(* (*   case_eq (unopEqBool u u0 && expEqBool e e0); intros. *) *)
(* (*   - assert (typeMap e (Unop u e) = Some m). *) *)
(* (*     + eapply equal_typing; eauto. simpl; auto. admit. *) *)
(* (*     +  *) *)
(* (*   unfold typeMap. *) *)
(* (*   (*  pose proof (typeMapSubExpr _ _ H). *) *) *)
(* (*   (*  assert (isSubExpression e (Unop u e) = true) by admit.*) *) *)
(* (*   case_eq (expEqBool (Unop u e) e0); intros. *) *)
(* (*   - assert (typeMap e (Unop u e) = Some m) by admit. *) *)
(* (*     simpl in *. *) *)
(* (* (*    pose proof (typeMapSubExpr _ _ H). *) *)
(* (*     assert (isSubExpression (Unop u e) e = true) by (eapply rewriteEqInSub; eauto; rewrite expEqBool_sym; auto). *) *)
(* (*         (* contradiction in H2 *) *) *)
(* (*     admit. *) *) *)
(* (*   - apply H. *) *)
(* (* Admitted. *) *)

(* (* Lemma binopTypeMapStrenghtening_l b e1 e2 e m: *) *)
(* (*   typeMap e1 e = Some m -> typeMap (Binop b e1 e2) e = Some m. *) *)
(* (* Proof. *) *)
(* (*   intros. unfold typeMap. *) *)
(* (*   case_eq (expEqBool (Binop b e1 e2) e); intros. *) *)
(* (*   - pose proof (typeMapSubExpr _ _ H). *) *)
(* (*     admit. *) *)
(* (*   - unfold typeMap in H; rewrite H. auto. *) *)
(* (* Admitted. *) *)

(* (* Lemma binopTypeMapStrenghtening_r b e1 e2 e m: *) *)
(* (*   typeMap e2 e = Some m -> typeMap (Binop b e1 e2) e = Some m. *) *)
(* (* Proof. *) *)
(* (*   intros. unfold typeMap. *) *)
(* (*   case_eq (expEqBool (Binop b e1 e2) e); intros. *) *)
(* (*   - pose proof (typeMapSubExpr _ _ H). *) *)
(* (*     admit. *) *)
(* (*   - unfold typeMap in H; rewrite H. auto. *) *)
(* (* Admitted. *) *)

(* (* Lemma roundinTypeMapStrengthening e e0 m m0: *) *)
(* (*   typeMap e e0 = Some m -> typeMap (Downcast m0 e) e0 = Some m. *) *)
(* (* Proof. *) *)
(* (*   intros; unfold typeMap. *) *)
(* (*   case_eq (expEqBool (Downcast m0 e) e0); intros. *) *)
(* (*   - pose proof (typeMapSubExpr _ _ H). *) *)
(* (*     admit. *) *)
(* (*   - unfold typeMap in H; rewrite H. auto. *) *)
(* (* Admitted. *) *)
='s avatar
= committed
1005
      
1006

1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
(* (* Lemma typeExpressionSoundness e m: *) *)
(* (*   typeExpression e = Some m -> *) *)
(* (*   validType (typeMap e) e m.  *) *)
(* (* Proof.                          *) *)
(* (*   revert m; induction e; intros; auto. *) *)
(* (*   - simpl in *. *) *)
(* (*     inversion H; subst; econstructor; eauto. *) *)
(* (*     rewrite <- beq_nat_refl,mTypeEqBool_refl. *) *)
(* (*     simpl; auto. *) *)
(* (*   - simpl in *. *) *)
(* (*     inversion H; subst; econstructor; eauto. *) *)
(* (*     assert (Qeq_bool v v = true) by (apply Qeq_bool_iff; lra).  *) *)
(* (*     rewrite H0,mTypeEqBool_refl; simpl; auto. *) *)
(* (*   - constructor. *) *)
(* (*     + simpl in H. specialize (IHe m H). *) *)
='s avatar
= committed
1022
      
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
(* (*       eapply Gamma_strengthening. *) *)
(* (*       Focus 2. apply IHe. apply unopTypeMapStrenghtening. *) *)
(* (*     + unfold typeMap. rewrite expEqBool_refl. auto. *) *)
(* (*   - simpl in H. *) *)
(* (*     case_eq (typeExpression e1); intros; rewrite H0 in H; [ | inversion H ]. *) *)
(* (*     case_eq (typeExpression e2); intros; rewrite H1 in H; inversion H. *) *)
(* (*     econstructor; eauto. *) *)
(* (*     + specialize (IHe1 _ H0). *) *)
(* (*       eapply Gamma_strengthening. *) *)
(* (*       Focus 2. apply IHe1. *) *)
(* (*       apply binopTypeMapStrenghtening_l. *) *)
(* (*     + specialize (IHe2 _ H1). *) *)
(* (*       eapply Gamma_strengthening. *) *)
(* (*       Focus 2. apply IHe2. *) *)
(* (*       apply binopTypeMapStrenghtening_r. *) *)
(* (*     + unfold typeMap. *) *)
(* (*       rewrite expEqBool_refl. *) *)
(* (*       simpl. *) *)
(* (*       rewrite H0, H1; auto. *) *)
(* (*   - simpl in H. *) *)
(* (*     case_eq (typeExpression e); intros; rewrite H0 in H; [ | inversion H ]. *) *)
(* (*     case_eq (isMorePrecise m1 m); intros; rewrite H1 in H; inversion H; subst. *) *)
(* (*     econstructor; eauto. *) *)
(* (*     + specialize (IHe _ H0). *) *)
(* (*       eapply Gamma_strengthening. *) *)
(* (*       Focus 2. apply IHe. *) *)
(* (*       intros e0 m; apply roundinTypeMapStrengthening. *) *)
(* (*     + unfold typeMap. *) *)
(* (*       rewrite expEqBool_refl; auto. *) *)
(* (* Qed. *) *)