From a67fc50ccfda64377e2c94c18c3a0d9265f651db Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 20 Mar 2019 12:30:38 +0100 Subject: [PATCH] update in ground_2 static_2 basic_2 + whd normal forms for terms with arity + positive abbreviations are not whd normal forms + minor additions --- .../{predtywhead_5.ma => predtywhead_4.ma} | 4 +- .../basic_2/rt_computation/cpms_cwhx.ma | 76 +++++++++++++++ .../basic_2/rt_computation/cpms_fpbg.ma | 6 +- .../basic_2/rt_transition/cnx_basic.ma | 33 +++++++ .../basic_2/rt_transition/cpr_drops_basic.ma | 49 ++++++++++ .../basic_2/rt_transition/cpr_tdeq.ma | 32 +++++++ .../basic_2/rt_transition/cpx_drops_basic.ma | 48 ++++++++++ .../lambdadelta/basic_2/rt_transition/cwhx.ma | 94 ++++++++++++++----- .../basic_2/rt_transition/cwhx_drops.ma | 46 +++++++++ .../basic_2/rt_transition/cwhx_rdeq.ma | 41 ++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 9 +- .../lambdadelta/ground_2/lib/arith.ma | 8 ++ .../ground_2/relocation/rtmap_basic_after.ma | 39 ++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +- .../static_2/notation/relations/rlift_4.ma | 19 ++++ .../static_2/relocation/lifts_basic.ma | 36 +++++++ .../lambdadelta/static_2/syntax/tdeq.ma | 7 ++ .../lambdadelta/static_2/web/static_2_src.tbl | 8 +- 18 files changed, 522 insertions(+), 37 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predtywhead_5.ma => predtywhead_4.ma} (91%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/notation/relations/rlift_4.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/relocation/lifts_basic.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma index bd6c4268c..05f4ee9c6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtywhead_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h, break term 46 o ] 𝐖𝐇 ⦃ break term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬈ [ break term 46 h ] 𝐖𝐇 ⦃ break term 46 T ⦄ )" non associative with precedence 45 - for @{ 'PRedTyWHead $h $o $G $L $T }. + for @{ 'PRedTyWHead $h $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma new file mode 100644 index 000000000..223efe3e0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cwhx.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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_transition/cpr_tdeq.ma". +include "basic_2/rt_transition/cwhx_drops.ma". +include "basic_2/rt_transition/cwhx_rdeq.ma". +include "basic_2/rt_computation/fsb_aaa.ma". +include "basic_2/rt_computation/cpms_cpms.ma". +include "basic_2/rt_computation/cpms_fpbg.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) + +(* Properties with whd normality for unbound rt-transition ******************) + +lemma aaa_cpms_cwhx (h) (G) (L): + ∀T1,A. ⦃G,L⦄ ⊢ T1 ⁝ A → + ∃∃n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄. +#h #G #L #T1 #A #H +letin o ≝ (sd_O h) +@(aaa_ind_fpbg … o … H) -G -L -T1 -A +#G #L #T1 #A * -G -L -T1 -A +[ #G #L #s #_ /2 width=4 by cwhx_sort, ex2_2_intro/ +| * #G #K #V1 #A #_ #IH -A + elim (IH … G K V1) [2,4: /3 width=1 by fpb_fpbg, fpb_fqu, fqu_lref_O/ ] -IH #n #V2 #HV12 #HV2 + elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2 + /5 width=10 by cpms_ell, cpms_delta, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/ +| #I #G #K #A #i #_ #IH -A + elim (IH … G K (#i)) [| /3 width=1 by fpb_fpbg, fpb_fqu/ ] -IH #n #V2 #HV12 #HV2 + elim (lifts_total … V2 (𝐔❴1❵)) #T2 #HVT2 + /5 width=10 by cpms_lref, cwhx_lifts, drops_refl, drops_drop, ex2_2_intro/ +| * #G #L #V #T1 #B #A #_ #_ #IH -B -A + [ elim (cpr_abbr_pos h o G L V T1) #T0 #HT10 #HnT10 + elim (IH G L T0) -IH [| /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HnT10 #n #T2 #HT02 #HT2 + /3 width=5 by cpms_step_sn, ex2_2_intro/ + | elim (IH … G (L.ⓓV) T1) -IH [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #n #T2 #HT12 #HT2 + /3 width=5 by cwhx_ldef, cpms_bind_dx, ex2_2_intro/ + ] +| #p #G #L #W #T1 #B #A #_ #_ #_ -B -A + /2 width=5 by cwhx_abst, ex2_2_intro/ +| #G #L #V #T1 #B #A #_ #HT1 #IH + elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n1 #T2 #HT12 #HT2 + elim (tdeq_dec h o T1 T2) [ -n1 #HT12 | -HT2 #HnT12 ] + [ lapply (tdeq_cwhx_trans … HT2 … HT12) -T2 + @(insert_eq_0 … L) #Y @(insert_eq_0 … T1) #X * -Y -X + [ #L0 #s0 #H1 #H2 destruct -IH + lapply (aaa_inv_sort … HT1) -HT1 #H destruct + | #p #L0 #W0 #T0 #H1 #H2 destruct -HT1 + elim (IH G L0 (ⓓ{p}ⓝW0.V.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_beta, ex2_2_intro/ ] + @fpb_fpbg @fpb_cpx [ /2 width=1 by cpx_beta/ ] #H + elim (tdeq_inv_pair … H) -H #H #_ #_ destruct + | #L0 #V0 #T0 #_ #H1 #H2 destruct -HT1 + elim (lifts_total V (𝐔❴1❵)) #W #HVW + elim (IH G L0 (-ⓓV0.ⓐW.T0)) -IH [ /4 width=5 by cpms_step_sn, cpm_theta, ex2_2_intro/ ] + @fpb_fpbg @fpb_cpx [ /2 width=3 by cpx_theta/ ] #H + elim (tdeq_inv_pair … H) -H #H #_ #_ destruct + ] + | elim (IH G L (ⓐV.T2)) -IH [ /4 width=5 by cpms_trans, cpms_appl_dx, ex2_2_intro/ ] + @(cpms_tdneq_fwd_fpbg … n1) [ /2 width=3 by cpms_appl_dx/ ] #H + elim (tdeq_inv_pair … H) -H #_ #_ #H /2 width=1 by/ + ] +| #G #L #U #T1 #A #_ #_ #IH -A + elim (IH … G L T1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #n #T2 #HT12 #HT2 + /3 width=4 by cpms_eps, ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma index 7584e81c9..8c0c3204e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma @@ -13,13 +13,17 @@ (**************************************************************************) include "basic_2/rt_computation/fpbg_fqup.ma". -include "basic_2/rt_computation/fpbg_fpbs.ma". +include "basic_2/rt_computation/fpbg_cpxs.ma". include "basic_2/rt_computation/cpms_fpbs.ma". (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) (* Forward lemmas with proper parallel rst-computation for closures *********) +lemma cpms_tdneq_fwd_fpbg (h) (o) (n): ∀G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → + (T1 ≛[h,o] T2 → ⊥) → ⦃G,L,T1⦄ >[h,o] ⦃G,L,T2⦄. +/3 width=2 by cpms_fwd_cpxs, cpxs_tdneq_fpbg/ qed-. + lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ → ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄. /3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma new file mode 100644 index 000000000..326de686e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/lifts_tdeq.ma". +include "basic_2/rt_transition/cpx_drops_basic.ma". +include "basic_2/rt_transition/cnx.ma". + +(* NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ********) + +(* Advanced inversion lemmas ************************************************) + +lemma cnx_inv_abbr_pos (h) (o) (G) (L): ∀V,T. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐍⦃+ⓓV.T⦄ → ⊥. +#h #o #G #L #V #U1 #H +elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 +elim (tdeq_dec h o U1 U2) #HnU12 [ -HU12 | -HTU2 ] +[ elim (tdeq_inv_lifts_dx … HnU12 … HTU2) -U2 #T1 #HTU1 #_ -T2 + lapply (H T1 ?) -H [ /2 width=3 by cpx_zeta/ ] #H + /2 width=9 by tdeq_lifts_inv_pair_sn/ +| lapply (H (+ⓓV.U2) ?) -H [ /2 width=1 by cpx_bind/ ] -HU12 #H + elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma new file mode 100644 index 000000000..705031ffd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops_basic.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/lifts_basic.ma". +include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_transition/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************) + +(* Properties with basic relocation *****************************************) + +lemma cpr_subst (h) (G) (L) (U1) (i): + ∀K,V. ⬇*[i] L ≘ K.ⓓV → + ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ➡[h] U2 & ⬆[i,1] T2 ≘ U2. +#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1 +#G0 #L0 #U0 #IH #G #L * * +[ #s #HG #HL #HT #i #K #V #_ destruct -IH + /2 width=4 by lifts_sort, ex2_2_intro/ +| #j #HG #HL #HT #i #K #V #HLK destruct -IH + elim (lt_or_eq_or_gt i j) #Hij + [ /3 width=4 by lifts_lref_ge_minus, cpr_refl, ex2_2_intro/ + | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2 + elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ] + /3 width=7 by cpm_delta_drops, ex2_2_intro/ + | /3 width=4 by lifts_lref_lt, cpr_refl, ex2_2_intro/ + ] +| #l #HG #HL #HT #i #K #V #_ destruct -IH + /2 width=4 by lifts_gref, ex2_2_intro/ +| #p #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct + elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2 + elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2 + /3 width=9 by cpm_bind, lifts_bind, ex2_2_intro/ +| #J #W1 #U1 #HG #HL #HT #i #K #V #HLK destruct + elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2 + elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2 + /3 width=8 by cpr_flat, lifts_flat, ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.ma new file mode 100644 index 000000000..f4a899d0d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_tdeq.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 "static_2/relocation/lifts_tdeq.ma". +include "basic_2/rt_transition/cpr_drops_basic.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************) + +(* Properties with context-free degree-based equivalence ********************) + +lemma cpr_abbr_pos (h) (o) (G) (L) (V) (T1): + ∃∃T2. ⦃G,L⦄ ⊢ +ⓓV.T1 ➡[h] T2 & (+ⓓV.T1 ≛[h, o] T2 → ⊥). +#h #o #G #L #V #U1 +elim (cpr_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2 +elim (tdeq_dec h o U1 U2) [ -HU12 #HU12 | -HTU2 #HnU12 ] +[ elim (tdeq_inv_lifts_dx … HU12 … HTU2) -U2 #T1 #HTU1 #_ -T2 + /3 width=9 by cpm_zeta, tdeq_lifts_inv_pair_sn, ex2_intro/ +| @(ex2_intro … (+ⓓV.U2)) [ /2 width=1 by cpm_bind/ ] -HU12 #H + elim (tdeq_inv_pair … H) -H #_ #_ /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma new file mode 100644 index 000000000..09b998bae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops_basic.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/lifts_basic.ma". +include "basic_2/rt_transition/cpx_drops.ma". + +(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Properties with basic relocation *****************************************) + +lemma cpx_subst (h) (G) (L) (U1) (i): + ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → + ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ⬈[h] U2 & ⬆[i,1] T2 ≘ U2. +#h #G #L #U1 @(fqup_wf_ind_eq (Ⓣ) … G L U1) -G -L -U1 +#G0 #L0 #U0 #IH #G #L * * +[ #s #HG #HL #HT #i #I #K #V #_ destruct -IH + /2 width=4 by lifts_sort, ex2_2_intro/ +| #j #HG #HL #HT #i #I #K #V #HLK destruct -IH + elim (lt_or_eq_or_gt i j) #Hij + [ /3 width=4 by lifts_lref_ge_minus, cpx_refl, ex2_2_intro/ + | elim (lifts_total V (𝐔❴↑i❵)) #U2 #HU2 + elim (lifts_split_trans … HU2 (𝐔❴i❵) (𝐁❴i,1❵)) [2: @(after_basic_rc i 0) ] + /3 width=7 by cpx_delta_drops, ex2_2_intro/ + | /3 width=4 by lifts_lref_lt, cpx_refl, ex2_2_intro/ + ] +| #l #HG #HL #HT #i #I #K #V #_ destruct -IH + /2 width=4 by lifts_gref, ex2_2_intro/ +| #p #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct + elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2 + elim (IH G (L.ⓑ{J}W1) U1 … (↑i)) [|*: /3 width=4 by drops_drop/ ] #U2 #T2 #HU12 #HTU2 + /3 width=9 by cpx_bind, lifts_bind, ex2_2_intro/ +| #J #W1 #U1 #HG #HL #HT #i #I #K #V #HLK destruct + elim (IH G L W1 … HLK) [| // ] #W2 #V2 #HW12 #HVW2 + elim (IH G L U1 … HLK) [| // ] #U2 #T2 #HU12 #HTU2 + /3 width=8 by cpx_flat, lifts_flat, ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma index 007c15e3f..0317cc097 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx.ma @@ -12,63 +12,105 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predtywhead_5.ma". -include "static_2/syntax/item_sd.ma". +include "basic_2/notation/relations/predtywhead_4.ma". +include "static_2/syntax/item_sh.ma". include "static_2/syntax/lenv.ma". include "static_2/syntax/genv.ma". (* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) -inductive cwhx (h) (o:sd h) (G:genv): relation2 lenv term ≝ -| cwhx_sort: ∀L,s. cwhx h o G L (⋆s) -| cwhx_abst: ∀p,L,W,T. cwhx h o G L (ⓛ{p}W.T) -| cwhx_neg : ∀L,V,T. cwhx h o G (L.ⓓV) T → cwhx h o G L (-ⓓV.T) +inductive cwhx (h:sh) (G:genv): relation2 lenv term ≝ +| cwhx_sort: ∀L,s. cwhx h G L (⋆s) +| cwhx_abst: ∀p,L,W,T. cwhx h G L (ⓛ{p}W.T) +| cwhx_ldef: ∀L,V,T. cwhx h G (L.ⓓV) T → cwhx h G L (-ⓓV.T) . interpretation "whd normality for unbound context-sensitive parallel rt-transition (term)" - 'PRedTyWHead h o G L T = (cwhx h o G L T). + 'PRedTyWHead h G L T = (cwhx h G L T). (* Basic inversion lemmas ***************************************************) -fact cwhx_inv_lref_aux (h) (o) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ → +fact cwhx_inv_lref_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → ∀i. X = #i → ⊥. -#h #o #G #Y #X * - X -Y +#h #G #Y #X * - X -Y [ #L #s #i #H destruct | #p #L #W #T #i #H destruct | #L #V #T #_ #i #H destruct ] qed-. -lemma cwhx_inv_lref (h) (o) (G): - ∀L,i. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃#i⦄ → ⊥. -/2 width=8 by cwhx_inv_lref_aux/ qed-. +lemma cwhx_inv_lref (h) (G): + ∀L,i. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃#i⦄ → ⊥. +/2 width=7 by cwhx_inv_lref_aux/ qed-. -fact cwhx_inv_gref_aux (h) (o) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ → +fact cwhx_inv_gref_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → ∀l. X = §l → ⊥. -#h #o #G #Y #X * - X -Y +#h #G #Y #X * - X -Y [ #L #s #l #H destruct | #p #L #W #T #l #H destruct | #L #V #T #_ #l #H destruct ] qed-. -lemma cwhx_inv_gref (h) (o) (G): - ∀L,l. ⦃G,L⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃§l⦄ → ⊥. -/2 width=8 by cwhx_inv_gref_aux/ qed-. +lemma cwhx_inv_gref (h) (G): + ∀L,l. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃§l⦄ → ⊥. +/2 width=7 by cwhx_inv_gref_aux/ qed-. -fact cwhx_inv_pos_aux (h) (o) (G): - ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃X⦄ → - ∀W,U. X = +ⓓW.U → ⊥. -#h #o #G #Y #X * - X -Y +fact cwhx_inv_abbr_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → + ∀V,T. X = +ⓓV.T → ⊥. +#h #G #Y #X * - X -Y [ #L #s #X1 #X2 #H destruct | #p #L #W #T #X1 #X2 #H destruct | #L #V #T #_ #X1 #X2 #H destruct ] qed-. -lemma cwhx_inv_pos (h) (o) (G): - ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h,o] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥. -/2 width=9 by cwhx_inv_pos_aux/ qed-. +lemma cwhx_inv_abbr (h) (G): + ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃+ⓓV.T⦄ → ⊥. +/2 width=8 by cwhx_inv_abbr_aux/ qed-. + +fact cwhx_inv_ldef_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → + ∀V,T. X = -ⓓV.T → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄. +#h #G #Y #X * - X -Y +[ #L #s #X1 #X2 #H destruct +| #p #L #W #T #X1 #X2 #H destruct +| #L #V #T #HT #X1 #X2 #H destruct // +] +qed-. + +lemma cwhx_inv_ldef (h) (G): + ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃-ⓓV.T⦄ → ⦃G,Y.ⓓV⦄ ⊢ ⬈[h] 𝐖𝐇⦃T⦄. +/2 width=3 by cwhx_inv_ldef_aux/ qed-. + +fact cwhx_inv_appl_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → + ∀V,T. X = ⓐV.T → ⊥. +#h #G #Y #X * - X -Y +[ #L #s #X1 #X2 #H destruct +| #p #L #W #T #X1 #X2 #H destruct +| #L #V #T #_ #X1 #X2 #H destruct +] +qed-. + +lemma cwhx_inv_appl (h) (G): + ∀Y,V,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓐV.T⦄ → ⊥. +/2 width=8 by cwhx_inv_appl_aux/ qed-. + +fact cwhx_inv_cast_aux (h) (G): + ∀Y,X. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃X⦄ → + ∀U,T. X = ⓝU.T → ⊥. +#h #G #Y #X * - X -Y +[ #L #s #X1 #X2 #H destruct +| #p #L #W #T #X1 #X2 #H destruct +| #L #V #T #_ #X1 #X2 #H destruct +] +qed-. + +lemma cwhx_inv_cast (h) (G): + ∀Y,U,T. ⦃G,Y⦄ ⊢ ⬈[h] 𝐖𝐇⦃ⓝU.T⦄ → ⊥. +/2 width=8 by cwhx_inv_cast_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma new file mode 100644 index 000000000..8ef7b522b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_drops.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/relocation/drops.ma". +include "basic_2/rt_transition/cwhx.ma". + +(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) + +(* Properties with generic slicing ******************************************) + +lemma cwhx_lifts (h) (G): d_liftable1 … (cwhx h G). +#h #G #K #T #H elim H -K -T +[ #K #s #b #f #L #HLK #X #H + lapply (lifts_inv_sort1 … H) -H #H destruct // +| #p #K #V #T #b #f #L #HLK #X #H + elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct // +| #K #V #T #_ #IH #b #f #L #HLK #X #H + elim (lifts_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct + /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/ +] +qed-. + +(* Inversion lemmas with generic slicing ************************************) + +lemma cwhx_inv_lifts (h) (G): d_deliftable1 … (cwhx h G). +#h #G #L #U #H elim H -L -U +[ #L #s #b #f #K #HLK #X #H + lapply (lifts_inv_sort2 … H) -H #H destruct // +| #p #L #W #U #b #f #K #HLK #X #H + elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct // +| #L #W #U #_ #IH #b #f #K #HLK #X #H + elim (lifts_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct + /5 width=4 by cwhx_ldef, drops_skip, ext2_pair/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma new file mode 100644 index 000000000..884093ad2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cwhx_rdeq.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/static/rdeq_fqup.ma". +include "basic_2/rt_transition/cwhx.ma". + +(* WHD NORMAL TERMS FOR UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ****) + +(* Properties with degree-based equivalence *********************************) + +lemma rdeq_tdeq_cwhx_trans (h) (o) (G): + ∀L2,T2. ⦃G,L2⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ → + ∀T1. T1 ≛[h,o] T2 → + ∀L1. L1 ≛[h,o,T1] L2 → ⦃G,L1⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄. +#h #o #G #L2 #T2 #H elim H -L2 -T2 +[ #L2 #s2 #X1 #HX #L1 #HL + elim (tdeq_inv_sort2 … HX) -HX #s1 #d #_ #_ #H destruct -s2 -d // +| #p #L2 #W2 #T2 #X1 #HX #L1 #HL + elim (tdeq_inv_pair2 … HX) -HX #W1 #T1 #_ #_ #H destruct -W2 -T2 // +| #L2 #V2 #T2 #_ #IH #X1 #HX #L1 #HL + elim (tdeq_inv_pair2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct + elim (rdeq_inv_bind … HL) -HL #HV1 #HT1 + /5 width=2 by cwhx_ldef, rdeq_bind_repl_dx, ext2_pair/ +] +qed-. + +lemma tdeq_cwhx_trans (h) (o) (G) (L): + ∀T2. ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T2⦄ → + ∀T1. T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐖𝐇⦃T1⦄. +/3 width=6 by rdeq_tdeq_cwhx_trans/ qed-. 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 850588ce1..bac5d2dd2 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 @@ -61,7 +61,7 @@ table { } ] [ { "t-bound context-sensitive parallel rt-computation" * } { - [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] + [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ] } ] [ { "unbound context-sensitive parallel rst-computation" * } { @@ -92,7 +92,7 @@ table { [ { "context-sensitive parallel r-transition" * } { [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] [ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] - [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_cpr" * ] + [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_drops_basic" + "cpr_tdeq" + "cpr_cpr" * ] } ] [ { "t-bound context-sensitive parallel rt-transition" * } { @@ -100,11 +100,12 @@ table { } ] [ { "unbound context-sensitive parallel rt-transition" * } { - [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] + [ [ "whd normal form for terms" ] "cwhx" + "( ⦃?,?⦄ ⊢ ⬈[?] 𝐖𝐇⦃?⦄ )" "cwhx_drops" + "cwhx_rdeq" * ] + [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_basic" + "cnx_cnx" * ] [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ] [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] - [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ] + [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_drops_basic" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ] } ] [ { "bound context-sensitive parallel rt-transition" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index a29899d45..0574e1757 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -127,6 +127,14 @@ qed-. lemma le_plus_to_minus_comm: ∀n,m,p. n ≤ p+m → n-p ≤ m. /2 width=1 by le_plus_to_minus/ qed-. +lemma le_inv_S1: ∀m,n. ↑m ≤ n → ∃∃p. m ≤ p & ↑p = n. +#m * +[ #H lapply (le_n_O_to_eq … H) -H + #H destruct +| /3 width=3 by monotonic_pred, ex2_intro/ +] +qed-. + (* Note: this might interfere with nat.ma *) lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n. #m #n #Hmn #Hm whd >(S_pred … Hm) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma new file mode 100644 index 000000000..788d8c24f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_basic_after.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/rtmap_after.ma". +include "ground_2/relocation/rtmap_basic.ma". + +(* RELOCATION MAP ***********************************************************) + +(* Properties with composition **********************************************) + +lemma after_basic_rc (m2,m1,n2,n1): + m1 ≤ m2 → m2 ≤ m1+n1 → 𝐁❴m2,n2❵ ⊚ 𝐁❴m1,n1❵ ≘ 𝐁❴m1,n2+n1❵. +#m2 elim m2 -m2 +[ #m1 #n2 #n1 #Hm21 #_ + <(le_n_O_to_eq … Hm21) -m1 // +| #m2 #IH * + [ #n2 #n1 #_ < plus_O_n #H + elim (le_inv_S1 … H) -H #x #Hx #H destruct + (plus_minus_m_m i n) in ⊢ (???%); +/3 width=2 by lifts_lref_ge, le_plus_to_minus_l, le_plus_b/ +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma index 828e2ad0f..358533f04 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/tdeq.ma @@ -92,6 +92,13 @@ lemma tdeq_inv_pair1: ∀h,o,I,V1,T1,Y. ②{I}V1.T1 ≛[h, o] Y → ∃∃V2,T2. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & Y = ②{I}V2.T2. /2 width=3 by tdeq_inv_pair1_aux/ qed-. +lemma tdeq_inv_sort2: ∀h,o,X1,s2. X1 ≛[h, o] ⋆s2 → + ∃∃s1,d. deg h o s1 d & deg h o s2 d & X1 = ⋆s1. +#h #o #X1 #s2 #H +elim (tdeq_inv_sort1 h o X1 s2) +/2 width=5 by tdeq_sym, ex3_2_intro/ +qed-. + lemma tdeq_inv_pair2: ∀h,o,I,X1,V2,T2. X1 ≛[h, o] ②{I}V2.T2 → ∃∃V1,T1. V1 ≛[h, o] V2 & T1 ≛[h, o] T2 & X1 = ②{I}V1.T1. #h #o #I #X1 #V2 #T2 #H diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 4dcb17989..990057cc1 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -75,11 +75,15 @@ table { ] class "orange" [ { "relocation" * } { - [ { "generic slicing" * } { + [ { "generic and uniform slicing" * } { [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_ltc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_sex" + "drops_lex" + "drops_seq" + "drops_drops" + "drops_vector" * ] } ] - [ { "generic relocation" * } { + [ { "basic relocation" * } { + [ [ "for terms" ] "lifts_basic" + "( ⬆[?,?] ? ≘ ? )" * ] + } + ] + [ { "generic and uniform relocation" * } { [ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≘ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] [ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≘ ? )" "lifts_lifts_vector" * ] [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≘ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] -- 2.39.2