From: Ferruccio Guidi Date: Thu, 8 Sep 2011 19:48:13 +0000 (+0000) Subject: - support for transitive closures started X-Git-Tag: make_still_working~2298 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b4240d93f7fd4c3e60d3495dc558edfc0e0f48e7;p=helm.git - support for transitive closures started - "unfold" component started - we corrected one axiom of drop --- diff --git a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt index c68d0701f..b45870449 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt +++ b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt @@ -268,32 +268,12 @@ pr2/clen pr2_gen_ctail # check ###################################################################### -pr2/clen pr2_gen_cbind -pr2/clen pr2_gen_cflat -pr2/fwd pr2_gen_sort -pr2/fwd pr2_gen_lref -pr2/fwd pr2_gen_abst -pr2/fwd pr2_gen_cast -pr2/fwd pr2_gen_csort -pr2/fwd pr2_gen_appl -pr2/fwd pr2_gen_abbr pr2/fwd pr2_gen_void -pr2/fwd pr2_gen_lift -pr2/pr2 pr2_confluence__pr2_free_free -pr2/pr2 pr2_confluence__pr2_free_delta -pr2/pr2 pr2_confluence__pr2_delta_delta -pr2/pr2 pr2_confluence -pr2/props pr2_thin_dx -pr2/props pr2_head_1 -pr2/props pr2_head_2 -pr2/props clear_pr2_trans -pr2/props pr2_cflat pr2/props pr2_ctail -pr2/props pr2_change -pr2/props pr2_lift -pr2/subst1 pr2_delta1 -pr2/subst1 pr2_subst1 -pr2/subst1 pr2_gen_cabbr + + +# waiting #################################################################### + pr3/fwd pr3_gen_sort pr3/fwd pr3_gen_abst pr3/fwd pr3_gen_cast @@ -396,17 +376,7 @@ sty1/props sty1_abbr sty1/props sty1_cast2 subst0/dec dnf_dec2 subst0/dec dnf_dec -subst1/fwd subst1_gen_lift_ge -subst1/fwd subst1_gen_lift_lt -subst1/fwd subst1_gen_lift_eq -subst1/props subst1_lift_ge -subst1/props subst1_lift_lt subst1/props subst1_ex -subst1/props subst1_lift_S -subst1/subst1 subst1_subst1 -subst1/subst1 subst1_subst1_back -subst1/subst1 subst1_trans -subst1/subst1 subst1_confluence_lift subst/fwd subst_sort subst/fwd subst_lref_lt subst/fwd subst_lref_eq diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma index b594c5a12..43b2174d9 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma @@ -12,13 +12,15 @@ (* *) (**************************************************************************) -(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS +(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES * Specification started: 2011 April 17 + * Confluence of context-free parallel reduction closed: 2011 September 6 * - Patience on me so that I gain peace and perfection! - * [ suggested invocation to start formal specifications with ] *) include "Ground-2/list.ma". +include "Ground-2/star.ma". include "Basic-2/notation.ma". (* ITEMS ********************************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma index 7612bcb85..ac5503d28 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/leq.ma @@ -16,18 +16,31 @@ include "Basic-2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENT EQUALITY ***********************************************) -inductive leq: lenv → nat → nat → lenv → Prop ≝ -| leq_sort: ∀d,e. leq (⋆) d e (⋆) -| leq_OO: ∀L1,L2. leq L1 0 0 L2 -| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V) +inductive leq: nat → nat → relation lenv ≝ +| leq_sort: ∀d,e. leq d e (⋆) (⋆) +| leq_OO: ∀L1,L2. leq 0 0 L1 L2 +| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 → + leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V) | leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2) + leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) . -interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2). +interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). + +definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R. + ∀L1,s1,s2. R L1 s1 s2 → + ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2. (* Basic properties *********************************************************) +lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))). +#S #R #HR #L1 #s1 #s2 #H elim H -H s2 +[ /3 width=5/ +| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 + lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ +] +qed. + lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. #d elim d -d [ #e elim e -e // #e #IHe #L elim L -L /2/ diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma index 876bd7fd9..23aa62e03 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/thom.ma @@ -16,7 +16,7 @@ include "Basic-2/grammar/term_simple.ma". (* HOMOMORPHIC TERMS ********************************************************) -inductive thom: term → term → Prop ≝ +inductive thom: relation term ≝ | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I}) | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2) | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] → diff --git a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma index 287ce0564..a84fa8ff8 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/notation.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/notation.ma @@ -72,11 +72,11 @@ notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )" non associative with precedence 45 - for @{ 'RLift $T1 $d $e $T2 }. + for @{ 'RLift $d $e $T1 $T2 }. notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )" non associative with precedence 45 - for @{ 'RDrop $L1 $d $e $L2 }. + for @{ 'RDrop $d $e $L1 $L2 }. notation "hvbox( T1 break [ d , break e ] ≫ break T2 )" non associative with precedence 45 @@ -86,6 +86,16 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫ break T2 )" non associative with precedence 45 for @{ 'PSubst $L $T1 $d $e $T2 }. +(* Unfold *******************************************************************) + +notation "hvbox( T1 break [ d , break e ] ≫* break T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $T1 $d $e $T2 }. + +notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≫* break T2 )" + non associative with precedence 45 + for @{ 'PSubstStar $L $T1 $d $e $T2 }. + (* Reduction ****************************************************************) notation "hvbox( T1 ⇒ break T2 )" @@ -99,3 +109,17 @@ notation "hvbox( L ⊢ break term 90 T1 ⇒ break T2 )" notation "hvbox( L1 ⊢ ⇒ break L2 )" non associative with precedence 45 for @{ 'CPRed $L1 $L2 }. + +(* Computation **************************************************************) + +notation "hvbox( T1 ⇒* break T2 )" + non associative with precedence 45 + for @{ 'PRedStar $T1 $T2 }. + +notation "hvbox( L ⊢ break term 90 T1 ⇒* break T2 )" + non associative with precedence 45 + for @{ 'PRedStar $L $T1 $T2 }. + +notation "hvbox( L1 ⊢ ⇒* break L2 )" + non associative with precedence 45 + for @{ 'CPRedStar $L1 $L2 }. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma index e8a586d3d..f4b175925 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -17,7 +17,8 @@ include "Basic-2/reduction/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) -definition cpr: lenv → term → term → Prop ≝ +(* Basic-1: includes: pr2_delta1 *) +definition cpr: lenv → relation term ≝ λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2. interpretation @@ -26,6 +27,7 @@ interpretation (* Basic properties *********************************************************) +(* Basic-1: was by definition: pr2_free *) lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. /2/ qed. @@ -40,6 +42,7 @@ lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → #I #L #V1 #V2 #T1 #T2 * /3 width=5/ qed. +(* Basic-1: was only: pr2_gen_cbind *) lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 @@ -48,7 +51,8 @@ lapply (tps_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0 /3 width=5/ qed. -(* NOTE: new property *) +(* Note: new property *) +(* Basic-1: was only: pr2_thin_dx *) lemma cpr_flat: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2. #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/ @@ -66,11 +70,40 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma cpr_inv_lsort: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. +(* Basic-1: was: pr2_gen_csort *) +lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. #T1 #T2 * #T #HT normalize #HT2 <(tps_inv_refl_O2 … HT2) -HT2 // qed. +(* Basic-1: was: pr2_gen_sort *) +lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k. +#L #T2 #k * #X #H +>(tpr_inv_atom1 … H) -H #H +>(tps_inv_sort1 … H) -H // +qed. + +(* Basic-1: was: pr2_gen_lref *) +lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 → + T2 = #i ∨ + ∃∃K,T. ↓[0, i] L ≡ K. 𝕓{Abbr} T & ↑[0, i + 1] T ≡ T2 & + i < |L|. +#L #T2 #i * #X #H +>(tpr_inv_atom1 … H) -H #H +elim (tps_inv_lref1 … H) -H /2/ +* #K #T #_ #Hi #HLK #HTT2 /3/ +qed. +(* +(* Basic-1: was: pr2_gen_cast *) +lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → ( + ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 & + U2 = 𝕔{Cast} V2. T2 + ) ∨ L ⊢ T1 ⇒ U2. +#L #V1 #T1 #U2 * #X #H #HU2 +elim (tpr_inv_cast1 … H) -H /3/ +* #V #T #HV1 #HT1 #H whd (* >H in HU2; *) destruct -X; +elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H +*) (* Basic forward lemmas *****************************************************) lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2. @@ -79,3 +112,19 @@ lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2. | normalize /3/ ]. qed. + +(* Basic-1: removed theorems 5: + pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans +*) + +(* +pr2/fwd pr2_gen_appl +pr2/fwd pr2_gen_abbr +pr2/pr2 pr2_confluence__pr2_free_free +pr2/pr2 pr2_confluence__pr2_free_delta +pr2/pr2 pr2_confluence__pr2_delta_delta +pr2/pr2 pr2_confluence +pr2/props pr2_change +pr2/subst1 pr2_subst1 +pr2/subst1 pr2_gen_cabbr +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma new file mode 100644 index 000000000..d544918ac --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpr_tpr.ma". +include "Basic-2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Main properties **********************************************************) +(* +(* Basic-1: was: pr2_confluence *) +theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 → + ∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T. +#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2 +elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2 +qed. +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma new file mode 100644 index 000000000..89f84afaa --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/tpr_lift.ma". +include "Basic-2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) + +(* Relocation properties ****************************************************) + +(* Basic-1: was: pr2_lift *) + +(* Basic-1: was: pr2_gen_lift *) + +(* Advanced inversion lemmas ************************************************) + +(* Basic-1: was: pr2_gen_abst *) +lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → + ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. +/2/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma index 03ed43683..f01daabce 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/lcpr.ma @@ -16,7 +16,7 @@ include "Basic-2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************) -inductive lcpr: lenv → lenv → Prop ≝ +inductive lcpr: relation lenv ≝ | lcpr_sort: lcpr (⋆) (⋆) | lcpr_item: ∀K1,K2,I,V1,V2. lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma index 97ef4901a..a9093a042 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr.ma @@ -16,7 +16,7 @@ include "Basic-2/reduction/tpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************) -inductive ltpr: lenv → lenv → Prop ≝ +inductive ltpr: relation lenv ≝ | ltpr_sort: ltpr (⋆) (⋆) | ltpr_item: ∀K1,K2,I,V1,V2. ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma index 99c0ae0d4..3c70e6a0b 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/ltpr_drop.ma @@ -22,8 +22,7 @@ lemma ltpr_drop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 → ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ -| #L1 #K1 #I #V1 #HLK1 #_ #X #H - <(drop_inv_refl … HLK1) -HLK1 K1; +| #K1 #I #V1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/ | #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X; @@ -40,8 +39,7 @@ lemma ltpr_drop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2. #L1 #K1 #d #e #H elim H -H L1 K1 d e [ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/ -| #L1 #K1 #I #V1 #HLK1 #_ #X #H - >(drop_inv_refl … HLK1) -HLK1 L1; +| #K1 #I #V1 #X #H elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/ | #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/ diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma index 6f90fd907..756527958 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -17,7 +17,7 @@ include "Basic-2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) (* Basic-1: includes: pr0_delta1 *) -inductive tpr: term → term → Prop ≝ +inductive tpr: relation term ≝ | tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I}) | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma index f06d8980a..311a1433a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma @@ -15,6 +15,8 @@ include "Basic-2/substitution/tps_lift.ma". include "Basic-2/reduction/tpr.ma". +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + (* Relocation properties ****************************************************) (* Basic-1: was: pr0_lift *) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma index b7d8801b2..4d31115b2 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma @@ -18,27 +18,26 @@ include "Basic-2/substitution/lift.ma". (* DROPPING *****************************************************************) (* Basic-1: includes: drop_skip_bind *) -inductive drop: lenv → nat → nat → lenv → Prop ≝ -| drop_sort: ∀d,e. drop (⋆) d e (⋆) -| drop_comp: ∀L1,L2,I,V. drop L1 0 0 L2 → drop (L1. 𝕓{I} V) 0 0 (L2. 𝕓{I} V) -| drop_drop: ∀L1,L2,I,V,e. drop L1 0 e L2 → drop (L1. 𝕓{I} V) 0 (e + 1) L2 +inductive drop: nat → nat → relation lenv ≝ +| drop_atom: ∀d,e. drop d e (⋆) (⋆) +| drop_pair: ∀L,I,V. drop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) +| drop_drop: ∀L1,L2,I,V,e. drop 0 e L1 L2 → drop 0 (e + 1) (L1. 𝕓{I} V) L2 | drop_skip: ∀L1,L2,I,V1,V2,d,e. - drop L1 d e L2 → ↑[d,e] V2 ≡ V1 → - drop (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) + drop d e L1 L2 → ↑[d,e] V2 ≡ V1 → + drop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) . -interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2). +interpretation "dropping" 'RDrop d e L1 L2 = (drop d e L1 L2). (* Basic inversion lemmas ***************************************************) fact drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2. -#d #e #L1 #L2 #H elim H -H d e L1 L2 +#d #e #L1 #L2 * -d e L1 L2 [ // -| #L1 #L2 #I #V #_ #IHL12 #H1 #H2 - >(IHL12 H1 H2) -IHL12 H1 H2 L1 // -| #L1 #L2 #I #V #e #_ #_ #_ #H +| // +| #L1 #L2 #I #V #e #_ #_ #H elim (plus_S_eq_O_false … H) -| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] qed. @@ -47,18 +46,18 @@ qed. lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2. /2 width=5/ qed. -fact drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → +fact drop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ → L2 = ⋆. #d #e #L1 #L2 * -d e L1 L2 [ // -| #L1 #L2 #I #V #_ #H destruct +| #L #I #V #H destruct | #L1 #L2 #I #V #e #_ #H destruct | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct ] qed. (* Basic-1: was: drop_gen_sort *) -lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. +lemma drop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed. fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → @@ -67,8 +66,7 @@ fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → (0 < e ∧ ↓[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #K #I #V #H destruct -| #L1 #L2 #I #V #HL12 #H #K #J #W #HX destruct -L1 I V - >(drop_inv_refl … HL12) -HL12 K /3/ +| #L #I #V #_ #K #J #W #HX destruct -L I V /3/ | #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/ | #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) ] @@ -94,7 +92,7 @@ fact drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → L2 = K2. 𝕓{I} V2. #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #I #K #V #H destruct -| #L1 #L2 #I #V #_ #H elim (lt_refl_false … H) +| #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) | #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z /2 width=5/ @@ -115,7 +113,7 @@ fact drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d → L1 = K1. 𝕓{I} V1. #d #e #L1 #L2 * -d e L1 L2 [ #d #e #_ #I #K #V #H destruct -| #L1 #L2 #I #V #_ #H elim (lt_refl_false … H) +| #L #I #V #H elim (lt_refl_false … H) | #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H) | #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z /2 width=5/ @@ -132,7 +130,7 @@ lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < (* Basic-1: was by definition: drop_refl *) lemma drop_refl: ∀L. ↓[0, 0] L ≡ L. -#L elim L -L /2/ +#L elim L -L // qed. lemma drop_drop_lt: ∀L1,L2,I,V,e. @@ -147,7 +145,7 @@ lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → ↓[0, i] L2 ≡ K2. 𝕓{I} V. #L1 #L2 #d #e #H elim H -H L1 L2 d e [ #d #e #I #K1 #V #i #H - lapply (drop_inv_sort1 … H) -H #H destruct + lapply (drop_inv_atom1 … H) -H #H destruct | #L1 #L2 #I #K1 #V #i #_ #_ #H elim (lt_zero_false … H) | #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie @@ -170,7 +168,7 @@ qed. lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ↓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H lapply (drop_inv_sort1 … H) -H #H destruct +[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (drop_inv_O1 … H) -H * #He #H [ -IHL1; destruct -e K2 I2 V2 /2/ @@ -182,7 +180,7 @@ qed. lemma drop_fwd_drop2_length: ∀L1,I2,K2,V2,e. ↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|. #L1 elim L1 -L1 -[ #I2 #K2 #V2 #e #H lapply (drop_inv_sort1 … H) -H #H destruct +[ #I2 #K2 #V2 #e #H lapply (drop_inv_atom1 … H) -H #H destruct | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H elim (drop_inv_O1 … H) -H * #He #H [ -IHL1; destruct -e K2 I2 V2 // @@ -193,7 +191,7 @@ qed. lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. #L1 elim L1 -L1 -[ #L2 #e #H >(drop_inv_sort1 … H) -H // +[ #L2 #e #H >(drop_inv_atom1 … H) -H // | #K1 #I1 #V1 #IHL1 #L2 #e #H elim (drop_inv_O1 … H) -H * #He #H [ -IHL1; destruct -e L2 // diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma index 297b21f11..934374853 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop_drop.ma @@ -24,9 +24,8 @@ theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → ∀L2. ↓[d, e] L ≡ L2 → L1 = L2. #d #e #L #L1 #H elim H -H d e L L1 [ #d #e #L2 #H - >(drop_inv_sort1 … H) -H L2 // -| #K1 #K2 #I #V #HK12 #_ #L2 #HL12 - <(drop_inv_refl … HK12) -HK12 K2 + >(drop_inv_atom1 … H) -H L2 // +| #K #I #V #L2 #HL12 <(drop_inv_refl … HL12) -HL12 L2 // | #L #K #I #V #e #_ #IHLK #L2 #H lapply (drop_inv_drop1 … H ?) -H /2/ @@ -43,9 +42,8 @@ theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ↓[0, e2 - e1] L1 ≡ L2. #d1 #e1 #L #L1 #H elim H -H d1 e1 L L1 [ #d #e #e2 #L2 #H - >(drop_inv_sort1 … H) -H L2 // -| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ (drop_inv_atom1 … H) -H L2 // +| // | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 lapply (drop_inv_drop1 … H ?) -H /2/ #HL2 (drop_inv_sort1 … H) -H L2 /2/ -| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #HL2 #H - >(drop_inv_refl … HK12) -HK12 K1; + >(drop_inv_atom1 … H) -H L2 /2/ +| #K #I #V #e2 #L2 #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H lapply (le_O_to_eq_O … H) -H #H destruct -e2; @@ -108,9 +105,8 @@ theorem drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2. #d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L [ #d #e #e2 #L2 #H - >(drop_inv_sort1 … H) -H L2 // -| #K1 #K2 #I #V #HK12 #_ #e2 #L2 #H #_ normalize - >(drop_inv_refl … HK12) -HK12 K1 // + >(drop_inv_atom1 … H) -H L2 // +| // | /3/ | #L1 #L2 #I #V1 #V2 #d #e #H_ #_ #IHL12 #e2 #L #H #Hde2 lapply (lt_to_le_to_lt 0 … Hde2) // #He2 diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma index 48e37d630..cccd3b03c 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/lift.ma @@ -19,19 +19,19 @@ include "Basic-2/grammar/term_weight.ma". (* Basic-1: includes: lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat *) -inductive lift: term → nat → nat → term → Prop ≝ -| lift_sort : ∀k,d,e. lift (⋆k) d e (⋆k) -| lift_lref_lt: ∀i,d,e. i < d → lift (#i) d e (#i) -| lift_lref_ge: ∀i,d,e. d ≤ i → lift (#i) d e (#(i + e)) +inductive lift: nat → nat → relation term ≝ +| lift_sort : ∀k,d,e. lift d e (⋆k) (⋆k) +| lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i) +| lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e)) | lift_bind : ∀I,V1,V2,T1,T2,d,e. - lift V1 d e V2 → lift T1 (d + 1) e T2 → - lift (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) + lift d e V1 V2 → lift (d + 1) e T1 T2 → + lift d e (𝕓{I} V1. T1) (𝕓{I} V2. T2) | lift_flat : ∀I,V1,V2,T1,T2,d,e. - lift V1 d e V2 → lift T1 d e T2 → - lift (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) + lift d e V1 V2 → lift d e T1 T2 → + lift d e (𝕗{I} V1. T1) (𝕗{I} V2. T2) . -interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2). +interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma index fc94df3ec..889704b44 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps.ma @@ -17,19 +17,19 @@ include "Basic-2/substitution/tps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) (* Basic-1: includes: csubst1_bind *) -inductive ltps: lenv → nat → nat → lenv → Prop ≝ -| ltps_atom: ∀d,e. ltps (⋆) d e (⋆) -| ltps_pair: ∀L,I,V. ltps (L. 𝕓{I} V) 0 0 (L. 𝕓{I} V) +inductive ltps: nat → nat → relation lenv ≝ +| ltps_atom: ∀d,e. ltps d e (⋆) (⋆) +| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V) | ltps_tps2: ∀L1,L2,I,V1,V2,e. - ltps L1 0 e L2 → L2 ⊢ V1 [0, e] ≫ V2 → - ltps (L1. 𝕓{I} V1) 0 (e + 1) L2. 𝕓{I} V2 + ltps 0 e L1 L2 → L2 ⊢ V1 [0, e] ≫ V2 → + ltps 0 (e + 1) (L1. 𝕓{I} V1) L2. 𝕓{I} V2 | ltps_tps1: ∀L1,L2,I,V1,V2,d,e. - ltps L1 d e L2 → L2 ⊢ V1 [d, e] ≫ V2 → - ltps (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2) + ltps d e L1 L2 → L2 ⊢ V1 [d, e] ≫ V2 → + ltps (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2) . interpretation "parallel substritution (local environment)" - 'PSubst L1 d e L2 = (ltps L1 d e L2). + 'PSubst L1 d e L2 = (ltps d e L1 L2). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma index 1f917b852..dec15efaa 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma @@ -20,7 +20,7 @@ lemma ltps_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H // +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H // | // | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 @@ -37,7 +37,7 @@ lemma ltps_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H // +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H // | // | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 lapply (plus_le_weak … He12) #He2 @@ -54,7 +54,7 @@ lemma ltps_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ @@ -76,7 +76,7 @@ lemma ltps_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 → ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/ | normalize #L #I #V #L2 #e2 #HL2 #_ #He2 lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2; lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/ @@ -98,7 +98,7 @@ lemma ltps_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L. #L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/ | /2/ | normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; @@ -116,7 +116,7 @@ lemma ltps_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 → ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L. #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1 -[ #d1 #e1 #L2 #e2 #H >(drop_inv_sort1 … H) -H /2/ +[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/ | /2/ | normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2 lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2; diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma index b6f14aa69..810295f95 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_tps.ma @@ -31,6 +31,7 @@ lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ] qed. +(* Basic-1: was: subst1_subst1_back *) lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ∀L1,d1,e1. L0 [d1, e1] ≫ L1 → ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T & @@ -77,6 +78,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ] qed. +(* Basic-1: was: subst1_subst1 *) lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T & diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma index d197da9e8..29b99ae41 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma @@ -16,20 +16,20 @@ include "Basic-2/substitution/drop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) -inductive tps: lenv → term → nat → nat → term → Prop ≝ -| tps_atom : ∀L,I,d,e. tps L (𝕒{I}) d e (𝕒{I}) +inductive tps: nat → nat → lenv → relation term ≝ +| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I}) | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e → - ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps L (#i) d e W + ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → tps d e L (#i) W | tps_bind : ∀L,I,V1,V2,T1,T2,d,e. - tps L V1 d e V2 → tps (L. 𝕓{I} V2) T1 (d + 1) e T2 → - tps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) + tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 → + tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2) | tps_flat : ∀L,I,V1,V2,T1,T2,d,e. - tps L V1 d e V2 → tps L T1 d e T2 → - tps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) + tps d e L V1 V2 → tps d e L T1 T2 → + tps d e L (𝕗{I} V1. T1) (𝕗{I} V2. T2) . interpretation "parallel substritution (term)" - 'PSubst L T1 d e T2 = (tps L T1 d e T2). + 'PSubst L T1 d e T2 = (tps d e L T1 T2). (* Basic properties *********************************************************) @@ -198,12 +198,12 @@ qed. lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2. /2 width=6/ qed. -(* Basic-1: removed theorems 23: +(* Basic-1: removed theorems 25: subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt subst0_confluence_neq subst0_confluence_eq subst0_tlt_head subst0_confluence_lift subst0_tlt - subst1_head subst1_gen_head + subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift *) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma index 80ed80f1c..58ebb3dd3 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma @@ -19,6 +19,7 @@ include "Basic-2/substitution/tps.ma". (* Relocation properties ****************************************************) +(* Basic-1: was: subst1_lift_lt *) lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → @@ -45,6 +46,7 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ] qed. +(* Basic-1: was: subst1_lift_ge *) lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ∀L,U1,U2,d,e. ↓[d, e] L ≡ K → ↑[d, e] T1 ≡ U1 → ↑[d, e] T2 ≡ U2 → @@ -69,6 +71,7 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ] qed. +(* Basic-1: was: subst1_gen_lift_lt *) lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → dt + et ≤ d → @@ -95,6 +98,7 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] qed. +(* Basic-1: was: subst1_gen_lift_ge *) lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 → d + e ≤ dt → @@ -129,6 +133,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] qed. +(* Basic-1: was: subst1_gen_lift_eq *) lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. L ⊢ U1 [d, e] ≫ U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2. #L #U1 #U2 #d #e #H elim H -H L U1 U2 d e @@ -149,10 +154,6 @@ lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. ] qed. (* - Theorem subst0_gen_lift_ge : (u,t1,x:?; i,h,d:?) (subst0 i u (lift h d t1) x) -> - (le (plus d h) i) -> - (EX t2 | x = (lift h d t2) & (subst0 (minus i h) u t1 t2)). - Theorem subst0_gen_lift_rev_ge: (t1,v,u2:?; i,h,d:?) (subst0 i v t1 (lift h d u2)) -> (le (plus d h) i) -> diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma index 10102eca5..fda5cbabd 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma @@ -84,6 +84,7 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → qed. (* Note: the constant 1 comes from tps_subst *) +(* Basic-1: was: subst1_trans *) theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 → ∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e → L ⊢ T1 [d, e] ≫ T2. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma new file mode 100644 index 000000000..26b97dcb4 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/tps.ma". + +(* PARTIAL UNFOLD ON TERMS **************************************************) + +definition tpss: nat → nat → lenv → relation term ≝ + λd,e,L. TC … (tps d e L). + +interpretation "partial unfold (term)" + 'PSubstStar L T1 d e T2 = (tpss d e L T1 T2). + +(* Basic properties *********************************************************) + diff --git a/matita/matita/contribs/lambda-delta/Ground-2/star.ma b/matita/matita/contribs/lambda-delta/Ground-2/star.ma new file mode 100644 index 000000000..d15768c53 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Ground-2/star.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 "basics/star.ma". +include "Ground-2/xoa_props.ma". + +(* PROPERTIES of RELATIONS **************************************************) + +definition confluent: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 → + ∃∃a. R a1 a & R a2 a. + +lemma TC_strip: ∀A,R. confluent A R → + ∀a0,a1. TC … R a0 a1 → ∀a2. R a0 a2 → + ∃∃a. R a1 a & TC … R a2 a. +#A #R #HR #a0 #a1 #H elim H -H a1 +[ #a1 #Ha01 #a2 #Ha02 + elim (HR … Ha01 … Ha02) -HR a0 /3/ +| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 + elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20 + elim (HR … Ha1 … Ha0) -HR a /4/ +] +qed. + +lemma TC_confluent: ∀A,R. confluent A R → confluent A (TC … R). +#A #R #HR #a0 #a1 #H elim H -H a1 +[ #a1 #Ha01 #a2 #Ha02 + elim (TC_strip … HR … Ha02 … Ha01) -HR a0 /3/ +| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 + elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20 + elim (TC_strip … HR … Ha0 … Ha1) -HR a /4/ +] +qed. + +lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R). +/2/ qed. +