From 5c35602808c464a9098b3f39afb7dced059e0d6d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Jan 2013 19:32:59 +0000 Subject: [PATCH] - paths and left residuals: third case of the equivalence proved! --- .../lambda/paths/labeled_st_computation.ma | 162 +++++++++++++----- .../lambda/paths/labeled_st_reduction.ma | 18 +- matita/matita/contribs/lambda/paths/path.ma | 54 +++++- .../contribs/lambda/paths/standard_order.ma | 17 ++ .../lambda/paths/standard_precedence.ma | 15 ++ .../contribs/lambda/paths/standard_trace.ma | 14 ++ matita/matita/contribs/lambda/paths/trace.ma | 39 +++-- 7 files changed, 240 insertions(+), 79 deletions(-) diff --git a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma index 2900f4d38..35ece1775 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma @@ -44,6 +44,11 @@ elim (pl_st_inv_pl_sred … HF2) -HF2 // -Hp #M2 #HM2 #H lapply (pl_sreds_step_dx … HM … HM2) -M /2 width=3/ qed-. +lemma pl_sts_inv_empty: ∀s,M1,F2. {⊥}⇑M1 Ⓡ↦*[s] F2 → ◊ = s ∧ {⊥}⇑M1 = F2. +#s #M1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 /2 width=1/ #p #s #F #F2 #_ #HF2 * #_ #H +elim (pl_st_inv_empty … HF2 … H) +qed-. + lemma pl_sts_refl: reflexive … (pl_sts (◊)). // qed. @@ -91,6 +96,32 @@ lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. ] qed-. +lemma pl_sts_inv_sn_appl_dx: ∀b2,s,F1,V2,T2. F1 Ⓡ↦*[s] {b2}@V2.T2 → ∀r. sn:::r = s → + ∃∃b1,V1,T1. V1 Ⓡ↦*[r] V2 & {b1}@V1.T1 = F1. +#b2 #s #F1 #V2 #T2 #H @(lstar_ind_l … s F1 H) -s -F1 +[ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=5/ +| #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2 + elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr + elim (pl_st_inv_sn … HF1 … Hp) -HF1 -p #b1 #V1 #V #T1 #HV1 #HF1 #HF destruct + elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + #b0 #V0 #T0 #HV02 #H destruct + lapply (pl_sts_step_sn … HV1 … HV02) -V /2 width=5/ +] +qed-. + +lemma pl_sts_inv_dx_appl_dx: ∀b,s,F1,V,T2. F1 Ⓡ↦*[s] {b}@V.T2 → ∀r. dx:::r = s → + ∃∃T1. T1 Ⓡ↦*[r] T2 & {b}@V.T1 = F1. +#b #s #F1 #V #T2 #H @(lstar_ind_l … s F1 H) -s -F1 +[ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=3/ +| #p #s #F1 #F #HF1 #_ #IHF2 #r #H + elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr + elim (pl_st_inv_dx … HF1 … Hp) -HF1 -p #b0 #V0 #T1 #T #HT1 #HF1 #HF destruct + elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + #T0 #HT02 #H destruct + lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=3/ +] +qed-. + lemma pl_sts_lift: ∀s. sliftable (pl_sts s). /2 width=1/ qed. @@ -111,10 +142,20 @@ theorem pl_sts_trans: ltransitive … pl_sts. /2 width=3 by lstar_ltransitive/ qed-. -theorem pl_sts_inv_trans: inv_ltransitive … pl_sts. +lemma pl_sts_inv_trans: inv_ltransitive … pl_sts. /2 width=3 by lstar_inv_ltransitive/ qed-. +lemma pl_sts_fwd_dx_sn_appl_dx: ∀b2,s,r,F1,V2,T2. F1 Ⓡ↦*[(dx:::s)@(sn:::r)] {b2}@V2.T2 → + ∃∃b1,V1,T1,T0. V1 Ⓡ↦*[r] V2 & T1 Ⓡ↦*[s] T0 & {b1}@V1.T1 = F1. +#b2 #s #r #F1 #V2 #T2 #H +elim (pl_sts_inv_trans … H) -H #F #HF1 #H +elim (pl_sts_inv_sn_appl_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +#b #V #T #HV2 #H destruct +elim (pl_sts_inv_dx_appl_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) +#T1 #HT1 #H destruct /2 width=7/ +qed-. + theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s. #s elim s -s // #p1 * // #p2 #s #IHs #F1 #F2 #H @@ -124,57 +165,72 @@ lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/ qed-. lemma pl_sts_fwd_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → - (∃r2. rc:::r2 = s) ∨ ∃∃r1,r2. r1@◊::rc:::r2 = s. + ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s. #b2 #s #F1 #T2 #H lapply (pl_sts_fwd_is_standard … H) @(lstar_ind_l … s F1 H) -s -F1 -[ #_ @or_introl @(ex_intro … ◊) // (**) (* auto needs some help here *) -| * [ | * #p ] #s #F1 #F #HF1 #HF #IHF #Hs +[ #_ @(ex2_2_intro … ◊ ◊) // (**) (* auto needs some help here *) +| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs lapply (is_standard_fwd_cons … Hs) #H - elim (IHF H) -IHF -H * [2,4,6,8: #r1 ] #r2 #H destruct -(* case 1: ◊, @ *) + elim (IHF1 ?) // -IHF1 -H #r1 #r2 #Hr1 #H destruct + elim (in_whd_or_in_inner p) #Hp [ -Hs -F1 -F -T2 -b2 - @or_intror @(ex1_2_intro … (◊::r1) r2) // (**) (* auto needs some help here *) -(* case 2: rc, @ *) - | -F1 -F -T2 -b2 - lapply (is_standard_fwd_sle … Hs) -Hs #H - lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct -(* case 3: sn, @ *) - | -F1 -F -T2 -b2 - lapply (is_standard_fwd_sle … Hs) -Hs #H - lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct -(* case 4: dx, @ *) - | -Hs -F1 -F -T2 -b2 - @or_intror @(ex1_2_intro … ((dx::p)::r1) r2) // (**) (* auto needs some help here *) -(* case 5: ◊, no @ *) - | -Hs -F1 -F -T2 -b2 - @or_intror @(ex1_2_intro … ◊ r2) // (**) (* auto needs some help here *) -(* case 6, rc, no @ *) - | -Hs -F1 -F -T2 -b2 - @or_introl @(ex_intro … (p::r2)) // (**) (* auto needs some help here *) -(* case 7: sn, no @ *) - | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *) - #b #T #_ #HT -Hs -T2 - elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) - #c #V1 #V #T0 #_ #_ #HT0 -c -V1 -F1 destruct -(* case 8: dx, no @ *) - | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *) - #b #T #_ #HT -Hs -T2 - elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) - #c #V #T1 #T0 #_ #_ #HT0 -T1 -F1 destruct + @(ex2_2_intro … (p::r1) r2) // /2 width=1/ (**) (* auto needs some help here *) + | lapply (is_standard_fwd_append_sn (p::r1) ? Hs) -Hs #H + lapply (is_standard_fwd_in_inner … H ?) -H // #H + lapply (is_whd_is_inner_inv … Hr1 ?) -Hr1 // -H #H destruct + elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp +(* case 1: dx *) + [ -IHq + elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *) + #b #T #_ #HT -T2 + elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) + #c #V #T1 #T0 #_ #_ #HT0 -q -T1 -F1 destruct +(* case 2: rc *) + | destruct -F1 -F -T2 -b2 + @(ex2_2_intro … ◊ (q::r2)) // (**) (* auto needs some help here *) +(* case 3: sn *) + | elim (pl_sts_inv_rc_abst_dx … HF2 ??) -b2 [3: // |2: skip ] (**) (* simplify line *) + #b #T #_ #HT -T2 + elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *) + #c #V1 #V #T0 #_ #_ #HT0 -c -q -V1 -F1 destruct + ] ] ] qed-. -lemma pl_sts_fwd_abst_dx_is_whd: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → - ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s. -#b2 #s #F1 #T2 #H +lemma pl_sts_fwd_appl_dx: ∀b2,s,F1,V2,T2. F1 Ⓡ↦*[s] {b2}@V2.T2 → + ∃∃r1,r2,r3. is_whd r1 & is_inner r2 & + r1@(dx:::r2)@sn:::r3 = s. +#b2 #s #F1 #V2 #T2 #H lapply (pl_sts_fwd_is_standard … H) -elim (pl_sts_fwd_abst_dx … H) -b2 -F1 -T2 * [ | #r1 ] #r2 #Hs destruct -[ #_ @(ex2_2_intro … ◊ r2) // -| <(associative_append … r1 (◊::◊) (rc:::r2)) #Hs - lapply (is_standard_fwd_append_sn … Hs) -Hs #H - lapply (is_standard_fwd_is_whd … H) -H // /4 width=4/ +@(lstar_ind_l … s F1 H) -s -F1 +[ #_ @(ex3_3_intro … ◊ ◊ ◊) // (**) (* auto needs some help here *) +| #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs + lapply (is_standard_fwd_cons … Hs) #H + elim (IHF1 ?) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct + elim (in_whd_or_in_inner p) #Hp + [ -Hs -F1 -F -V2 -T2 -b2 + @(ex3_3_intro … (p::r1) r2 r3) // /2 width=1/ (**) (* auto needs some help here *) + | lapply (is_standard_fwd_append_sn (p::r1) ? Hs) -Hs #H + lapply (is_standard_fwd_in_inner … H ?) -H // #H + lapply (is_whd_is_inner_inv … Hr1 ?) -Hr1 // -H #H destruct + elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp +(* case 1: dx *) + [ destruct -F1 -F -V2 -T2 -b2 + @(ex3_3_intro … ◊ (q::r2) r3) // /2 width=1/ (**) (* auto needs some help here *) +(* case 2: rc *) + | -Hr2 + elim (pl_sts_fwd_dx_sn_appl_dx … HF2) -b2 #b #V #T #T0 #_ #_ #HT -V2 -T2 -T0 + elim (pl_st_inv_rc … HF1 … Hp) -HF1 #c #V0 #T0 #_ #_ #HT0 -c -V0 -q -F1 destruct +(* case 3: sn *) + | -Hr2 + elim (pl_sts_fwd_dx_sn_appl_dx … HF2) -b2 #b #V #T #T0 #_ #HT0 #HT -V2 -T2 + elim (pl_st_inv_sn … HF1 … Hp) -HF1 #c #V1 #V0 #T1 #_ #_ #H -c -V1 -F1 destruct -V + elim (pl_sts_inv_empty … HT0) -HT0 #H #_ -T0 -T1 destruct + @(ex3_3_intro … ◊ ◊ (q::r3)) // (**) (* auto needs some help here *) + ] + ] ] qed-. @@ -190,7 +246,7 @@ axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → >carrier_boolean in HF; #H destruct normalize /2 width=3/ | #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct - elim (pl_sts_fwd_abst_dx_is_whd … HM1) #r1 #r2 #Hr1 #H destruct + elim (pl_sts_fwd_abst_dx … HM1) #r1 #r2 #Hr1 #H destruct elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *) @@ -200,10 +256,22 @@ axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → <(map_cons_append … r2 (p::◊)) #H lapply (is_standard_inv_compatible_rc … H) -H #H elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H - @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *) -(* - elim (carrier_inv_appl … HF) -HF #b1 #V #G #HV #HG #HF -*) + @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *) +| #p #B1 #B2 #A #_ #IHB12 #F #HF #s #M1 #HM1 #Hs + elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct + elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #_ #H destruct + elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT + elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct + elim (pl_sts_fwd_dx_sn_appl_dx … HT) -HT #b0 #V0 #T0 #T1 #HV0 #_ #H -T1 + elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #H #_ #_ -b0 -M0 -T0 destruct + >associative_append in Hs; #Hs + lapply (is_standard_fwd_append_dx … Hs) -r1 #Hs + >associative_append in Hs; #Hs + lapply (is_standard_fwd_append_dx … Hs) -r2 + <(map_cons_append … r3 (p::◊)) #H + lapply (is_standard_inv_compatible_sn … H) -H #H + elim (IHB12 … HV0 ?) // -r3 -B0 -IHB12 #F2 #HF2 #H + @(ex2_intro … ({⊥}@F2.{⊥}⇕T)) normalize // /2 width=1/ (**) (* auto needs some help here *) *) theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s → ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2. diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma index cdbe979a5..e18c1d405 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma @@ -170,16 +170,16 @@ lemma pl_st_dsubst: ∀p. sdsubstable_f_dx … (booleanized ⊥) (pl_st p). ] qed. -lemma pl_st_inv_empty: ∀p,G1,G2. G1 Ⓡ↦[p] G2 → ∀F1. {⊥}⇕F1 = G1 → ⊥. +lemma pl_st_inv_empty: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ∀M1. {⊥}⇑M1 = F1 → ⊥. #p #F1 #F2 #H elim H -p -F1 -F2 -[ #V #T #F1 #H - elim (booleanized_inv_appl … H) -H #c #W #U #H destruct -| #b #p #T1 #T2 #_ #IHT12 #F1 #H - elim (booleanized_inv_abst … H) -H /2 width=2/ -| #b #p #V1 #V2 #T #_ #IHV12 #F1 #H - elim (booleanized_inv_appl … H) -H /2 width=2/ -| #b #p #V #T1 #T2 #_ #IHT12 #F1 #H - elim (booleanized_inv_appl … H) -H /2 width=2/ +[ #V #T #M1 #H + elim (boolean_inv_appl … H) -H #B #A #H destruct +| #b #p #T1 #T2 #_ #IHT12 #M1 #H + elim (boolean_inv_abst … H) -H /2 width=2/ +| #b #p #V1 #V2 #T #_ #IHV12 #M1 #H + elim (boolean_inv_appl … H) -H /2 width=2/ +| #b #p #V #T1 #T2 #_ #IHT12 #M1 #H + elim (boolean_inv_appl … H) -H /2 width=2/ ] qed-. diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma index 7105c519f..1993d056b 100644 --- a/matita/matita/contribs/lambda/paths/path.ma +++ b/matita/matita/contribs/lambda/paths/path.ma @@ -34,7 +34,16 @@ definition is_dx: predicate step ≝ λo. dx = o. (* Note: this is a path in the tree representation of a term, heading to a redex *) definition path: Type[0] ≝ list step. -(* Note: a redex is "in whd" when is not under an abstraction nor in the lefr argument of an application *) +definition compatible_rc: predicate (path→relation term) ≝ λR. + ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2). + +definition compatible_sn: predicate (path→relation term) ≝ λR. + ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A). + +definition compatible_dx: predicate (path→relation term) ≝ λR. + ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2). + +(* Note: a redex is "in the whd" when is not under an abstraction nor in the left argument of an application *) definition in_whd: predicate path ≝ All … is_dx. lemma in_whd_ind: ∀R:predicate path. R (◊) → @@ -44,11 +53,42 @@ lemma in_whd_ind: ∀R:predicate path. R (◊) → #p #IHp * #H1 #H2 destruct /3 width=1/ qed-. -definition compatible_rc: predicate (path→relation term) ≝ λR. - ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2). +(* Note: a redex is "inner" when is not in the whd *) +definition in_inner: predicate path ≝ λp. in_whd p → ⊥. -definition compatible_sn: predicate (path→relation term) ≝ λR. - ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A). +lemma in_inner_rc: ∀p. in_inner (rc::p). +#p * normalize #H destruct +qed. -definition compatible_dx: predicate (path→relation term) ≝ λR. - ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2). +lemma in_inner_sn: ∀p. in_inner (sn::p). +#p * normalize #H destruct +qed. + +lemma in_inner_cons: ∀o,p. in_inner p → in_inner (o::p). +#o #p #H1p * /2 width=1/ +qed. + +lemma in_inner_inv_dx: ∀p. in_inner (dx::p) → in_inner p. +/3 width=1/ +qed-. + +lemma in_whd_or_in_inner: ∀p. in_whd p ∨ in_inner p. +#p elim p -p /2 width=1/ #o #p * #Hp /3 width=1/ cases o -o /2 width=1/ /3 width=1/ +qed-. + +lemma in_inner_ind: ∀R:predicate path. + (∀p. R (rc::p)) → (∀p. R (sn::p)) → + (∀p. in_inner p → R p → R (dx::p)) → + ∀p. in_inner p → R p. +#R #H1 #H2 #IH #p elim p -p +[ #H elim (H ?) -H // +| * #p #IHp // #H + lapply (in_inner_inv_dx … H) -H /3 width=1/ +] +qed-. + +lemma in_inner_inv: ∀p. in_inner p → + ∨∨ ∃q. rc::q = p | ∃q. sn::q = p + | ∃∃q. in_inner q & dx::q = p. +@in_inner_ind /3 width=2/ /3 width=3/ +qed-. diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma index 672ba56f1..5ff11ea34 100644 --- a/matita/matita/contribs/lambda/paths/standard_order.ma +++ b/matita/matita/contribs/lambda/paths/standard_order.ma @@ -73,6 +73,19 @@ lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1. ] qed-. +lemma sle_inv_dx: ∀p,q. p ≤ q → ∀q0. dx::q0 = q → + in_whd p ∨ ∃∃p0. p0 ≤ q0 & dx::p0 = p. +#p #q #H @(star_ind_l … p H) -p [ /3 width=3/ ] +#p0 #p #Hp0 #_ #IHpq #q1 #H destruct +elim (IHpq ??) -IHpq [4: // |3: skip ] (**) (* simplify line *) +[ lapply (sprec_fwd_in_whd … Hp0) -Hp0 /3 width=1/ +| * #p1 #Hpq1 #H elim (sprec_inv_dx … Hp0 … H) -p + [ #H destruct /2 width=1/ + | * /4 width=3/ + ] +] +qed-. + lemma sle_inv_rc: ∀p,q. p ≤ q → ∀p0. rc::p0 = p → (∃∃q0. p0 ≤ q0 & rc::q0 = q) ∨ ∃q0. sn::q0 = q. @@ -113,3 +126,7 @@ qed-. lemma sle_fwd_in_whd: ∀p,q. p ≤ q → in_whd q → in_whd p. #p #q #H @(star_ind_l … p H) -p // /3 width=3 by sprec_fwd_in_whd/ qed-. + +lemma sle_fwd_in_inner: ∀p,q. p ≤ q → in_inner p → in_inner q. +/3 width=3 by sle_fwd_in_whd/ +qed-. diff --git a/matita/matita/contribs/lambda/paths/standard_precedence.ma b/matita/matita/contribs/lambda/paths/standard_precedence.ma index e67a96d04..a4ff9e9fb 100644 --- a/matita/matita/contribs/lambda/paths/standard_precedence.ma +++ b/matita/matita/contribs/lambda/paths/standard_precedence.ma @@ -40,6 +40,17 @@ lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p → ] qed-. +lemma sprec_inv_dx: ∀p,q. p ≺ q → ∀q0. dx::q0 = q → + ◊ = p ∨ ∃∃p0. p0 ≺ q0 & dx::p0 = p. +#p #q * -p -q +[ #o #q #q0 #H destruct /2 width=1/ +| #p #q #q0 #H destruct +| #p #q #q0 #H destruct +| #o #p #q #Hpq #q0 #H destruct /3 width=3/ +| #q0 #H destruct +] +qed-. + lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p → (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨ ∃q0. sn::q0 = q. @@ -70,3 +81,7 @@ lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p. | #o #p #q #_ #IHpq * #H destruct /3 width=1/ ] qed-. + +lemma sprec_fwd_in_inner: ∀p,q. p ≺ q → in_inner p → in_inner q. +/3 width=3 by sprec_fwd_in_whd/ +qed-. diff --git a/matita/matita/contribs/lambda/paths/standard_trace.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma index 379c85f37..edc77df25 100644 --- a/matita/matita/contribs/lambda/paths/standard_trace.ma +++ b/matita/matita/contribs/lambda/paths/standard_trace.ma @@ -61,6 +61,15 @@ elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) ] qed-. +lemma is_standard_inv_compatible_dx: ∀s. is_standard (dx:::s) → + is_inner s → is_standard s. +#s elim s -s // #a1 * // #a2 #s #IHs * #H +elim (sle_inv_dx … H ??) -H [4: // |3: skip ] (**) (* simplify line *) +[ * #_ #H1a1 #_ * #H2a1 #_ -IHs + elim (H2a1 ?) -H2a1 -a2 -s // +| * #a #Ha2 #H destruct #H * #_ /3 width=1/ +qed-. + lemma is_standard_fwd_sle: ∀s2,p2,s1,p1. is_standard ((p1::s1)@(p2::s2)) → p1 ≤ p2. #s2 #p2 #s1 elim s1 -s1 [ #p1 * // @@ -90,3 +99,8 @@ lapply (is_standard_fwd_cons … H) lapply (is_standard_fwd_sle … H) #Hqp lapply (sle_fwd_in_whd … Hqp Hp) /3 width=1/ qed-. + +lemma is_standard_fwd_in_inner: ∀s,p. is_standard (p::s) → in_inner p → is_inner s. +#s elim s -s // #q #s #IHs #p * #Hpq #Hs #Hp +lapply (sle_fwd_in_inner … Hpq ?) // -p /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda/paths/trace.ma b/matita/matita/contribs/lambda/paths/trace.ma index c8e427e27..d92d25b9b 100644 --- a/matita/matita/contribs/lambda/paths/trace.ma +++ b/matita/matita/contribs/lambda/paths/trace.ma @@ -19,22 +19,6 @@ include "paths/path.ma". (* Policy: trace metavariables: r, s *) definition trace: Type[0] ≝ list path. -(* Note: a "whd" computation contracts just redexes in the whd *) -definition is_whd: predicate trace ≝ All … in_whd. - -lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s). -#s elim s -s // -#p #s #IHs * /3 width=1/ -qed. - -lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). -/2 width=1 by All_append/ -qed. - -lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s. -/2 width=1 by All_inv_append/ -qed-. - definition ho_compatible_rc: predicate (trace→relation term) ≝ λR. ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). @@ -55,3 +39,26 @@ qed. lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R). #R #HR #s #B #A1 #A2 #H @(lstar_ind_l … s A1 H) -s -A1 // /3 width=3/ qed. + +(* Note: a "whd" computation contracts just redexes in the whd *) +definition is_whd: predicate trace ≝ All … in_whd. + +lemma is_whd_dx: ∀s. is_whd s → is_whd (dx:::s). +#s elim s -s // +#p #s #IHs * /3 width=1/ +qed. + +lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). +/2 width=1 by All_append/ +qed. + +lemma is_whd_inv_append: ∀r,s. is_whd (r@s) → is_whd r ∧ is_whd s. +/2 width=1 by All_inv_append/ +qed-. + +(* Note: an "inner" computation contracts just redexes not in the whd *) +definition is_inner: predicate trace ≝ All … in_inner. + +lemma is_whd_is_inner_inv: ∀s. is_whd s → is_inner s → ◊ = s. +* // #p #s * #H1p #_ * #H2p #_ elim (H2p ?) -H2p // +qed-. -- 2.39.2