/
TypeInv.v
144 lines (124 loc) · 2.58 KB
/
TypeInv.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
Require Import Lambda.
Require Import List.
Require Import String.
(* Inversion of the typing relation *)
Lemma VarRel :
forall (tenv : list (string * type)) (x : string) (r : type),
Some r = typing (Var x) tenv -> In (x,r) tenv.
Proof.
simpl in |- *.
intro tenv.
induction tenv.
intros.
simpl in H.
discriminate H.
intros x r.
simpl in |- *.
destruct a.
case (string_dec x s).
intros.
left.
rewrite e in |- *.
inversion H.
reflexivity.
intros.
right.
apply IHtenv.
assumption.
Qed.
Lemma LambdaRel :
forall (x : string)
(t r1 : type)
(body : term)
(tenv : list (string * type)),
Some r1 = typing (Lambda x t body) tenv ->
exists r2 : type,
Some r2 = typing body ((x,t)::tenv) /\
r1 = FunT t r2.
Proof.
simpl in |- *.
intros until tenv.
case (typing body ((x, t) :: tenv)).
intros.
inversion H.
exists t0.
split; reflexivity; reflexivity.
intro.
discriminate H.
Qed.
Lemma ApplyRel:
forall (r : type)
(f x : term)
(tenv : list (string * type)),
Some r = typing (Apply f x) tenv ->
exists t : type,
Some (FunT t r) = typing f tenv /\
Some t = typing x tenv.
Proof.
intros until tenv.
simpl in |- *.
case (typing f tenv).
intro.
case t.
intro.
discriminate H.
case (typing x tenv).
intros t0 t1.
case (type_dec t1 t0).
intros.
exists t1.
rewrite e in |- *.
inversion H.
split; reflexivity; reflexivity.
intros; discriminate.
intros; discriminate.
intro; discriminate.
Qed.
Lemma TrueRel:
forall (tenv : list (string * type)) (r : type),
Some r = typing (Bool true) tenv -> r = BoolT.
Proof.
intros until r.
simpl in |- *.
intro.
inversion H.
reflexivity.
Qed.
Lemma FalseRel:
forall (tenv : list (string * type)) (r : type),
Some r = typing (Bool false) tenv -> r = BoolT.
Proof.
intros until r.
simpl in |- *.
intro.
inversion H.
reflexivity.
Qed.
Lemma IfRel:
forall (tenv : list (string * type)) (r : type) (t1 t2 t3 : term),
Some r = typing (If t1 t2 t3) tenv ->
Some BoolT = typing t1 tenv /\ Some r = typing t2 tenv /\ Some r = typing t3 tenv.
Proof.
intros until t3.
simpl in |- *.
case (typing t1 tenv).
intro; case t.
case (typing t2 tenv).
intro; case (typing t3 tenv).
intro t4; case (type_dec t0 t4).
intros.
rewrite e in |- *.
inversion H.
rewrite e in |- *.
split.
reflexivity.
split.
reflexivity.
reflexivity.
intros.
discriminate.
intro; discriminate.
intro; discriminate.
intros; discriminate.
intro; discriminate.
Qed.