From 18ac3a120a3887b144c1d0e13d64d6e1c2d10d93 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 26 Nov 2011 13:15:24 +0000 Subject: [PATCH] - "grammar" component updated to new syntax ... - notation for lthin - bugfix in replace.sh --- .../lambda_delta/Basic_2/grammar/cl_weight.ma | 2 +- .../lambda_delta/Basic_2/grammar/item.ma | 4 +-- .../lambda_delta/Basic_2/grammar/lsubs.ma | 36 ++++++++++--------- .../lambda_delta/Basic_2/grammar/term.ma | 9 ++--- .../Basic_2/grammar/term_weight.ma | 4 +-- .../lambda_delta/Basic_2/grammar/thom.ma | 20 +++++------ .../contribs/lambda_delta/Basic_2/notation.ma | 4 +++ .../matita/contribs/lambda_delta/replace.sh | 6 ++-- 8 files changed, 47 insertions(+), 38 deletions(-) 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 0414499a5..c5e93ce16 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 @@ -38,7 +38,7 @@ qed. lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T]. #L elim L // #K #I #V #IHL #T -@transitive_le [3: @IHL |2: /2/ | skip ] +@transitive_le [3: @IHL |2: /2 width=1/ | skip ] qed. (* Basic_1: removed theorems 6: 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 56c5a2b8c..48ff1ec9a 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -13,10 +13,10 @@ (**************************************************************************) (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES - * Specification started: 2011 April 17 * Confluence of context-sensitive parallel reduction closed: 2011 September 21 * Confluence of context-free parallel reduction closed: 2011 September 6 - * - Patience on me so that I gain peace and perfection! - + * Specification started: 2011 April 17 + * - Patience on me to gain peace and perfection! - * [ suggested invocation to start formal specifications with ] *) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma index cf90a6134..1f750064e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma @@ -27,7 +27,9 @@ inductive lsubs: nat → nat → relation lenv ≝ lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) . -interpretation "local environment refinement (substitution)" 'SubEq L1 d e L2 = (lsubs d e L1 L2). +interpretation + "local environment refinement (substitution)" + 'SubEq L1 d e L2 = (lsubs d e L1 L2). definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R. ∀L1,s1,s2. R L1 s1 s2 → @@ -36,29 +38,29 @@ definition lsubs_conf: ∀S. (lenv → relation S) → Prop ≝ λS,R. (* Basic properties *********************************************************) 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 +#S #R #HR #L1 #s1 #s2 #H elim H -s2 [ /3 width=5/ | #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 - lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ + lapply (HR … Hs2 … HL12) -HR -Hs2 -HL12 /3 width=3/ ] qed. lemma lsubs_bind_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/ +#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ 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/ +[ #e elim e -e // #e #IHe #L elim L -L // /2 width=1/ +| #d #IHd #e #L elim L -L // /2 width=1/ ] qed. 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/ +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ qed. (* Basic inversion lemmas ***************************************************) @@ -67,14 +69,14 @@ qed. fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → d = 0 → e = |L1| → |L1| ≤ |L2|. -#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize [ // -| /2/ -| /3/ -| /3/ +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ | #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H elim (plus_S_eq_O_false … H) -] +] qed. lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. @@ -82,14 +84,14 @@ lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|. fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → d = 0 → e = |L2| → |L2| ≤ |L1|. -#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize [ // -| /2/ -| /3/ -| /3/ +| /2 width=1/ +| /3 width=1/ +| /3 width=1/ | #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H elim (plus_S_eq_O_false … H) -] +] qed. lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|. 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 376061b70..f3f307cd6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -42,9 +42,8 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False. #I #T #V elim V -V [ #J #H destruct | #J #W #U #IHW #_ #H destruct -(* - (generalize in match e1) -e1 >e0 normalize -*) -I /2/ (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) + -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) + /2 width=1/ ] qed-. @@ -52,7 +51,9 @@ qed-. lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False. #I #V #T elim T -T [ #J #H destruct -| #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* destruct: the destucted equality is not erased *) +| #J #W #U #_ #IHU #H destruct + -H (**) (* destruct: the destucted equality is not erased *) + /2 width=1/ ] qed-. 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 8eaa24aca..1cf414b38 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 @@ -27,7 +27,7 @@ interpretation "weight (term)" 'Weight T = (tw T). (* Basic_1: was: tweight_lt *) lemma tw_pos: ∀T. 1 ≤ #[T]. -#T elim T -T /2/ +#T elim T -T // qed. (* Basic eliminators ********************************************************) @@ -38,6 +38,6 @@ axiom tw_wf_ind: ∀R:predicate term. (* 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 + 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 4bb9748d2..aaade3b54 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -28,32 +28,32 @@ interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2). (* Basic properties *********************************************************) lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1. -#T1 #T2 #H elim H -H T1 T2 /2/ +#T1 #T2 #H elim H -T1 -T2 /2 width=1/ qed. lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2. -#T1 #T2 #H elim H -H T1 T2 /2/ +#T1 #T2 #H elim H -T1 -T2 // /2 width=1/ qed. lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. -/3/ qed. +/3 width=2/ qed. lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝕊[T1] → 𝕊[T2]. -#T1 #T2 #H elim H -H T1 T2 // +#T1 #T2 #H elim H -T1 -T2 // #V1 #V2 #T1 #T2 #H elim (simple_inv_bind … H) qed. (**) (* remove from index *) lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. -/3/ qed-. +/3 width=3/ qed-. (* Basic inversion lemmas ***************************************************) fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 → ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2. -#T1 #T2 * -T1 T2 +#T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -V1 T1 /2/ +| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/ | #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct ] qed. @@ -65,17 +65,17 @@ lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 → fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 → ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & I = Appl & T2 = 𝕔{Appl} W2. U2. -#T1 #T2 * -T1 T2 +#T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct | #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct -| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct -V1 T1 /2 width=5/ +| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/ ] qed. lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 → ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & I = Appl & T2 = 𝕔{Appl} W2. U2. -/2/ qed-. +/2 width=4/ qed-. (* Basic_1: removed theorems 7: iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 5fcf58833..dcbbbffed 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -100,6 +100,10 @@ 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 }. +notation "hvbox( T1 break [ d , break e ] ≡ break T2 )" + non associative with precedence 45 + for @{ 'TSubst $T1 $d $e $T2 }. + notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/replace.sh b/matita/matita/contribs/lambda_delta/replace.sh index 33bf0e3a1..5e281b251 100644 --- a/matita/matita/contribs/lambda_delta/replace.sh +++ b/matita/matita/contribs/lambda_delta/replace.sh @@ -1,8 +1,10 @@ #!/bin/sh for MA in `find -name "*.ma"`; do - echo ${MA}; sed "s/$1/$2/g" ${MA} > ${MA}.new + 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 + then rm -f ${MA}.new; + else mv -f ${MA} ${MA}.old; mv -f ${MA}.new ${MA}; + fi done unset MA -- 2.39.2