From: Ferruccio Guidi Date: Sun, 27 Oct 2013 21:22:27 +0000 (+0000) Subject: - lambdadelta: tentative definition of lazy equivalence for closures + X-Git-Tag: make_still_working~1061 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dec157aae89a4c1830f18eeb0b4152c8c5162ca7;p=helm.git - lambdadelta: tentative definition of lazy equivalence for closures + Makefile update/bugfix to support matitadep update - matitadep: bug fix in redundancy check + new option shows leaf nodes --- diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml index 0415a5111..4e0651be4 100644 --- a/matita/components/binaries/matitadep/matitadep.ml +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -1,15 +1,17 @@ module StringSet = Set.Make (String) type file = { - ddeps: string list; - rdeps: StringSet.t option + ddeps: string list; (* direct dependences *) + rdeps: StringSet.t option (* recursive dependences *) } let graph = Hashtbl.create 503 -let rec purge dname bdeps = match bdeps with - | [] -> bdeps - | hd :: tl -> if hd = dname then bdeps else purge dname tl +let debug = ref 0 + +let rec purge dname vdeps = match vdeps with + | [] -> vdeps + | hd :: tl -> if hd = dname then tl else hd :: purge dname tl let add fname = if Hashtbl.mem graph fname then () else @@ -20,30 +22,39 @@ let add_ddep fname dname = Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} let init fname dname = + if !debug land 1 > 0 then Printf.eprintf "init: %s: %s.\n" fname dname; add fname; add dname; add_ddep fname dname -let rec compute bdeps fname file = match file.rdeps with +(* vdeps: visited dependences for loop detection *) +let rec compute_from_file vdeps fname file = match file.rdeps with | Some rdeps -> rdeps - | None -> - let bdeps = fname :: bdeps in - let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in - Hashtbl.replace graph fname {file with rdeps = Some rdeps}; + | None -> + if !debug land 2 > 0 then Printf.eprintf " compute file: %s\n" fname; + let vdeps = fname :: vdeps in + List.iter (redundant vdeps fname file.ddeps) file.ddeps; + let rdeps = compute_from_ddeps vdeps file.ddeps in + Hashtbl.replace graph fname {file with rdeps = Some rdeps}; rdeps -and iter fname bdeps rdeps dname = - if StringSet.mem dname rdeps then begin - Printf.printf "%s: redundant %s\n" fname dname; - rdeps - end else if List.mem dname bdeps then begin - let loop = purge dname (List.rev bdeps) in +and compute_from_dname vdeps rdeps dname = + if List.mem dname vdeps then begin + let loop = purge dname (List.rev vdeps) in Printf.printf "circular: %s\n" (String.concat " " loop); StringSet.add dname rdeps end else let file = Hashtbl.find graph dname in - StringSet.add dname (StringSet.union (compute bdeps dname file) rdeps) + StringSet.add dname (StringSet.union (compute_from_file vdeps dname file) rdeps) + +and compute_from_ddeps vdeps ddeps = + List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps + +and redundant vdeps fname ddeps dname = + let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in + if StringSet.mem dname rdeps then + Printf.printf "%s: redundant %s\n" fname dname let check () = - let iter fname file = ignore (compute [] fname file) in + let iter fname file = ignore (compute_from_file [] fname file) in Hashtbl.iter iter graph let get_unions () = @@ -53,22 +64,45 @@ let get_unions () = in Hashtbl.fold map2 graph (StringSet.empty, StringSet.empty) +let get_leafs () = + let map fname file fnames = + if file.ddeps = [] then StringSet.add fname fnames else fnames + in + Hashtbl.fold map graph StringSet.empty + let top () = - let iter dname = Printf.printf "top: %s\n" dname in + let iter fname = Printf.printf "top: %s\n" fname in let fnames, ddeps = get_unions () in StringSet.iter iter (StringSet.diff fnames ddeps) +let leaf () = + let iter fname = Printf.printf "leaf: %s\n" fname in + let fnames = get_leafs () in + StringSet.iter iter fnames + let rec read ich = let _ = Scanf.sscanf (input_line ich) "%s@:include \"%s@\"." init in read ich let _ = + let show_check = ref false in let show_top = ref false in + let show_leaf = ref false in let process_file name = () in + let show () = + if !show_check then check (); + if !show_top then top (); + if !show_leaf then leaf () + in let help = "" in + let help_c = " Print the redundant and looping arcs of the dependences graph" in + let help_d = " Set these debug options" in + let help_l = " Print the leaf nodes of the dependences graph" in let help_t = " Print the top nodes of the dependences graph" in Arg.parse [ + "-c", Arg.Set show_check, help_c; + "-d", Arg.Int (fun x -> debug := x), help_d; + "-l", Arg.Set show_leaf, help_l; "-t", Arg.Set show_top, help_t; ] process_file help; - try read stdin with End_of_file -> - if !show_top then top () else check () + try read stdin with End_of_file -> show () diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 9bf98bda6..18258ae90 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -14,8 +14,10 @@ XOA2_CONF := ground_2/xoa2.conf.xml XOA2_TARGETS := ground_2/xoa2_notation.ma ground_2/xoa2.ma XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF) +DEP_INPUT := .depend DEP_DIR := ../../../components/binaries/matitadep DEP := matitadep.native +DEP_OPTS := MAC_DIR := ../../../components/binaries/mac MAC := mac.native @@ -28,7 +30,7 @@ PRB_OPTS := $(XOA_OPTS) -g ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig -TAGS := all xoa xoa2 orig elim deps top stats tbls trim +TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim PACKAGES := ground_2 basic_2 apps_2 @@ -83,17 +85,29 @@ orig: $(ORIGS) @echo " ORIG basic_2" $(H)$(ORIG) basic_2 < $< +# dep input ################################################################## + +$(DEP_INPUT): $(MAS) + @echo " GREP include" + $(H)grep "include \"" $^ > $(DEP_INPUT) + # dep ######################################################################## -deps: $(DEP_DIR)/$(DEP) - @echo " MATITADEP" - $(H)grep "include \"" $(MAS) | $< +deps: $(DEP_INPUT) + @echo " MATITADEP -c" + $(H)$(DEP_DIR)/$(DEP) -c $(DEP_OPTS) < $< # top ######################################################################## -top: $(DEP_DIR)/$(DEP) +top: $(DEP_INPUT) @echo " MATITADEP -t" - $(H)grep "include \"" $(MAS) | $< -t + $(H)$(DEP_DIR)/$(DEP) -t $(DEP_OPTS) < $< + +# leaf ####################################################################### + +leaf: $(DEP_INPUT) + @echo " MATITADEP -l" + $(H)$(DEP_DIR)/$(DEP) -l $(DEP_OPTS) < $< # stats ###################################################################### 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 e508aac31..13d69acd4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -20,7 +20,7 @@ include "basic_2/computation/lsubc_ldrops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) -(* Main propertis ***********************************************************) +(* Main properties **********************************************************) (* Basic_1: was: sc3_arity_csubc *) theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma new file mode 100644 index 000000000..2448b5260 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fleq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/fleq_8.ma". +include "basic_2/computation/lpxs.ma". + +(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) + +(* Note: this definition works but is not symmetric nor decidable *) +definition fleq: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g,G1,L1,T1,G2,L2,T2. + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2. + +interpretation + "equivalent 'big tree' normal forms (closure)" + 'FLEq h g G1 L1 T1 G2 L2 T2 = (fleq h g G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma fleq_refl: ∀h,g. tri_reflexive … (fleq h g). +/2 width=1 by and3_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index 047aee3d4..9022732dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/computation/fpbs_alt.ma". -include "basic_2/computation/fpbs_fpbs.ma". include "basic_2/computation/fpbg.ma". (* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) @@ -26,6 +25,21 @@ lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L /3 width=5 by cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ qed-. +lemma fpbg_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 +[ #L2 #T2 #HT12 #H #HL12 + elim (cpxs_neq_inv_step_sn … HT12 H) -HT12 -H + /4 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro/ +| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct + [ -HT1 elim (fqup_inv_step_sn … HT2) -HT2 + /4 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro/ + | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, fqup_fqus, ex3_2_intro, ex2_3_intro/ + ] +] +qed-. + (* Advanced properties ******************************************************) lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma index f0d79dc33..24d0634b5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma @@ -15,7 +15,7 @@ include "basic_2/computation/fpbg_fpbg.ma". include "basic_2/computation/fpbr.ma". -(* RESTRICTED "BIG TREE" ORDER FOR CLOSURES *********************************) +(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********) (* Advanced forward lemmas **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma new file mode 100644 index 000000000..826500bf1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/fpbc.ma". +include "basic_2/computation/fleq.ma". +include "basic_2/computation/fpbs_alt.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Forward lemmas on equivalent "big tree" normal forms *********************) + +lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H +#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #HT2 elim (fqup_inv_step_sn … HT2) -HT2 + /5 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct /3 width=1 by and3_intro, or_introl/ + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, ex3_2_intro, ex2_3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index e89bf398a..a6d662799 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -28,6 +28,18 @@ interpretation "'big tree' strong normalization (closure)" 'BTSN h g G L T = (fsb h g G L T). +(* Basic eliminators ********************************************************) + +lemma fsb_ind_alt: ∀h,g. ∀R: relation3 …. ( + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 + ) → R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T. +#h #g #R #IH #G #L #T #H elim H -G -L -T +/4 width=1 by fsb_intro/ +qed-. + (* Basic inversion lemmas ***************************************************) lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index ceb1230ab..39b97103d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/btsnalt_5.ma". include "basic_2/computation/fpbg.ma". include "basic_2/computation/fsb.ma". -(* GENERAL "BIG TREE" STRONGLY NORMALIZING TERMS ****************************) +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma new file mode 100644 index 000000000..72f4695ca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fpbs_fleq.ma". +include "basic_2/computation/fpbg_fpbg.ma". +include "basic_2/computation/fsb.ma". + +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) + +axiom fleq_fpbc_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. + +axiom fleq_fpbg_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. + +(* Properties ******************************************************) + +lemma fsb_fleq_trans: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2. +#h #g #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +/4 width=5 by fsb_intro, fleq_fpbc_trans/ +qed-. + +(* Advanced eliminators *****************************************************) + +lemma fsb_ind_fpbg_fpbs: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #g #R #IH #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 +#G1 #L1 #T1 #H1 #IH1 #G2 #L2 #T2 #H12 elim (fpbs_fwd_fpb_sn … H12) -H12 +[ #H12 @IH -IH /2 width=5 by fsb_fleq_trans/ + -H1 #G0 #L0 #T0 #H20 lapply (fleq_fpbg_trans … H12 H20) -G2 -L2 -T2 + #H10 elim (fpbg_fwd_fpb_sn … H10) -H10 /2 width=5 by/ +| -H1 -IH * /2 width=5 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbc_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbc_lift.etc new file mode 100644 index 000000000..286290135 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbc_lift.etc @@ -0,0 +1,9 @@ +include "basic_2/reduction/lpx_ldrop.ma". + +lemma lpx_fpbc_trans: ∀h,g,G1,G2,K1,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, g] T & ⦃G1, K1, T⦄ ≻[h, g] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #K1 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 + /3 width=5 by fpbc_fqu, ex3_2_intro/ +| #T2 #HT12 #H #HKL1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc new file mode 100644 index 000000000..546994dfa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fleq/fpbs.etc @@ -0,0 +1,22 @@ +(* alternative proof that needs decidability of bteq to go in fpbs.ma + * or lpx_fpbc_trans to go in fpbs_lift.ma (possibly) +*) + +axiom lpx_bteq_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1⦄ ⊢➡ [h, g] L → + ⦃G1, L, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄. + +lemma fpbs_fwd_fpb_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⋕[h, g] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 [ /2 width=1 by or_introl/ ] (**) (* auto fails without brackets *) +#G1 #G #L1 #L #T1 #T * +[ #G0 #L0 #T0 #H #H02 #IH1 elim (fquq_inv_gen … H) -H + [ -IH1 /4 width=5 by fpbc_fqu, ex2_3_intro, or_intror/ + | -H02 * #HG #HL #HT destruct /2 width=1 by/ + ] +| #T0 #HT10 #H02 #IH02 elim (eq_term_dec T1 T0) #H destruct + [ -H02 /2 width=1 by/ + | -IH02 /5 width=5 by fpbc_cpx, ex2_3_intro, or_intror/ + ] +| #L0 #HL10 #_ * [ /3 width=3 by or_introl, lpx_bteq_trans/ ] + * #G3 #L3 #T3 #H13 #H32 diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.ma new file mode 100644 index 000000000..4e30eb6fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/fleq_8.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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break [ term 46 h , break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'FLEq $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 5ebf0e0b3..f596851ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -50,7 +50,7 @@ Mutual recursive preservation of stratified native validity - for hyper computation on closures. + for "big tree" computation on closures. Confluence for context-free parallel reduction on closures. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index a78ccb133..d91e8d629 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -80,7 +80,7 @@ table { } ] [ { "strongly normalizing \"big tree\" computation" * } { - [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_csx" * ] + [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_fleq" + "fsb_csx" * ] } ] [ { "strongly normalizing extended computation" * } { @@ -91,7 +91,7 @@ table { [ { "\"big tree\" parallel computation" * } { [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_fpbs" * ] } ] [ { "decomposed extended computation" * } { @@ -233,7 +233,11 @@ table { [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] } ] - [ { "global env. slicing" * } { + [ { "lazy equivalence for closures" * } { + [ "fleq ( ⦃?,?,?⦄ ⋕ ⦃?,?,?⦄ )" "fleq_fleq" * ] + } + ] + [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } ]