From 9aa9a54946719d3fdb4cadb7c7d33fd13956c083 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Dec 2011 17:51:52 +0000 Subject: [PATCH] - support for atomic arities and candidates of reducibility started - integrations to standard library reduced - some refactoring --- .../apr_cr.ma => computation/acp_cr.ma} | 36 +--- .../lambda_delta/Basic_2/grammar/cl_weight.ma | 2 +- .../lambda_delta/Basic_2/grammar/term.ma | 2 +- .../contribs/lambda_delta/Basic_2/notation.ma | 30 +++ .../Basic_2/reducibility/cpr_lift.ma | 6 +- .../Basic_2/reducibility/tpr_tpr.ma | 22 +- .../Basic_2/{grammar => static}/sh.ma | 0 .../Basic_2/substitution/ldrop.ma | 8 +- .../Basic_2/substitution/ldrop_ldrop.ma | 6 +- .../lambda_delta/Basic_2/substitution/lift.ma | 4 +- .../Basic_2/substitution/lift_lift.ma | 13 +- .../Basic_2/substitution/ltps_ldrop.ma | 12 +- .../Basic_2/substitution/ltps_tps.ma | 20 +- .../lambda_delta/Basic_2/substitution/tps.ma | 11 +- .../Basic_2/substitution/tps_lift.ma | 28 +-- .../lambda_delta/Basic_2/unfold/tpss_lift.ma | 2 +- .../lambda_delta/Basic_2/unfold/tpss_ltps.ma | 6 +- .../lambda_delta/Basic_2/unfold/tpss_tpss.ma | 4 +- .../contribs/lambda_delta/Ground_2/arith.ma | 203 +++++++++--------- .../lambda_delta/Ground_2/notation.ma | 8 +- .../contribs/lambda_delta/Ground_2/star.ma | 48 ++--- 21 files changed, 237 insertions(+), 234 deletions(-) rename matita/matita/contribs/lambda_delta/Basic_2/{reducibility/apr_cr.ma => computation/acp_cr.ma} (52%) rename matita/matita/contribs/lambda_delta/Basic_2/{grammar => static}/sh.ma (100%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma similarity index 52% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma rename to matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma index b46de8470..449dd7b69 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/apr_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma @@ -12,32 +12,18 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/term_simple.ma". +include "Basic_2/grammar/aarity.ma". +include "Basic_2/grammar/lenv.ma". -(* CANDIDATES OF REDUCIBILITY ***********************************************) +(* ABSTRACT CANDIDATES OF REDUCIBILITY **************************************) -(* abstract conditions for candidates *) - -definition CR1: predicate term → predicate term → Prop ≝ - λRD,RC. ∀T. RC T → RD T. - -definition CR2: relation term → predicate term → Prop ≝ - λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2. - -definition CR3: relation term → predicate term → Prop ≝ - λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1. - -(* a candidate *) -record cr (RR:relation term) (RD:predicate term): Type[0] ≝ { - in_cr: predicate term; - cr1: CR1 RD in_cr; - cr2: CR2 RR in_cr; - cr3: CR3 RR in_cr -}. +(* the abstract candidate of reducibility associated to an atomic arity *) +let rec acr (R:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝ +λT. match A with +[ AAtom ⇒ R L T +| APair B A ⇒ ∀V. acr R B L V → acr R A L (𝕔{Appl} V. T) +]. interpretation - "context-free parallel reduction (term)" - 'InSubset T R = (in_cr ? ? R T). - -definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝ - λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C. + "candidate of reducibility (abstract)" + 'InEInt R L T A = (acr R A L T). 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 c5e93ce16..22818a980 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 width=1/ | skip ] +@transitive_le [3: @IHL |2: /2 width=2/ | skip ] qed. (* Basic_1: removed theorems 6: 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 f3f307cd6..42e7b8633 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -43,7 +43,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False. [ #J #H destruct | #J #W #U #IHW #_ #H destruct -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) - /2 width=1/ + /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index dcbbbffed..0ec1b1466 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -32,10 +32,18 @@ notation "hvbox( § term 90 p )" non associative with precedence 90 for @{ 'GRef $p }. +notation "hvbox( 𝕒 )" + non associative with precedence 90 + for @{ 'SItem }. + notation "hvbox( 𝕒 { I } )" non associative with precedence 90 for @{ 'SItem $I }. +notation "hvbox( 𝕔 term 90 T1 . break term 90 T )" + non associative with precedence 90 + for @{ 'SItem $T1 $T }. + notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )" non associative with precedence 90 for @{ 'SItem $I $T1 $T }. @@ -108,6 +116,12 @@ 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 }. +(* Static Typing ************************************************************) + +notation "hvbox( L ⊢ break term 90 T ÷ break A )" + non associative with precedence 45 + for @{ 'AtomicArity $L $T $A }. + (* Reducibility *************************************************************) notation "hvbox( ℝ [ T ] )" @@ -191,3 +205,19 @@ notation "hvbox( ⇓ T )" notation "hvbox( L ⊢ ⇓ T )" non associative with precedence 45 for @{ 'SN $L $T }. + +notation "hvbox( { L, break T } ϵ break 〚 A 〛 )" + non associative with precedence 45 + for @{ 'InEInt $L $T $A }. + +notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )" + non associative with precedence 45 + for @{ 'InEInt $R $L $T $A }. + +notation "hvbox( T1 ⊑ break T2 )" + non associative with precedence 45 + for @{ 'CrSubEq $T1 $T2 }. + +notation "hvbox( T1 break [ R ] ⊑ break T2 )" + non associative with precedence 45 + for @{ 'CrSubEq $T1 $R $T2 }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma index 0775cefd2..f33692b42 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma @@ -58,7 +58,7 @@ lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → elim (lift_total T d e) #U #HTU lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1 elim (lt_or_ge (|K|) d) #HKd -[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=1/ | /3 width=4/ ] +[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 -T -HLK [ /2 width=2/ | /3 width=4/ ] | lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 -T -HLK // /3 width=4/ ] qed. @@ -70,9 +70,9 @@ lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K → #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1 elim (lt_or_ge (|L|) d) #HLd -[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=1/ ] +[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ] | elim (lt_or_ge (|L|) (d + e)) #HLde - [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=1/ ] + [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=2/ ] | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/ ] ] diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma index 332575c21..40feeff2f 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma @@ -45,8 +45,8 @@ fact tpr_conf_flat_beta: ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X. #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 -elim (IH … HT02 … HU01) -HT02 -HU01 -IH // /3 width=5/ +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HT02 … HU01) -HT02 -HU01 -IH /2 width=1/ /3 width=5/ qed. (* basic-1: was: @@ -63,14 +63,14 @@ fact tpr_conf_flat_theta: W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 → ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X. #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H -elim (IH … HV01 … HV02) -HV01 -HV02 // #VV #HVV1 #HVV2 +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2 elim (lift_total VV 0 1) #VVV #HVV lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV elim (tpr_inv_abbr1 … H) -H * (* case 1: delta *) [ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct - elim (IH … HW02 … HWW2) -HW02 -HWW2 // #W #HW02 #HWW2 - elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH // #U #HU2 #HUUU2 + elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2 + elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2 elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 @ex2_1_intro [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] @@ -81,7 +81,7 @@ elim (tpr_inv_abbr1 … H) -H * | -HW02 -HVV -HVVV #UU1 #HUU10 #HUUT1 elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1 lapply (tw_lift … HUU10) -HUU10 #HUU10 - elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH // -HUU10 #U #HU2 #HUUU2 + elim (IH … HUUT1 … HUU1) -HUUT1 -HUU1 -IH /2 width=1/ -HUU10 #U #HU2 #HUUU2 @ex2_1_intro [2: @tpr_flat |1: skip @@ -111,8 +111,8 @@ fact tpr_conf_beta_beta: V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 → ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X. #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02 -elim (IH … HV01 … HV02) -HV01 -HV02 // -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/ +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ +elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/ qed. (* Basic_1: was: pr0_cong_delta pr0_delta_delta *) @@ -162,9 +162,9 @@ fact tpr_conf_theta_theta: ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 → ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X. #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2 -elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 -elim (IH … HW01 … HW02) -HW01 -HW02 // #W #HW1 #HW2 -elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 +elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 +elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2 +elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ #T #HT1 #HT2 elim (lift_total V 0 1) #VV #HVV lapply (tpr_lift … HV1 … HVV1 … HVV) -V1 #HVV1 lapply (tpr_lift … HV2 … HVV2 … HVV) -V2 -HVV #HVV2 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/sh.ma rename to matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma index db31dfaab..2b8f3f953 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma @@ -152,17 +152,17 @@ lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 → [ -IHL12 -Hie destruct arith_g1 // /3 width=3/ + elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/ ] | #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie elim (ldrop_inv_O1 … H) -H * #Hi #HLK1 [ -IHL12 -Hie -Hi destruct - | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/ + | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=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 + elim (le_inv_plus_l … Hdi) #Hdim #Hi lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1 - elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/ + elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/ ] qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma index f4b20bcb5..3aef19c0e 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma @@ -46,7 +46,7 @@ theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 → | // | #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2 lapply (ldrop_inv_ldrop1 … H ?) -H /2 width=2/ #HL2 - minus_minus_comm /3 width=1/ | #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2 lapply (transitive_le 1 … Hdee2) // #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // -He2 #HL2 @@ -85,9 +85,9 @@ theorem ldrop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L → [ #d #e #e2 #L2 #H >(ldrop_inv_atom1 … H) -L2 /2 width=3/ | #K #I #V #e2 #L2 #HL2 #H - lapply (le_O_to_eq_O … H) -H #H destruct /2 width=3/ + lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/ | #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H - lapply (le_O_to_eq_O … H) -H #H destruct + lapply (le_n_O_to_eq … H) -H #H destruct elim (IHL12 … HL2 ?) -IHL12 -HL2 // #L0 #H #HL0 lapply (ldrop_inv_refl … H) -H #H destruct /3 width=5/ | #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d 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 f58c1906e..30296c685 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -303,8 +303,8 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/ | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12 - lapply (transitive_le …(i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21 - <(arith_d1 i e2 e1) // /3 width=3/ + lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21 + >(plus_minus_m_m e2 e1 ?) // /3 width=3/ | /3 width=3/ | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12 elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b 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 2f92251bd..3f5b8ab6a 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 @@ -50,11 +50,11 @@ theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12 elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct [ -Hd12 lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3 width=3/ - | -Hid1 lapply (arith1 … Hid2) -Hid2 #Hid2 - @(ex2_1_intro … #(i - e2)) - [ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2 width=1/ | -Hd12 /2 width=2/ ] - | -Hd12 >(plus_minus_m_m i e2) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=1/ - ] + | -Hid1 >plus_plus_comm_23 in Hid2; #H lapply (le_inv_plus_plus_r … H) -H #H + elim (le_inv_plus_l … H) -H #Hide2 #He2i + lapply (transitive_le … Hd12 Hide2) -Hd12 #Hd12 + >le_plus_minus_comm // >(plus_minus_m_m i e2) in ⊢ (? ? ? %); // -He2i + /4 width=3/ ] | #p #d1 #e1 #d2 #e2 #T2 #Hk #Hd12 lapply (lift_inv_gref2 … Hk) -Hk #Hk destruct /3 width=3/ @@ -154,8 +154,7 @@ theorem lift_trans_ge: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T → lapply (lt_to_le_to_lt … Hid1e Hded) -Hid1e -Hded #Hid2 lapply (lift_inv_lref1_lt … HX ?) -HX // #HX destruct /3 width=3/ | #i #d1 #e1 #Hid1 #d2 #e2 #X #HX #_ - elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct - [ /4 width=3/ | >plus_plus_comm_23 /4 width=3/ ] + elim (lift_inv_lref1 … HX) -HX * #Hied #HX destruct /4 width=3/ | #p #d1 #e1 #d2 #e2 #X #HX #_ >(lift_inv_gref1 … HX) -HX /2 width=3/ | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma index 7996f53a6..f777d1cd7 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma @@ -23,11 +23,11 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12 - lapply (plus_le_weak … He12) #He2 + elim (le_inv_plus_l … He12) #_ #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 - lapply (plus_le_weak … Hd1e2) #He2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/ ] @@ -40,11 +40,11 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 → [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H // | // | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12 - lapply (plus_le_weak … He12) #He2 + elim (le_inv_plus_l … He12) #_ #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/ | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 - lapply (plus_le_weak … Hd1e2) #He2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2 lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/ ] @@ -65,7 +65,7 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 → elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/ ] | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1 - lapply (plus_le_weak … Hd1e2) #He2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1 - lapply (plus_le_weak … Hd1e2) #He2 + elim (le_inv_plus_l … Hd1e2) #_ #He2 arith_a2 // /3 width=4/ + lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -V0 -H // >minus_plus arith_i2 // + lapply (tps_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/ | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/ ] ] @@ -73,7 +73,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/ | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 - @tps_bind [ /2 width=4/ | @IHTU2 /2 width=4/ ] (**) (* explicit constructor *) + @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltps_tps1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *) | /3 width=4/ ] qed. @@ -87,18 +87,18 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → [ /2 width=3/ | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 elim (lt_or_ge i2 d1) #Hi2d1 - [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=1/ #X #H #HLK1 + [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1 elim (ltps_inv_tps12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 - lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >arith_a2 // /3 width=4/ + lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -V0 -H // >minus_plus arith_i2 // + lapply (tps_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/ | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/ ] ] 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 762e2a9a0..969e67485 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma @@ -58,7 +58,7 @@ lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) → elim (lt_or_eq_or_gt i d) #Hid /3 width=4/ destruct elim (lift_total V 0 (i+1)) #W #HVW - elim (lift_split … HVW i i ? ? ?) // (plus_minus_m_m_comm j d) in ⊢ (% → ?); // -Hdj /3 width=4/ + >(plus_minus_m_m j d) in ⊢ (% → ?); // -Hdj /3 width=4/ | -Hdi -Hdj #Hid generalize in match Hide; -Hide (**) (* rewriting in the premises, rewrites in the goal too *) - >(plus_minus_m_m_comm … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/ + >(plus_minus_m_m … Hjde) in ⊢ (% → ?); -Hjde /4 width=4/ ] | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2 elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/ - -Hdi -Hide >arith_c1 >arith_c1x #T #HT1 #HT2 + -Hdi -Hide >arith_c1x #T #HT1 #HT2 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 // 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 ff42a7ac4..6e3565e73 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 @@ -52,7 +52,7 @@ lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid lapply (lift_inv_lref1_lt … H … Hid) -H #H destruct elim (lift_trans_ge … HVW … HWU2 ?) -W // (lift_mono … HVY … HVW) -Y -HVW #H destruct /2 width=4/ | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd @@ -78,7 +78,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → [ -Hdtd lapply (lt_to_le_to_lt … (dt+et+e) Hidet ?) // -Hidet #Hidete elim (lift_trans_ge … HVW … HWU2 ?) -W // (lift_mono … HVY … HVW) -V #H destruct /2 width=4/ | -Hdti @@ -90,7 +90,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 → elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] - ] (**) (* /3 width=6/ is too slow, arith3 needed to avoid crash, simplification like tps_lift_le is too slow *) + ] (**) (* /3 width=6/ is too slow, simplification like tps_lift_le is too slow *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ @@ -136,7 +136,7 @@ lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → lapply (lt_to_le_to_lt … Hidet … Hdetd) -Hdetd #Hid lapply (lift_inv_lref2_lt … H … Hid) -H #H destruct elim (ldrop_conf_lt … HLK … HLKV ?) -L // #L #U #HKL #_ #HUV - elim (lift_trans_le … HUV … HVW ?) -V // >arith_a2 // -Hid /3 width=4/ + elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus arith_a2 // -Hid /3 width=4/ + elim (lift_trans_le … HUV … HVW ?) -V // >minus_plus arith_e2 // /4 width=4/ + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid + #V1 #HV1 >plus_minus // plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] + elim (IHU12 … HTU1 ? ?) -U1 [5: @ldrop_skip // |2: skip |3: >plus_plus_comm_23 >(plus_plus_comm_23 dt) /2 width=1/ |4: /2 width=1/ ] (**) (* 29s without the rewrites *) /3 width=5/ | #L #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdtd #Hdedet elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct @@ -197,15 +198,16 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 → ] | #L #KV #V #W #i #dt #et #Hdti #Hidet #HLKV #HVW #K #d #e #HLK #T1 #H #Hdedt lapply (transitive_le … Hdedt … Hdti) #Hdei - lapply (plus_le_weak … Hdedt) -Hdedt #Hedt - lapply (plus_le_weak … Hdei) #Hei + elim (le_inv_plus_l … Hdedt) -Hdedt #_ #Hedt + elim (le_inv_plus_l … Hdei) #_ #Hei lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |2,3: normalize /2 width=1/ ] -Hdei >arith_e2 // #V0 #HV10 #HV02 + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei + #V0 #HV10 >plus_minus // commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -U -L // arith_i2 // | /2 width=1/ | /2 width=3/ ] + lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ] ] qed. 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 18b181741..f07ee8ee3 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 @@ -67,7 +67,7 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. [ // | #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct lapply (ldrop_fwd_lw … HLK1) normalize #H1 - elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 /2 width=1/ #X #H #HLK0 + elim (ltps_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0 elim (ltps_inv_tps22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct lapply (tps_fwd_tw … HV01) #H2 lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H @@ -75,11 +75,11 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ] | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12 - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] #HV12 + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12 lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12 lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/ | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct - lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3,5: normalize // |2,4: skip ] + lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ] lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/ ] 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 fc340e1ad..cd7e666b2 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 @@ -53,7 +53,7 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → [ /2 width=3/ | #T #T2 #_ #HT12 * #T3 #HT13 #HT3 elim (tps_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02 - elim (tpss_strap1_down … HT3 … HT0 ?) -T [2: commutative_plus /2 width=1/ ] /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *) ] qed. @@ -64,7 +64,7 @@ lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 → ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2. #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2 -lapply (tpss_weak … HU1 d e ? ?) -HU1 // commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1 lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 -HLK -HTU1 // (le_n_O_to_eq … H) -H // +| #b #IHb #c elim c -c // + #c #_ #a #Hcb + lapply (le_S_S_to_le … Hcb) -Hcb #Hcb + minus_plus @eq_f2 /2 width=1/ +qed. -lemma lt_to_le: ∀a,b. a < b → a ≤ b. -/2 width=2/ qed. +lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. +#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/ +qed. -lemma lt_refl_false: ∀n. n < n → False. -#n #H elim (lt_to_not_eq … H) -H /2 width=1/ -qed-. +lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. +/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. -lemma lt_zero_false: ∀n. n < 0 → False. -#n #H elim (lt_to_not_le … H) -H /2 width=1/ -qed-. +lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → + a1 - c1 + a2 - (b - c1) = a1 + a2 - b. +#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/ +qed. + +(* inversion & forward lemmas ***********************************************) + +axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). + +axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m. #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/ -qed. +qed-. lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. #m elim m -m @@ -61,13 +73,25 @@ lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. | #m #IHm * /2 width=1/ #n elim (IHm n) -IHm #H [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *) -qed. +qed-. -lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n. -/2 width=1/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *) +lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y. +/2 by le_plus_to_le/ qed-. -lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p. -/2 width=2/ qed. +lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z. +/3 width=2/ qed-. + +lemma lt_refl_false: ∀n. n < n → False. +#n #H elim (lt_to_not_eq … H) -H /2 width=1/ +qed-. + +lemma lt_zero_false: ∀n. n < 0 → False. +#n #H elim (lt_to_not_le … H) -H /2 width=1/ +qed-. + +lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False. +#n #m (commutative_plus p) plus_minus // @monotonic_lt_minus_l // qed. -lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b. -#b elim b -b -[ #c #a #H >(le_O_to_eq_O … H) -H // -| #b #IHb #c elim c -c // - #c #_ #a #Hcb - lapply (le_S_S_to_le … Hcb) -Hcb #Hcb - minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l // qed. +(* remove *******************************************************************) +(* lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b). // qed. -lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b. -/3 width=1/ qed. +lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p. +/2 by ltn_to_ltO/ qed. -lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c). -/2 width=1/ qed. +lemma minus_le: ∀m,n. m - n ≤ m. +/2 by monotonic_le_minus_l/ qed. -lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m). -/2 width=1/ qed. +lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0. +/2 by le_n_O_to_eq/ qed. -lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m. -/2 width=1/ qed. +lemma lt_to_le: ∀a,b. a < b → a ≤ b. +/2 by le_plus_b/ qed. -lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a. -/2 width=1/ qed. +lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n. +/2 by le_to_or_lt_eq/ qed. -lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/ -qed. +lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p. +/2 by le_plus_b/ qed. -lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. -#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/ -qed. +lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b. +/2 by le_plus_to_minus_r/ qed. + +lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d. +/2 by monotonic_lt_minus_l/ qed. + +lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a. +/2 by plus_minus/ qed. lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b. // qed. -lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -#x #a #b #c1 >plus_plus_comm_23 // -qed. - lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b. -/2 width=1/ qed. +/2 by plus_minus/ qed. lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a. -/3 width=1/ qed. +/2 by minus_le_minus_minus_comm/ qed. lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b. -#a #b #c1 #H >minus_plus minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l // -qed. +(* backward form of le_inv_plus_l *) +lemma P2: ∀x,y,z. x ≤ z - y → y ≤ z → x + y ≤ z. +/2 by le_minus_to_plus_r/ qed. +*) diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma index 65cb0a029..45109878f 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/notation.ma @@ -14,18 +14,12 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -(* Subsets ******************************************************************) - -notation "hvbox( T ϵ break R )" - non associative with precedence 45 - for @{ 'InSubset $T $R }. - (* Lists ********************************************************************) notation "hvbox( hd break :: tl )" right associative with precedence 47 for @{'Cons $hd $tl}. -notation "hvbox( l1 break @ l2)" +notation "hvbox( l1 break @ l2 )" right associative with precedence 47 for @{'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma index ee6a901e8..56181da2f 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma @@ -15,22 +15,19 @@ include "basics/star.ma". include "Ground_2/xoa_props.ma". -(* PROPERTIES of RELATIONS **************************************************) +(* PROPERTIES OF RELATIONS **************************************************) -definition predicate: Type[0] → Type[0] ≝ λA. A → Prop. +definition Decidable: Prop → Prop ≝ λR. R ∨ (R → False). -definition Decidable: Prop → Prop ≝ - λR. R ∨ (R → False). +definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. + ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a2 a. -definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. - ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a2 a. +definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. + ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a a2. -definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. - ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a a2. - -lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 → +lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 → ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & TC … R1 a2 a. #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 @@ -42,7 +39,7 @@ lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 → ] qed. -lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 → +lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 → ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 → ∃∃a. TC … R2 a1 a & R1 a2 a. #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 @@ -54,8 +51,8 @@ lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 → ] qed. -lemma TC_confluent: ∀A,R1,R2. - confluent A R1 R2 → confluent A (TC … R1) (TC … R2). +lemma TC_confluent2: ∀A,R1,R2. + confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2). #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 [ #a1 #Ha01 #a2 #Ha02 elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/ @@ -65,11 +62,7 @@ lemma TC_confluent: ∀A,R1,R2. ] qed. -lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2. - R a1 a → TC … R a a2 → TC … R a1 a2. -/3 width=3/ qed. - -lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 → +lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 → ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & TC … R1 a a2. #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 @@ -81,7 +74,7 @@ lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 → ] qed. -lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 → +lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 → ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 → ∃∃a. TC … R2 a1 a & R1 a a2. #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 @@ -93,8 +86,8 @@ lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 → ] qed. -lemma TC_transitive: ∀A,R1,R2. - transitive A R1 R2 → transitive A (TC … R1) (TC … R2). +lemma TC_transitive2: ∀A,R1,R2. + transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2). #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 [ #a0 #Ha10 #a2 #Ha02 elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/ @@ -104,15 +97,6 @@ lemma TC_transitive: ∀A,R1,R2. ] qed. -lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R). -/2 width=1/ qed. - -lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A. - P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) → - ∀a2. TC … R a1 a2 → P a2. -#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/ -qed. - definition NF: ∀A. relation A → relation A → predicate A ≝ λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2. -- 2.39.2