-
Notifications
You must be signed in to change notification settings - Fork 1
/
Term.v
184 lines (160 loc) · 4.73 KB
/
Term.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
Require Import Arith.
Require Import Omega.
Require Import List.
Add LoadPath "Listkit" as Listkit.
Require Import Listkit.Foreach.
(** Definitions *)
Inductive Ty : Set := TyBase | TyPair : Ty -> Ty -> Ty | TyArr : Ty -> Ty -> Ty.
(** Terms *)
Inductive Term : Set :=
TmConst
| TmVar (x : nat) : Term
| TmPair : Term -> Term -> Term
| TmProj : bool -> Term -> Term
| TmAbs : Term -> Term
| TmApp : Term -> Term -> Term.
Notation "L @ M" := (TmApp L M) (at level 500).
Notation "〈 L , M 〉" := (TmPair L M) (at level 400).
(** Typing derivations *)
Inductive Typing env : Term -> Ty -> Set :=
| TBase : Typing env TmConst TyBase
| TVar : forall (x:nat) ty,
value ty = nth_error env x ->
Typing env (TmVar x) ty
| TPair : forall l m s t, Typing env l s -> Typing env m t ->
Typing env (TmPair l m) (TyPair s t)
| TApp : forall l m a b,
Typing env l (TyArr a b) -> Typing env m a ->
Typing env (TmApp l m) b
| TAbs : forall n s t,
Typing (s :: env) n t ->
Typing env (TmAbs n) (TyArr s t)
| TProj1 : forall m s t,
Typing env m (TyPair s t) ->
Typing env (TmProj false m) s
| TProj2 : forall m s t,
Typing env m (TyPair s t) ->
Typing env (TmProj true m) t
.
Hint Constructors Typing.
(** [env_typing] relates a value environment to its typing. It asserts
the types (in a [nil] environment) of each of a series of values. *)
Definition env_typing Vs Ts :=
((length Vs = length Ts) *
foreach2_ty _ _ Vs Ts (fun x y => (Typing nil x y)))%type.
(** [env_typing_env] also relates a value environment to its typing. It asserts
the types (in a given environment) of each of a series of values. *)
Definition env_typing_env env Vs Ts :=
((length Vs = length Ts) *
foreach2_ty _ _ Vs Ts (fun x y => (Typing env x y)))%type.
Hint Unfold env_typing.
(** [env_typing_env] environments can be extended, one term-type pair at a time. *)
Lemma env_typing_intro:
forall env V Vs T Ts,
Typing env V T ->
env_typing_env env (Vs) (Ts) ->
env_typing_env env (V::Vs) (T::Ts).
Proof.
intros.
unfold env_typing_env in *.
unfold foreach2_ty in *.
simpl in *.
intuition.
Qed.
(** [env_typing_env] environments can be destructed into their first
pair and a remaining [env_typing_env] environment. *)
Lemma env_typing_elim:
forall env V Vs T Ts,
env_typing_env env (V::Vs) (T::Ts) ->
(env_typing_env env Vs Ts
* Typing env V T).
Proof.
intros ? ? ? ? ? X.
unfold env_typing_env in X.
unfold foreach2_ty in X.
unfold env_typing_env.
simpl in *.
intuition.
Qed.
Lemma env_typing_env_app:
forall env Vs Ws Ts,
env_typing_env env (Vs++Ws) Ts ->
{T1s : list Ty & { T2s : list Ty &
((length T1s = length Vs) *
(length T2s = length Ws) *
(Ts = T1s ++ T2s) *
(env_typing_env env (Vs ++ Ws) (T1s ++ T2s)))%type } }.
Proof.
induction Vs.
simpl.
intros Ws Ts H.
exists nil.
exists Ts.
simpl.
inversion H.
auto.
simpl.
intros Ws Ts H.
inversion H as [H0 X].
simpl in H0.
destruct Ts.
simpl in H0.
omega.
destruct (IHVs Ws Ts) as [T1s' H1].
apply env_typing_elim in H.
destruct H; auto.
destruct H1 as [T2s' H2].
exists (t::T1s').
exists (T2s').
simpl.
destruct H2 as [[[H3 H4] H5] H6].
split; [split; [split |]|].
omega.
auto.
congruence.
apply env_typing_intro.
intuition.
simpl in *.
subst Ts.
unfold foreach2_ty in X.
simpl in X.
intuition.
auto.
Qed.
Lemma env_typing_cons :
forall V T Vs env,
Typing nil V T -> env_typing Vs env -> env_typing (V::Vs) (T::env).
Proof.
intros.
simpl; firstorder.
unfold foreach2_ty; simpl; intuition.
Qed.
Hint Resolve env_typing_cons.
Require Import Coq.Lists.ListSet.
Require Import Listkit.Sets.
Definition set_remove := Listkit.Sets.set_remove.
(** The free variables of a Term, as a set of nats. *)
Fixpoint freevars (M:Term) : set nat :=
match M with
| TmConst => empty_set nat
| TmVar x => set_add eq_nat_dec x (empty_set nat)
| TmPair L M => set_union eq_nat_dec (freevars L) (freevars M)
| TmProj b M => freevars M
| TmAbs N => set_map eq_nat_dec (fun x => x-1)
(set_remove _ eq_nat_dec 0 (freevars N))
| TmApp L M => set_union eq_nat_dec (freevars L) (freevars M)
end.
Definition free_in x M := set_In x (freevars M).
Definition in_env_domain (n:nat) (env:list Term) := fun x => n <= x < n+length env.
(* (* Alt definition, reuses outside_range; consider it! *)
Definition in_env_domain (n:nat) (env:list Term) :=
fun x => false = outside_range n (n+length env) x. *)
(* TODO: in_env_domain and outside_range are essentially logical inverses,
but are defined in different sorts. Consolidate them! *)
Lemma in_env_domain_map :
forall n f env, in_env_domain n (map f env) = in_env_domain n env.
unfold in_env_domain.
intros.
rewrite map_length.
auto.
Qed.