From 78f21d7d9014e5c7655f58239e4f1a128ea2c558 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Oct 2011 12:37:58 +0000 Subject: [PATCH] refactoring completed! --- .../lambda_delta/Basic_2/grammar/cl_shift.ma | 2 +- .../lambda_delta/Basic_2/grammar/cl_weight.ma | 12 ++--- .../lambda_delta/Basic_2/grammar/item.ma | 8 +-- .../lambda_delta/Basic_2/grammar/lenv.ma | 2 +- .../Basic_2/grammar/lenv_length.ma | 2 +- .../Basic_2/grammar/lenv_weight.ma | 6 +-- .../Basic_2/grammar/{leq.ma => lsubs.ma} | 45 +++++++++-------- .../lambda_delta/Basic_2/grammar/sh.ma | 2 +- .../lambda_delta/Basic_2/grammar/term.ma | 2 +- .../Basic_2/grammar/term_simple.ma | 2 +- .../Basic_2/grammar/term_weight.ma | 4 +- .../lambda_delta/Basic_2/grammar/thom.ma | 4 +- .../contribs/lambda_delta/Basic_2/notation.ma | 4 +- .../lambda_delta/Basic_2/reduction/cpr.ma | 22 ++++----- .../lambda_delta/Basic_2/reduction/cpr_cpr.ma | 10 ++-- .../Basic_2/reduction/cpr_lift.ma | 14 +++--- .../lambda_delta/Basic_2/reduction/lcpr.ma | 2 +- .../lambda_delta/Basic_2/reduction/ltpr.ma | 8 +-- .../Basic_2/reduction/ltpr_drop.ma | 8 +-- .../lambda_delta/Basic_2/reduction/tpr.ma | 18 +++---- .../Basic_2/reduction/tpr_lift.ma | 10 ++-- .../lambda_delta/Basic_2/reduction/tpr_tpr.ma | 10 ++-- .../reduction/{tpr_tps.ma => tpr_tpss.ma} | 14 +++--- .../lambda_delta/Basic_2/substitution/drop.ma | 49 ++++++++++--------- .../Basic_2/substitution/drop_drop.ma | 16 +++--- .../lambda_delta/Basic_2/substitution/lift.ma | 26 +++++----- .../Basic_2/substitution/lift_lift.ma | 12 ++--- .../lambda_delta/Basic_2/substitution/ltps.ma | 8 +-- .../Basic_2/substitution/ltps_drop.ma | 2 +- .../Basic_2/substitution/ltps_tps.ma | 8 +-- .../lambda_delta/Basic_2/substitution/tps.ma | 18 +++---- .../Basic_2/substitution/tps_lift.ma | 14 +++--- .../Basic_2/substitution/tps_tps.ma | 28 +++++------ .../lambda_delta/Basic_2/unfold/ltpss.ma | 4 +- .../lambda_delta/Basic_2/unfold/ltpss_drop.ma | 2 +- .../Basic_2/unfold/ltpss_ltpss.ma | 2 +- .../lambda_delta/Basic_2/unfold/ltpss_tpss.ma | 4 +- .../lambda_delta/Basic_2/unfold/tpss.ma | 10 ++-- .../lambda_delta/Basic_2/unfold/tpss_lift.ma | 4 +- .../lambda_delta/Basic_2/unfold/tpss_ltps.ma | 16 +++--- .../lambda_delta/Basic_2/unfold/tpss_tpss.ma | 4 +- .../contribs/lambda_delta/Ground_2/arith.ma | 2 +- .../contribs/lambda_delta/Ground_2/list.ma | 4 +- .../contribs/lambda_delta/Ground_2/star.ma | 2 +- .../lambda_delta/Ground_2/xoa.conf.xml | 2 +- .../lambda_delta/Ground_2/xoa_props.ma | 4 +- .../matita/contribs/lambda_delta/replace.sh | 10 ++-- 47 files changed, 235 insertions(+), 227 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/grammar/{leq.ma => lsubs.ma} (53%) rename matita/matita/contribs/lambda_delta/Basic_2/reduction/{tpr_tps.ma => tpr_tpss.ma} (92%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma index d72b6c4cb..c2fd85899 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/lenv.ma". +include "Basic_2/grammar/lenv.ma". (* SHIFT OF A CLOSURE *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma index 35bf32a9d..355b8a797 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/lenv_weight.ma". -include "Basic-2/grammar/cl_shift.ma". +include "Basic_2/grammar/lenv_weight.ma". +include "Basic_2/grammar/cl_shift.ma". (* WEIGHT OF A CLOSURE ******************************************************) @@ -23,14 +23,14 @@ interpretation "weight (closure)" 'Weight L T = (cw L T). (* Basic properties *********************************************************) -(* Basic-1: was: flt_wf__q_ind *) +(* Basic_1: was: flt_wf__q_ind *) -(* Basic-1: was: flt_wf_ind *) +(* Basic_1: was: flt_wf_ind *) axiom cw_wf_ind: ∀R:lenv→term→Prop. (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) → ∀L,T. R L T. -(* Basic-1: was: flt_shift *) +(* Basic_1: was: flt_shift *) lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T]. normalize // qed. @@ -41,6 +41,6 @@ lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. @transitive_le [3: @IHL |2: /2/ | skip ] qed. -(* Basic-1: removed theorems 6: +(* Basic_1: removed theorems 6: flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans *) 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 ead47b546..4ee4731b1 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -20,9 +20,9 @@ * [ suggested invocation to start formal specifications with ] *) -include "Ground-2/list.ma". -include "Ground-2/star.ma". -include "Basic-2/notation.ma". +include "Ground_2/list.ma". +include "Ground_2/star.ma". +include "Basic_2/notation.ma". (* ITEMS ********************************************************************) @@ -54,7 +54,7 @@ coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. -(* Basic-1: removed theorems 19: +(* Basic_1: removed theorems 19: s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc s_arith0 s_arith1 r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma index dfec09808..15ca1ed17 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term.ma". +include "Basic_2/grammar/term.ma". (* LOCAL ENVIRONMENTS *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma index 23e445907..357301333 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/lenv.ma". +include "Basic_2/grammar/lenv.ma". (* LENGTH OF A LOCAL ENVIRONMENT ********************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma index 9f45673ba..414d3f1ab 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term_weight.ma". -include "Basic-2/grammar/lenv.ma". +include "Basic_2/grammar/term_weight.ma". +include "Basic_2/grammar/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) @@ -24,4 +24,4 @@ let rec lw L ≝ match L with interpretation "weight (local environment)" 'Weight L = (lw L). -(* Basic-1: removed theorems 2: clt_cong clt_head *) +(* Basic_1: removed theorems 2: clt_cong clt_head *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/leq.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma similarity index 53% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/leq.ma rename to matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index ac5503d28..93afc607a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/leq.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -12,28 +12,30 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/lenv_length.ma". +include "Basic_2/grammar/lenv_length.ma". -(* LOCAL ENVIRONMENT EQUALITY ***********************************************) +(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************) -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 d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) +inductive lsubs: nat → nat → relation lenv ≝ +| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆) +| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2 +| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 → + lsubs 0 (e + 1) (L1. 𝕓{Abbr} V) (L2.𝕓{Abbr} V) +| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 → + lsubs 0 (e + 1) (L1. 𝕓{Abst} V1) (L2.𝕓{I} V2) +| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) . -interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). +interpretation "local environment refinement (substitution)" 'SubEq L1 d e L2 = (lsubs 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. +definition lsubs_conf: ∀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))). +lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf 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 @@ -41,19 +43,20 @@ lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R ] qed. -lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. +lemma lsubs_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V. + L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V. +#L1 #L2 #e #HL12 #I #V elim I -I /2/ +qed. + +lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L. #d elim d -d [ #e elim e -e // #e #IHe #L elim L -L /2/ | #d #IHd #e #L elim L -L /2/ ] qed. -lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. -#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ -qed. - -lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → - ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. +lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d → + ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2. #L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma index bec437a75..1708b7970 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Ground-2/list.ma". +include "Ground_2/list.ma". (* SORT HIERARCHY ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index 3b6614361..46ba2cef2 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/item.ma". +include "Basic_2/grammar/item.ma". (* TERMS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma index c182ba360..be508e49c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term.ma". +include "Basic_2/grammar/term.ma". (* SIMPLE (NEUTRAL) TERMS ***************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma index d383ded4d..24150f0bc 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term.ma". +include "Basic_2/grammar/term.ma". (* WEIGHT OF A TERM *********************************************************) @@ -35,7 +35,7 @@ axiom tw_wf_ind: ∀R:term→Prop. (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) → ∀T. R T. -(* Basic-1: removed theorems 11: +(* Basic_1: removed theorems 11: wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind removed local theorems 1: q_ind 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 23aa62e03..32bae83d3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term_simple.ma". +include "Basic_2/grammar/term_simple.ma". (* HOMOMORPHIC TERMS ********************************************************) @@ -50,7 +50,7 @@ lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. (* Basic inversion lemmas ***************************************************) -(* Basic-1: removed theorems 7: +(* Basic_1: removed theorems 7: iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans iso_flats_lref_bind_false iso_flats_flat_bind_false *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index a84fa8ff8..aa5cba8b9 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -64,9 +64,9 @@ notation "hvbox( 𝕊 [ T ] )" non associative with precedence 45 for @{ 'Simple $T }. -notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" +notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" non associative with precedence 45 - for @{ 'Eq $T1 $d $e $T2 }. + for @{ 'SubEq $T1 $d $e $T2 }. (* Substitution *************************************************************) 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 9187765da..03a500cf4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/cl_shift.ma". -include "Basic-2/unfold/tpss.ma". -include "Basic-2/reduction/tpr.ma". +include "Basic_2/grammar/cl_shift.ma". +include "Basic_2/unfold/tpss.ma". +include "Basic_2/reduction/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) -(* Basic-1: includes: pr2_delta1 *) +(* Basic_1: includes: pr2_delta1 *) definition cpr: lenv → relation term ≝ λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2. @@ -28,7 +28,7 @@ interpretation (* Basic properties *********************************************************) -(* Basic-1: was by definition: pr2_free *) +(* Basic_1: was by definition: pr2_free *) lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. /2/ qed. @@ -39,7 +39,7 @@ lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T. /2/ qed. (* Note: new property *) -(* Basic-1: was only: pr2_thin_dx *) +(* 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/ @@ -52,20 +52,20 @@ qed. (* Basic inversion lemmas ***************************************************) -(* Basic-1: was: pr2_gen_csort *) +(* Basic_1: was: pr2_gen_csort *) lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2. #T1 #T2 * #T #HT normalize #HT2 <(tpss_inv_refl_O2 … HT2) -HT2 // qed. -(* Basic-1: was: pr2_gen_sort *) +(* 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 >(tpss_inv_sort1 … H) -H // qed. -(* Basic-1: was: pr2_gen_cast *) +(* 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 @@ -76,9 +76,9 @@ elim (tpr_inv_cast1 … H) -H /3/ elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/ qed. -(* Basic-1: removed theorems 5: +(* Basic_1: removed theorems 5: pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans - Basic-1: removed local theorems 3: + Basic_1: removed local theorems 3: pr2_free_free pr2_free_delta pr2_delta_delta *) 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 index 086209007..ff802bfb3 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reduction/cpr_cpr.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/reduction/tpr_tpr.ma". -include "Basic-2/reduction/cpr.ma". +include "Basic_2/reduction/tpr_tpr.ma". +include "Basic_2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) @@ -25,12 +25,12 @@ lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → @ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *) qed. -(* Basic-1: was only: pr2_gen_cbind *) +(* 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 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (plus_minus_m_m e 1) /2/ qed. -lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → - ∀I,K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{I} V → - d ≤ i → i < d + e → - ∃∃K2. K1 [0, d + e - i - 1] ≈ K2 & - ↓[0, i] L2 ≡ K2. 𝕓{I} V. +lemma drop_lsubs_drop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → + ∀K1,V,i. ↓[0, i] L1 ≡ K1. 𝕓{Abbr} V → + d ≤ i → i < d + e → + ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 & + ↓[0, i] L2 ≡ K2. 𝕓{Abbr} V. #L1 #L2 #d #e #H elim H -H L1 L2 d e -[ #d #e #I #K1 #V #i #H +[ #d #e #K1 #V #i #H lapply (drop_inv_atom1 … H) -H #H destruct -| #L1 #L2 #I #K1 #V #i #_ #_ #H +| #L1 #L2 #K1 #V #i #_ #_ #H elim (lt_zero_false … H) -| #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie +| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie elim (drop_inv_O1 … H) -H * #Hi #HLK1 - [ -IHL12 Hie; destruct -i K1 J W; + [ -IHL12 Hie; destruct -i K1 W; arith_g1 // /3/ ] -| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #I #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide +| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie + elim (drop_inv_O1 … H) -H * #Hi #HLK1 + [ -IHL12 Hie Hi; destruct + | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/ + ] +| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide lapply (plus_S_le_to_pos … Hdi) #Hi lapply (drop_inv_drop1 … H ?) -H // #HLK1 elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/ @@ -165,7 +170,7 @@ qed. (* Basic forvard lemmas *****************************************************) -(* Basic-1: was: drop_S *) +(* Basic_1: was: drop_S *) lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 → ↓[O, e + 1] L1 ≡ K2. #L1 elim L1 -L1 @@ -210,7 +215,7 @@ lemma drop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e. ] qed. -(* Basic-1: removed theorems 49: +(* Basic_1: removed theorems 49: drop_skip_flat cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf drop_clear drop_clear_O drop_clear_S 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 934374853..b8a790fb5 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 @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/lift_lift.ma". -include "Basic-2/substitution/drop.ma". +include "Basic_2/substitution/lift_lift.ma". +include "Basic_2/substitution/drop.ma". (* DROPPING *****************************************************************) (* Main properties **********************************************************) -(* Basic-1: was: drop_mono *) +(* Basic_1: was: drop_mono *) 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 @@ -36,7 +36,7 @@ theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 → ] qed. -(* Basic-1: was: drop_conf_ge *) +(* Basic_1: was: drop_conf_ge *) theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0, e2 - e1] L1 ≡ L2. @@ -55,7 +55,7 @@ theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ] qed. -(* Basic-1: was: drop_conf_lt *) +(* Basic_1: was: drop_conf_lt *) theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 → e2 < d1 → let d ≝ d1 - e2 - 1 in @@ -77,7 +77,7 @@ theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → ] qed. -(* Basic-1: was: drop_trans_le *) +(* Basic_1: was: drop_trans_le *) theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 → ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2. @@ -100,7 +100,7 @@ theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → ] qed. -(* Basic-1: was: drop_trans_ge *) +(* Basic_1: was: drop_trans_ge *) 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 @@ -122,6 +122,6 @@ theorem drop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L. #e1 #e1 #e2 >commutative_plus /2 width=5/ qed. -(* Basic-1: was: drop_conf_rev *) +(* Basic_1: was: drop_conf_rev *) axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L → ∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1. 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 cccd3b03c..5f16e9aaf 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/term_weight.ma". +include "Basic_2/grammar/term_weight.ma". (* RELOCATION ***************************************************************) -(* Basic-1: includes: +(* Basic_1: includes: lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat *) inductive lift: nat → nat → relation term ≝ @@ -35,12 +35,12 @@ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2). (* Basic properties *********************************************************) -(* Basic-1: was: lift_lref_gt *) +(* Basic_1: was: lift_lref_gt *) lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i. #d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/ qed. -(* Basic-1: was: lift_r *) +(* Basic_1: was: lift_r *) lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T. #T elim T -T [ * #i // #d elim (lt_or_ge i d) /2/ @@ -59,7 +59,7 @@ lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2. ] qed. -(* Basic-1: was: lift_free (right to left) *) +(* Basic_1: was: lift_free (right to left) *) lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 → ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2. @@ -176,7 +176,7 @@ fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k ] qed. -(* Basic-1: was: lift_gen_sort *) +(* Basic_1: was: lift_gen_sort *) lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k. /2 width=5/ qed. @@ -191,21 +191,21 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i → ] qed. -(* Basic-1: was: lift_gen_lref *) +(* Basic_1: was: lift_gen_lref *) lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)). /2/ qed. -(* Basic-1: was: lift_gen_lref_lt *) +(* Basic_1: was: lift_gen_lref_lt *) lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i. #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd elim (plus_lt_false … Hdd) qed. -(* Basic-1: was: lift_gen_lref_false *) +(* Basic_1: was: lift_gen_lref_false *) -(* Basic-1: was: lift_gen_lref_ge *) +(* Basic_1: was: lift_gen_lref_ge *) lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e). #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * // #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd @@ -225,7 +225,7 @@ fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. -(* Basic-1: was: lift_gen_bind *) +(* Basic_1: was: lift_gen_bind *) lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕓{I} V2. U2 → ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 & T1 = 𝕓{I} V1. U1. @@ -244,13 +244,13 @@ fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ] qed. -(* Basic-1: was: lift_gen_flat *) +(* Basic_1: was: lift_gen_flat *) lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ 𝕗{I} V2. U2 → ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 & T1 = 𝕗{I} V1. U1. /2/ qed. -(* Basic-1: removed theorems 7: +(* Basic_1: removed theorems 7: lift_head lift_gen_head lift_weight_map lift_weight lift_weight_add lift_weight_add_O lift_tlt_dx diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma index f9c99457d..3a5d85355 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/lift.ma". +include "Basic_2/substitution/lift.ma". (* RELOCATION ***************************************************************) (* Main properies ***********************************************************) -(* Basic-1: was: lift_inj *) +(* Basic_1: was: lift_inj *) theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U → T1 = T2. #d #e #T1 #U #H elim H -H d e T1 U [ #k #d #e #X #HX @@ -34,7 +34,7 @@ theorem lift_inj: ∀d,e,T1,U. ↑[d,e] T1 ≡ U → ∀T2. ↑[d,e] T2 ≡ U ] qed. -(* Basic-1: was: lift_gen_lift *) +(* Basic_1: was: lift_gen_lift *) theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T → d1 ≤ d2 → @@ -80,7 +80,7 @@ theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 ] qed. -(* Basic-1: was: lift_free (left to right) *) +(* Basic_1: was: lift_free (left to right) *) theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2. @@ -106,7 +106,7 @@ theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. -(* Basic-1: was: lift_d (right to left) *) +(* Basic_1: was: lift_d (right to left) *) theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d2 ≤ d1 → ∃∃T0. ↑[d2, e2] T1 ≡ T0 & ↑[d1 + e2, e1] T0 ≡ T2. @@ -131,7 +131,7 @@ theorem lift_trans_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ] qed. -(* Basic-1: was: lift_d (left to right) *) +(* Basic_1: was: lift_d (left to right) *) theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 → d1 + e1 ≤ d2 → ∃∃T0. ↑[d2 - e1, e2] T1 ≡ T0 & ↑[d1, e1] T0 ≡ T2. 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 3982ed2f9..c8c2a1aec 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps.ma". +include "Basic_2/substitution/tps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) -(* Basic-1: includes: csubst1_bind *) +(* Basic_1: includes: csubst1_bind *) 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) @@ -47,7 +47,7 @@ lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e. >(plus_minus_m_m d 1) /2/ qed. -(* Basic-1: was by definition: csubst1_refl *) +(* Basic_1: was by definition: csubst1_refl *) lemma ltps_refl: ∀L,d,e. L [d, e] ≫ L. #L elim L -L // #L #I #V #IHL * /2/ * /2/ @@ -169,7 +169,7 @@ lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d L1 = K1. 𝕓{I} V1. /2/ qed. -(* Basic-1: removed theorems 27: +(* Basic_1: removed theorems 27: csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back 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 dec15efaa..6c3288358 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 @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/ltps.ma". +include "Basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) 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 810295f95..3feca6201 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 @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_lift.ma". -include "Basic-2/substitution/ltps_drop.ma". +include "Basic_2/substitution/tps_lift.ma". +include "Basic_2/substitution/ltps_drop.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) @@ -31,7 +31,7 @@ lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ] qed. -(* Basic-1: was: subst1_subst1_back *) +(* 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 & @@ -78,7 +78,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → ] qed. -(* Basic-1: was: subst1_subst1 *) +(* 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 7197a53d9..f364dda8b 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/grammar/cl_weight.ma". -include "Basic-2/substitution/drop.ma". +include "Basic_2/grammar/cl_weight.ma". +include "Basic_2/substitution/drop.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) @@ -34,12 +34,12 @@ interpretation "parallel substritution (term)" (* Basic properties *********************************************************) -lemma tps_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → - ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫ T2. +lemma tps_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫ T2. #L1 #T1 #T2 #d #e #H elim H -H L1 T1 T2 d e [ // | #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12 - elim (drop_leq_drop1 … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ + elim (drop_lsubs_drop1_abbr … HL12 … HLK1 ? ?) -HL12 HLK1 // /2/ | /4/ | /3/ ] @@ -99,7 +99,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i → elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2 elim (IHT12 (i + 1) ? ?) -IHT12 [2: /2 by arith4/ |3: /2/ ] (* just /2/ is too slow *) -Hdi Hide >arith_c1 >arith_c1x #T #HT1 #HT2 - lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/ + lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/ | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 // -Hdi Hide /3 width=5/ @@ -131,14 +131,14 @@ lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫ T2 → /2/ qed. -(* Basic-1: was: subst1_gen_sort *) +(* Basic_1: was: subst1_gen_sort *) lemma tps_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫ T2 → T2 = ⋆k. #L #T2 #k #d #e #H elim (tps_inv_atom1 … H) -H // * #K #V #i #_ #_ #_ #_ #H destruct qed. -(* Basic-1: was: subst1_gen_lref *) +(* Basic_1: was: subst1_gen_lref *) lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 → T2 = #i ∨ ∃∃K,V. d ≤ i & i < d + e & @@ -210,7 +210,7 @@ lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → #[T1] ≤ #[T2]. ] qed. -(* Basic-1: removed theorems 25: +(* 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 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 c5fca2ca3..e7243c212 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 @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/drop_drop.ma". -include "Basic-2/substitution/tps.ma". +include "Basic_2/substitution/drop_drop.ma". +include "Basic_2/substitution/tps.ma". (* PARTIAL SUBSTITUTION ON TERMS ********************************************) @@ -39,7 +39,7 @@ lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 → (* Relocation properties ****************************************************) -(* Basic-1: was: subst1_lift_lt *) +(* 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 → @@ -66,7 +66,7 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ] qed. -(* Basic-1: was: subst1_lift_ge *) +(* 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 → @@ -91,7 +91,7 @@ lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → ] qed. -(* Basic-1: was: subst1_gen_lift_lt *) +(* 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 → @@ -118,7 +118,7 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] qed. -(* Basic-1: was: subst1_gen_lift_ge *) +(* 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 → @@ -153,7 +153,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] qed. -(* Basic-1: was: subst1_gen_lift_eq *) +(* 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 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 fda5cbabd..d9e9e12f9 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 @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_lift.ma". +include "Basic_2/substitution/tps_lift.ma". (* PARALLEL SUBSTITUTION ON TERMS *******************************************) (* Main properties **********************************************************) -(* Basic-1: was: subst1_confluence_eq *) +(* Basic_1: was: subst1_confluence_eq *) theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 → ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫ T. @@ -33,11 +33,11 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 → ] | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02 + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2/ #HT02 elim (IHV01 … HV02) -IHV01 HV02 #V #HV1 #HV2 elim (IHT01 … HT02) -IHT01 HT02 #T #HT1 #HT2 - lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1 /2/ - lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/ + lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2/ + lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/ | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; elim (IHV01 … HV02) -IHV01 HV02; @@ -45,7 +45,7 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫ T1 → ] qed. -(* Basic-1: was: subst1_confluence_neq *) +(* Basic_1: was: subst1_confluence_neq *) theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫ T2 → (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) → @@ -71,8 +71,8 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → elim (IHV01 … HV02 H) -IHV01 HV02 #V #HV1 #HV2 elim (IHT01 … HT02 ?) -IHT01 HT02 [ -H #T #HT1 #HT2 - lapply (tps_leq_repl_dx … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/ - lapply (tps_leq_repl_dx … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/ + lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2/ + lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -HT2 /3 width=5/ | -HV1 HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %) elim H -H #H [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3/ is too slow *) ] @@ -84,7 +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 *) +(* 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. @@ -100,9 +100,9 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 → <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2/ | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X; - lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 lapply (IHT10 … HT02 He) -IHT10 HT02 #HT12 - lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/ + lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/ | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X /3/ ] @@ -119,11 +119,11 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 → <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4/ | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; - lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 + lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 elim (IHV10 … HV02 ?) -IHV10 HV02 // #V elim (IHT10 … HT02 ?) -IHT10 HT02 [2: /2/ ] #T #HT1 #HT2 - lapply (tps_leq_repl_dx … HT1 (L. 𝕓{I} V) ?) -HT1; - lapply (tps_leq_repl_dx … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/ + lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1; + lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /3 width=6/ | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1 elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct -X; elim (IHV10 … HV02 ?) -IHV10 HV02 // diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma index 4f2062a14..e63dbb9a4 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/ltps.ma". -include "Basic-2/unfold/tpss.ma". +include "Basic_2/substitution/ltps.ma". +include "Basic_2/unfold/tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma index 4b5088638..6b45b4628 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) (* -include "Basic-2/substitution/ltps.ma". +include "Basic_2/substitution/ltps.ma". (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma index 0bf94ae76..9a023056d 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/unfold/ltpss_tpss.ma". +include "Basic_2/unfold/ltpss_tpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma index b8e425e63..b855d9f43 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/unfold/tpss_ltps.ma". -include "Basic-2/unfold/ltpss.ma". +include "Basic_2/unfold/tpss_ltps.ma". +include "Basic_2/unfold/ltpss.ma". (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma index 6b63c4e1b..44587e3bd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps.ma". +include "Basic_2/substitution/tps.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) @@ -36,8 +36,8 @@ lemma tpss_strap: ∀L,T1,T,T2,d,e. L ⊢ T1 [d, e] ≫ T → L ⊢ T [d, e] ≫* T2 → L ⊢ T1 [d, e] ≫* T2. /2/ qed. -lemma tpss_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 → - ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫* T2. +lemma tpss_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 → + ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ≫* T2. /3/ qed. lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T. @@ -52,7 +52,7 @@ lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ≫* V2 → | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] | #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12 - lapply (tpss_leq_repl_dx … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12 + lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12 lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *) ] qed. @@ -115,7 +115,7 @@ lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 [ /2 width=5/ | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U; elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H - lapply (tpss_leq_repl_dx … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/ + lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma index f28ff3896..4e1cfd5e6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_lift.ma". -include "Basic-2/unfold/tpss.ma". +include "Basic_2/substitution/tps_lift.ma". +include "Basic_2/unfold/tpss.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma index 645d9d08d..1f4a2de3e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/ltps_tps.ma". -include "Basic-2/unfold/tpss_tpss.ma". +include "Basic_2/substitution/ltps_tps.ma". +include "Basic_2/unfold/tpss_tpss.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) @@ -71,15 +71,15 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K0 #V0 #HK01 #HV01 #H destruct -X; lapply (tps_fwd_tw … HV01) #H2 lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 [ /2/ ] -H2 #H - lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | /2/ | /3 width=6/ ] + lapply (IH … HV01 … HK01 ? ?) -IH HV01 HK01 [1,3: // |2,4: skip | normalize /2/ | /3 width=6/ ] | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2; - lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12 - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: // |2,4: skip ] #HV12 + lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2/ #HT12 + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12 lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH HT12 [1,3,5: /2/ |2,4: skip | normalize // ] -HL0 #HT12 - lapply (tpss_leq_repl_dx … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/ + lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2/ | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct -Y1 X2; - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: // |2,4: skip ] - lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: // |2,4: skip ] -HL0 /2/ + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] + lapply (IH … HT12 … HL0 ? ?) -IH HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma index a84928453..57e4fb199 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_tps.ma". -include "Basic-2/unfold/tpss_lift.ma". +include "Basic_2/substitution/tps_tps.ma". +include "Basic_2/unfold/tpss_lift.ma". (* PARTIAL UNFOLD ON TERMS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index 3bb6514be..c17ef80d0 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "arithmetics/nat.ma". -include "Ground-2/xoa_props.ma". +include "Ground_2/xoa_props.ma". (* ARITHMETICAL PROPERTIES **************************************************) diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/Ground_2/list.ma index 1b64bacce..9bdc5c126 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/list.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/list.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground-2/arith.ma". -include "Ground-2/notation.ma". +include "Ground_2/arith.ma". +include "Ground_2/notation.ma". (* LISTS ********************************************************************) diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma index baed9b78e..ffc5ab1ac 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basics/star.ma". -include "Ground-2/xoa_props.ma". +include "Ground_2/xoa_props.ma". (* PROPERTIES of RELATIONS **************************************************) diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml index f749fe18a..8634d7256 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml @@ -10,7 +10,7 @@ -->
- contribs/lambda-delta/Ground-2 + contribs/lambda_delta/Ground-2/ xoa xoa_notation basics/pts.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma index f1ed781c3..c2d7e2f41 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "Ground-2/xoa_notation.ma". -include "Ground-2/xoa.ma". +include "Ground_2/xoa_notation.ma". +include "Ground_2/xoa.ma". lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. #A0 #P0 #P1 * /2/ diff --git a/matita/matita/contribs/lambda_delta/replace.sh b/matita/matita/contribs/lambda_delta/replace.sh index 6caaacdb8..33bf0e3a1 100644 --- a/matita/matita/contribs/lambda_delta/replace.sh +++ b/matita/matita/contribs/lambda_delta/replace.sh @@ -1,8 +1,8 @@ #!/bin/sh -for V in `cat Make`; do - echo ${V}; sed "s/$1/$2/g" ${V} > ${V}.new - if diff ${V} ${V}.new > /dev/null; - then rm -f ${V}.new; else mv -f ${V}.new ${V}; fi +for MA in `find -name "*.ma"`; do + echo ${MA}; sed "s/$1/$2/g" ${MA} > ${MA}.new + if diff ${MA} ${MA}.new > /dev/null; + then rm -f ${MA}.new; else mv -f ${MA}.new ${MA}; fi done -unset V +unset MA -- 2.39.2