From: Claudio Sacerdoti Coen Date: Fri, 28 Dec 2018 15:31:45 +0000 (+0100) Subject: finite_lambda restored X-Git-Tag: make_still_working~229^2~1^2~6 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=37f410bd78733673954a8d2890302d6df6032fad finite_lambda restored --- diff --git a/matita/matita/broken_lib/finite_lambda/confluence.ma b/matita/matita/broken_lib/finite_lambda/confluence.ma deleted file mode 100644 index 32b7e3ff0..000000000 --- a/matita/matita/broken_lib/finite_lambda/confluence.ma +++ /dev/null @@ -1,226 +0,0 @@ -(* - ||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 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 append_cons associative_append >associative_append normalize @rvec // - ] - ] - ] - ] -qed. - - - - diff --git a/matita/matita/broken_lib/finite_lambda/reduction.ma b/matita/matita/broken_lib/finite_lambda/reduction.ma deleted file mode 100644 index 98c56e10a..000000000 --- a/matita/matita/broken_lib/finite_lambda/reduction.ma +++ /dev/null @@ -1,308 +0,0 @@ -(* - ||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/terms_and_types.ma". - -(* some auxiliary lemmas *) - -lemma nth_to_default: ∀A,l,n,d. - |l| ≤ n → nth n A l d = d. -#A #l elim l [//] #a #tl #Hind #n cases n - [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le // - |#m #d normalize #H @Hind @le_S_S_to_le @H - ] -qed. - -lemma mem_nth: ∀A,l,n,d. - n < |l| → mem ? (nth n A l d) l. -#A #l elim l - [#n #d normalize #H @False_ind @(absurd … H) @lt_to_not_le // - |#a #tl #Hind * normalize - [#_ #_ %1 //| #m #d #HSS %2 @Hind @le_S_S_to_le @HSS] - ] -qed. - -lemma nth_map: ∀A,B,l,f,n,d1,d2. - n < |l| → nth n B (map … f l) d1 = f (nth n A l d2). -#n #B #l #f elim l - [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le // - |#a #tl #Hind #m #d1 #d2 cases m normalize // - #m1 #H @Hind @le_S_S_to_le @H - ] -qed. - - - -(* end of auxiliary lemmas *) - -let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝ - match ty return (λty.FinSet_of_FType O D ty → T O D) with - [atom o ⇒ λa.Val O D o a - |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1 - (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2)) - (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a)) - ] -. - -lemma is_closed_to_T: ∀O,D,ty,a. is_closed O D 0 (to_T O D ty a). -#O #D #ty elim ty // -#ty1 #ty2 #Hind1 #Hind2 #a normalize @cvec #m #Hmem -lapply (mem_map ????? Hmem) * #a1 * #H1 #H2

H //] -Hl1 -Hl2 - lapply e0 -e0 lapply l2 -l2 elim l1 - [#l2 cases l2 normalize [// |#a1 #tl1 #H destruct] - |#a1 #tl1 #Hind #l2 cases l2 - [normalize #H destruct - |#a2 #tl2 normalize #H @eq_f2 - [@Hind2 *) - -let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝ - match l1 with - [ nil ⇒ None ? - | cons hd1 tl1 ⇒ match l2 with - [ nil ⇒ None ? - | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2 - ] - ]. - -lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1. - assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1 - ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2). -#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1 - [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/] -qed. - -lemma assoc_to_mem: ∀A,B,a,l1,l2,b. - assoc A B a l1 l2 = Some ? b → mem ? b l2. -#A #B #a #l1 elim l1 - [#l2 #b normalize #H destruct - |#hd1 #tl1 #Hind * - [#b normalize #H destruct - |#hd2 #tl2 #b normalize cases (a==hd1) normalize - [#H %1 destruct //|#H %2 @Hind @H] - ] - ] -qed. - -lemma assoc_to_mem2: ∀A,B,a,l1,l2,b. - assoc A B a l1 l2 = Some ? b → ∃l21,l22.l2=l21@b::l22. -#A #B #a #l1 elim l1 - [#l2 #b normalize #H destruct - |#hd1 #tl1 #Hind * - [#b normalize #H destruct - |#hd2 #tl2 #b normalize cases (a==hd1) normalize - [#H %{[]} %{tl2} destruct // - |#H lapply (Hind … H) * #la * #lb #H1 - %{(hd2::la)} %{lb} >H1 //] - ] - ] -qed. - -lemma assoc_map: ∀A,B,C,a,l1,l2,f,b. - assoc A B a l1 l2 = Some ? b → assoc A C a l1 (map ?? f l2) = Some ? (f b). -#A #B #C #a #l1 elim l1 - [#l2 #f #b normalize #H destruct - |#hd1 #tl1 #Hind * - [#f #b normalize #H destruct - |#hd2 #tl2 #f #b normalize cases (a==hd1) normalize - [#H destruct // |#H @(Hind … H)] - ] - ] -qed. - -(*************************** One step reduction *******************************) - -inductive red (O:Type[0]) (D:O→FinSet) : T O D →T O D → Prop ≝ - | (* we only allow beta on closed arguments *) - rbeta: ∀P,M,N. is_closed O D 0 N → - red O D (App O D (Lambda O D P M) N) (subst O D M 0 N) - | riota: ∀ty,v,a,M. - assoc ?? a (enum (FinSet_of_FType O D ty)) v = Some ? M → - red O D (App O D (Vec O D ty v) (to_T O D ty a)) M - | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N) - | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1) - | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1) - | rmem: ∀ty,M. red O D (Lambda O D ty M) - (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) - (enum (FinSet_of_FType O D ty)))) - | rvec: ∀ty,N,N1,v,v1. red O D N N1 → - red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)). - -(*********************************** inversion ********************************) -lemma red_vec: ∀O,D,ty,v,M. - red O D (Vec O D ty v) M → ∃N,N1,v1,v2. - red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2). -#O #D #ty #v #M #Hred inversion Hred - [#ty1 #M0 #N #Hc #H destruct - |#ty1 #v1 #a #M0 #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#ty1 #M #M1 #_ #_ #H destruct - |#ty1 #M0 #H destruct - |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/ - ] -qed. - -lemma red_lambda: ∀O,D,ty,M,N. - red O D (Lambda O D ty M) N → - (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨ - N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) - (enum (FinSet_of_FType O D ty))). -#O #D #ty #M #N #Hred inversion Hred - [#ty1 #M0 #N #Hc #H destruct - |#ty1 #v1 #a #M0 #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % // - |#ty1 #M0 #H destruct #_ %2 // - |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct - ] -qed. - -lemma red_val: ∀O,D,ty,a,N. - red O D (Val O D ty a) N → False. -#O #D #ty #M #N #Hred inversion Hred - [#ty1 #M0 #N #Hc #H destruct - |#ty1 #v1 #a #M0 #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#ty1 #N1 #N2 #_ #_ #H destruct - |#ty1 #M0 #H destruct #_ - |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct - ] -qed. - -lemma red_rel: ∀O,D,n,N. - red O D (Rel O D n) N → False. -#O #D #n #N #Hred inversion Hred - [#ty1 #M0 #N #Hc #H destruct - |#ty1 #v1 #a #M0 #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#M0 #M1 #N #_ #_ #H destruct - |#ty1 #N1 #N2 #_ #_ #H destruct - |#ty1 #M0 #H destruct #_ - |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct - ] -qed. - -(*************************** multi step reduction *****************************) -lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 → - star ? (red O D) (App O D M N) (App O D M1 N). -#O #D #M #N #N1 #H elim H // -#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ -qed. - -lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 → - star ? (red O D) (App O D M N) (App O D M N1). -#O #D #M #N #N1 #H elim H // -#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ -qed. - -lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 → - star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)). -#O #D #ty #N #N1 #v1 #v2 #H elim H // -#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ -qed. - -lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| → - (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → - star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)). -#O #D #ty #v1 elim v1 - [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize // - |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS - #H @(trans_star … (Vec O D ty (v@N2::tl1))) - [@star_red_vec @(H 0 N1) @le_S_S // - |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS)) - #n #M #H1 @(H (S n)) @le_S_S @H1 - ] - ] -qed. - -lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| → - (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → - star ? (red O D) (Vec O D ty v1) (Vec O D ty v2). -#O #D #ty #v1 #v2 @(star_red_vec1 … [ ]) -qed. - -lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 → - star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1). -#O #D #ty #N #N1 #H elim H // -#P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ -qed. - -(************************ reduction and substitution **************************) - -lemma red_star_subst : ∀O,D,M,N,N1,i. - star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1). -#O #D #M #N #N1 #i #Hred lapply i -i @(T_elim … M) normalize - [#o #a #i // - |#i #n cases (leb n i) normalize // cases (eqb n i) normalize // - |#P #Q #HindP #HindQ #n normalize - @(trans_star … (App O D (subst O D P n N1) (subst O D Q n N))) - [@star_red_appl @HindP |@star_red_appr @HindQ] - |#ty #P #HindP #i @star_red_lambda @HindP - |#ty #v #Hindv #i @star_red_vec2 [>length_map >length_map //] - #j #Q inversion v [#_ normalize //] #a #tl #_ #Hv - cases (true_or_false (leb (S j) (|a::tl|))) #Hcase - [lapply (leb_true_to_le … Hcase) -Hcase #Hcase - >(nth_map ?????? a Hcase) >(nth_map ?????? a Hcase) #_ @Hindv >Hv @mem_nth // - |>nth_to_default - [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] - >nth_to_default - [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] // - ] - ] -qed. - -lemma red_star_subst2 : ∀O,D,M,M1,N,i. is_closed O D 0 N → - red O D M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N). -#O #D #M #M1 #N #i #HNc #Hred lapply i -i elim Hred - [#ty #P #Q #HQc #i normalize @starl_to_star @sstepl - [|@rbeta >(subst_closed … HQc) //] >(subst_closed … HQc) // - lapply (subst_lemma ?? P ?? i 0 (is_closed_mono … HQc) HNc) // - (subst_closed … (le_O_n …)) // - @R_to_star @riota @assoc_map @HP - |#P #P1 #Q #Hred #Hind #i normalize @star_red_appl @Hind - |#P #P1 #Q #Hred #Hind #i normalize @star_red_appr @Hind - |#ty #P #P1 #Hred #Hind #i normalize @star_red_lambda @Hind - |#ty #P #i normalize @starl_to_star @sstepl [|@rmem] - @star_to_starl @star_red_vec2 [>length_map >length_map >length_map //] - #n #Q >length_map #H - cut (∃a:(FinSet_of_FType O D ty).True) - [lapply H -H lapply (enum_complete (FinSet_of_FType O D ty)) - cases (enum (FinSet_of_FType O D ty)) - [#x normalize #H @False_ind @(absurd … H) @lt_to_not_le // - |#x #l #_ #_ %{x} // - ] - ] * #a #_ - >(nth_map ?????? a H) >(nth_map ?????? Q) [2:>length_map @H] - >(nth_map ?????? a H) - lapply (subst_lemma O D P (to_T O D ty - (nth n (FinSet_of_FType O D ty) (enum (FinSet_of_FType O D ty)) a)) - N i 0 (is_closed_mono … (is_closed_to_T …)) HNc) // H1 - Hx @Hind2 normalize // - |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize // - ] - ] - ] -qed. - -(* since we only consider beta reduction with closed arguments we could avoid -lifting. We define it for the sake of generality *) - -(* arguments: k is the nesting depth (starts from 0), p is the lift -let rec lift O D t k p on t ≝ - match t with - [ Val o a ⇒ Val O D o a - | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n - | App m n ⇒ App O D (lift O D m k p) (lift O D n k p) - | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p) - | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v) - ]. - -notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}. -notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}. - -interpretation "Lift" 'Lift n k M = (lift ?? M k n). - -let rec subst O D t k s on t ≝ - match t with - [ Val o a ⇒ Val O D o a - | Rel n ⇒ if (leb k n) then - (if (eqb k n) then lift O D s 0 n else Rel O D (n-1)) - else(Rel O D n) - | App m n ⇒ App O D (subst O D m k s) (subst O D n k s) - | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s) - | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) - ]. -*) - -(* simplified version of subst, assuming the argument s is closed *) - -let rec subst O D t k s on t ≝ - match t with - [ Val o a ⇒ Val O D o a - | Rel n ⇒ if (leb k n) then - (if (eqb k n) then (* lift O D s 0 n*) s else Rel O D (n-1)) - else(Rel O D n) - | App m n ⇒ App O D (subst O D m k s) (subst O D n k s) - | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s) - | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) - ]. -(* notation "hvbox(M break [ k ≝ N ])" - non associative with precedence 90 - for @{'Subst1 $M $k $N}. *) - -interpretation "Subst" 'Subst1 M k N = (subst M k N). - -(* -lemma subst_rel1: ∀O,D,A.∀k,i. i < k → - (Rel O D i) [k ≝ A] = Rel O D i. -#A #k #i normalize #ltik >(lt_to_leb_false … ltik) // -qed. - -lemma subst_rel2: ∀O,D, A.∀k. - (Rel k) [k ≝ A] = lift A 0 k. -#A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) // -qed. - -lemma subst_rel3: ∀A.∀k,i. k < i → - (Rel i) [k ≝ A] = Rel (i-1). -#A #k #i normalize #ltik >(le_to_leb_true k i) /2/ ->(not_eq_to_eqb_false k i) // @lt_to_not_eq // -qed. *) - - -(* closed terms ???? -let rec closed_k O D (t: T O D) k on t ≝ - match t with - [ Val o a ⇒ True - | Rel n ⇒ n < k - | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k) - | Lambda T n ⇒ closed_k O D n (k+1) - | Vec T v ⇒ closed_list O D v k - ] - -and closed_list O D (l: list (T O D)) k on l ≝ - match l with - [ nil ⇒ True - | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k - ] -. *) - -inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝ -| cval : ∀k,o,a.is_closed O D k (Val O D o a) -| crel : ∀k,n. n < k → is_closed O D k (Rel O D n) -| capp : ∀k,m,n. is_closed O D k m → is_closed O D k n → - is_closed O D k (App O D m n) -| clam : ∀T,k,m. is_closed O D (S k) m → is_closed O D k (Lambda O D T m) -| cvec: ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) → - is_closed O D k (Vec O D T v). - -lemma is_closed_rel: ∀O,D,n,k. - is_closed O D k (Rel O D n) → n < k. -#O #D #n #k #H inversion H - [#k0 #o #a #eqk #H destruct - |#k0 #n0 #ltn0 #eqk #H destruct // - |#k0 #M #N #_ #_ #_ #_ #_ #H destruct - |#T #k0 #M #_ #_ #_ #H destruct - |#T #k0 #v #_ #_ #_ #H destruct - ] -qed. - -lemma is_closed_app: ∀O,D,k,M, N. - is_closed O D k (App O D M N) → is_closed O D k M ∧ is_closed O D k N. -#O #D #k #M #N #H inversion H - [#k0 #o #a #eqk #H destruct - |#k0 #n0 #ltn0 #eqk #H destruct - |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct % // - |#T #k0 #M #_ #_ #_ #H destruct - |#T #k0 #v #_ #_ #_ #H destruct - ] -qed. - -lemma is_closed_lam: ∀O,D,k,ty,M. - is_closed O D k (Lambda O D ty M) → is_closed O D (S k) M. -#O #D #k #ty #M #H inversion H - [#k0 #o #a #eqk #H destruct - |#k0 #n0 #ltn0 #eqk #H destruct - |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct - |#T #k0 #M1 #HM1 #_ #_ #H1 destruct // - |#T #k0 #v #_ #_ #_ #H destruct - ] -qed. - -lemma is_closed_vec: ∀O,D,k,ty,v. - is_closed O D k (Vec O D ty v) → ∀m. mem ? m v → is_closed O D k m. -#O #D #k #ty #M #H inversion H - [#k0 #o #a #eqk #H destruct - |#k0 #n0 #ltn0 #eqk #H destruct - |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct - |#T #k0 #M1 #HM1 #_ #_ #H1 destruct - |#T #k0 #v #Hv #_ #_ #H1 destruct @Hv - ] -qed. - -lemma is_closed_S: ∀O,D,M,m. - is_closed O D m M → is_closed O D (S m) M. -#O #D #M #m #H elim H // - [#k #n0 #Hlt @crel @le_S // - |#k #P #Q #HP #HC #H1 #H2 @capp // - |#ty #k #P #HP #H1 @clam // - |#ty #k #v #Hind #Hv @cvec @Hv - ] -qed. - -lemma is_closed_mono: ∀O,D,M,m,n. m ≤ n → - is_closed O D m M → is_closed O D n M. -#O #D #M #m #n #lemn elim lemn // #i #j #H #H1 @is_closed_S @H @H1 -qed. - - -(*** properties of lift and subst ***) - -(* -lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t. -#O #D #t @(T_elim … t) normalize // - [#n #k cases (leb k n) normalize // - |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // - #hd #tl #Hind #Hind1 normalize @eq_f2 - [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //] - ] -qed. - -lemma lift_closed: ∀O,D.∀t:T O D.∀k,p. - is_closed O D k t → lift O D t k p = t. -#O #D #t @(T_elim … t) normalize // - [#n #k #p #H >(not_le_to_leb_false … (lt_to_not_le … (is_closed_rel … H))) // - |#M #N #HindM #HindN #k #p #H lapply (is_closed_app … H) * #HcM #HcN - >(HindM … HcM) >(HindN … HcN) // - |#ty #M #HindM #k #p #H lapply (is_closed_lam … H) -H #H >(HindM … H) // - |#ty #v #HindM #k #p #H lapply (is_closed_vec … H) -H #H @eq_f - cut (∀m. mem ? m v → lift O D m k p = m) - [#m #Hmem @HindM [@Hmem | @H @Hmem]] -HindM - elim v // #a #tl #Hind #H1 normalize @eq_f2 - [@H1 %1 //|@Hind #m #Hmem @H1 %2 @Hmem] - ] -qed. - -*) - -lemma subst_closed: ∀O,D,M,N,k,i. k ≤ i → - is_closed O D k M → subst O D M i N = M. -#O #D #M @(T_elim … M) - [#o #a normalize // - |#n #N #k #j #Hlt #Hc lapply (is_closed_rel … Hc) #Hnk normalize - >not_le_to_leb_false [2:@lt_to_not_le @(lt_to_le_to_lt … Hnk Hlt)] // - |#P #Q #HindP #HindQ #N #k #i #ltki #Hc lapply (is_closed_app … Hc) * - #HcP #HcQ normalize >(HindP … ltki HcP) >(HindQ … ltki HcQ) // - |#ty #P #HindP #N #k #i #ltki #Hc lapply (is_closed_lam … Hc) - #HcP normalize >(HindP … HcP) // @le_S_S @ltki - |#ty #v #Hindv #N #k #i #ltki #Hc lapply (is_closed_vec … Hc) - #Hcv normalize @eq_f - cut (∀m:T O D.mem (T O D) m v→ subst O D m i N=m) - [#m #Hmem @(Hindv … Hmem N … ltki) @Hcv @Hmem] - elim v // #a #tl #Hind #H normalize @eq_f2 - [@H %1 //| @Hind #Hmem #Htl @H %2 @Htl] - ] -qed. - -lemma subst_lemma: ∀O,D,A,B,C,k,i. is_closed O D k B → is_closed O D i C → - subst O D (subst O D A i B) (k+i) C = - subst O D (subst O D A (k+S i) C) i B. -#O #D #A #B #C #k @(T_elim … A) normalize - [// - |#n #i #HBc #HCc @(leb_elim i n) #Hle - [@(eqb_elim i n) #eqni - [(lt_to_leb_false (k+(S i)) i) // normalize - >(subst_closed … HBc) // >le_to_leb_true // >eq_to_eqb_true // - |(cut (i < n)) - [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin - (cut (0 < n)) [@(le_to_lt_to_lt … ltin) //] #posn - normalize @(leb_elim (k+i) (n-1)) #nk - [@(eqb_elim (k+i) (n-1)) #H normalize - [cut (k+(S i) = n); [/2 by S_pred/] #H1 - >(le_to_leb_true (k+(S i)) n) /2/ - >(eq_to_eqb_true … H1) normalize >(subst_closed … HCc) // - |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt - >(le_to_leb_true (k+(S i)) n) normalize - [>(not_eq_to_eqb_false (k+(S i)) n) normalize - [>le_to_leb_true [2:@lt_to_le @(le_to_lt_to_lt … Hlt) //] - >not_eq_to_eqb_false // @lt_to_not_eq @(le_to_lt_to_lt … Hlt) // - |@(not_to_not … H) #Hn /2 by plus_minus/ - ] - |(not_le_to_leb_false (k+(S i)) n) normalize - [>(le_to_leb_true … Hle) >(not_eq_to_eqb_false … eqni) // - |@(not_to_not … nk) #H @le_plus_to_minus_r // - ] - ] - ] - |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2 by not_le_to_lt/] #ltn - >not_le_to_leb_false [2: @lt_to_not_le @(transitive_lt …ltn) //] normalize - >not_le_to_leb_false [2: @lt_to_not_le //] normalize - >(not_le_to_leb_false … Hle) // - ] - |#M #N #HindM #HindN #i #HBC #HCc @eq_f2 [@HindM // |@HindN //] - |#ty #M #HindM #i #HBC #HCc @eq_f >plus_n_Sm >plus_n_Sm @HindM // - @is_closed_S // - |#ty #v #Hindv #i #HBC #HCc @eq_f - cut (∀m.mem ? m v → subst O D (subst O D m i B) (k+i) C = - subst O D (subst O D m (k+S i) C) i B) - [#m #Hmem @Hindv //] -Hindv elim v normalize [//] - #a #tl #Hind #H @eq_f2 [@H %1 // | @Hind #m #Hmem @H %2 //] - ] -qed. - - diff --git a/matita/matita/broken_lib/finite_lambda/typing.ma b/matita/matita/broken_lib/finite_lambda/typing.ma deleted file mode 100644 index 791e27d66..000000000 --- a/matita/matita/broken_lib/finite_lambda/typing.ma +++ /dev/null @@ -1,229 +0,0 @@ -(* - ||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". - - -(****************************************************************) - -inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝ - | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o) - | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty - | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 → - TJ O D G (App O D M N) ty2 - | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 → - TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2) - | tvec: ∀G,v,ty1,ty2. - (|v| = |enum (FinSet_of_FType O D ty1)|) → - (∀M. mem ? M v → TJ O D G M ty2) → - TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2). - -lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty. -#O #D #G #ty elim ty - [#o #a normalize @tval - |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec - [length_map >length_map // - |#M elim v - [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]] - ] - ] -qed. - -lemma inv_rel: ∀O,D,G,n,ty. - TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2. -#O #D #G #n #ty #Hrel inversion Hrel - [#G1 #o #a #_ #H destruct - |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/ - |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct - |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct - |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct - ] -qed. - -lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3. - TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) → - ty1 = ty2 ∧ TJ O D (ty2::G) M ty3. -#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam - [#G1 #o #a #_ #H destruct - |#G1 #ty #G2 #n #_ #_ #H destruct - |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct - |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % // - |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct - ] -qed. - -lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3. - TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) → - (|v| = |enum (FinSet_of_FType O D ty1)|) ∧ - (∀M. mem ? M v → TJ O D G M ty3). -#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec - [#G #o #a #_ #H destruct - |#G1 #ty #G2 #n #_ #_ #H destruct - |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct - |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct - |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem - ] -qed. - -(* could be generalized *) -lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → - TJ O D (G1@G2) (Rel O D n) ty1 → - TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1. -#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel) -* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2) -* #G5 * - [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4 - @(absurd … H4) @le_to_not_lt // - |* #H3 #H4 >H4 >append_cons length_append >length_append

H3 >length_append normalize - >plus_n_Sm >associative_plus @eq_f // - ] -qed. - -lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → - TJ O D (G1@ty2::G2) (Rel O D n) ty1 → - TJ O D (G1@G2) (Rel O D (n-1)) ty1. -#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel) -* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2) -* #G5 * - [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4 - @(absurd … H4) @le_to_not_lt // - |lapply G5 -G5 * - [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1) - @le_to_not_lt // - |#ty3 #G5 * #H3 normalize #H4 destruct (H4) H3 >length_append >length_append normalize H1 >length_append // - |* cases G6 - [>append_nil normalize #H1 @False_ind - @(absurd ? Hlt) @le_to_not_lt H1 // - |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel // - ] - ] - |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3 - #Heq #Hc lapply (is_closed_app … Hc) -Hc * #HMc #HNc - @(tapp … (HindM … Heq HMc) (HindN … Heq HNc)) - |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq #Hc - lapply (is_closed_lam … Hc) -Hc #HMc - @tlambda @(HindM (ty1::G1) G2) [>Heq // |@HMc] - |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 #Hc @tvec - [>length_map // - |#M #Hmem @Hind // lapply (is_closed_vec … Hc) #Hvc @Hvc // - ] - ] -qed. - -lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a. -#A #a #d #l1 elim l1 normalize - [#l2 #n #Hn H cases (le_to_or_lt_eq … (leb_true_to_le … H)) - [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize - lapply (compare_append … HG) * #G3 * - [* #HG1 #HG2 @(strength_rel … tyN … ltn) HG in ltn; >length_append #ltn @False_ind - @(absurd … ltn) @le_to_not_lt >Hlen // - ] - |#HG21 >(eq_to_eqb_true … HG21) - cut (ty = tyN) - [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty - normalize H normalize lapply (compare_append … HG) * #G3 * - [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1 - >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt - @(leb_false_to_not_le … H) - |cases G3 - [>append_nil * #H1 @False_ind @(absurd ? Hlen)

associative_append @trel // - ] - ] - ] - |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG - #HN0 #Hc normalize @(tapp … ty1) - [@(HindM … eqG HN0 Hc) |@(HindN … eqG HN0 Hc)] - |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG - #HN0 #Hc normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) // >eqG // - |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG - #HN0 #Hc normalize @(tvec … ty1) - [>length_map @Hlen - |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM HM1 @tlambda @Hind // - |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN) - * #a * #mema #eqN H3 @tvec - [H2 >length_append >length_append @eq_f // - |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem - [@Hv >H2 @mem_append_l1 // - |cases Hmem - [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 // - |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 // - ] - ] - ] - ] -qed. - diff --git a/matita/matita/lib/basics/deqlist.ma b/matita/matita/lib/basics/deqlist.ma new file mode 100644 index 000000000..c559448ba --- /dev/null +++ b/matita/matita/lib/basics/deqlist.ma @@ -0,0 +1,63 @@ +(* + ||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 "basics/deqsets.ma". +include "basics/lists/listb.ma". + +(* + +record DeqSet : Type[1] ≝ { + carr :> Type[0]; + eqb: carr → carr → bool; + eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y) +}. *) + + +(* list *) + +let rec eq_list (A:DeqSet) (l1,l2:list A) on l1 ≝ + match l1 with + [ nil ⇒ match l2 with [nil ⇒ true | _ ⇒ false] + | cons a1 tl1 ⇒ + match l2 with [nil ⇒ false | cons a2 tl2 ⇒ a1 ==a2 ∧ eq_list A tl1 tl2]]. + +lemma eq_list_true: ∀A:DeqSet.∀l1,l2:list A. + eq_list A l1 l2 = true ↔ l1 = l2. +#A #l1 elim l1 + [* [% // |#a #tl % normalize #H destruct ] + |#a1 #tl1 #Hind * + [normalize % #H destruct + |#a2 #tl2 normalize % + [cases (true_or_false (a1==a2)) #Heq >Heq normalize + [#Htl >(\P Heq) >(proj1 … (Hind tl2) Htl) // | #H destruct ] + |#H destruct >(\b (refl … )) >(proj2 … (Hind tl2) (refl …)) // + ] + ] + ] +qed. + +definition DeqList ≝ λA:DeqSet. + mk_DeqSet (list A) (eq_list A) (eq_list_true A). + +unification hint 0 ≔ C; + T ≟ carr C, + X ≟ DeqList C +(* ---------------------------------------- *) ⊢ + list T ≡ carr X. + +alias id "eqb" = "cic:/matita/basics/deqsets/eqb#fix:0:0:3". +alias symbol "hint_decl" (instance 1) = "hint_decl_Type0". +unification hint 0 ≔ T,a1,a2; + X ≟ DeqList T +(* ---------------------------------------- *) ⊢ + eq_list T a1 a2 ≡ eqb X a1 a2. + + diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma index df8d0a87c..24a5e16ce 100644 --- a/matita/matita/lib/basics/finset.ma +++ b/matita/matita/lib/basics/finset.ma @@ -9,7 +9,7 @@ \ / GNU General Public License Version 2 V_______________________________________________________________ *) -include "basics/lists/listb.ma". +include "basics/deqlist.ma". (****** DeqSet: a set with a decidable equality ******) @@ -270,3 +270,184 @@ f a = b → memb ? 〈a,b〉 (graph_enum A B f) = true. #A #B #f #a #b #eqf @memb_filter_l [@(\b eqf)] @enum_prod_complete // qed. + +(* FinFun *) + +definition enum_fun_raw: ∀A,B:DeqSet.list A → list B → list (list (DeqProd A B)) ≝ + λA,B,lA,lB.foldr A (list (list (DeqProd A B))) + (λa.compose ??? (λb. cons ? 〈a,b〉) lB) [[]] lA. + +lemma enum_fun_raw_cons: ∀A,B,a,lA,lB. + enum_fun_raw A B (a::lA) lB = + compose ??? (λb. cons ? 〈a,b〉) lB (enum_fun_raw A B lA lB). +// +qed. + +definition is_functional ≝ λA,B:DeqSet.λlA:list A.λl: list (DeqProd A B). + map ?? (fst A B) l = lA. + +definition carr_fun ≝ λA,B:FinSet. + DeqSig (DeqList (DeqProd A B)) (is_functional A B (enum A)). + +definition carr_fun_l ≝ λA,B:DeqSet.λl. + DeqSig (DeqList (DeqProd A B)) (is_functional A B l). + +lemma compose_spec1 : ∀A,B,C:DeqSet.∀f:A→B→C.∀a:A.∀b:B.∀lA:list A.∀lB:list B. + a ∈ lA = true → b ∈ lB = true → ((f a b) ∈ (compose A B C f lA lB)) = true. +#A #B #C #f #a #b #lA elim lA + [normalize #lB #H destruct + |#a1 #tl #Hind #lB #Ha #Hb cases (orb_true_l ?? Ha) #Hcase + [>(\P Hcase) normalize @memb_append_l1 @memb_map // + |@memb_append_l2 @Hind // + ] + ] +qed. + +lemma compose_cons: ∀A,B,C.∀f:A→B→C.∀l1,l2,a. + compose A B C f (a::l1) l2 = + (map ?? (f a) l2)@(compose A B C f l1 l2). +// qed. + +lemma compose_spec2 : ∀A,B,C:DeqSet.∀f:A→B→C.∀c:C.∀lA:list A.∀lB:list B. + c ∈ (compose A B C f lA lB) = true → + ∃a,b.a ∈ lA = true ∧ b ∈ lB = true ∧ c = f a b. +#A #B #C #f #c #lA elim lA + [normalize #lB #H destruct + |#a1 #tl #Hind #lB >compose_cons #Hc cases (memb_append … Hc) #Hcase + [lapply(memb_map_to_exists … Hcase) * #b * #Hb #Hf + %{a1} %{b} /3/ + |lapply(Hind ? Hcase) * #a2 * #b * * #Ha #Hb #Hf %{a2} %{b} % // % // + @orb_true_r2 // + ] + ] +qed. + +definition compose2 ≝ + λA,B:DeqSet.λa:A.λl. compose B (carr_fun_l A B l) (carr_fun_l A B (a::l)) + (λb,tl. mk_Sig ?? (〈a,b〉::(pi1 … tl)) ?). +normalize @eq_f @(pi2 … tl) +qed. + +let rec Dfoldr (A:Type[0]) (B:list A → Type[0]) + (f:∀a:A.∀l.B l → B (a::l)) (b:B [ ]) (l:list A) on l : B l ≝ + match l with [ nil ⇒ b | cons a l ⇒ f a l (Dfoldr A B f b l)]. + +definition empty_graph: ∀A,B:DeqSet. carr_fun_l A B []. +#A #B %{[]} // qed. + +definition enum_fun: ∀A,B:DeqSet.∀lA:list A.list B → list (carr_fun_l A B lA) ≝ + λA,B,lA,lB.Dfoldr A (λl.list (carr_fun_l A B l)) + (λa,l.compose2 ?? a l lB) [empty_graph A B] lA. + +lemma mem_enum_fun: ∀A,B:DeqSet.∀lA,lB.∀x:carr_fun_l A B lA. + pi1 … x ∈ map ?? (pi1 … ) (enum_fun A B lA lB) = true → + x ∈ enum_fun A B lA lB = true . +#A #B #lA #lB #x @(memb_map_inj + (DeqSig (DeqList (DeqProd A B)) + (λx0:DeqList (DeqProd A B).is_functional A B lA x0)) + (DeqList (DeqProd A B)) (pi1 …)) +* #l1 #H1 * #l2 #H2 #Heq lapply H1 lapply H2 >Heq // +qed. + +lemma enum_fun_cons: ∀A,B,a,lA,lB. + enum_fun A B (a::lA) lB = + compose ??? (λb,tl. mk_Sig ?? (〈a,b〉::(pi1 … tl)) ?) lB (enum_fun A B lA lB). +// +qed. + +lemma map_map: ∀A,B,C.∀f:A→B.∀g:B→C.∀l. + map ?? g (map ?? f l) = map ?? (g ∘ f) l. +#A #B #C #f #g #l elim l [//] +#a #tl #Hind normalize @eq_f @Hind +qed. + +lemma map_compose: ∀A,B,C,D.∀f:A→B→C.∀g:C→D.∀l1,l2. + map ?? g (compose A B C f l1 l2) = compose A B D (λa,b. g (f a b)) l1 l2. +#A #B #C #D #f #g #l1 elim l1 [//] +#a #tl #Hind #l2 >compose_cons >compose_cons (enum_fun_cons A B a tl lB) >enum_fun_raw_cons >map_compose +cut (∀lB2. compose B (Σx:DeqList (DeqProd A B).is_functional A B tl x) + (DeqList (DeqProd A B)) + (λa0:B + .λb:Σx:DeqList (DeqProd A B).is_functional A B tl x + .〈a,a0〉 + ::pi1 (list (A×B)) (λx:DeqList (DeqProd A B).is_functional A B tl x) b) lB + (enum_fun A B tl lB2) + =compose B (list (A×B)) (list (A×B)) (λb:B.cons (A×B) 〈a,b〉) lB + (enum_fun_raw A B tl lB2)) + [#lB2 elim lB + [normalize // + |#b #tlb #Hindb >compose_cons in ⊢ (???%); >compose_cons + @eq_f2 [map_map // |@Hindb]]] +#Hcut @Hcut +qed. + +lemma uniqueb_compose: ∀A,B,C:DeqSet.∀f,l1,l2. + (∀a1,a2,b1,b2. f a1 b1 = f a2 b2 → a1 = a2 ∧ b1 = b2) → + uniqueb ? l1 = true → uniqueb ? l2 = true → + uniqueb ? (compose A B C f l1 l2) = true. +#A #B #C #f #l1 #l2 #Hinj elim l1 // +#a #tl #Hind #HuA #HuB >compose_cons @uniqueb_append + [@(unique_map_inj … HuB) #b1 #b2 #Hb1b2 @(proj2 … (Hinj … Hb1b2)) + |@Hind // @(andb_true_r … HuA) + |#c #Hc lapply(memb_map_to_exists … Hc) * #b * #Hb2 #Hfab % #Hc + lapply(compose_spec2 … Hc) * #a1 * #b1 * * #Ha1 #Hb1 H + normalize #H1 destruct (H1) + ] + ] +qed. + +lemma enum_fun_unique: ∀A,B:DeqSet.∀lA,lB. + uniqueb ? lA = true → uniqueb ? lB = true → + uniqueb ? (enum_fun A B lA lB) = true. +#A #B #lA elim lA + [#lB #_ #ulB // + |#a #tlA #Hind #lB #uA #uB lapply (enum_fun_cons A B a tlA lB) #H >H + @(uniqueb_compose B (carr_fun_l A B tlA) (carr_fun_l A B (a::tlA))) + [#b1 #b2 * #l1 #funl1 * #l2 #funl2 #H1 destruct (H1) /2/ + |// + |@(Hind … uB) @(andb_true_r … uA) + ] + ] +qed. + +lemma enum_fun_complete: ∀A,B:FinSet.∀l1,l2. + (∀x:A. memb A x l1 = true) → + (∀x:B. memb B x l2 = true) → + ∀x:carr_fun_l A B l1. memb ? x (enum_fun A B l1 l2) = true. +#A #B #l1 #l2 #H1 #H2 * #g #H @mem_enum_fun >enum_fun_graphs +lapply H -H lapply g -g elim l1 + [* // #p #tlg normalize #H destruct (H) + |#a #tl #Hind #g cases g + [normalize in ⊢ (%→?); #H destruct (H) + |* #a1 #b #tl1 normalize in ⊢ (%→?); #H + cut (is_functional A B tl tl1) [destruct (H) //] #Hfun + >(cons_injective_l ????? H) + >(enum_fun_raw_cons … ) @(compose_spec1 … (λb. cons ? 〈a,b〉)) + [@H2 |@Hind @Hfun] + ] + ] +qed. + +definition FinFun ≝ +λA,B:FinSet.mk_FinSet (carr_fun A B) + (enum_fun A B (enum A) (enum B)) + (enum_fun_unique A B … (enum_unique A) (enum_unique B)) + (enum_fun_complete A B … (enum_complete A) (enum_complete B)). + +(* +unification hint 0 ≔ C1,C2; + T1 ≟ FinSetcarr C1, + T2 ≟ FinSetcarr C2, + X ≟ FinProd C1 C2 +(* ---------------------------------------- *) ⊢ + T1×T2 ≡ FinSetcarr X. *) \ No newline at end of file diff --git a/matita/matita/lib/finite_lambda/confluence.ma b/matita/matita/lib/finite_lambda/confluence.ma new file mode 100644 index 000000000..32b7e3ff0 --- /dev/null +++ b/matita/matita/lib/finite_lambda/confluence.ma @@ -0,0 +1,226 @@ +(* + ||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 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 append_cons associative_append >associative_append normalize @rvec // + ] + ] + ] + ] +qed. + + + + diff --git a/matita/matita/lib/finite_lambda/reduction.ma b/matita/matita/lib/finite_lambda/reduction.ma new file mode 100644 index 000000000..98c56e10a --- /dev/null +++ b/matita/matita/lib/finite_lambda/reduction.ma @@ -0,0 +1,308 @@ +(* + ||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/terms_and_types.ma". + +(* some auxiliary lemmas *) + +lemma nth_to_default: ∀A,l,n,d. + |l| ≤ n → nth n A l d = d. +#A #l elim l [//] #a #tl #Hind #n cases n + [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le // + |#m #d normalize #H @Hind @le_S_S_to_le @H + ] +qed. + +lemma mem_nth: ∀A,l,n,d. + n < |l| → mem ? (nth n A l d) l. +#A #l elim l + [#n #d normalize #H @False_ind @(absurd … H) @lt_to_not_le // + |#a #tl #Hind * normalize + [#_ #_ %1 //| #m #d #HSS %2 @Hind @le_S_S_to_le @HSS] + ] +qed. + +lemma nth_map: ∀A,B,l,f,n,d1,d2. + n < |l| → nth n B (map … f l) d1 = f (nth n A l d2). +#n #B #l #f elim l + [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le // + |#a #tl #Hind #m #d1 #d2 cases m normalize // + #m1 #H @Hind @le_S_S_to_le @H + ] +qed. + + + +(* end of auxiliary lemmas *) + +let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝ + match ty return (λty.FinSet_of_FType O D ty → T O D) with + [atom o ⇒ λa.Val O D o a + |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1 + (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2)) + (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a)) + ] +. + +lemma is_closed_to_T: ∀O,D,ty,a. is_closed O D 0 (to_T O D ty a). +#O #D #ty elim ty // +#ty1 #ty2 #Hind1 #Hind2 #a normalize @cvec #m #Hmem +lapply (mem_map ????? Hmem) * #a1 * #H1 #H2

H //] -Hl1 -Hl2 + lapply e0 -e0 lapply l2 -l2 elim l1 + [#l2 cases l2 normalize [// |#a1 #tl1 #H destruct] + |#a1 #tl1 #Hind #l2 cases l2 + [normalize #H destruct + |#a2 #tl2 normalize #H @eq_f2 + [@Hind2 *) + +let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝ + match l1 with + [ nil ⇒ None ? + | cons hd1 tl1 ⇒ match l2 with + [ nil ⇒ None ? + | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2 + ] + ]. + +lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1. + assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1 + ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2). +#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1 + [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/] +qed. + +lemma assoc_to_mem: ∀A,B,a,l1,l2,b. + assoc A B a l1 l2 = Some ? b → mem ? b l2. +#A #B #a #l1 elim l1 + [#l2 #b normalize #H destruct + |#hd1 #tl1 #Hind * + [#b normalize #H destruct + |#hd2 #tl2 #b normalize cases (a==hd1) normalize + [#H %1 destruct //|#H %2 @Hind @H] + ] + ] +qed. + +lemma assoc_to_mem2: ∀A,B,a,l1,l2,b. + assoc A B a l1 l2 = Some ? b → ∃l21,l22.l2=l21@b::l22. +#A #B #a #l1 elim l1 + [#l2 #b normalize #H destruct + |#hd1 #tl1 #Hind * + [#b normalize #H destruct + |#hd2 #tl2 #b normalize cases (a==hd1) normalize + [#H %{[]} %{tl2} destruct // + |#H lapply (Hind … H) * #la * #lb #H1 + %{(hd2::la)} %{lb} >H1 //] + ] + ] +qed. + +lemma assoc_map: ∀A,B,C,a,l1,l2,f,b. + assoc A B a l1 l2 = Some ? b → assoc A C a l1 (map ?? f l2) = Some ? (f b). +#A #B #C #a #l1 elim l1 + [#l2 #f #b normalize #H destruct + |#hd1 #tl1 #Hind * + [#f #b normalize #H destruct + |#hd2 #tl2 #f #b normalize cases (a==hd1) normalize + [#H destruct // |#H @(Hind … H)] + ] + ] +qed. + +(*************************** One step reduction *******************************) + +inductive red (O:Type[0]) (D:O→FinSet) : T O D →T O D → Prop ≝ + | (* we only allow beta on closed arguments *) + rbeta: ∀P,M,N. is_closed O D 0 N → + red O D (App O D (Lambda O D P M) N) (subst O D M 0 N) + | riota: ∀ty,v,a,M. + assoc ?? a (enum (FinSet_of_FType O D ty)) v = Some ? M → + red O D (App O D (Vec O D ty v) (to_T O D ty a)) M + | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N) + | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1) + | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1) + | rmem: ∀ty,M. red O D (Lambda O D ty M) + (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) + (enum (FinSet_of_FType O D ty)))) + | rvec: ∀ty,N,N1,v,v1. red O D N N1 → + red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)). + +(*********************************** inversion ********************************) +lemma red_vec: ∀O,D,ty,v,M. + red O D (Vec O D ty v) M → ∃N,N1,v1,v2. + red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2). +#O #D #ty #v #M #Hred inversion Hred + [#ty1 #M0 #N #Hc #H destruct + |#ty1 #v1 #a #M0 #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#ty1 #M #M1 #_ #_ #H destruct + |#ty1 #M0 #H destruct + |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/ + ] +qed. + +lemma red_lambda: ∀O,D,ty,M,N. + red O D (Lambda O D ty M) N → + (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨ + N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) + (enum (FinSet_of_FType O D ty))). +#O #D #ty #M #N #Hred inversion Hred + [#ty1 #M0 #N #Hc #H destruct + |#ty1 #v1 #a #M0 #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % // + |#ty1 #M0 #H destruct #_ %2 // + |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct + ] +qed. + +lemma red_val: ∀O,D,ty,a,N. + red O D (Val O D ty a) N → False. +#O #D #ty #M #N #Hred inversion Hred + [#ty1 #M0 #N #Hc #H destruct + |#ty1 #v1 #a #M0 #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#ty1 #N1 #N2 #_ #_ #H destruct + |#ty1 #M0 #H destruct #_ + |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct + ] +qed. + +lemma red_rel: ∀O,D,n,N. + red O D (Rel O D n) N → False. +#O #D #n #N #Hred inversion Hred + [#ty1 #M0 #N #Hc #H destruct + |#ty1 #v1 #a #M0 #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#M0 #M1 #N #_ #_ #H destruct + |#ty1 #N1 #N2 #_ #_ #H destruct + |#ty1 #M0 #H destruct #_ + |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct + ] +qed. + +(*************************** multi step reduction *****************************) +lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 → + star ? (red O D) (App O D M N) (App O D M1 N). +#O #D #M #N #N1 #H elim H // +#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ +qed. + +lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 → + star ? (red O D) (App O D M N) (App O D M N1). +#O #D #M #N #N1 #H elim H // +#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ +qed. + +lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 → + star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)). +#O #D #ty #N #N1 #v1 #v2 #H elim H // +#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ +qed. + +lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| → + (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → + star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)). +#O #D #ty #v1 elim v1 + [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize // + |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS + #H @(trans_star … (Vec O D ty (v@N2::tl1))) + [@star_red_vec @(H 0 N1) @le_S_S // + |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS)) + #n #M #H1 @(H (S n)) @le_S_S @H1 + ] + ] +qed. + +lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| → + (∀n,M. n < |v1| → star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → + star ? (red O D) (Vec O D ty v1) (Vec O D ty v2). +#O #D #ty #v1 #v2 @(star_red_vec1 … [ ]) +qed. + +lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 → + star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1). +#O #D #ty #N #N1 #H elim H // +#P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ +qed. + +(************************ reduction and substitution **************************) + +lemma red_star_subst : ∀O,D,M,N,N1,i. + star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1). +#O #D #M #N #N1 #i #Hred lapply i -i @(T_elim … M) normalize + [#o #a #i // + |#i #n cases (leb n i) normalize // cases (eqb n i) normalize // + |#P #Q #HindP #HindQ #n normalize + @(trans_star … (App O D (subst O D P n N1) (subst O D Q n N))) + [@star_red_appl @HindP |@star_red_appr @HindQ] + |#ty #P #HindP #i @star_red_lambda @HindP + |#ty #v #Hindv #i @star_red_vec2 [>length_map >length_map //] + #j #Q inversion v [#_ normalize //] #a #tl #_ #Hv + cases (true_or_false (leb (S j) (|a::tl|))) #Hcase + [lapply (leb_true_to_le … Hcase) -Hcase #Hcase + >(nth_map ?????? a Hcase) >(nth_map ?????? a Hcase) #_ @Hindv >Hv @mem_nth // + |>nth_to_default + [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] + >nth_to_default + [2:>length_map @le_S_S_to_le @not_le_to_lt @leb_false_to_not_le //] // + ] + ] +qed. + +lemma red_star_subst2 : ∀O,D,M,M1,N,i. is_closed O D 0 N → + red O D M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N). +#O #D #M #M1 #N #i #HNc #Hred lapply i -i elim Hred + [#ty #P #Q #HQc #i normalize @starl_to_star @sstepl + [|@rbeta >(subst_closed … HQc) //] >(subst_closed … HQc) // + lapply (subst_lemma ?? P ?? i 0 (is_closed_mono … HQc) HNc) // + (subst_closed … (le_O_n …)) // + @R_to_star @riota @assoc_map @HP + |#P #P1 #Q #Hred #Hind #i normalize @star_red_appl @Hind + |#P #P1 #Q #Hred #Hind #i normalize @star_red_appr @Hind + |#ty #P #P1 #Hred #Hind #i normalize @star_red_lambda @Hind + |#ty #P #i normalize @starl_to_star @sstepl [|@rmem] + @star_to_starl @star_red_vec2 [>length_map >length_map >length_map //] + #n #Q >length_map #H + cut (∃a:(FinSet_of_FType O D ty).True) + [lapply H -H lapply (enum_complete (FinSet_of_FType O D ty)) + cases (enum (FinSet_of_FType O D ty)) + [#x normalize #H @False_ind @(absurd … H) @lt_to_not_le // + |#x #l #_ #_ %{x} // + ] + ] * #a #_ + >(nth_map ?????? a H) >(nth_map ?????? Q) [2:>length_map @H] + >(nth_map ?????? a H) + lapply (subst_lemma O D P (to_T O D ty + (nth n (FinSet_of_FType O D ty) (enum (FinSet_of_FType O D ty)) a)) + N i 0 (is_closed_mono … (is_closed_to_T …)) HNc) // H1 + Hx @Hind2 normalize // + |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize // + ] + ] + ] +qed. + +(* since we only consider beta reduction with closed arguments we could avoid +lifting. We define it for the sake of generality *) + +(* arguments: k is the nesting depth (starts from 0), p is the lift +let rec lift O D t k p on t ≝ + match t with + [ Val o a ⇒ Val O D o a + | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n + | App m n ⇒ App O D (lift O D m k p) (lift O D n k p) + | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p) + | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v) + ]. + +notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}. +notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}. + +interpretation "Lift" 'Lift n k M = (lift ?? M k n). + +let rec subst O D t k s on t ≝ + match t with + [ Val o a ⇒ Val O D o a + | Rel n ⇒ if (leb k n) then + (if (eqb k n) then lift O D s 0 n else Rel O D (n-1)) + else(Rel O D n) + | App m n ⇒ App O D (subst O D m k s) (subst O D n k s) + | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s) + | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) + ]. +*) + +(* simplified version of subst, assuming the argument s is closed *) + +let rec subst O D t k s on t ≝ + match t with + [ Val o a ⇒ Val O D o a + | Rel n ⇒ if (leb k n) then + (if (eqb k n) then (* lift O D s 0 n*) s else Rel O D (n-1)) + else(Rel O D n) + | App m n ⇒ App O D (subst O D m k s) (subst O D n k s) + | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s) + | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) + ]. +(* notation "hvbox(M break [ k ≝ N ])" + non associative with precedence 90 + for @{'Subst1 $M $k $N}. *) + +interpretation "Subst" 'Subst1 M k N = (subst M k N). + +(* +lemma subst_rel1: ∀O,D,A.∀k,i. i < k → + (Rel O D i) [k ≝ A] = Rel O D i. +#A #k #i normalize #ltik >(lt_to_leb_false … ltik) // +qed. + +lemma subst_rel2: ∀O,D, A.∀k. + (Rel k) [k ≝ A] = lift A 0 k. +#A #k normalize >(le_to_leb_true k k) // >(eq_to_eqb_true … (refl …)) // +qed. + +lemma subst_rel3: ∀A.∀k,i. k < i → + (Rel i) [k ≝ A] = Rel (i-1). +#A #k #i normalize #ltik >(le_to_leb_true k i) /2/ +>(not_eq_to_eqb_false k i) // @lt_to_not_eq // +qed. *) + + +(* closed terms ???? +let rec closed_k O D (t: T O D) k on t ≝ + match t with + [ Val o a ⇒ True + | Rel n ⇒ n < k + | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k) + | Lambda T n ⇒ closed_k O D n (k+1) + | Vec T v ⇒ closed_list O D v k + ] + +and closed_list O D (l: list (T O D)) k on l ≝ + match l with + [ nil ⇒ True + | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k + ] +. *) + +inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝ +| cval : ∀k,o,a.is_closed O D k (Val O D o a) +| crel : ∀k,n. n < k → is_closed O D k (Rel O D n) +| capp : ∀k,m,n. is_closed O D k m → is_closed O D k n → + is_closed O D k (App O D m n) +| clam : ∀T,k,m. is_closed O D (S k) m → is_closed O D k (Lambda O D T m) +| cvec: ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) → + is_closed O D k (Vec O D T v). + +lemma is_closed_rel: ∀O,D,n,k. + is_closed O D k (Rel O D n) → n < k. +#O #D #n #k #H inversion H + [#k0 #o #a #eqk #H destruct + |#k0 #n0 #ltn0 #eqk #H destruct // + |#k0 #M #N #_ #_ #_ #_ #_ #H destruct + |#T #k0 #M #_ #_ #_ #H destruct + |#T #k0 #v #_ #_ #_ #H destruct + ] +qed. + +lemma is_closed_app: ∀O,D,k,M, N. + is_closed O D k (App O D M N) → is_closed O D k M ∧ is_closed O D k N. +#O #D #k #M #N #H inversion H + [#k0 #o #a #eqk #H destruct + |#k0 #n0 #ltn0 #eqk #H destruct + |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct % // + |#T #k0 #M #_ #_ #_ #H destruct + |#T #k0 #v #_ #_ #_ #H destruct + ] +qed. + +lemma is_closed_lam: ∀O,D,k,ty,M. + is_closed O D k (Lambda O D ty M) → is_closed O D (S k) M. +#O #D #k #ty #M #H inversion H + [#k0 #o #a #eqk #H destruct + |#k0 #n0 #ltn0 #eqk #H destruct + |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct + |#T #k0 #M1 #HM1 #_ #_ #H1 destruct // + |#T #k0 #v #_ #_ #_ #H destruct + ] +qed. + +lemma is_closed_vec: ∀O,D,k,ty,v. + is_closed O D k (Vec O D ty v) → ∀m. mem ? m v → is_closed O D k m. +#O #D #k #ty #M #H inversion H + [#k0 #o #a #eqk #H destruct + |#k0 #n0 #ltn0 #eqk #H destruct + |#k0 #M1 #N1 #HM #HN #_ #_ #_ #H1 destruct + |#T #k0 #M1 #HM1 #_ #_ #H1 destruct + |#T #k0 #v #Hv #_ #_ #H1 destruct @Hv + ] +qed. + +lemma is_closed_S: ∀O,D,M,m. + is_closed O D m M → is_closed O D (S m) M. +#O #D #M #m #H elim H // + [#k #n0 #Hlt @crel @le_S // + |#k #P #Q #HP #HC #H1 #H2 @capp // + |#ty #k #P #HP #H1 @clam // + |#ty #k #v #Hind #Hv @cvec @Hv + ] +qed. + +lemma is_closed_mono: ∀O,D,M,m,n. m ≤ n → + is_closed O D m M → is_closed O D n M. +#O #D #M #m #n #lemn elim lemn // #i #j #H #H1 @is_closed_S @H @H1 +qed. + + +(*** properties of lift and subst ***) + +(* +lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t. +#O #D #t @(T_elim … t) normalize // + [#n #k cases (leb k n) normalize // + |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // + #hd #tl #Hind #Hind1 normalize @eq_f2 + [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //] + ] +qed. + +lemma lift_closed: ∀O,D.∀t:T O D.∀k,p. + is_closed O D k t → lift O D t k p = t. +#O #D #t @(T_elim … t) normalize // + [#n #k #p #H >(not_le_to_leb_false … (lt_to_not_le … (is_closed_rel … H))) // + |#M #N #HindM #HindN #k #p #H lapply (is_closed_app … H) * #HcM #HcN + >(HindM … HcM) >(HindN … HcN) // + |#ty #M #HindM #k #p #H lapply (is_closed_lam … H) -H #H >(HindM … H) // + |#ty #v #HindM #k #p #H lapply (is_closed_vec … H) -H #H @eq_f + cut (∀m. mem ? m v → lift O D m k p = m) + [#m #Hmem @HindM [@Hmem | @H @Hmem]] -HindM + elim v // #a #tl #Hind #H1 normalize @eq_f2 + [@H1 %1 //|@Hind #m #Hmem @H1 %2 @Hmem] + ] +qed. + +*) + +lemma subst_closed: ∀O,D,M,N,k,i. k ≤ i → + is_closed O D k M → subst O D M i N = M. +#O #D #M @(T_elim … M) + [#o #a normalize // + |#n #N #k #j #Hlt #Hc lapply (is_closed_rel … Hc) #Hnk normalize + >not_le_to_leb_false [2:@lt_to_not_le @(lt_to_le_to_lt … Hnk Hlt)] // + |#P #Q #HindP #HindQ #N #k #i #ltki #Hc lapply (is_closed_app … Hc) * + #HcP #HcQ normalize >(HindP … ltki HcP) >(HindQ … ltki HcQ) // + |#ty #P #HindP #N #k #i #ltki #Hc lapply (is_closed_lam … Hc) + #HcP normalize >(HindP … HcP) // @le_S_S @ltki + |#ty #v #Hindv #N #k #i #ltki #Hc lapply (is_closed_vec … Hc) + #Hcv normalize @eq_f + cut (∀m:T O D.mem (T O D) m v→ subst O D m i N=m) + [#m #Hmem @(Hindv … Hmem N … ltki) @Hcv @Hmem] + elim v // #a #tl #Hind #H normalize @eq_f2 + [@H %1 //| @Hind #Hmem #Htl @H %2 @Htl] + ] +qed. + +lemma subst_lemma: ∀O,D,A,B,C,k,i. is_closed O D k B → is_closed O D i C → + subst O D (subst O D A i B) (k+i) C = + subst O D (subst O D A (k+S i) C) i B. +#O #D #A #B #C #k @(T_elim … A) normalize + [// + |#n #i #HBc #HCc @(leb_elim i n) #Hle + [@(eqb_elim i n) #eqni + [(lt_to_leb_false (k+(S i)) i) // normalize + >(subst_closed … HBc) // >le_to_leb_true // >eq_to_eqb_true // + |(cut (i < n)) + [cases (le_to_or_lt_eq … Hle) // #eqin @False_ind /2/] #ltin + (cut (0 < n)) [@(le_to_lt_to_lt … ltin) //] #posn + normalize @(leb_elim (k+i) (n-1)) #nk + [@(eqb_elim (k+i) (n-1)) #H normalize + [cut (k+(S i) = n); [/2 by S_pred/] #H1 + >(le_to_leb_true (k+(S i)) n) /2/ + >(eq_to_eqb_true … H1) normalize >(subst_closed … HCc) // + |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt + >(le_to_leb_true (k+(S i)) n) normalize + [>(not_eq_to_eqb_false (k+(S i)) n) normalize + [>le_to_leb_true [2:@lt_to_le @(le_to_lt_to_lt … Hlt) //] + >not_eq_to_eqb_false // @lt_to_not_eq @(le_to_lt_to_lt … Hlt) // + |@(not_to_not … H) #Hn /2 by plus_minus/ + ] + |(not_le_to_leb_false (k+(S i)) n) normalize + [>(le_to_leb_true … Hle) >(not_eq_to_eqb_false … eqni) // + |@(not_to_not … nk) #H @le_plus_to_minus_r // + ] + ] + ] + |(cut (n < k+i)) [@(lt_to_le_to_lt ? i) /2 by not_le_to_lt/] #ltn + >not_le_to_leb_false [2: @lt_to_not_le @(transitive_lt …ltn) //] normalize + >not_le_to_leb_false [2: @lt_to_not_le //] normalize + >(not_le_to_leb_false … Hle) // + ] + |#M #N #HindM #HindN #i #HBC #HCc @eq_f2 [@HindM // |@HindN //] + |#ty #M #HindM #i #HBC #HCc @eq_f >plus_n_Sm >plus_n_Sm @HindM // + @is_closed_S // + |#ty #v #Hindv #i #HBC #HCc @eq_f + cut (∀m.mem ? m v → subst O D (subst O D m i B) (k+i) C = + subst O D (subst O D m (k+S i) C) i B) + [#m #Hmem @Hindv //] -Hindv elim v normalize [//] + #a #tl #Hind #H @eq_f2 [@H %1 // | @Hind #m #Hmem @H %2 //] + ] +qed. + + diff --git a/matita/matita/lib/finite_lambda/typing.ma b/matita/matita/lib/finite_lambda/typing.ma new file mode 100644 index 000000000..791e27d66 --- /dev/null +++ b/matita/matita/lib/finite_lambda/typing.ma @@ -0,0 +1,229 @@ +(* + ||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". + + +(****************************************************************) + +inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝ + | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o) + | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty + | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 → + TJ O D G (App O D M N) ty2 + | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 → + TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2) + | tvec: ∀G,v,ty1,ty2. + (|v| = |enum (FinSet_of_FType O D ty1)|) → + (∀M. mem ? M v → TJ O D G M ty2) → + TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2). + +lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty. +#O #D #G #ty elim ty + [#o #a normalize @tval + |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec + [length_map >length_map // + |#M elim v + [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]] + ] + ] +qed. + +lemma inv_rel: ∀O,D,G,n,ty. + TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2. +#O #D #G #n #ty #Hrel inversion Hrel + [#G1 #o #a #_ #H destruct + |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/ + |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct + |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct + |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct + ] +qed. + +lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3. + TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) → + ty1 = ty2 ∧ TJ O D (ty2::G) M ty3. +#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam + [#G1 #o #a #_ #H destruct + |#G1 #ty #G2 #n #_ #_ #H destruct + |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct + |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % // + |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct + ] +qed. + +lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3. + TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) → + (|v| = |enum (FinSet_of_FType O D ty1)|) ∧ + (∀M. mem ? M v → TJ O D G M ty3). +#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec + [#G #o #a #_ #H destruct + |#G1 #ty #G2 #n #_ #_ #H destruct + |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct + |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct + |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem + ] +qed. + +(* could be generalized *) +lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → + TJ O D (G1@G2) (Rel O D n) ty1 → + TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1. +#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel) +* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2) +* #G5 * + [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4 + @(absurd … H4) @le_to_not_lt // + |* #H3 #H4 >H4 >append_cons length_append >length_append

H3 >length_append normalize + >plus_n_Sm >associative_plus @eq_f // + ] +qed. + +lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → + TJ O D (G1@ty2::G2) (Rel O D n) ty1 → + TJ O D (G1@G2) (Rel O D (n-1)) ty1. +#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel) +* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2) +* #G5 * + [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4 + @(absurd … H4) @le_to_not_lt // + |lapply G5 -G5 * + [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1) + @le_to_not_lt // + |#ty3 #G5 * #H3 normalize #H4 destruct (H4) H3 >length_append >length_append normalize H1 >length_append // + |* cases G6 + [>append_nil normalize #H1 @False_ind + @(absurd ? Hlt) @le_to_not_lt H1 // + |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel // + ] + ] + |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3 + #Heq #Hc lapply (is_closed_app … Hc) -Hc * #HMc #HNc + @(tapp … (HindM … Heq HMc) (HindN … Heq HNc)) + |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq #Hc + lapply (is_closed_lam … Hc) -Hc #HMc + @tlambda @(HindM (ty1::G1) G2) [>Heq // |@HMc] + |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 #Hc @tvec + [>length_map // + |#M #Hmem @Hind // lapply (is_closed_vec … Hc) #Hvc @Hvc // + ] + ] +qed. + +lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a. +#A #a #d #l1 elim l1 normalize + [#l2 #n #Hn H cases (le_to_or_lt_eq … (leb_true_to_le … H)) + [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize + lapply (compare_append … HG) * #G3 * + [* #HG1 #HG2 @(strength_rel … tyN … ltn) HG in ltn; >length_append #ltn @False_ind + @(absurd … ltn) @le_to_not_lt >Hlen // + ] + |#HG21 >(eq_to_eqb_true … HG21) + cut (ty = tyN) + [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty + normalize H normalize lapply (compare_append … HG) * #G3 * + [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1 + >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt + @(leb_false_to_not_le … H) + |cases G3 + [>append_nil * #H1 @False_ind @(absurd ? Hlen)

associative_append @trel // + ] + ] + ] + |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG + #HN0 #Hc normalize @(tapp … ty1) + [@(HindM … eqG HN0 Hc) |@(HindN … eqG HN0 Hc)] + |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG + #HN0 #Hc normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) // >eqG // + |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG + #HN0 #Hc normalize @(tvec … ty1) + [>length_map @Hlen + |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM HM1 @tlambda @Hind // + |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN) + * #a * #mema #eqN H3 @tvec + [H2 >length_append >length_append @eq_f // + |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem + [@Hv >H2 @mem_append_l1 // + |cases Hmem + [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 // + |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 // + ] + ] + ] + ] +qed. +