From 50001ac0b45a3f6376e8cbfd9200149a01d68148 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 25 Nov 2013 14:42:31 +0000 Subject: [PATCH] - xoa: the definitions file now includes the notations file - probe: improved "list" algorithm, and bugfixed "remove" algorithm - lib/lambda: updated and bugfixed dependences to cope with new xoa - lambdadelta/ground_2: decentralized and bugfixed notation, now copes with new xoa, some refactoring --- .../components/binaries/probe/matitaList.ml | 59 ++++++++++++------- .../components/binaries/probe/matitaRemove.ml | 13 ++-- matita/components/binaries/xoa/xoa.ml | 1 + matita/matita/contribs/lambdadelta/Makefile | 4 +- .../lambdadelta/apps_2/functional/rtm_step.ma | 4 +- .../basic_2/computation/acp_aaa.ma | 24 ++++---- .../lambdadelta/basic_2/computation/acp_cr.ma | 36 +++++------ .../lambdadelta/basic_2/grammar/aarity.ma | 2 +- .../lambdadelta/basic_2/grammar/genv.ma | 2 +- .../lambdadelta/basic_2/grammar/item.ma | 2 +- .../basic_2/grammar/lenv_append.ma | 1 + .../basic_2/grammar/term_vector.ma | 2 +- .../lambdadelta/basic_2/relocation/ldrop.ma | 2 +- .../basic_2/relocation/lift_vector.ma | 16 ++--- .../contribs/lambdadelta/basic_2/static/sh.ma | 2 +- .../lambdadelta/basic_2/substitution/gr2.ma | 14 ++--- .../basic_2/substitution/gr2_gr2.ma | 4 +- .../basic_2/substitution/gr2_minus.ma | 21 ++++--- .../basic_2/substitution/ldrops.ma | 24 ++++---- .../lambdadelta/basic_2/substitution/lifts.ma | 43 +++++++------- .../basic_2/substitution/lifts_vector.ma | 10 ++-- .../lambdadelta/ground_2/{ => lib}/arith.ma | 2 +- .../lambdadelta/ground_2/{ => lib}/list.ma | 15 +++-- .../lambdadelta/ground_2/{ => lib}/lstar.ma | 0 .../lambdadelta/ground_2/{ => lib}/star.ma | 3 +- .../ground_2/notation/constructors/cons_3.ma | 19 ++++++ .../ground_2/notation/constructors/cons_5.ma | 19 ++++++ .../ground_2/notation/constructors/nil_1.ma | 19 ++++++ .../ground_2/notation/constructors/nil_2.ma | 19 ++++++ .../functions/append_2.ma} | 30 +--------- .../ground_2/notation/xoa/false_0.ma | 19 ++++++ .../ground_2/notation/xoa/true_0.ma | 19 ++++++ .../ground_2/{ => notation}/xoa_notation.ma | 0 .../lambdadelta/ground_2/xoa.conf.xml | 6 +- .../lambdadelta/ground_2/{ => xoa}/xoa.ma | 2 + .../ground_2/{ => xoa}/xoa_props.ma | 5 +- .../matita/lib/lambda/background/preamble.ma | 2 +- matita/matita/lib/lambda/background/xoa.ma | 2 + matita/matita/lib/lambda/xoa.conf.xml | 6 +- 39 files changed, 293 insertions(+), 180 deletions(-) rename matita/matita/contribs/lambdadelta/ground_2/{ => lib}/arith.ma (99%) rename matita/matita/contribs/lambdadelta/ground_2/{ => lib}/list.ma (77%) rename matita/matita/contribs/lambdadelta/ground_2/{ => lib}/lstar.ma (100%) rename matita/matita/contribs/lambdadelta/ground_2/{ => lib}/star.ma (99%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma rename matita/matita/contribs/lambdadelta/ground_2/{notation.ma => notation/functions/append_2.ma} (63%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma rename matita/matita/contribs/lambdadelta/ground_2/{ => notation}/xoa_notation.ma (100%) rename matita/matita/contribs/lambdadelta/ground_2/{ => xoa}/xoa.ma (99%) rename matita/matita/contribs/lambdadelta/ground_2/{ => xoa}/xoa_props.ma (90%) diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 9f6248c0f..22b2f91b5 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -17,17 +17,34 @@ module Y = Sys module U = NUri module US = U.UriSet +module H = HExtlib module O = Options module E = Engine -let is_obj path = - F.check_suffix path ".con.ng" || - F.check_suffix path ".ind.ng" || - F.check_suffix path ".var.ng" - +let chop_extension file = + try F.chop_extension file + with Invalid_argument("Filename.chop_extension") -> file + let src_exists path = !O.no_devel || Y.file_exists path +let is_obj base path = + if H.is_regular (F.concat base path) then + F.check_suffix path ".con.ng" || + F.check_suffix path ".ind.ng" || + F.check_suffix path ".var.ng" + else false + +let is_src base path = + H.is_regular (F.concat base path) && + F.check_suffix path ".ng" + +let is_dir base path = + H.is_dir (F.concat base path) + +let is_script devel = + src_exists (chop_extension devel ^ ".ma") + let mk_file path = if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) else path ^ ".ng" @@ -38,24 +55,25 @@ let add_obj path = O.objs := US.add (U.uri_of_string str) !O.objs let add_src devel path = - if src_exists (F.chop_extension devel ^ ".ma") then - let path = F.chop_extension path in - let str = F.concat "cic:" path ^ "/" in - O.srcs := US.add (U.uri_of_string str) !O.srcs + let path = F.chop_extension path in + let str = F.concat "cic:" path ^ "/" in + O.srcs := US.add (U.uri_of_string str) !O.srcs let add_remove base path = O.remove := F.concat base path :: !O.remove -let rec scan_entry base devel path = - if is_obj path then add_obj path else - if F.check_suffix path ".ng" then - if src_exists (F.chop_extension devel ^ ".ma") - then add_src devel path else add_remove base path - else - if src_exists devel || src_exists (devel ^ ".ma") then - let files = Y.readdir (F.concat base path) in - let map base file = scan_entry base (F.concat devel file) (F.concat path file) in - A.iter (map base) files +let rec scan_entry inner base devel path = +(* Printf.eprintf "%b %s %s%!\n" inner devel path; *) + if is_obj base path && inner then add_obj path else + if is_src base path && is_script devel then add_src devel path else + if is_dir base path && is_script devel then scan_dir true base devel path else + if is_dir base path && src_exists devel then scan_dir false base devel path else + add_remove base path + +and scan_dir inner base devel path = + let files = Y.readdir (F.concat base path) in + let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in + A.iter (map base) files let from_uri base devel uri = O.no_devel := devel = ""; @@ -65,7 +83,8 @@ let from_uri base devel uri = if protocol = "cic:" then let path = S.sub str (succ i) (S.length str - succ i) in let file = mk_file path in - if Y.file_exists (F.concat base file) then scan_entry base devel file + if Y.file_exists (F.concat base file) then + scan_entry (is_script devel) base devel file else E.missing path else E.unsupported protocol diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml index 87be45521..72624f0f0 100644 --- a/matita/components/binaries/probe/matitaRemove.ml +++ b/matita/components/binaries/probe/matitaRemove.ml @@ -16,8 +16,11 @@ module U = Unix module O = Options -let remove_dir dir = - let map name = Y.remove (F.concat dir name) in +let rec remove_obj name = + try Y.remove name with Sys_error _ -> remove_dir name + +and remove_dir dir = + let map name = remove_obj (F.concat dir name) in let rec rmdir dir = U.rmdir dir; (* Sys.remove does not seem to remove empty directories *) rmdir (F.dirname dir) @@ -28,8 +31,4 @@ let remove_dir dir = end let objects () = - let map name = - Y.remove name; - remove_dir (F.chop_extension name) - in - List.iter map !O.remove + List.iter remove_obj !O.remove diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index ae5bd03ab..e4e0e7c69 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -32,6 +32,7 @@ let process conf = let ooch = L.open_out preamble (R.get_string "xoa.objects") in let noch = L.open_out preamble (R.get_string "xoa.notations") in List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); + L.out_include ooch (R.get_string "xoa.notations" ^ ".ma"); List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex"); List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or"); List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and"); diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 18258ae90..6eed87bc1 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -4,14 +4,14 @@ H := @ TRIM := sed "s/ \\+$$//" XOA_CONF := ground_2/xoa.conf.xml -XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma +XOA_TARGETS := ground_2/notation/xoa_notation.ma ground_2/xoa/xoa.ma XOA_DIR := ../../../components/binaries/xoa XOA := xoa.native XOA_OPTS := ../../matita.conf.xml $(XOA_CONF) XOA2_CONF := ground_2/xoa2.conf.xml -XOA2_TARGETS := ground_2/xoa2_notation.ma ground_2/xoa2.ma +XOA2_TARGETS := ground_2/notation/xoa2_notation.ma ground_2/xoa/xoa2.ma XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF) DEP_INPUT := .depend diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma index 40f2eddc2..5ca6add44 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma @@ -46,8 +46,8 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) | rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E ⟠ (+ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) + rtm_step (mk_rtm G u E (⟠) (+ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (⟠) T) | rtm_theta : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (+ⓓV. T)) (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 13d69acd4..3656d36f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -32,7 +32,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom - @(s4 … HAtom … ◊) // + @(s4 … HAtom … (◊)) // | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (aacr_acr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct @@ -45,7 +45,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #K2 #HK20 #H destruct elim (lift_total V0 0 (i0 +1)) #V #HV0 elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 - @(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) + @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by ldrops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b @@ -53,40 +53,40 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s5 … HB … ◊ … (ⓝV3.V) … HLK2) [2: /2 width=1/ ] - @(s7 … HB … ◊) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] + @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ] + @(s7 … HB … (◊)) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s6 … HA … ◊ ◊) // /3 width=5/ + @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, ldrops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct - @(aacr_abst … H1RP H2RP) [ /2 width=5/ ] + @(aacr_abst … H1RP H2RP) [ /2 width=5 by/ ] #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B - @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5/ + lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3 by ldrops_trans, lifts_trans/ #HLW2B + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip/ | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - /3 width=10/ + /3 width=10 by ldrops_nil, lifts_nil/ | #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA - @(s7 … HA … ◊) /2 width=5/ + @(s7 … HA … (◊)) /2 width=5 by/ ] qed. (* Basic_1: was: sc3_arity *) lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. -/2 width=8/ qed. +/2 width=8 by ldrops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed. lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT lapply (aacr_acr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4/ +@(s1 … HA) /2 width=4 by aacr_aaa/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index 482349b69..1b0d56c7c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -89,7 +89,7 @@ lemma acr_lifts: ∀C. S8 C → S8s C. [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=9/ + elim (lifts_inv_cons … H) -H /3 width=9 by/ ] qed. @@ -97,7 +97,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → ∀des,G,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 → RP G L V → RP G L0 V0. #RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@acr_lifts /width=6/ +@acr_lifts /width=6 by/ @(s8 … HRP) qed. @@ -106,8 +106,7 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → ∀des,G,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L → all … (RP G L) Vs → all … (RP G L0) V0s. #RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize // -#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s -@conj /2 width=1/ /2 width=6 by rp_lifts/ +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * /3 width=6 by rp_lifts, conj/ qed. (* Basic_1: was: @@ -119,25 +118,26 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) #B #A #IHB #IHA @mk_acr normalize [ #G #L #T #H elim (cp1 … H1RP G L) #k #HK - lapply (H ? (⋆k) ? ⟠ ? ? ?) -H + lapply (H ? (⋆k) ? (⟠) ? ? ?) -H [1,3: // |2,4: skip - | @(s2 … IHB … ◊) // + | @(s2 … IHB … (◊)) // | #H @(cp3 … H1RP … k) @(s1 … IHA) // ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 - @(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/ + @(s2 … IHA … (V0 @ V0s)) + /3 width=13 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/ | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct - @(s3 … IHA … (V0 @ V0s)) /5 width=5/ + @(s3 … IHA … (V0 @ V0s)) /5 width=5 by lifts_applv, lifts_flat, lifts_bind/ | #G #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct >(lifts_inv_sort1 … HY) -Y lapply (s1 … IHB … HB) #HV0 - @(s4 … IHA … (V0 @ V0s)) /3 width=6/ + @(s4 … IHA … (V0 @ V0s)) /3 width=6 by rp_liftsv_all, conj/ | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct @@ -147,15 +147,15 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 - @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4 by lifts_applv/ | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /3 width=6 by rp_lifts/ - @(HA … (des + 1)) /2 width=1/ - [ @(s8 … IHB … HB … HV120) /2 width=1/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=6 by rp_lifts, liftv_cons/ + @(HA … (des + 1)) /2 width=1 by ldrops_skip/ + [ @(s8 … IHB … HB … HV120) /2 width=1 by ldrop_ldrop/ | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // @@ -163,8 +163,8 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) | #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0 @ V0s)) /3 width=4/ -| /3 width=7/ + @(s7 … IHA … (V0 @ V0s)) /3 width=4 by lifts_applv/ +| /3 width=7 by ldrops_cons, lifts_cons/ ] qed. @@ -179,11 +179,11 @@ lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s8 … HCB) ] #HW0 -@(s3 … HCA … ◊) -@(s6 … HCA … ◊ ◊) // +@(s3 … HCA … (◊)) +@(s6 … HCA … (◊) (◊)) // [ @(HA … HL0) // | lapply (s1 … HCB) -HCB #HCB - @(cp4 … H1RP) /2 width=1/ + @(cp4 … H1RP) /2 width=1 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma index 72ae1cd80..88486384a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma @@ -16,7 +16,7 @@ * Initial invocation: - Patience on me to gain peace and perfection! - *) -include "ground_2/star.ma". +include "ground_2/lib/star.ma". include "basic_2/notation/constructors/item0_0.ma". include "basic_2/notation/constructors/snitem2_2.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma index 2ab808305..27d019994 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/list.ma". +include "ground_2/lib/list.ma". include "basic_2/notation/constructors/star_0.ma". include "basic_2/notation/constructors/dxbind2_3.ma". include "basic_2/notation/constructors/dxabbr_2.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma index b85496fa5..df330a7df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "ground_2/lib/arith.ma". (* ITEMS ********************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 24e08d151..8771d46fb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/append_2.ma". include "basic_2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENTS *******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 1ff586359..748e5cb63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/list.ma". +include "ground_2/lib/list.ma". include "basic_2/notation/functions/snapplv_2.ma". include "basic_2/grammar/term_simple.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index bce477f21..68b23637c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/lstar.ma". +include "ground_2/lib/lstar.ma". include "basic_2/notation/relations/rdrop_4.ma". include "basic_2/grammar/lenv_length.ma". include "basic_2/grammar/cl_restricted_weight.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma index 482eea166..52b7861be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma @@ -18,7 +18,7 @@ include "basic_2/relocation/lift.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) inductive liftv (d,e:nat) : relation (list term) ≝ -| liftv_nil : liftv d e ◊ ◊ +| liftv_nil : liftv d e (◊) (◊) | liftv_cons: ∀T1s,T2s,T1,T2. ⇧[d, e] T1 ≡ T2 → liftv d e T1s T2s → liftv d e (T1 @ T1s) (T2 @ T2s) @@ -31,10 +31,10 @@ interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s). fact liftv_inv_nil1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T1s = ◊ → T2s = ◊. #T1s #T2s #d #e * -T1s -T2s // #T1s #T2s #T1 #T2 #_ #_ #H destruct -qed. +qed-. lemma liftv_inv_nil1: ∀T2s,d,e. ⇧[d, e] ◊ ≡ T2s → T2s = ◊. -/2 width=5/ qed-. +/2 width=5 by liftv_inv_nil1_aux/ qed-. fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → ∀U1,U1s. T1s = U1 @ U1s → @@ -42,21 +42,21 @@ fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T2s = U2 @ U2s. #T1s #T2s #d #e * -T1s -T2s [ #U1 #U1s #H destruct -| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5/ +| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/ ] -qed. +qed-. lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 @ U1s ≡ T2s → ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s & T2s = U2 @ U2s. -/2 width=3/ qed-. +/2 width=3 by liftv_inv_cons1_aux/ qed-. (* Basic properties *********************************************************) lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇧[d, e] T1s ≡ T2s. #d #e #T1s elim T1s -T1s -[ /2 width=2/ +[ /2 width=2 by liftv_nil, ex_intro/ | #T1 #T1s * #T2s #HT12s - elim (lift_total T1 d e) /3 width=2/ + elim (lift_total T1 d e) /3 width=2 by liftv_cons, ex_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma index f43b9b31d..bab748f75 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "ground_2/lib/arith.ma". (* SORT HIERARCHY ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma index 4cee5b104..57bb952b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma @@ -18,7 +18,7 @@ include "basic_2/grammar/term_vector.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) inductive at: list2 nat nat → relation nat ≝ -| at_nil: ∀i. at ⟠ i i +| at_nil: ∀i. at (⟠) i i | at_lt : ∀des,d,e,i1,i2. i1 < d → at des i1 i2 → at ({d, e} @ des) i1 i2 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 → @@ -36,10 +36,10 @@ fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = | #des #d #e #i1 #i2 #_ #_ #H destruct | #des #d #e #i1 #i2 #_ #_ #H destruct ] -qed. +qed-. lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. -/2 width=3/ qed-. +/2 width=3 by at_inv_nil_aux/ qed-. fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → ∀d,e,des0. des = {d, e} @ des0 → @@ -47,15 +47,15 @@ fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2. #des #i1 #i2 * -des -i1 -i2 [ #i #d #e #des #H destruct -| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ -| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ +| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ +| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/ ] -qed. +qed-. lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨ d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2. -/2 width=3/ qed-. +/2 width=3 by at_inv_cons_aux/ qed-. lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → i1 < d → @⦃i1, des⦄ ≡ i2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma index 9e8ced3a8..22bf6af97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma @@ -22,8 +22,8 @@ theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ #des #i #i1 #H elim H -des -i -i1 [ #i #x #H <(at_inv_nil … H) -x // | #des #d #e #i #i1 #Hid #_ #IHi1 #x #H - lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1/ + lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/ | #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H - lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1/ + lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma index ba6dbd544..3c32514d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/gr2.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) inductive minuss: nat → relation (list2 nat nat) ≝ -| minuss_nil: ∀i. minuss i ⟠ ⟠ +| minuss_nil: ∀i. minuss i (⟠) (⟠) | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → minuss i ({d, e} @ des1) ({d - i, e} @ des2) | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → @@ -36,10 +36,10 @@ fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → | #des1 #des2 #d #e #i #_ #_ #H destruct | #des1 #des2 #d #e #i #_ #_ #H destruct ] -qed. +qed-. lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. -/2 width=4/ qed-. +/2 width=4 by minuss_inv_nil1_aux/ qed-. fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → ∀d,e,des. des1 = {d, e} @ des → @@ -48,16 +48,16 @@ fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des2 = {d - i, e} @ des0. #des1 #des2 #i * -des1 -des2 -i [ #i #d #e #des #H destruct -| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/ -| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/ +| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/ +| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ ] -qed. +qed-. lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨ ∃∃des. i < d & des1 ▭ i ≡ des & des2 = {d - i, e} @ des. -/2 width=3/ qed-. +/2 width=3 by minuss_inv_cons1_aux/ qed-. lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → d ≤ i → des1 ▭ e + i ≡ des2. @@ -70,8 +70,7 @@ qed-. lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → i < d → ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des. -#des1 #des2 #d #e #i #H -elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid -lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi -elim (lt_refl_false … Hi) +#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ +#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi +#Hi elim (lt_refl_false … Hi) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma index 069f632f4..912487a44 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma @@ -20,7 +20,7 @@ include "basic_2/substitution/lifts.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) inductive ldrops: list2 nat nat → relation lenv ≝ -| ldrops_nil : ∀L. ldrops ⟠ L L +| ldrops_nil : ∀L. ldrops (⟠) L L | ldrops_cons: ∀L1,L,L2,des,d,e. ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2 . @@ -33,11 +33,11 @@ interpretation "generic local environment slicing" fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2. #L1 #L2 #des * -L1 -L2 -des // #L1 #L #L2 #d #e #des #_ #_ #H destruct -qed. +qed-. (* Basic_1: was: drop1_gen_pnil *) lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2. -/2 width=3/ qed-. +/2 width=3 by ldrops_inv_nil_aux/ qed-. fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀d,e,tl. des = {d, e} @ tl → @@ -45,13 +45,13 @@ fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → #L1 #L2 #des * -L1 -L2 -des [ #L #d #e #tl #H destruct | #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct - /2 width=3/ -qed. + /2 width=3 by ex2_intro/ +qed-. (* Basic_1: was: drop1_gen_pcons *) lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 → ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2. -/2 width=3/ qed-. +/2 width=3 by ldrops_inv_cons_aux/ qed-. lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 → @@ -61,16 +61,16 @@ lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → L1 = K1. ⓑ{I} V1. #I #des #i #des2 #H elim H -des -i -des2 [ #i #L1 #K2 #V2 #H - >(ldrops_inv_nil … H) -L1 /2 width=7/ + >(ldrops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, ldrops_nil/ | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H elim (ldrops_inv_cons … H) -H #L #HL1 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct elim (IHdes2 … HL1) -IHdes2 -HL1 #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct - @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7/ | skip ] - normalize >plus_minus // @minuss_lt // /2 width=1/ (**) (* explicit constructors, /3 width=1/ is a bit slow *) + @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7 by lifts_cons, ldrops_cons/ | skip ] + normalize >plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *) | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H elim (IHdes2 … H) -IHdes2 -H #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct - /4 width=7/ + /4 width=7 by minuss_ge, ex4_3_intro, le_S_S/ ] qed-. @@ -83,7 +83,7 @@ lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 [ #L #V1 #V2 #HV12 #I >(lifts_inv_nil … HV12) -HV12 // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I - elim (lifts_inv_cons … H) -H /3 width=5/ + elim (lifts_inv_cons … H) -H /3 width=5 by ldrop_skip, ldrops_cons/ ]. qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma index 20727c4cd..31b383145 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/gr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) inductive lifts: list2 nat nat → relation term ≝ -| lifts_nil : ∀T. lifts ⟠ T T +| lifts_nil : ∀T. lifts (⟠) T T | lifts_cons: ∀T1,T,T2,des,d,e. ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2 . @@ -32,10 +32,10 @@ interpretation "generic relocation (term)" fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2. #T1 #T2 #des * -T1 -T2 -des // #T1 #T #T2 #d #e #des #_ #_ #H destruct -qed. +qed-. lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2. -/2 width=3/ qed-. +/2 width=3 by lifts_inv_nil_aux/ qed-. fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → ∀d,e,tl. des = {d, e} @ tl → @@ -43,12 +43,12 @@ fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → #T1 #T2 #des * -T1 -T2 -des [ #T #d #e #tl #H destruct | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct - /2 width=3/ -qed. + /2 width=3 by ex2_intro/ +qed-. lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 → ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2. -/2 width=3/ qed-. +/2 width=3 by lifts_inv_cons_aux/ qed-. (* Basic_1: was: lift1_sort *) lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k. @@ -56,7 +56,7 @@ lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k. [ #H <(lifts_inv_nil … H) -H // | #d #e #des #IH #H elim (lifts_inv_cons … H) -H #X #H - >(lift_inv_sort1 … H) -H /2 width=1/ + >(lift_inv_sort1 … H) -H /2 width=1 by/ ] qed-. @@ -64,11 +64,11 @@ qed-. lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 → ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2. #T2 #des elim des -des -[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/ +[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/ | #d #e #des #IH #i1 #H elim (lifts_inv_cons … H) -H #X #H1 #H2 elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct - elim (IH … H2) -IH -H2 /3 width=3/ + elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/ ] qed-. @@ -77,7 +77,7 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p. [ #H <(lifts_inv_nil … H) -H // | #d #e #des #IH #H elim (lifts_inv_cons … H) -H #X #H - >(lift_inv_gref1 … H) -H /2 width=1/ + >(lift_inv_gref1 … H) -H /2 width=1 by/ ] qed-. @@ -87,12 +87,12 @@ lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 → T2 = ⓑ{a,I} V2. U2. #a #I #T2 #des elim des -des [ #V1 #U1 #H - <(lifts_inv_nil … H) -H /2 width=5/ + <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/ | #d #e #des #IHdes #V1 #U1 #H elim (lifts_inv_cons … H) -H #X #H #HT2 elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct - /3 width=5/ + /3 width=5 by ex3_2_intro, lifts_cons/ ] qed-. @@ -102,23 +102,23 @@ lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 → T2 = ⓕ{I} V2. U2. #I #T2 #des elim des -des [ #V1 #U1 #H - <(lifts_inv_nil … H) -H /2 width=5/ + <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/ | #d #e #des #IHdes #V1 #U1 #H elim (lifts_inv_cons … H) -H #X #H #HT2 elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct - /3 width=5/ + /3 width=5 by ex3_2_intro, lifts_cons/ ] qed-. (* Basic forward lemmas *****************************************************) lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/ +#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/ qed-. lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/ +#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/ qed-. (* Basic properties *********************************************************) @@ -129,7 +129,7 @@ lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → #a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H - elim (lifts_inv_cons … H) -H /3 width=3/ + elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/ ] qed. @@ -139,13 +139,12 @@ lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H - elim (lifts_inv_cons … H) -H /3 width=3/ + elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/ ] qed. lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2. -#des elim des -des /2 width=2/ -#d #e #des #IH #T1 -elim (lift_total T1 d e) #T #HT1 -elim (IH T) -IH /3 width=4/ +#des elim des -des /2 width=2 by lifts_nil, ex_intro/ +#d #e #des #IH #T1 elim (lift_total T1 d e) +#T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma index 7046c9d32..e86d928d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/lifts.ma". (* GENERIC TERM VECTOR RELOCATION *******************************************) inductive liftsv (des:list2 nat nat) : relation (list term) ≝ -| liftsv_nil : liftsv des ◊ ◊ +| liftsv_nil : liftsv des (◊) (◊) | liftsv_cons: ∀T1s,T2s,T1,T2. ⇧*[des] T1 ≡ T2 → liftsv des T1s T2s → liftsv des (T1 @ T1s) (T2 @ T2s) @@ -34,12 +34,12 @@ lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 → ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 & T2 = Ⓐ V2s. U2. #V1s elim V1s -V1s normalize -[ #T1 #T2 #des #HT12 - @(ex3_2_intro) [3,4: // |1,2: skip | // ] (**) (* explicit constructor *) +[ #T1 #T2 #des #HT12 + @ex3_2_intro [3,4: // |1,2: skip | // ] (**) (* explicit constructor *) | #V1 #V1s #IHV1s #T1 #X #des #H elim (lifts_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct - @(ex3_2_intro) [4: // |3: /2 width=2/ |1,2: skip | // ] (**) (* explicit constructor *) + @(ex3_2_intro) [4: // |3: /2 width=2 by liftsv_cons/ |1,2: skip | // ] (**) (* explicit constructor *) ] qed-. @@ -49,5 +49,5 @@ qed-. lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → ∀T1,T2. ⇧*[des] T1 ≡ T2 → ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. -#V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/ +#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/ground_2/arith.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 2c47b2873..7d6f5dda4 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "arithmetics/nat.ma". -include "ground_2/star.ma". +include "ground_2/lib/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma similarity index 77% rename from matita/matita/contribs/lambdadelta/ground_2/list.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index 9a5ac0aeb..d21e1b52b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -12,7 +12,12 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "ground_2/notation/constructors/nil_1.ma". +include "ground_2/notation/constructors/nil_2.ma". +include "ground_2/notation/constructors/cons_3.ma". +include "ground_2/notation/constructors/cons_5.ma". +include "ground_2/notation/functions/append_2.ma". +include "ground_2/lib/arith.ma". (* LISTS ********************************************************************) @@ -20,9 +25,9 @@ inductive list (A:Type[0]) : Type[0] := | nil : list A | cons: A → list A → list A. -interpretation "nil (list)" 'Nil = (nil ?). +interpretation "nil (list)" 'Nil A = (nil A). -interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). +interpretation "cons (list)" 'Cons A hd tl = (cons A hd tl). let rec all A (R:predicate A) (l:list A) on l ≝ match l with @@ -34,9 +39,9 @@ inductive list2 (A1,A2:Type[0]) : Type[0] := | nil2 : list2 A1 A2 | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. -interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). +interpretation "nil (list of pairs)" 'Nil A1 A2 = (nil2 A1 A2). -interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl). +interpretation "cons (list of pairs)" 'Cons A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl). let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with [ nil2 ⇒ l2 diff --git a/matita/matita/contribs/lambdadelta/ground_2/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/lstar.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/ground_2/star.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index 29131d108..e5b788766 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -13,8 +13,7 @@ (**************************************************************************) include "basics/star1.ma". -include "ground_2/xoa_props.ma". -include "ground_2/notation.ma". +include "ground_2/xoa/xoa_props.ma". (* PROPERTIES OF RELATIONS **************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma new file mode 100644 index 000000000..97fd6e963 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( hd @ break tl )" + right associative with precedence 47 + for @{ 'Cons ? $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma new file mode 100644 index 000000000..c8bf11f01 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )" + non associative with precedence 47 + for @{ 'Cons ? ? $hd1 $hd2 $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma new file mode 100644 index 000000000..a6c5e6d54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "◊" + non associative with precedence 46 + for @{ 'Nil ? }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma new file mode 100644 index 000000000..1a48e23f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⟠" + non associative with precedence 46 + for @{ 'Nil ? ? }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma similarity index 63% rename from matita/matita/contribs/lambdadelta/ground_2/notation.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma index 4ac2e6e64..f6d95184b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma @@ -14,34 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -(* Logic ********************************************************************) - -notation "⊥" - non associative with precedence 90 - for @{'false}. - -notation "⊤" - non associative with precedence 90 - for @{'true}. - -(* Lists ********************************************************************) - -notation "◊" - non associative with precedence 90 - for @{'Nil}. - -notation "hvbox( hd @ break tl )" - right associative with precedence 47 - for @{'Cons $hd $tl}. - notation "hvbox( l1 @@ break l2 )" right associative with precedence 47 - for @{'Append $l1 $l2 }. - -notation "⟠" - non associative with precedence 90 - for @{'Nil2}. - -notation "hvbox( { hd1 , break hd2 } @ break tl )" - non associative with precedence 47 - for @{'Cons $hd1 $hd2 $tl}. + for @{ 'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma new file mode 100644 index 000000000..b96432510 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⊥" + non associative with precedence 19 + for @{'false}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma new file mode 100644 index 000000000..7a9ad4366 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⊤" + non associative with precedence 19 + for @{'true}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 79cd48b52..43d1b9366 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -1,9 +1,9 @@
- contribs/lambdadelta/ground_2/ - xoa - xoa_notation + contribs/lambdadelta/ + ground_2/xoa/xoa + ground_2/notation/xoa_notation basics/pts.ma 1 2 1 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/ground_2/xoa.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index 625be0c7f..a4281da4a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -16,6 +16,8 @@ include "basics/pts.ma". +include "ground_2/notation/xoa_notation.ma". + (* multiple existental quantifier (1, 2) *) inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma rename to matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma index 06bfbc739..e917bacd2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma @@ -13,8 +13,9 @@ (**************************************************************************) include "basics/logic.ma". -include "ground_2/xoa_notation.ma". -include "ground_2/xoa.ma". +include "ground_2/notation/xoa/false_0.ma". +include "ground_2/notation/xoa/true_0.ma". +include "ground_2/xoa/xoa.ma". interpretation "logical false" 'false = False. diff --git a/matita/matita/lib/lambda/background/preamble.ma b/matita/matita/lib/lambda/background/preamble.ma index a4400abce..6a087e3aa 100644 --- a/matita/matita/lib/lambda/background/preamble.ma +++ b/matita/matita/lib/lambda/background/preamble.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basics/star.ma". +include "basics/star1.ma". include "basics/lists/lstar.ma". include "arithmetics/exp.ma". diff --git a/matita/matita/lib/lambda/background/xoa.ma b/matita/matita/lib/lambda/background/xoa.ma index a2f19a6b7..96a1fb95c 100644 --- a/matita/matita/lib/lambda/background/xoa.ma +++ b/matita/matita/lib/lambda/background/xoa.ma @@ -16,6 +16,8 @@ include "basics/pts.ma". +include "lambda/background/xoa_notation.ma". + (* multiple existental quantifier (1, 2) *) inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ diff --git a/matita/matita/lib/lambda/xoa.conf.xml b/matita/matita/lib/lambda/xoa.conf.xml index 04cbcf59e..2d188536d 100644 --- a/matita/matita/lib/lambda/xoa.conf.xml +++ b/matita/matita/lib/lambda/xoa.conf.xml @@ -4,9 +4,9 @@ $(MATITA_RT_BASE_DIR)
- contribs/lambda/background/ - xoa - xoa_notation + lib/ + lambda/background/xoa + lambda/background/xoa_notation basics/pts.ma 1 2 2 2 -- 2.39.2