2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "finite_lambda/reduction.ma".
15 axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
16 ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
18 axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
20 axiom red_closed: ∀O,D,M,M1.
21 is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
23 lemma critical: ∀O,D,ty,M,N.
25 .star (T O D) (red O D) (subst O D M 0 N) M3
26 ∧star (T O D) (red O D)
29 (map (FinSet_of_FType O D ty) (T O D)
30 (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
31 (enum (FinSet_of_FType O D ty)))) N) M3.
33 lapply (canonical_to_T O D N ty) * #a #Ha
34 %{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
36 |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
37 lapply (enum_complete (FinSet_of_FType O D ty) a)
38 elim (enum (FinSet_of_FType O D ty))
39 [normalize #H1 destruct (H1)
40 |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
41 [normalize >Hcase >(\P Hcase) //
42 |normalize cases (true_or_false (a==hd)) #Hcase1
43 [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
49 lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
50 red O D (Vec O D ty v) M →
51 red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
52 assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
55 .star (T O D) (red O D) M2 M3
56 ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
57 #O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
58 * #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
59 cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
60 [* >Ha -Ha #H1 destruct (H1) #Ha
61 %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
62 |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
67 lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
68 ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
69 ∧star (T O D) (red O D)
71 (map (FinSet_of_FType O D ty) (T O D)
72 (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
73 (enum (FinSet_of_FType O D ty)))) M3.
74 #O #D #ty #M1 #M2 #Hred
76 (map (FinSet_of_FType O D ty) (T O D)
77 (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
78 (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
80 |@star_red_vec2 [>length_map >length_map //] #n #M0
81 cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
82 [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
83 >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
84 |cut (n < |enum (FinSet_of_FType O D ty)|)
85 [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
86 cut (∃a:FinSet_of_FType O D ty.True)
87 [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
88 cases (enum (FinSet_of_FType O D ty))
89 [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
93 >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) #_
99 (* we need to proceed by structural induction on the term and then
100 by inversion on the two redexes. The problem are the moves in a
101 same subterm, since we need an induction hypothesis, there *)
103 lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
104 ∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
105 #O #D #M @(T_elim … M)
106 [#o #a #M1 #M2 #H elim(red_val ????? H)
107 |#n #M1 #M2 #H elim(red_rel ???? H)
108 |(* app : this is the interesting case *)
110 #M1 #M2 #H1 inversion H1 -H1
111 [(* right redex is beta *)
112 #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
113 [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
114 %{(subst O D Q1 0 N1)} (* CR-term *) /2/
115 |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
116 |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
117 [* #Q1 * #redQ #HM10 >HM10
118 %{(subst O D Q1 0 N0)} (* CR-term *) %
119 [@red_star_subst2 //|@R_to_star @rbeta @Hc]
122 |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
123 %{(subst O D Q 0 N1)} (* CR-term *)
124 %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
125 |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
126 |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
127 |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
129 |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
130 [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
131 |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
132 >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
133 |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
134 |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
135 |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
136 |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
137 |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
139 |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
141 [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
142 [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
143 [@R_to_star @rbeta @Hc|@red_star_subst2 // ]
144 |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
147 |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
148 lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
149 |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
150 lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
151 %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
152 |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
153 %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
154 |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
155 |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
156 |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
158 |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
160 [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
161 %{(subst O D M0 0 N1)} (* CR-term *) %
162 [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
163 |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
164 |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
165 %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
166 |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
167 lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
168 %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
169 |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
170 |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
171 |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
173 |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
174 |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
175 |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
176 #H1 destruct (H1) (* vacuous *)
178 |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
179 lapply (red_lambda … H1) *
180 [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
181 [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
182 %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
183 |#H5 >H5 @critical3 //
185 |#HM2 >HM2 lapply (red_lambda … H2) *
186 [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
187 * #H3 #H4 %{M5} (* CR-term *) % //
188 |#HM3 >HM3 %{M3} (* CR-term *) % //
191 |#ty #v1 #Hind #M1 #M2 #H1 #H2
192 lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
193 lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
194 >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
195 (* we must proceed by cases on the list *) * normalize
197 [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
198 [@mem_append_l2 %1 //]
200 %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
201 % [@star_red_vec //|@star_red_vec //]
202 |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
203 [@mem_append_l2 %1 //]
205 %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
206 % [@star_red_vec //|@star_red_vec //]
208 |(* N11 ≠ N21 *) -Hind #P #l *
209 [* #Hv11 #Hv22 destruct
210 %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
211 [>associative_append >associative_append normalize @rvec //
212 |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
214 |* #Hv11 #Hv22 destruct
215 %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
216 [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
217 |>associative_append >associative_append normalize @rvec //