--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "ground_2/lib/ltc.ma".
+include "basic_2/relocation/lreq_lreq.ma".
+
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties with labeled transitive closure *******************************)
+
+lemma d2_liftable_sn_ltc: ∀A,f. associative … f →
+ ∀C,S,R. (∀n. d_liftable2_sn C S (λL. R L n)) →
+ ∀n. d_liftable2_sn C S (λL. ltc A f … (R L) n).
+#A #g #Hg #C #S #R #HR #n #K #T1 #T2 #H
+@(ltc_ind_dx … Hg ???? H) -n -T2
+[ #n #T2 #HT12 #b #g #L #HLK #U1 #HTU1
+ elim (HR … HT12 … HLK … HTU1) -b -K -T1 -HR
+ /3 width=3 by ltc_rc, ex2_intro/
+| #n1 #n2 #T #T2 #_ #IHT1 #HT2 #b #f #L #HLK #U1 #HTU1
+ elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
+ elim (HR … HT2 … HLK … HTU) -HR -K -T
+ /3 width=5 by ltc_dx, ex2_intro/
+]
+qed-.
+
+lemma d2_deliftable_sn_ltc: ∀A,f. associative … f →
+ ∀C,S,R. (∀n. d_deliftable2_sn C S (λL. R L n)) →
+ ∀n. d_deliftable2_sn C S (λL. ltc A f … (R L) n).
+#A #g #Hg #C #S #R #HR #n #L #U1 #U2 #H
+@(ltc_ind_dx … Hg ???? H) -n -U2
+[ #n #U2 #HU12 #b #g #K #HLK #T1 #HTU1
+ elim (HR … HU12 … HLK … HTU1) -b -L -U1 -HR
+ /3 width=3 by ltc_rc, ex2_intro/
+| #n1 #n2 #U #U2 #_ #IHU1 #HU2 #b #f #K #HLK #T1 #HTU1
+ elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+ elim (HR … HU2 … HLK … HTU) -L -U -HR
+ /3 width=5 by ltc_dx, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_sn_ltc: ∀A,f. associative … f →
+ ∀R. (∀n. co_dropable_sn (λL. R L n)) →
+ ∀n. co_dropable_sn (λL. ltc A f … (R L) n).
+#A #g #Hg #R #HR #n #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H
+@(ltc_ind_dx … Hg ???? H) -n -L2
+[ #n #L2 #HL12 #g1 #H
+ elim (HR … HLK1 … Hf … HL12 … H) -f2 -L1 -HR -Hf
+ /3 width=3 by ltc_rc, ex2_intro/
+| #n1 #n2 #L #L2 #_ #IH #HL2 #f1 #H
+ elim (IH … H) -IH #K #HK1 #HLK
+ elim (HR … HLK … HL2 … H) -f2 -L -HR
+ /3 width=3 by ltc_dx, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_dx_ltc: ∀A,f. associative … f →
+ ∀R. (∀n. co_dropable_dx (λL. R L n)) →
+ ∀n. co_dropable_dx (λL. ltc A f … (R L) n).
+#A #g #Hg #R #HR #n #f2 #L1 #L2 #H
+@(ltc_ind_dx … Hg ???? H) -n -L2
+[ #n #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2
+ elim (HR … HL12 … HLK2 … Hf … Hf2) -f2 -L2 -HR -Hf
+ /3 width=3 by ltc_rc, ex2_intro/
+| #n1 #n2 #L #L2 #_ #IHL1 #HL2 #b #f #K2 #HLK2 #Hf #f1 #Hf2
+ elim (HR … HL2 … HLK2 … Hf … Hf2) -L2 -HR #K #HLK #HK2
+ elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
+ /3 width=5 by ltc_dx, ex2_intro/
+]
+qed-.
+
+lemma co_dedropable_sn_ltc: ∀A,f. associative … f →
+ ∀R. (∀n. co_dedropable_sn (λL. R L n)) →
+ ∀n. co_dedropable_sn (λL. ltc A f … (R L) n).
+#A #g #Hg #R #HR #n #b #f #L1 #K1 #HLK1 #f1 #K2 #H
+@(ltc_ind_dx … Hg ???? H) -n -K2
+[ #n #K2 #HK12 #f2 #Hf
+ elim (HR … HLK1 … HK12 … Hf) -f1 -K1 -HR
+ /3 width=4 by ltc_rc, ex3_intro/
+| #n1 #n2 #K #K2 #_ #IH #HK2 #f2 #Hf
+ elim (IH … Hf) -K1 -IH #L #H1L1 #HLK #H2L1
+ elim (HR … HLK … HK2 … Hf) -f1 -K -HR
+ /3 width=6 by lreq_trans, ltc_dx, ex3_intro/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/relocation/drops_ltc.ma".
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Advanced properties ******************************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+(* Basic_2A1: uses: cprs_delta *)
+lemma cpms_delta_drops (n) (h) (G):
+ ∀L,K,V,i. ⬇*[i] L ≘ K.ⓓV →
+ ∀V2. ⦃G, K⦄ ⊢ V ➡*[n, h] V2 →
+ ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡*[n, h] W2.
+#n #h #G #L #K #V #i #HLK #V2 #H @(cpms_ind_dx … H) -V2
+[ /3 width=6 by cpm_cpms, cpm_delta_drops/
+| #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2
+ lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
+ elim (lifts_total V1 (𝐔❴↑i❵)) #W1 #HVW1
+ /3 width=11 by cpm_lifts_bi, cpms_step_dx/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpms_inv_lref1_drops (n) (h) (G):
+ ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[n, h] T2 →
+ ∨∨ ∧∧ T2 = #i & n = 0
+ | ∃∃K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G, K⦄ ⊢ V ➡*[n, h] V2 &
+ ⬆*[↑i] V2 ≘ T2
+ | ∃∃m,K,V,V2. ⬇*[i] L ≘ K.ⓛV & ⦃G, K⦄ ⊢ V ➡*[m, h] V2 &
+ ⬆*[↑i] V2 ≘ T2 & n = ↑m.
+#n #h #G #L #T2 #i #H @(cpms_ind_dx … H) -T2
+[ /3 width=1 by or3_intro0, conj/
+| #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH *
+ [ #H1 #H2 destruct
+ elim (cpm_inv_lref1_drops … HT2) -HT2 *
+ [ /3 width=1 by or3_intro0, conj/
+ | /4 width=6 by cpm_cpms, or3_intro1, ex3_3_intro/
+ | /4 width=8 by cpm_cpms, or3_intro2, ex4_4_intro/
+ ]
+ | #K #V0 #V #HLK #HV0 #HVT
+ lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+ elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+ /4 width=6 by cpms_step_dx, ex3_3_intro, or3_intro1/
+ | #m #K #V0 #V #HLK #HV0 #HVT #H destruct
+ lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
+ elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
+ /4 width=8 by cpms_step_dx, ex4_4_intro, or3_intro2/
+ ]
+]
+qed-.
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: uses: scpds_lift *)
+(* Basic_2A1: includes: cprs_lift *)
+(* Basic_1: includes: pr3_lift *)
+lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n).
+/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: uses: scpds_inv_lift1 *)
+(* Basic_2A1: includes: cprs_inv_lift1 *)
+(* Basic_1: includes: pr3_gen_lift *)
+lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
+/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
include "basic_2/rt_transition/cpr.ma".
include "basic_2/rt_computation/cpms.ma".
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION FOR TERMS *************************)
+(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************)
(* Basic eliminators ********************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/rt_computation/cpms_drops.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: pr3_gen_lref *)
+(* Basic_2A1: was: cprs_inv_lref1 *)
+lemma cprs_inv_lref1_drops (h) (G): ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h] T2 →
+ ∨∨ T2 = #i
+ | ∃∃K,V1,T1. ⬇*[i] L ≘ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡*[h] T1 &
+ ⬆*[↑i] T1 ≘ T2.
+#h #G #L #T2 #i #H elim (cpms_inv_lref1_drops … H) -H *
+[ /2 width=1 by or_introl/
+| /3 width=6 by ex3_3_intro, or_intror/
+| #m #K #V #V2 #_ #_ #_ #H destruct
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/cpr_lift.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Advanced properties ******************************************************)
-
-(* Note: apparently this was missing in basic_1 *)
-lemma cprs_delta: ∀G,L,K,V,V2,i.
- ⬇[i] L ≘ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 →
- ∀W2. ⬆[0, i + 1] V2 ≘ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.
-#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6 by cpr_cprs, cpr_delta/ ]
-#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
-lapply (drop_fwd_drop2 … HLK) -HLK #HLK
-elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was: pr3_gen_lref *)
-lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
- T2 = #i ∨
- ∃∃K,V1,T1. ⬇[i] L ≘ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 &
- ⬆[0, i + 1] T1 ≘ T2.
-#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1 by or_introl/
-#T #T2 #_ #HT2 *
-[ #H destruct
- elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
- * /4 width=6 by cpr_cprs, ex3_3_intro, or_intror/
-| * #K #V1 #T1 #HLK #HVT1 #HT1
- lapply (drop_fwd_drop2 … HLK) #H0LK
- elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
- /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
-]
-qed-.
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: was: pr3_lift *)
-lemma cprs_lift: ∀G. d_liftable (cprs G).
-/3 width=10 by d_liftable_CTC, cpr_lift/ qed.
-
-(* Basic_1: was: pr3_gen_lift *)
-lemma cprs_inv_lift1: ∀G. d_deliftable_sn (cprs G).
-/3 width=6 by d_deliftable_sn_CTC, cpr_inv_lift1/
-qed-.
fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma
fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
-cpms.ma
-cprs.ma
+cpms.ma cpms_drops.ma
+cprs.ma cprs_drops.ma
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/static/da_lift.ma".
-include "basic_2/unfold/lstas_lift.ma".
-include "basic_2/computation/cprs_lift.ma".
-include "basic_2/computation/scpds.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
-
-(* Relocation properties ****************************************************)
-
-lemma scpds_lift: ∀h,o,G,d. d_liftable (scpds h o d G).
-#h #o #G #d2 #K #T1 #T2 * #T #d1 #Hd21 #Hd1 #HT1 #HT2 #L #b #l #k
-elim (lift_total T l k)
-/3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/
-qed.
-
-lemma scpds_inv_lift1: ∀h,o,G,d. d_deliftable_sn (scpds h o d G).
-#h #o #G #d2 #L #U1 #U2 * #U #d1 #Hd21 #Hd1 #HU1 #HU2 #K #b #l #k #HLK #T1 #HTU1
-lapply (da_inv_lift … Hd1 … HLK … HTU1) -Hd1 #Hd1
-elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1
-elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L
-/3 width=8 by ex4_2_intro, ex2_intro/
-qed-.
(*
[ [ "" ] "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
*)
- [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" (* "cprs_lift" + "cprs_cprs" *) * ]
+ [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_drops" (* + "cprs_cprs" *) * ]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
- [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" * ]
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" * ]
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
class "orange"
[ { "relocation" * } {
[ { "generic slicing" * } {
- [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
+ [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
}
]
[ { "generic relocation" * } {
projects / helm.git / commitdiff