/
SubstExpExp.v
58 lines (47 loc) · 1.26 KB
/
SubstExpExp.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
Require Import Iron.Language.SystemF2.SubstTypeType.
Require Import Iron.Language.SystemF2.SubstTypeExp.
Require Import Iron.Language.SystemF2.TyJudge.
(* Substitution of exps in exps preserves typing *)
Theorem subst_exp_exp_ix
: forall ix ke te x1 t1 x2 t2
, get ix te = Some t2
-> TYPE ke te x1 t1
-> TYPE ke (delete ix te) x2 t2
-> TYPE ke (delete ix te) (substXX ix x2 x1) t1.
Proof.
intros. gen ix ke te t1 x2 t2.
induction x1; intros; inverts_type; simpl; eauto.
Case "XVar".
fbreak_nat_compare.
SCase "n = ix".
rewrite H in H3. inverts H3. auto.
SCase "n < ix".
apply TYVar; auto.
SCase "n > ix".
apply TYVar; auto.
rewrite <- H3.
destruct n.
burn.
simpl. nnat. apply get_delete_below; burn.
Case "XLAM".
eapply (IHx1 ix) in H5.
apply TYLAM.
unfold liftTE. rewrite map_delete. eauto.
eapply get_map. eauto.
unfold liftTE. rewrite <- map_delete.
apply type_kienv_weaken. auto.
Case "XLam".
apply TYLam; auto.
rewrite delete_rewind.
eauto using type_tyenv_weaken.
Qed.
Theorem subst_exp_exp
: forall ke te x1 t1 x2 t2
, TYPE ke (te :> t2) x1 t1
-> TYPE ke te x2 t2
-> TYPE ke te (substXX 0 x2 x1) t1.
Proof.
intros.
rrwrite (te = delete 0 (te :> t2)).
eapply subst_exp_exp_ix; burn.
Qed.