--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "finite_lambda/reduction.ma".
+
+
+axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
+ ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
+
+axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
+
+axiom red_closed: ∀O,D,M,M1.
+ is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
+
+lemma critical: ∀O,D,ty,M,N.
+ ∃M3:T O D
+ .star (T O D) (red O D) (subst O D M 0 N) M3
+ ∧star (T O D) (red O D)
+ (App O D
+ (Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
+ (enum (FinSet_of_FType O D ty)))) N) M3.
+#O #D #ty #M #N
+lapply (canonical_to_T O D N ty) * #a #Ha
+%{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
+%[@red_star_subst @Ha
+ |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
+ lapply (enum_complete (FinSet_of_FType O D ty) a)
+ elim (enum (FinSet_of_FType O D ty))
+ [normalize #H1 destruct (H1)
+ |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
+ [normalize >Hcase >(\P Hcase) //
+ |normalize cases (true_or_false (a==hd)) #Hcase1
+ [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
+ ]
+ ]
+ ]
+qed.
+
+lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
+ red O D (Vec O D ty v) M →
+ red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
+ assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
+ =Some (T O D) M2 →
+ ∃M3:T O D
+ .star (T O D) (red O D) M2 M3
+ ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
+#O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
+* #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
+cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
+ [* >Ha -Ha #H1 destruct (H1) #Ha
+ %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
+ |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
+ ]
+qed.
+
+
+lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
+ ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
+ ∧star (T O D) (red O D)
+ (Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty)))) M3.
+#O #D #ty #M1 #M2 #Hred
+ %{(Vec O D ty
+ (map (FinSet_of_FType O D ty) (T O D)
+ (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
+ (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
+ [@R_to_star @rmem
+ |@star_red_vec2 [>length_map >length_map //] #n #M0
+ cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
+ [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
+ >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
+ |cut (n < |enum (FinSet_of_FType O D ty)|)
+ [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
+ cut (∃a:FinSet_of_FType O D ty.True)
+ [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
+ cases (enum (FinSet_of_FType O D ty))
+ [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
+ |#a #l #_ #_ %{a} //
+ ]
+ ] * #a #_
+ >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) #_
+ @red_star_subst2 //
+ ]
+ ]
+qed.
+
+(* we need to proceed by structural induction on the term and then
+by inversion on the two redexes. The problem are the moves in a
+same subterm, since we need an induction hypothesis, there *)
+
+lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
+∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
+#O #D #M @(T_elim … M)
+ [#o #a #M1 #M2 #H elim(red_val ????? H)
+ |#n #M1 #M2 #H elim(red_rel ???? H)
+ |(* app : this is the interesting case *)
+ #P #Q #HindP #HindQ
+ #M1 #M2 #H1 inversion H1 -H1
+ [(* right redex is beta *)
+ #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
+ [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
+ %{(subst O D Q1 0 N1)} (* CR-term *) /2/
+ |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
+ [* #Q1 * #redQ #HM10 >HM10
+ %{(subst O D Q1 0 N0)} (* CR-term *) %
+ [@red_star_subst2 //|@R_to_star @rbeta @Hc]
+ |#HM1 >HM1 @critical
+ ]
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
+ %{(subst O D Q 0 N1)} (* CR-term *)
+ %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
+ [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
+ >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
+ #Hl inversion Hl
+ [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
+ [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
+ [@R_to_star @rbeta @Hc|@red_star_subst2 // ]
+ |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
+ %{M3} /2/
+ ]
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
+ lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
+ lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
+ %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
+ |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
+ %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
+ #Hl inversion Hl
+ [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
+ %{(subst O D M0 0 N1)} (* CR-term *) %
+ [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
+ |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
+ |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
+ %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
+ |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
+ lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
+ %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
+ |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
+ |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ ]
+ |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
+ |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
+ |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
+ #H1 destruct (H1) (* vacuous *)
+ ]
+ |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
+ lapply (red_lambda … H1) *
+ [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
+ [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
+ %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
+ |#H5 >H5 @critical3 //
+ ]
+ |#HM2 >HM2 lapply (red_lambda … H2) *
+ [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
+ * #H3 #H4 %{M5} (* CR-term *) % //
+ |#HM3 >HM3 %{M3} (* CR-term *) % //
+ ]
+ ]
+ |#ty #v1 #Hind #M1 #M2 #H1 #H2
+ lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
+ lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
+ >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
+ (* we must proceed by cases on the list *) * normalize
+ [(* N11 = N21 *) *
+ [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
+ [@mem_append_l2 %1 //]
+ * #M3 * #HM31 #HM32
+ %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
+ % [@star_red_vec //|@star_red_vec //]
+ |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
+ [@mem_append_l2 %1 //]
+ * #M3 * #HM31 #HM32
+ %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
+ % [@star_red_vec //|@star_red_vec //]
+ ]
+ |(* N11 ≠ N21 *) -Hind #P #l *
+ [* #Hv11 #Hv22 destruct
+ %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
+ [>associative_append >associative_append normalize @rvec //
+ |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
+ ]
+ |* #Hv11 #Hv22 destruct
+ %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
+ [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
+ |>associative_append >associative_append normalize @rvec //
+ ]
+ ]
+ ]
+ ]
+qed.
+
+
+
+
projects / helm.git / blobdiff