From 4853e6e91abc124f9e6db1006cd731dbcf5708b9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 18 Jan 2013 23:27:46 +0000 Subject: [PATCH] - paths and left residuals: second case of the equivalence proved! - some additions to lstar and Allr --- .../contribs/lambda/background/preamble.ma | 19 ++++- .../matita/contribs/lambda/background/xoa.ma | 8 ++ .../lambda/background/xoa_notation.ma | 10 +++ .../lambda/paths/labeled_st_computation.ma | 83 +++++++++++++++++++ .../contribs/lambda/paths/standard_order.ma | 12 +++ .../lambda/paths/standard_precedence.ma | 23 +++++ .../contribs/lambda/paths/standard_trace.ma | 18 ++++ matita/matita/contribs/lambda/xoa.conf.xml | 1 + matita/matita/lib/basics/lists/list.ma | 5 ++ matita/matita/lib/basics/lists/lstar.ma | 13 ++- 10 files changed, 190 insertions(+), 2 deletions(-) diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma index 31efafd7e..01874eb72 100644 --- a/matita/matita/contribs/lambda/background/preamble.ma +++ b/matita/matita/contribs/lambda/background/preamble.ma @@ -96,13 +96,30 @@ notation "hvbox(a ::: break l)" right associative with precedence 47 for @{'ho_cons $a $l}. +lemma map_cons_inv_nil: ∀A,a,l1. map_cons A a l1 = ◊ → ◊ = l1. +#A #a * // normalize #a1 #l1 #H destruct +qed-. + +lemma map_cons_inv_cons: ∀A,a,a2,l2,l1. map_cons A a l1 = a2::l2 → + ∃∃a1,l. a::a1 = a2 & a:::l = l2 & a1::l = l1. +#A #a #a2 #l2 * normalize +[ #H destruct +| #a1 #l1 #H destruct /2 width=5/ +] +qed-. + +lemma map_cons_append: ∀A,a,l1,l2. map_cons A a (l1@l2) = + map_cons A a l1 @ map_cons A a l2. +#A #a #l1 elim l1 -l1 // normalize /2 width=1/ +qed. + (* lstar *) (* Note: this cannot be in lib because of the missing xoa quantifier *) lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| → ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2. #A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1 -[ #H elim (lt_refl_false … H) +[ #H elim (lt_refl_false … H) | #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *) ] qed-. diff --git a/matita/matita/contribs/lambda/background/xoa.ma b/matita/matita/contribs/lambda/background/xoa.ma index f18b06ec9..a2f19a6b7 100644 --- a/matita/matita/contribs/lambda/background/xoa.ma +++ b/matita/matita/contribs/lambda/background/xoa.ma @@ -16,6 +16,14 @@ include "basics/pts.ma". +(* multiple existental quantifier (1, 2) *) + +inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ + | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? +. + +interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). + (* multiple existental quantifier (2, 2) *) inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda/background/xoa_notation.ma b/matita/matita/contribs/lambda/background/xoa_notation.ma index 37443443b..240c1dd5d 100644 --- a/matita/matita/contribs/lambda/background/xoa_notation.ma +++ b/matita/matita/contribs/lambda/background/xoa_notation.ma @@ -14,6 +14,16 @@ (* This file was generated by xoa.native: do not edit *********************) +(* multiple existental quantifier (1, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. + (* multiple existental quantifier (2, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" diff --git a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma index 6050696f9..2900f4d38 100644 --- a/matita/matita/contribs/lambda/paths/labeled_st_computation.ma +++ b/matita/matita/contribs/lambda/paths/labeled_st_computation.ma @@ -78,6 +78,19 @@ lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| → /2 width=1 by lstar_inv_pos/ qed-. +lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. rc:::r = s → + ∃∃b1,T1. T1 Ⓡ↦*[r] T2 & {b1}𝛌.T1 = F1. +#b2 #s #F1 #T2 #H @(lstar_ind_l … s F1 H) -s -F1 +[ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=4/ +| #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_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct + elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *) + #b0 #T0 #HT02 #H destruct + lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/ +] +qed-. + lemma pl_sts_lift: ∀s. sliftable (pl_sts s). /2 width=1/ qed. @@ -98,6 +111,10 @@ theorem pl_sts_trans: ltransitive … pl_sts. /2 width=3 by lstar_ltransitive/ qed-. +theorem pl_sts_inv_trans: inv_ltransitive … pl_sts. +/2 width=3 by lstar_inv_ltransitive/ +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 @@ -106,6 +123,61 @@ elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simpli 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. +#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 + lapply (is_standard_fwd_cons … Hs) #H + elim (IHF H) -IHF -H * [2,4,6,8: #r1 ] #r2 #H destruct +(* case 1: ◊, @ *) + [ -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 + ] +] +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 +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/ +] +qed-. + axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M → ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F → is_standard (s@(p::◊)) → @@ -118,6 +190,17 @@ 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_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 *) + elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct + >associative_append in Hs; #Hs + lapply (is_standard_fwd_append_dx … Hs) -r1 + <(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 *) diff --git a/matita/matita/contribs/lambda/paths/standard_order.ma b/matita/matita/contribs/lambda/paths/standard_order.ma index 09d143874..672ba56f1 100644 --- a/matita/matita/contribs/lambda/paths/standard_order.ma +++ b/matita/matita/contribs/lambda/paths/standard_order.ma @@ -73,6 +73,18 @@ lemma sle_dichotomy: ∀p1,p2:path. p1 ≤ p2 ∨ p2 ≤ p1. ] qed-. +lemma sle_inv_rc: ∀p,q. p ≤ q → ∀p0. rc::p0 = p → + (∃∃q0. p0 ≤ q0 & rc::q0 = q) ∨ + ∃q0. sn::q0 = q. +#p #q #H elim H -q /3 width=3/ +#q #q0 #_ #Hq0 #IHpq #p0 #H destruct +elim (IHpq p0 ?) -IHpq // * +[ #p1 #Hp01 #H + elim (sprec_inv_rc … Hq0 … H) -q * /3 width=3/ /4 width=3/ +| #p1 #H elim (sprec_inv_sn … Hq0 … H) -q /3 width=2/ +] +qed-. + lemma sle_inv_sn: ∀p,q. p ≤ q → ∀p0. sn::p0 = p → ∃∃q0. p0 ≤ q0 & sn::q0 = q. #p #q #H elim H -q /2 width=3/ diff --git a/matita/matita/contribs/lambda/paths/standard_precedence.ma b/matita/matita/contribs/lambda/paths/standard_precedence.ma index a55770aa8..e67a96d04 100644 --- a/matita/matita/contribs/lambda/paths/standard_precedence.ma +++ b/matita/matita/contribs/lambda/paths/standard_precedence.ma @@ -40,6 +40,29 @@ lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p → ] qed-. +lemma sprec_inv_rc: ∀p,q. p ≺ q → ∀p0. rc::p0 = p → + (∃∃q0. p0 ≺ q0 & rc::q0 = q) ∨ + ∃q0. sn::q0 = q. +#p #q * -p -q +[ #o #q #p0 #H destruct +| #p #q #p0 #H destruct +| #p #q #p0 #H destruct /3 width=2/ +| #o #p #q #Hpq #p0 #H destruct /3 width=3/ +| #p0 #H destruct +] +qed-. + +lemma sprec_inv_comp: ∀p1,p2. p1 ≺ p2 → + ∀o,q1,q2. o::q1 = p1 → o::q2 = p2 → q1 ≺ q2. +#p1 #p2 * -p1 -p2 +[ #o #q #o0 #q1 #q2 #H destruct +| #p #q #o0 #q1 #q2 #H1 #H2 destruct +| #p #q #o0 #q1 #q2 #H1 #H2 destruct +| #o #p #q #Hpq #o0 #q1 #q2 #H1 #H2 destruct // +| #o0 #q1 #q2 #_ #H destruct +] +qed-. + lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p. #p #q #H elim H -p -q // /2 width=1/ [ #p #q * #H destruct diff --git a/matita/matita/contribs/lambda/paths/standard_trace.ma b/matita/matita/contribs/lambda/paths/standard_trace.ma index 0550ab24f..379c85f37 100644 --- a/matita/matita/contribs/lambda/paths/standard_trace.ma +++ b/matita/matita/contribs/lambda/paths/standard_trace.ma @@ -28,6 +28,10 @@ lemma is_standard_fwd_cons: ∀p,s. is_standard (p::s) → is_standard s. /2 width=2 by Allr_fwd_cons/ qed-. +lemma is_standard_fwd_append_dx: ∀s,r. is_standard (s@r) → is_standard r. +/2 width=2 by Allr_fwd_append_dx/ +qed-. + lemma is_standard_compatible: ∀o,s. is_standard s → is_standard (o:::s). #o #s elim s -s // #p * // #q #s #IHs * /3 width=1/ @@ -43,6 +47,20 @@ lemma is_standard_append: ∀r. is_standard r → ∀s. is_standard s → is_sta #q #r #IHr * /3 width=1/ qed. +lemma is_standard_inv_compatible_sn: ∀s. is_standard (sn:::s) → is_standard s. +#s elim s -s // #a1 * // #a2 #s #IHs * #H +elim (sle_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) +#a #Ha1 #H destruct /3 width=1/ +qed-. + +lemma is_standard_inv_compatible_rc: ∀s. is_standard (rc:::s) → is_standard s. +#s elim s -s // #a1 * // #a2 #s #IHs * #H +elim (sle_inv_rc … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) +[ #a #Ha1 #H destruct /3 width=1/ +| #a #H destruct +] +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 * // diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml index a0d089841..04cbcf59e 100644 --- a/matita/matita/contribs/lambda/xoa.conf.xml +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -8,6 +8,7 @@ xoa xoa_notation basics/pts.ma + 1 2 2 2 2 3 3 1 diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma index 725f57135..8a41a15dc 100644 --- a/matita/matita/lib/basics/lists/list.ma +++ b/matita/matita/lib/basics/lists/list.ma @@ -490,6 +490,11 @@ lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l. #A #R #a * // #a0 #l * // qed-. +lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2. +#A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H +lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/ +qed-. + (**************************** Exists *******************************) let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ diff --git a/matita/matita/lib/basics/lists/lstar.ma b/matita/matita/lib/basics/lists/lstar.ma index 780f7759d..2b9937d1b 100644 --- a/matita/matita/lib/basics/lists/lstar.ma +++ b/matita/matita/lib/basics/lists/lstar.ma @@ -11,11 +11,15 @@ include "basics/lists/list.ma". -(* labelled reflexive and transitive closure ********************************) +(* labeled reflexive and transitive closure *********************************) definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R. ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2. +definition inv_ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ + λA,B,R. ∀l1,l2,b1,b2. R (l1@l2) b1 b2 → + ∃∃b. R l1 b1 b & R l2 b b2. + inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝ | lstar_nil : ∀b. lstar A B R ([]) b b | lstar_cons: ∀a,b1,b. R a b1 b → @@ -79,6 +83,13 @@ theorem lstar_ltransitive: ∀A,B,R. ltransitive … (lstar A B R). #A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/ qed-. +lemma lstar_inv_ltransitive: ∀A,B,R. inv_ltransitive … (lstar A B R). +#A #B #R #l1 elim l1 -l1 normalize /2 width=3/ +#a #l1 #IHl1 #l2 #b1 #b2 #H +elim (lstar_inv_cons … b2 H ???) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *) +elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/ +qed-. + lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 → lstar A B R (l@[a]) b1 b2. #A #B #R #l #b1 #b #H @(lstar_ind_l ????????? H) -l -b1 /2 width=1/ -- 2.39.2