-
Notifications
You must be signed in to change notification settings - Fork 3
/
CloseLemmas.v
134 lines (118 loc) · 3.02 KB
/
CloseLemmas.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
58
59
60
61
62
63
64
65
66
67
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
99
100
101
102
103
104
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
Require Export SystemFR.Tactics.
Require Export SystemFR.SubstitutionLemmas.
Require Export SystemFR.FVLemmasLists.
Require Export SystemFR.TOpenTClose.
Lemma close_nothing:
forall x t k,
~(x ∈ pfv t term_var) ->
close k t x = t.
Proof.
induction t;
repeat step || t_equality || list_utils.
Qed.
Lemma close_nothing2:
forall x t k,
pfv t term_var = nil ->
close k t x = t.
Proof.
intros; apply close_nothing; repeat step || rewrite_any.
Qed.
Lemma open_close3:
forall t k1 k2 x rep,
fv rep = nil ->
wf rep 0 ->
k1 <> k2 ->
open k1 (close k2 t x) rep =
close k2 (open k1 t rep) x.
Proof.
induction t; repeat step || t_equality || rewrite_any || rewrite close_nothing2 by auto.
Qed.
Lemma substitute_close:
forall t l tag x k,
~(x ∈ support l) ->
pclosed_mapping l term_var ->
psubstitute (close k t x) l tag = close k (psubstitute t l tag) x.
Proof.
induction t;
repeat step || t_equality || t_lookup || rewrite close_nothing2 by (steps; eauto with fv).
Qed.
Lemma tclose_nothing:
forall x t k,
~(x ∈ pfv t type_var) ->
tclose k t x = t.
Proof.
induction t;
repeat step || t_equality || list_utils.
Qed.
Lemma tclose_nothing2:
forall x t k,
pfv t type_var = nil ->
tclose k t x = t.
Proof.
intros; apply tclose_nothing; repeat step || rewrite_any.
Qed.
Lemma substitute_tclose:
forall t l tag x k,
~(x ∈ support l) ->
pclosed_mapping l type_var ->
psubstitute (tclose k t x) l tag = tclose k (psubstitute t l tag) x.
Proof.
induction t;
repeat step || t_equality || t_lookup || rewrite tclose_nothing2 by (steps; eauto with fv).
Qed.
Fixpoint closes k T xs :=
match xs with
| nil => T
| x :: xs => close k (closes (S k) T xs) x
end.
Lemma is_erased_term_close:
forall t k x,
is_erased_term t ->
is_erased_term (close k t x).
Proof.
induction t; steps.
Qed.
Lemma is_erased_type_close:
forall T k x,
is_erased_type T ->
is_erased_type (close k T x).
Proof.
induction T; steps; eauto using is_erased_term_close.
Qed.
#[export]
Hint Resolve is_erased_term_close: erased.
#[export]
Hint Resolve is_erased_type_close: erased.
Lemma is_erased_type_closes:
forall xs k T,
is_erased_type T ->
is_erased_type (closes k T xs).
Proof.
induction xs; steps; eauto with erased.
Qed.
#[export]
Hint Resolve is_erased_type_closes: erased.
Lemma open_closes:
forall xs x T v i,
fv v = nil ->
wf v 0 ->
wf T 0 ->
open (length xs + i) (closes i T (xs ++ x :: nil)) v =
closes i (psubstitute T ((x, v) :: nil) term_var) xs.
Proof.
induction xs; repeat step || rewrite open_close; eauto with wf.
rewrite open_close3; steps; eauto with lia.
rewrite <- PeanoNat.Nat.add_succ_r.
rewrite_any; steps.
Qed.
Lemma open_closes_zero:
forall xs x T v,
fv v = nil ->
wf v 0 ->
wf T 0 ->
open (length xs) (closes 0 T (xs ++ x :: nil)) v =
closes 0 (psubstitute T ((x, v) :: nil) term_var) xs.
Proof.
intros.
rewrite <- (PeanoNat.Nat.add_0_r (length xs)); eauto using open_closes.
Qed.