-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathConv.v
187 lines (146 loc) · 4.52 KB
/
Conv.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
Require Export Term.
Section Church_Rosser.
Definition str_confluent R := commut _ R (transp term R).
Lemma str_confluence_par_red1 : str_confluent par_red1.
red in |- *; red in |- *.
simple induction 1; intros.
inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (subst x1 x0); unfold subst in |- *; auto with coc.
inversion_clear H5.
elim H1 with M'1; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (subst x1 x0); auto with coc; unfold subst in |- *; auto with coc.
inversion_clear H0.
exists (Srt s); auto with coc.
inversion_clear H0.
exists (Ref n); auto with coc.
inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with T'0; auto with coc; intros.
exists (Abs x1 x0); auto with coc.
generalize H0 H1.
clear H0 H1.
inversion_clear H4.
intro.
inversion_clear H4.
intros.
elim H4 with (Abs T M'0); auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
apply inv_par_red_abs with T' M'1 x0; intros; auto with coc.
generalize H7 H8.
rewrite H11.
clear H7 H8; intros.
inversion_clear H7.
inversion_clear H8.
exists (subst x1 U'); auto with coc.
unfold subst in |- *; auto with coc.
intros.
elim H5 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (App x0 x1); auto with coc.
intros.
inversion_clear H4.
elim H1 with M'0; auto with coc; intros.
elim H3 with N'0; auto with coc; intros.
exists (Prod x0 x1); auto with coc.
Qed.
Lemma strip_lemma : commut _ par_red (transp _ par_red1).
unfold commut, par_red in |- *; simple induction 1; intros.
elim str_confluence_par_red1 with z x0 y0; auto with coc; intros.
exists x1; auto with coc.
elim H1 with z0; auto with coc; intros.
elim H3 with x1; intros; auto with coc.
exists x2; auto with coc.
apply t_trans with x1; auto with coc.
Qed.
Lemma confluence_par_red : str_confluent par_red.
red in |- *; red in |- *.
simple induction 1; intros.
elim strip_lemma with z x0 y0; intros; auto with coc.
exists x1; auto with coc.
elim H1 with z0; intros; auto with coc.
elim H3 with x1; intros; auto with coc.
exists x2; auto with coc.
red in |- *.
apply t_trans with x1; auto with coc.
Qed.
Lemma confluence_red : str_confluent red.
red in |- *; red in |- *.
intros.
elim confluence_par_red with x y z; auto with coc; intros.
exists x0; auto with coc.
Qed.
Theorem church_rosser :
forall u v, conv u v -> exists2 t, red u t & red v t.
simple induction 1; intros.
exists u; auto with coc.
elim H1; intros.
elim confluence_red with x P N; auto with coc; intros.
exists x0; auto with coc.
apply trans_red_red with x; auto with coc.
elim H1; intros.
exists x; auto with coc.
apply trans_red_red with P; auto with coc.
Qed.
Lemma inv_conv_prod_l :
forall a b c d, conv (Prod a c) (Prod b d) -> conv a b.
intros.
elim church_rosser with (Prod a c) (Prod b d); intros; auto with coc.
apply red_prod_prod with a c x; intros; auto with coc.
apply red_prod_prod with b d x; intros; auto with coc.
apply trans_conv_conv with a0; auto with coc.
apply sym_conv.
generalize H2.
rewrite H5; intro.
injection H8.
simple induction 2; auto with coc.
Qed.
Lemma inv_conv_prod_r :
forall a b c d, conv (Prod a c) (Prod b d) -> conv c d.
intros.
elim church_rosser with (Prod a c) (Prod b d); intros; auto with coc.
apply red_prod_prod with a c x; intros; auto with coc.
apply red_prod_prod with b d x; intros; auto with coc.
apply trans_conv_conv with b0; auto with coc.
apply sym_conv.
generalize H2.
rewrite H5; intro.
injection H8.
simple induction 1; auto with coc.
Qed.
Lemma nf_uniqueness : forall u v, conv u v -> normal u -> normal v -> u = v.
intros.
elim church_rosser with u v; intros; auto with coc.
rewrite (red_normal u x); auto with coc.
elim red_normal with v x; auto with coc.
Qed.
Lemma conv_sort : forall s1 s2, conv (Srt s1) (Srt s2) -> s1 = s2.
intros.
cut (Srt s1 = Srt s2); intros.
injection H0; auto with coc.
apply nf_uniqueness; auto with coc.
red in |- *; red in |- *; intros.
inversion_clear H0.
red in |- *; red in |- *; intros.
inversion_clear H0.
Qed.
Lemma conv_kind_prop : ~ conv (Srt kind) (Srt prop).
red in |- *; intro.
absurd (kind = prop).
discriminate.
apply conv_sort; auto with coc.
Qed.
Lemma conv_sort_prod : forall s t u, ~ conv (Srt s) (Prod t u).
red in |- *; intros.
elim church_rosser with (Srt s) (Prod t u); auto with coc.
do 2 intro.
elim red_normal with (Srt s) x; auto with coc.
intro.
apply red_prod_prod with t u (Srt s); auto with coc; intros.
discriminate H2.
red in |- *; red in |- *; intros.
inversion_clear H1.
Qed.
End Church_Rosser.