-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsubstitution.elf
51 lines (33 loc) · 1.63 KB
/
substitution.elf
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
%% Lemma A_6 Substituion, pg. 242.
%% Status: not clear I can prove these in Twelf.
%% substitution_k
%% Note: TODO missing delta alpha K, so I'm fundamentally misunderstanding context representation.
Lemma_A_6_1 : {T} {K} {T'} {K'} ak T K -> ({AL} k (T' AL) K') -> k (T' T) K' -> type.
%mode Lemma_A_6_1 +T +K +T' +K' +DakTK +D1 -D2.
- : Lemma_A_6_1 T K T' K' DakTK D1 (D1 T).
%worlds () (Lemma_A_6_1 _ _ _ _ _ _ _).
%total {} (Lemma_A_6_1 _ _ _ _ _ _ _).
Lemma_A_6_2 : {T} {K} {T'} {K'} ak T K -> ({AL} ak (T' AL) K') -> ak (T' T) K' -> type.
%mode Lemma_A_6_2 +T +K +T' +K' +DakTK +D1 -D2.
- : Lemma_A_6_2 T K T' K' DakTK D1 (D1 T).
%worlds () (Lemma_A_6_2 _ _ _ _ _ _ _).
%total {} (Lemma_A_6_2 _ _ _ _ _ _ _).
Lemma_A_6_3 : {T} {K} {T'} ak T K -> ({AL} assgn (T' AL)) -> assgn (T' T) -> type.
%mode Lemma_A_6_3 +T +K +T' +DakTK +D1 -D2.
- : Lemma_A_6_3 T K T' DakTK D1 (D1 T).
%worlds () (Lemma_A_6_3 _ _ _ _ _ _).
%total {} (Lemma_A_6_3 _ _ _ _ _ _).
% Lemma_A_6_4 and 5 are moot as they are about the well formedness of contexts.
% NOTE: TODO Lemma_A_6_6 it's really not clear what this means in a Twelf formulation.
% Dan is saying that ret does not care about types which is obvious by inspection.
% Nor can I get proof by derivation cases for some reason I can't undertand.
% It has to do with the application of the function to produce the state.
%%Lemma_A_6_6 : {S : tau -> st} ret (S T) -> ret (S T') -> type.
%%mode Lemma_A_6_6 +S +D1 -D2.
%%
%% - : Lemma_A_6_6 S (ret_return) _.
%%
%%worlds () (Lemma_A_6_6 _ _ _).
%%total {S D} (Lemma_A_6_6 S D _).
% NOTE: TODO Lemma_A_6_7 skip for now.
% NOTE: TODO Lemma_A_6_8 skip for now.