From b4f76b0d8fa0e5365fb48e91474febe200b647a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 30 Sep 2019 20:12:31 +0200 Subject: [PATCH] update in ground_2 and basic_2 + initial support for t-transition (the core of inferred type assignment) --- .../basic_2/notation/relations/pty_6.ma | 19 ++++ .../basic_2/notation/relations/ptystar_6.ma | 19 ++++ .../lambdadelta/basic_2/rt_transition/cpt.ma | 95 +++++++++++++++++++ .../basic_2/rt_transition/cpt_cpm.ma | 66 +++++++++++++ .../basic_2/rt_transition/cpt_drops.ma | 46 +++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 + .../ground_2/notation/relations/istype_2.ma | 19 ++++ .../lambdadelta/ground_2/steps/rtc_ist.ma | 52 ++++++++++ .../lambdadelta/ground_2/steps/rtc_ist_max.ma | 60 ++++++++++++ .../ground_2/steps/rtc_ist_plus.ma | 60 ++++++++++++ .../ground_2/steps/rtc_ist_shift.ma | 38 ++++++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 3 +- 12 files changed, 480 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/pty_6.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/ptystar_6.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/istype_2.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_max.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_shift.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pty_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pty_6.ma new file mode 100644 index 000000000..0fb47e92f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pty_6.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 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬆[ break term 46 h, break term 46 n ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PTy $h $n $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ptystar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ptystar_6.ma new file mode 100644 index 000000000..884303830 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/ptystar_6.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 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬆*[ break term 46 h, break term 46 n ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PTyStar $h $n $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma new file mode 100644 index 000000000..0ccb505e6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma @@ -0,0 +1,95 @@ +(**************************************************************************) +(* ___ *) +(* ||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/steps/rtc_ist_shift.ma". +include "ground_2/steps/rtc_ist_plus.ma". +include "ground_2/steps/rtc_ist_max.ma". +include "basic_2/notation/relations/pty_6.ma". +include "basic_2/rt_transition/cpg.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************) + +definition cpt (h) (G) (L) (n): relation2 term term ≝ + λT1,T2. ∃∃c. 𝐓⦃n,c⦄ & ⦃G,L⦄ ⊢ T1 ⬈[eq …,c,h] T2. + +interpretation + "t-bound context-sensitive parallel t-transition (term)" + 'PTy h n G L T1 T2 = (cpt h G L n T1 T2). + +(* Basic properties *********************************************************) + +lemma cpt_ess (h) (G) (L): + ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s). +/2 width=3 by cpg_ess, ex2_intro/ qed. + +lemma cpt_delta (h) (n) (G) (K): + ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 → + ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆[h,n] W2. +#h #n #G #K #V1 #V2 * +/3 width=5 by cpg_delta, ex2_intro/ +qed. + +lemma cpt_ell (h) (n) (G) (K): + ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 → + ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆[h,↑n] W2. +#h #n #G #K #V1 #V2 * +/3 width=5 by cpg_ell, ex2_intro, ist_succ/ +qed. + +lemma cpt_lref (h) (n) (G) (K): + ∀T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T → ∀U. ⇧*[1] T ≘ U → + ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆[h,n] U. +#h #n #G #K #T #i * +/3 width=5 by cpg_lref, ex2_intro/ +qed. + +lemma cpt_bind (h) (n) (G) (L): + ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 → + ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] ⓑ{p,I}V2.T2. +#h #n #G #L #V1 #V2 * #cV #HcV #HV12 #I #T1 #T2 * +/3 width=5 by cpg_bind, ist_max_O1, ex2_intro/ +qed. + +lemma cpt_appl (h) (n) (G) (L): + ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] ⓐV2.T2. +#h #n #G #L #V1 #V2 * #cV #HcV #HV12 #T1 #T2 * +/3 width=5 by ist_max_O1, cpg_appl, ex2_intro/ +qed. + +lemma cpt_cast (h) (n) (G) (L): + ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 → + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆[h,n] ⓝU2.T2. +#h #n #G #L #U1 #U2 * #cU #HcU #HU12 #T1 #T2 * +/3 width=6 by cpg_cast, ex2_intro/ +qed. + +lemma cpt_ee (h) (n) (G) (L): + ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 → ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆[h,↑n] U2. +#h #n #G #L #V1 #V2 * +/3 width=3 by cpg_ee, ist_succ, ex2_intro/ +qed. + +(* Basic properties *********************************************************) + +lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0). +/3 width=3 by cpg_refl, ex2_intro/ qed. + +(* Advanced properties ******************************************************) + +lemma cpt_sort (h) (G) (L): + ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s). +#h #G #L * // +#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.ma new file mode 100644 index 000000000..c37ddc224 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_cpm.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpm_drops.ma". +include "basic_2/rt_transition/cpt_drops.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************) + +(* Properties with t-bound rt-transition for terms **************************) + +lemma cpm_cpt_cpr (h) (n) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2. +#h #n #G #L #T1 #T2 #H +@(cpm_ind … H) -n -G -L -T1 -T2 +[ #I #G #L /2 width=3 by ex2_intro/ +| #G #L #s /3 width=3 by cpm_sort, ex2_intro/ +| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2 + elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0 + lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02 + /3 width=3 by cpt_delta, ex2_intro/ +| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2 + elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0 + lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02 + /3 width=3 by cpt_ell, ex2_intro/ +| #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2 + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02 + /3 width=3 by cpt_lref, ex2_intro/ +| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02 + /3 width=5 by cpt_bind, cpm_bind, ex2_intro/ +| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02 + /3 width=5 by cpt_appl, cpm_appl, ex2_intro/ +| #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02 + /3 width=5 by cpt_cast, cpm_cast, ex2_intro/ +| #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02 + elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1 + [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10 + /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/ +| #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02 +| #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02 + /3 width=3 by cpt_ee, ex2_intro/ +| #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 + /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/ +| #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20 + /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/ +] + +(* Forward lemmas with t-bound rt-transition for terms **********************) + +lemma cpt_fwd_cpm (h) (n) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2. \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma new file mode 100644 index 000000000..6447e51ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_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 "basic_2/rt_transition/cpg_drops.ma". +include "basic_2/rt_transition/cpt.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************) + +(* Properties with generic slicing for local environments *******************) + +lemma cpt_lifts_sn (h) (n) (G): + d_liftable2_sn … lifts (λL. cpt h G L n). +#h #n #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1 +elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1 +/3 width=5 by ex2_intro/ +qed-. + +lemma cpt_lifts_bi (h) (n) (G): + d_liftable2_bi … lifts (λL. cpt h G L n). +#h #n #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +lemma cpt_inv_lifts_sn (h) (n) (G): + d_deliftable2_sn … lifts (λL. cpt h G L n). +#h #n #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1 +elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1 +/3 width=5 by ex2_intro/ +qed-. + +lemma cpt_inv_lifts_bi (h) (n) (G): + d_deliftable2_bi … lifts (λL. cpt h G L n). +#h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/ +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 62987557d..671bd5bae 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 @@ -92,6 +92,10 @@ table { ] class "cyan" [ { "rt-transition" * } { + [ { "context-sensitive parallel t-transition" * } { + [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_cpm" * ] + } + ] [ { "context-sensitive parallel r-transition" * } { [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ] [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istype_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istype_2.ma new file mode 100644 index 000000000..795d811ab --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/istype_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 "hvbox( 𝐓⦃ term 46 n, break term 46 c ⦄ )" + non associative with precedence 45 + for @{ 'IsType $n $c }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist.ma new file mode 100644 index 000000000..6b9b64681 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/istype_2.ma". +include "ground_2/steps/rtc.ma". + +(* T-TRANSITION COUNTER *****************************************************) + +definition ist: relation2 nat rtc ≝ + λts,c. 〈0,0,0,ts〉 = c. + +interpretation "test for t-transition counter (rtc)" + 'IsType ts c = (ist ts c). + +(* Basic properties *********************************************************) + +lemma isr_00: 𝐓⦃0,𝟘𝟘⦄. +// qed. + +lemma ist_01: 𝐓⦃1,𝟘𝟙⦄. +// qed. + +(* Basic inversion properties ***********************************************) + +lemma ist_inv_00: ∀n. 𝐓⦃n,𝟘𝟘⦄ → 0 = n. +#n #H destruct // +qed-. + +lemma ist_inv_01: ∀n. 𝐓⦃n,𝟘𝟙⦄ → 1 = n. +#n #H destruct // +qed-. + +(* Main inversion properties ************************************************) + +theorem ist_inj: ∀n1,n2,c. 𝐓⦃n1,c⦄ → 𝐓⦃n2,c⦄ → n1 = n2. +#n1 #n2 #c #H1 #H2 destruct // +qed-. + +theorem ist_mono: ∀n,c1,c2. 𝐓⦃n,c1⦄ → 𝐓⦃n,c2⦄ → c1 = c2. +#n #c1 #c2 #H1 #H2 destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_max.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_max.ma new file mode 100644 index 000000000..ba31b7faa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_max.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/steps/rtc_max.ma". +include "ground_2/steps/rtc_ist.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +(* Properties with test for t-transition counter ****************************) + +lemma ist_max: ∀n1,n2,c1,c2. 𝐓⦃n1,c1⦄ → 𝐓⦃n2,c2⦄ → 𝐓⦃n1∨n2,c1∨c2⦄. +#n1 #n2 #c1 #c2 #H1 #H2 destruct // +qed. + +lemma ist_max_O1: ∀n,c1,c2. 𝐓⦃0,c1⦄ → 𝐓⦃n,c2⦄ → 𝐓⦃n,c1∨c2⦄. +/2 width=1 by ist_max/ qed. + +lemma ist_max_O2: ∀n,c1,c2. 𝐓⦃n,c1⦄ → 𝐓⦃0,c2⦄ → 𝐓⦃n,c1∨c2⦄. +#n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by ist_max/ +qed. + +lemma ist_max_idem1: ∀n,c1,c2. 𝐓⦃n,c1⦄ → 𝐓⦃n,c2⦄ → 𝐓⦃n,c1∨c2⦄. +#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by ist_max/ +qed. + +(* Inversion properties with test for t-transition counter ******************) + +lemma ist_inv_max: + ∀n,c1,c2. 𝐓⦃n,c1 ∨ c2⦄ → + ∃∃n1,n2. 𝐓⦃n1,c1⦄ & 𝐓⦃n2,c2⦄ & (n1 ∨ n2) = n. +#n #c1 #c2 #H +elim (max_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct +elim (max_inv_O3 … H1) -H1 #H11 #H12 destruct +elim (max_inv_O3 … H2) -H2 #H21 #H22 destruct +elim (max_inv_O3 … H3) -H3 #H31 #H32 destruct +/2 width=5 by ex3_2_intro/ +qed-. + +lemma ist_O_inv_max: ∀c1,c2. 𝐓⦃0,c1 ∨ c2⦄ → ∧∧ 𝐓⦃0,c1⦄ & 𝐓⦃0,c2⦄. +#c1 #c2 #H +elim (ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H +elim (max_inv_O3 … H) -H #H1 #H2 destruct +/2 width=1 by conj/ +qed-. + +lemma ist_inv_max_O_dx: ∀n,c1,c2. 𝐓⦃n,c1 ∨ c2⦄ → 𝐓⦃0,c2⦄ → 𝐓⦃n,c1⦄. +#n #c1 #c2 #H #H2 +elim (ist_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma new file mode 100644 index 000000000..c17eec5b6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_plus.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/steps/rtc_plus.ma". +include "ground_2/steps/rtc_ist.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +(* Properties with test for t-transition counter ****************************) + +lemma ist_plus: ∀n1,n2,c1,c2. 𝐓⦃n1,c1⦄ → 𝐓⦃n2,c2⦄ → 𝐓⦃n1+n2,c1+c2⦄. +#n1 #n2 #c1 #c2 #H1 #H2 destruct // +qed. + +lemma ist_plus_O1: ∀n,c1,c2. 𝐓⦃0,c1⦄ → 𝐓⦃n,c2⦄ → 𝐓⦃n,c1+c2⦄. +/2 width=1 by ist_plus/ qed. + +lemma ist_plus_O2: ∀n,c1,c2. 𝐓⦃n,c1⦄ → 𝐓⦃0,c2⦄ → 𝐓⦃n,c1+c2⦄. +#n #c1 #c2 #H1 #H2 >(plus_n_O n) /2 width=1 by ist_plus/ +qed. + +lemma ist_succ: ∀n,c. 𝐓⦃n,c⦄ → 𝐓⦃↑n,c+𝟘𝟙⦄. +/2 width=1 by ist_plus/ qed. + +(* Inversion properties with test for constrained rt-transition counter *****) + +lemma ist_inv_plus: + ∀n,c1,c2. 𝐓⦃n,c1 + c2⦄ → + ∃∃n1,n2. 𝐓⦃n1,c1⦄ & 𝐓⦃n2,c2⦄ & n1 + n2 = n. +#n #c1 #c2 #H +elim (plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H1 #H2 #H3 #H4 #H5 #H6 destruct +elim (plus_inv_O3 … H1) -H1 #H11 #H12 destruct +elim (plus_inv_O3 … H2) -H2 #H21 #H22 destruct +elim (plus_inv_O3 … H3) -H3 #H31 #H32 destruct +/3 width=5 by ex3_2_intro/ +qed-. + +lemma ist_inv_plus_O_dx: ∀n,c1,c2. 𝐓⦃n,c1 + c2⦄ → 𝐓⦃0,c2⦄ → 𝐓⦃n,c1⦄. +#n #c1 #c2 #H #H2 +elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct // +qed-. + +lemma ist_inv_plus_SO_dx: + ∀n,c1,c2. 𝐓⦃n,c1 + c2⦄ → 𝐓⦃1,c2⦄ → + ∃∃m. 𝐓⦃m,c1⦄ & n = ↑m. +#n #c1 #c2 #H #H2 destruct +elim (ist_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +/2 width=3 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_shift.ma new file mode 100644 index 000000000..99ad5a092 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_ist_shift.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/steps/rtc_shift.ma". +include "ground_2/steps/rtc_ist.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +(* Properties with test for t-transition counter ****************************) + +lemma ist_zero_shift: ∀c. 𝐓⦃0,c⦄ → 𝐓⦃0,↕*c⦄. +#c #H destruct // +qed. + +(* Inversion properties with test for t-transition counter ******************) + +lemma ist_inv_shift: ∀n,c. 𝐓⦃n,↕*c⦄ → ∧∧ 𝐓⦃0,c⦄ & 0 = n. +#n #c #H +elim (shift_inv_dx … H) -H #rt0 #rs0 #ti0 #ts0 #H1 #_ #H2 #H3 #H4 destruct +elim (max_inv_O3 … H1) -H1 #H11 #H12 destruct +elim (max_inv_O3 … H2) -H2 #H21 #H22 destruct +/2 width=1 by conj/ +qed-. + +lemma ist_inv_zero_shift: ∀c. 𝐓⦃0,↕*c⦄ → 𝐓⦃0,c⦄. +#c #H elim (ist_inv_shift … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index bf3287912..474eb2778 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -12,7 +12,8 @@ table { class "water" [ { "generic rt-transition counter" * } { [ { "" * } { - [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_isrc ( 𝐑𝐓⦃?, ?⦄ )" "rtc_shift ( ↕*? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ] + [ "rtc_ist ( 𝐓⦃?,?⦄ )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ] + [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_isrc ( 𝐑𝐓⦃?,?⦄ )" "rtc_shift ( ↕*? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ] } ] } -- 2.39.2