-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsyntax.v
291 lines (215 loc) · 20.8 KB
/
syntax.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
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
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
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
Require Export fintype.
Section ty.
Inductive ty : Type :=
| Fun : ty -> ty -> ty
| Nat : ty .
Lemma congr_Fun { s0 : ty } { s1 : ty } { t0 : ty } { t1 : ty } (H1 : s0 = t0) (H2 : s1 = t1) : Fun s0 s1 = Fun t0 t1 .
Proof. congruence. Qed.
Lemma congr_Nat : Nat = Nat .
Proof. congruence. Qed.
End ty.
Section tm.
Inductive tm (ntm : nat) : Type :=
| var_tm : (fin) (ntm) -> tm (ntm)
| Lam : ty -> tm ((S) ntm) -> tm (ntm)
| App : tm (ntm) -> tm (ntm) -> tm (ntm)
| Zero : tm (ntm)
| Succ : tm (ntm) -> tm (ntm)
| Rec : tm (ntm) -> tm (ntm) -> tm ((S) ((S) ntm)) -> tm (ntm).
Lemma congr_Lam { mtm : nat } { s0 : ty } { s1 : tm ((S) mtm) } { t0 : ty } { t1 : tm ((S) mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : Lam (mtm) s0 s1 = Lam (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_App { mtm : nat } { s0 : tm (mtm) } { s1 : tm (mtm) } { t0 : tm (mtm) } { t1 : tm (mtm) } (H1 : s0 = t0) (H2 : s1 = t1) : App (mtm) s0 s1 = App (mtm) t0 t1 .
Proof. congruence. Qed.
Lemma congr_Zero { mtm : nat } : Zero (mtm) = Zero (mtm) .
Proof. congruence. Qed.
Lemma congr_Succ { mtm : nat } { s0 : tm (mtm) } { t0 : tm (mtm) } (H1 : s0 = t0) : Succ (mtm) s0 = Succ (mtm) t0 .
Proof. congruence. Qed.
Lemma congr_Rec { mtm : nat } { s0 : tm (mtm) } { s1 : tm (mtm) } { s2 : tm ((S) ((S) mtm)) } { t0 : tm (mtm) } { t1 : tm (mtm) } { t2 : tm ((S) ((S) mtm)) } (H1 : s0 = t0) (H2 : s1 = t1) (H3 : s2 = t2) : Rec (mtm) s0 s1 s2 = Rec (mtm) t0 t1 t2 .
Proof. congruence. Qed.
Definition upRen_tm_tm { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : (fin) ((S) (m)) -> (fin) ((S) (n)) :=
(up_ren) xi.
Fixpoint ren_tm { mtm : nat } { ntm : nat } (xitm : (fin) (mtm) -> (fin) (ntm)) (s : tm (mtm)) : tm (ntm) :=
match s return tm (ntm) with
| var_tm (_) s => (var_tm (ntm)) (xitm s)
| Lam (_) s0 s1 => Lam (ntm) ((fun x => x) s0) ((ren_tm (upRen_tm_tm xitm)) s1)
| App (_) s0 s1 => App (ntm) ((ren_tm xitm) s0) ((ren_tm xitm) s1)
| Zero (_) => Zero (ntm)
| Succ (_) s0 => Succ (ntm) ((ren_tm xitm) s0)
| Rec (_) s0 s1 s2 => Rec (ntm) ((ren_tm xitm) s0) ((ren_tm xitm) s1) ((ren_tm (upRen_tm_tm (upRen_tm_tm xitm))) s2)
end.
Definition up_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) : (fin) ((S) (m)) -> tm ((S) ntm) :=
(scons) ((var_tm ((S) ntm)) (var_zero)) ((funcomp) (ren_tm (shift)) sigma).
Fixpoint subst_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (s : tm (mtm)) : tm (ntm) :=
match s return tm (ntm) with
| var_tm (_) s => sigmatm s
| Lam (_) s0 s1 => Lam (ntm) ((fun x => x) s0) ((subst_tm (up_tm_tm sigmatm)) s1)
| App (_) s0 s1 => App (ntm) ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1)
| Zero (_) => Zero (ntm)
| Succ (_) s0 => Succ (ntm) ((subst_tm sigmatm) s0)
| Rec (_) s0 s1 s2 => Rec (ntm) ((subst_tm sigmatm) s0) ((subst_tm sigmatm) s1) ((subst_tm (up_tm_tm (up_tm_tm sigmatm))) s2)
end.
Definition upId_tm_tm { mtm : nat } (sigma : (fin) (mtm) -> tm (mtm)) (Eq : forall x, sigma x = (var_tm (mtm)) x) : forall x, (up_tm_tm sigma) x = (var_tm ((S) mtm)) x :=
fun n => match n with
| Some fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| None => eq_refl
end.
Fixpoint idSubst_tm { mtm : nat } (sigmatm : (fin) (mtm) -> tm (mtm)) (Eqtm : forall x, sigmatm x = (var_tm (mtm)) x) (s : tm (mtm)) : subst_tm sigmatm s = s :=
match s return subst_tm sigmatm s = s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((idSubst_tm (up_tm_tm sigmatm) (upId_tm_tm (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((idSubst_tm sigmatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((idSubst_tm sigmatm Eqtm) s0) ((idSubst_tm sigmatm Eqtm) s1) ((idSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (upId_tm_tm (_) (upId_tm_tm (_) Eqtm))) s2)
end.
Definition upExtRen_tm_tm { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) (zeta : (fin) (m) -> (fin) (n)) (Eq : forall x, xi x = zeta x) : forall x, (upRen_tm_tm xi) x = (upRen_tm_tm zeta) x :=
fun n => match n with
| Some fin_n => (ap) (shift) (Eq fin_n)
| None => eq_refl
end.
Fixpoint extRen_tm { mtm : nat } { ntm : nat } (xitm : (fin) (mtm) -> (fin) (ntm)) (zetatm : (fin) (mtm) -> (fin) (ntm)) (Eqtm : forall x, xitm x = zetatm x) (s : tm (mtm)) : ren_tm xitm s = ren_tm zetatm s :=
match s return ren_tm xitm s = ren_tm zetatm s with
| var_tm (_) s => (ap) (var_tm (ntm)) (Eqtm s)
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((extRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upExtRen_tm_tm (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((extRen_tm xitm zetatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((extRen_tm xitm zetatm Eqtm) s0) ((extRen_tm xitm zetatm Eqtm) s1) ((extRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upExtRen_tm_tm (_) (_) (upExtRen_tm_tm (_) (_) Eqtm))) s2)
end.
Definition upExt_tm_tm { m : nat } { ntm : nat } (sigma : (fin) (m) -> tm (ntm)) (tau : (fin) (m) -> tm (ntm)) (Eq : forall x, sigma x = tau x) : forall x, (up_tm_tm sigma) x = (up_tm_tm tau) x :=
fun n => match n with
| Some fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| None => eq_refl
end.
Fixpoint ext_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) (tautm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, sigmatm x = tautm x) (s : tm (mtm)) : subst_tm sigmatm s = subst_tm tautm s :=
match s return subst_tm sigmatm s = subst_tm tautm s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((ext_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (upExt_tm_tm (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((ext_tm sigmatm tautm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((ext_tm sigmatm tautm Eqtm) s0) ((ext_tm sigmatm tautm Eqtm) s1) ((ext_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (upExt_tm_tm (_) (_) (upExt_tm_tm (_) (_) Eqtm))) s2)
end.
Definition up_ren_ren_tm_tm { k : nat } { l : nat } { m : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> (fin) (m)) (theta : (fin) (k) -> (fin) (m)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (upRen_tm_tm tau) (upRen_tm_tm xi)) x = (upRen_tm_tm theta) x :=
up_ren_ren xi tau theta Eq.
Fixpoint compRenRen_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (rhotm : (fin) (mtm) -> (fin) (ltm)) (Eqtm : forall x, ((funcomp) zetatm xitm) x = rhotm x) (s : tm (mtm)) : ren_tm zetatm (ren_tm xitm s) = ren_tm rhotm s :=
match s return ren_tm zetatm (ren_tm xitm s) = ren_tm rhotm s with
| var_tm (_) s => (ap) (var_tm (ltm)) (Eqtm s)
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((compRenRen_tm (upRen_tm_tm xitm) (upRen_tm_tm zetatm) (upRen_tm_tm rhotm) (up_ren_ren (_) (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((compRenRen_tm xitm zetatm rhotm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((compRenRen_tm xitm zetatm rhotm Eqtm) s0) ((compRenRen_tm xitm zetatm rhotm Eqtm) s1) ((compRenRen_tm (upRen_tm_tm (upRen_tm_tm xitm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (upRen_tm_tm (upRen_tm_tm rhotm)) (up_ren_ren (_) (_) (_) (up_ren_ren (_) (_) (_) Eqtm))) s2)
end.
Definition up_ren_subst_tm_tm { k : nat } { l : nat } { mtm : nat } (xi : (fin) (k) -> (fin) (l)) (tau : (fin) (l) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) tau xi) x = theta x) : forall x, ((funcomp) (up_tm_tm tau) (upRen_tm_tm xi)) x = (up_tm_tm theta) x :=
fun n => match n with
| Some fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| None => eq_refl
end.
Fixpoint compRenSubst_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) tautm xitm) x = thetatm x) (s : tm (mtm)) : subst_tm tautm (ren_tm xitm s) = subst_tm thetatm s :=
match s return subst_tm tautm (ren_tm xitm s) = subst_tm thetatm s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((compRenSubst_tm (upRen_tm_tm xitm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_ren_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((compRenSubst_tm xitm tautm thetatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((compRenSubst_tm xitm tautm thetatm Eqtm) s0) ((compRenSubst_tm xitm tautm thetatm Eqtm) s1) ((compRenSubst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_ren_subst_tm_tm (_) (_) (_) (up_ren_subst_tm_tm (_) (_) (_) Eqtm))) s2)
end.
Definition up_subst_ren_tm_tm { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (zetatm : (fin) (ltm) -> (fin) (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (ren_tm zetatm) sigma) x = theta x) : forall x, ((funcomp) (ren_tm (upRen_tm_tm zetatm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| Some fin_n => (eq_trans) (compRenRen_tm (shift) (upRen_tm_tm zetatm) ((funcomp) (shift) zetatm) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compRenRen_tm zetatm (shift) ((funcomp) (shift) zetatm) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm (shift)) (Eq fin_n)))
| None => eq_refl
end.
Fixpoint compSubstRen_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (ren_tm zetatm) sigmatm) x = thetatm x) (s : tm (mtm)) : ren_tm zetatm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s return ren_tm zetatm (subst_tm sigmatm s) = subst_tm thetatm s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((compSubstRen_tm (up_tm_tm sigmatm) (upRen_tm_tm zetatm) (up_tm_tm thetatm) (up_subst_ren_tm_tm (_) (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s0) ((compSubstRen_tm sigmatm zetatm thetatm Eqtm) s1) ((compSubstRen_tm (up_tm_tm (up_tm_tm sigmatm)) (upRen_tm_tm (upRen_tm_tm zetatm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_ren_tm_tm (_) (_) (_) (up_subst_ren_tm_tm (_) (_) (_) Eqtm))) s2)
end.
Definition up_subst_subst_tm_tm { k : nat } { ltm : nat } { mtm : nat } (sigma : (fin) (k) -> tm (ltm)) (tautm : (fin) (ltm) -> tm (mtm)) (theta : (fin) (k) -> tm (mtm)) (Eq : forall x, ((funcomp) (subst_tm tautm) sigma) x = theta x) : forall x, ((funcomp) (subst_tm (up_tm_tm tautm)) (up_tm_tm sigma)) x = (up_tm_tm theta) x :=
fun n => match n with
| Some fin_n => (eq_trans) (compRenSubst_tm (shift) (up_tm_tm tautm) ((funcomp) (up_tm_tm tautm) (shift)) (fun x => eq_refl) (sigma fin_n)) ((eq_trans) ((eq_sym) (compSubstRen_tm tautm (shift) ((funcomp) (ren_tm (shift)) tautm) (fun x => eq_refl) (sigma fin_n))) ((ap) (ren_tm (shift)) (Eq fin_n)))
| None => eq_refl
end.
Fixpoint compSubstSubst_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (thetatm : (fin) (mtm) -> tm (ltm)) (Eqtm : forall x, ((funcomp) (subst_tm tautm) sigmatm) x = thetatm x) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s :=
match s return subst_tm tautm (subst_tm sigmatm s) = subst_tm thetatm s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((compSubstSubst_tm (up_tm_tm sigmatm) (up_tm_tm tautm) (up_tm_tm thetatm) (up_subst_subst_tm_tm (_) (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s0) ((compSubstSubst_tm sigmatm tautm thetatm Eqtm) s1) ((compSubstSubst_tm (up_tm_tm (up_tm_tm sigmatm)) (up_tm_tm (up_tm_tm tautm)) (up_tm_tm (up_tm_tm thetatm)) (up_subst_subst_tm_tm (_) (_) (_) (up_subst_subst_tm_tm (_) (_) (_) Eqtm))) s2)
end.
Definition rinstInst_up_tm_tm { m : nat } { ntm : nat } (xi : (fin) (m) -> (fin) (ntm)) (sigma : (fin) (m) -> tm (ntm)) (Eq : forall x, ((funcomp) (var_tm (ntm)) xi) x = sigma x) : forall x, ((funcomp) (var_tm ((S) ntm)) (upRen_tm_tm xi)) x = (up_tm_tm sigma) x :=
fun n => match n with
| Some fin_n => (ap) (ren_tm (shift)) (Eq fin_n)
| None => eq_refl
end.
Fixpoint rinst_inst_tm { mtm : nat } { ntm : nat } (xitm : (fin) (mtm) -> (fin) (ntm)) (sigmatm : (fin) (mtm) -> tm (ntm)) (Eqtm : forall x, ((funcomp) (var_tm (ntm)) xitm) x = sigmatm x) (s : tm (mtm)) : ren_tm xitm s = subst_tm sigmatm s :=
match s return ren_tm xitm s = subst_tm sigmatm s with
| var_tm (_) s => Eqtm s
| Lam (_) s0 s1 => congr_Lam ((fun x => (eq_refl) x) s0) ((rinst_inst_tm (upRen_tm_tm xitm) (up_tm_tm sigmatm) (rinstInst_up_tm_tm (_) (_) Eqtm)) s1)
| App (_) s0 s1 => congr_App ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1)
| Zero (_) => congr_Zero
| Succ (_) s0 => congr_Succ ((rinst_inst_tm xitm sigmatm Eqtm) s0)
| Rec (_) s0 s1 s2 => congr_Rec ((rinst_inst_tm xitm sigmatm Eqtm) s0) ((rinst_inst_tm xitm sigmatm Eqtm) s1) ((rinst_inst_tm (upRen_tm_tm (upRen_tm_tm xitm)) (up_tm_tm (up_tm_tm sigmatm)) (rinstInst_up_tm_tm (_) (_) (rinstInst_up_tm_tm (_) (_) Eqtm))) s2)
end.
Lemma rinstInst_tm { mtm : nat } { ntm : nat } (xitm : (fin) (mtm) -> (fin) (ntm)) : ren_tm xitm = subst_tm ((funcomp) (var_tm (ntm)) xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => rinst_inst_tm xitm (_) (fun n => eq_refl) x)). Qed.
Lemma instId_tm { mtm : nat } : subst_tm (var_tm (mtm)) = id .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => idSubst_tm (var_tm (mtm)) (fun n => eq_refl) ((id) x))). Qed.
Lemma rinstId_tm { mtm : nat } : @ren_tm (mtm) (mtm) (id) = id .
Proof. exact ((eq_trans) (rinstInst_tm ((id) (_))) instId_tm). Qed.
Lemma varL_tm { mtm : nat } { ntm : nat } (sigmatm : (fin) (mtm) -> tm (ntm)) : (funcomp) (subst_tm sigmatm) (var_tm (mtm)) = sigmatm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma varLRen_tm { mtm : nat } { ntm : nat } (xitm : (fin) (mtm) -> (fin) (ntm)) : (funcomp) (ren_tm xitm) (var_tm (mtm)) = (funcomp) (var_tm (ntm)) xitm .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun x => eq_refl)). Qed.
Lemma compComp_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : tm (mtm)) : subst_tm tautm (subst_tm sigmatm s) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) s .
Proof. exact (compSubstSubst_tm sigmatm tautm (_) (fun n => eq_refl) s). Qed.
Lemma compComp'_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_tm tautm) (subst_tm sigmatm) = subst_tm ((funcomp) (subst_tm tautm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compComp_tm sigmatm tautm n)). Qed.
Lemma compRen_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (s : tm (mtm)) : ren_tm zetatm (subst_tm sigmatm s) = subst_tm ((funcomp) (ren_tm zetatm) sigmatm) s .
Proof. exact (compSubstRen_tm sigmatm zetatm (_) (fun n => eq_refl) s). Qed.
Lemma compRen'_tm { ktm : nat } { ltm : nat } { mtm : nat } (sigmatm : (fin) (mtm) -> tm (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) : (funcomp) (ren_tm zetatm) (subst_tm sigmatm) = subst_tm ((funcomp) (ren_tm zetatm) sigmatm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => compRen_tm sigmatm zetatm n)). Qed.
Lemma renComp_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) (s : tm (mtm)) : subst_tm tautm (ren_tm xitm s) = subst_tm ((funcomp) tautm xitm) s .
Proof. exact (compRenSubst_tm xitm tautm (_) (fun n => eq_refl) s). Qed.
Lemma renComp'_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (tautm : (fin) (ktm) -> tm (ltm)) : (funcomp) (subst_tm tautm) (ren_tm xitm) = subst_tm ((funcomp) tautm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renComp_tm xitm tautm n)). Qed.
Lemma renRen_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) (s : tm (mtm)) : ren_tm zetatm (ren_tm xitm s) = ren_tm ((funcomp) zetatm xitm) s .
Proof. exact (compRenRen_tm xitm zetatm (_) (fun n => eq_refl) s). Qed.
Lemma renRen'_tm { ktm : nat } { ltm : nat } { mtm : nat } (xitm : (fin) (mtm) -> (fin) (ktm)) (zetatm : (fin) (ktm) -> (fin) (ltm)) : (funcomp) (ren_tm zetatm) (ren_tm xitm) = ren_tm ((funcomp) zetatm xitm) .
Proof. exact ((FunctionalExtensionality.functional_extensionality _ _ ) (fun n => renRen_tm xitm zetatm n)). Qed.
End tm.
Arguments var_tm {ntm}.
Arguments Lam {ntm}.
Arguments App {ntm}.
Arguments Zero {ntm}.
Arguments Succ {ntm}.
Arguments Rec {ntm}.
Global Instance Subst_tm { mtm : nat } { ntm : nat } : Subst1 ((fin) (mtm) -> tm (ntm)) (tm (mtm)) (tm (ntm)) := @subst_tm (mtm) (ntm) .
Global Instance Ren_tm { mtm : nat } { ntm : nat } : Ren1 ((fin) (mtm) -> (fin) (ntm)) (tm (mtm)) (tm (ntm)) := @ren_tm (mtm) (ntm) .
Global Instance VarInstance_tm { mtm : nat } : Var ((fin) (mtm)) (tm (mtm)) := @var_tm (mtm) .
Notation "x '__tm'" := (var_tm x) (at level 5, format "x __tm") : subst_scope.
Notation "x '__tm'" := (@ids (_) (_) VarInstance_tm x) (at level 5, only printing, format "x __tm") : subst_scope.
Notation "'var'" := (var_tm) (only printing, at level 1) : subst_scope.
Class Up_tm X Y := up_tm : X -> Y.
Notation "↑__tm" := (up_tm) (only printing) : subst_scope.
Notation "↑__tm" := (up_tm_tm) (only printing) : subst_scope.
Global Instance Up_tm_tm { m : nat } { ntm : nat } : Up_tm (_) (_) := @up_tm_tm (m) (ntm) .
Notation "s [ sigmatm ]" := (subst_tm sigmatm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "[ sigmatm ]" := (subst_tm sigmatm) (at level 1, left associativity, only printing) : fscope.
Notation "s ⟨ xitm ⟩" := (ren_tm xitm s) (at level 7, left associativity, only printing) : subst_scope.
Notation "⟨ xitm ⟩" := (ren_tm xitm) (at level 1, left associativity, only printing) : fscope.
Ltac auto_unfold := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Ren_tm, VarInstance_tm.
Tactic Notation "auto_unfold" "in" "*" := repeat unfold subst1, subst2, Subst1, Subst2, ids, ren1, ren2, Ren1, Ren2, Subst_tm, Ren_tm, VarInstance_tm in *.
Ltac asimpl' := repeat first [progress rewrite ?instId_tm| progress rewrite ?compComp_tm| progress rewrite ?compComp'_tm| progress rewrite ?rinstId_tm| progress rewrite ?compRen_tm| progress rewrite ?compRen'_tm| progress rewrite ?renComp_tm| progress rewrite ?renComp'_tm| progress rewrite ?renRen_tm| progress rewrite ?renRen'_tm| progress rewrite ?varL_tm| progress rewrite ?varLRen_tm| progress (unfold up_ren, upRen_tm_tm, up_tm_tm)| progress (cbn [subst_tm ren_tm])| fsimpl].
Ltac asimpl := repeat try unfold_funcomp; auto_unfold in *; asimpl'; repeat try unfold_funcomp.
Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J.
Tactic Notation "auto_case" := auto_case (asimpl; cbn; eauto).
Tactic Notation "asimpl" "in" "*" := auto_unfold in *; repeat first [progress rewrite ?instId_tm in *| progress rewrite ?compComp_tm in *| progress rewrite ?compComp'_tm in *| progress rewrite ?rinstId_tm in *| progress rewrite ?compRen_tm in *| progress rewrite ?compRen'_tm in *| progress rewrite ?renComp_tm in *| progress rewrite ?renComp'_tm in *| progress rewrite ?renRen_tm in *| progress rewrite ?renRen'_tm in *| progress rewrite ?varL_tm in *| progress rewrite ?varLRen_tm in *| progress (unfold up_ren, upRen_tm_tm, up_tm_tm in *)| progress (cbn [subst_tm ren_tm] in *)| fsimpl in *].
Ltac substify := auto_unfold; try repeat (erewrite rinstInst_tm).
Ltac renamify := auto_unfold; try repeat (erewrite <- rinstInst_tm).