From 835d26af0fdaa835b6aa1b35765cb22fb3590c4b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 Oct 2021 16:42:33 +0200 Subject: [PATCH] partial update in static_2 + propagation of ground library in static_2/relocation begins + additions in ground --- .../ground/relocation/pr_after_ist.ma | 9 ++ .../ground/relocation/pr_after_nat.ma | 43 +++++++++ .../ground/relocation/pr_compose.ma | 14 ++- .../ground/relocation/pr_isi_nat.ma | 33 +++++++ .../ground/relocation/pr_isi_pat.ma | 2 +- .../lambdadelta/ground/relocation/pr_ist.ma | 14 +++ .../ground/relocation/pr_ist_ist.ma | 10 ++ .../lambdadelta/ground/web/ground_src.tbl | 4 +- .../lambdadelta/static_2/relocation/lifts.ma | 95 +++++++++++-------- 9 files changed, 177 insertions(+), 47 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma index f25cd9b51..212888521 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground/relocation/pr_pat_lt.ma". +include "ground/relocation/pr_nat.ma". include "ground/relocation/pr_ist.ma". include "ground/relocation/pr_after_pat.ma". @@ -52,6 +53,14 @@ lemma pr_after_des_ist_pat: /3 width=8 by pr_after_des_pat, ex2_intro/ qed-. +lemma pr_after_des_ist_nat: + ∀f1,l1,l2. @↑❪l1, f1❫ ≘ l2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f → + ∃∃l. @↑❪l2, f2❫ ≘ l & @↑❪l1, f❫ ≘ l. +#f1 #l1 #l2 #H1 #f2 #H2 #f #Hf +elim (pr_after_des_ist_pat … H1 … H2 … Hf) -f1 -H2 +/2 width=3 by ex2_intro/ +qed-. + (* Inversions with pr_ist ***************************************************) (*** after_inv_istot *) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma new file mode 100644 index 000000000..238a9116f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_nat.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/pr_nat.ma". +include "ground/relocation/pr_after_pat.ma". + +(* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************) + +(* Destructions with pr_nat *************************************************) + +lemma pr_after_nat_des (l) (l1): + ∀f. @↑❪l1, f❫ ≘ l → ∀f2,f1. f2 ⊚ f1 ≘ f → + ∃∃l2. @↑❪l1, f1❫ ≘ l2 & @↑❪l2, f2❫ ≘ l. +#l #l1 #f #H1 #f2 #f1 #Hf +elim (pr_after_pat_des … H1 … Hf) -f #i2 #H1 #H2 +/2 width=3 by ex2_intro/ +qed-. + +lemma pr_after_des_nat (l) (l2) (l1): + ∀f1,f2. @↑❪l1, f1❫ ≘ l2 → @↑❪l2, f2❫ ≘ l → + ∀f. f2 ⊚ f1 ≘ f → @↑❪l1, f❫ ≘ l. +/2 width=6 by pr_after_des_pat/ qed-. + +lemma pr_after_des_nat_sn (l1) (l): + ∀f. @↑❪l1, f❫ ≘ l → ∀f1,l2. @↑❪l1, f1❫ ≘ l2 → + ∀f2. f2 ⊚ f1 ≘ f → @↑❪l2, f2❫ ≘ l. +/2 width=6 by pr_after_des_pat_sn/ qed-. + +lemma pr_after_des_nat_dx (l) (l2) (l1): + ∀f,f2. @↑❪l1, f❫ ≘ l → @↑❪l2, f2❫ ≘ l → + ∀f1. f2 ⊚ f1 ≘ f → @↑❪l1, f1❫ ≘ l2. +/2 width=6 by pr_after_des_pat_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma index 0629472e2..4cd185f2a 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "ground/relocation/pr_after.ma". +include "ground/relocation/pr_after_after.ma". -(* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************) +(* FUNCTIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************) corec definition pr_compose: pr_map → pr_map → pr_map. * * #g2 [ #f1 | * * #g1 ] @@ -40,6 +40,7 @@ lemma pr_compose_unfold_push (f2) (f1): ↑(f2∘f1) = (⫯f2)∘(↑f1). <(stream_unfold … ((⫯f2)∘(↑f1))) in ⊢ (???%); // qed. +(*** compose_next *) lemma pr_compose_unfold_next (f2) (f1): ↑(f2∘f1) = (↑f2)∘f1. #f2 #f1 @@ -48,7 +49,8 @@ qed. (* Main constructions *******************************************************) -corec theorem pr_after_compose (f2) (f1): +(*** after_total *) +corec theorem pr_after_total (f2) (f1): f2 ⊚ f1 ≘ f2∘f1. cases (pr_map_split_tl f2)* [ cases (pr_map_split_tl f1) * ] @@ -57,3 +59,9 @@ cases (pr_map_split_tl f2)* | @pr_after_next /2 width=5 by/ ] qed. + +(* Main inversions **********************************************************) + +(*** after_inv_total *) +lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f. +/2 width=4 by pr_after_mono/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma new file mode 100644 index 000000000..655282638 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_nat.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/pr_nat.ma". +include "ground/relocation/pr_isi_pat.ma". + +(* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************) + +(* Advanced constructions with pr_isi and pr_nat ****************************) + +lemma pr_isi_nat (f): (∀l. @↑❪l,f❫ ≘ l) → 𝐈❪f❫. +/2 width=1 by pr_isi_pat/ qed. + +(* Inversions with pr_nat ***************************************************) + +lemma pr_isi_inv_nat (f) (l): 𝐈❪f❫ → @↑❪l,f❫ ≘ l. +/2 width=1 by pr_isi_inv_pat/ qed-. + +(* Destructions with pr_nat *************************************************) + +lemma pr_isi_nat_des (f) (l1) (l2): 𝐈❪f❫ → @↑❪l1,f❫ ≘ l2 → l1 = l2. +/3 width=3 by pr_isi_pat_des, eq_inv_npsucc_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma index 7ee376ea1..9d4997f10 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma @@ -17,7 +17,7 @@ include "ground/relocation/pr_pat_pat_id.ma". (* IDENTITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************) -(* Advanced constructions with pr_isi ***************************************) +(* Advanced constructions with pr_isi and pr_pat ****************************) (*** isid_at *) lemma pr_isi_pat (f): (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma index c1ab3435e..607a16e97 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma @@ -39,6 +39,20 @@ lemma pr_ist_inv_next (g): 𝐓❪g❫ → ∀f. ↑f = g → 𝐓❪f❫. #j #Hg elim (pr_pat_inv_next … Hg … H) -Hg -H /2 width=2 by ex_intro/ qed-. +(* Basic constructions ******************************************************) + +lemma pr_ist_push (f): 𝐓❪f❫ → 𝐓❪⫯f❫. +#f #Hf * +[ /3 width=2 by pr_pat_refl, ex_intro/ +| #i elim (Hf i) -Hf /3 width=8 by pr_pat_push, ex_intro/ +] +qed. + +lemma pr_ist_next (f): 𝐓❪f❫ → 𝐓❪↑f❫. +#f #Hf #i elim (Hf i) -Hf +/3 width=6 by pr_pat_next, ex_intro/ +qed. + (* Constructions with pr_tl *************************************************) (*** istot_tl *) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma index 1d76991d1..0b4a769f8 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma @@ -15,6 +15,7 @@ include "ground/relocation/pr_eq.ma". include "ground/relocation/pr_pat_lt.ma". include "ground/relocation/pr_pat_pat.ma". +include "ground/relocation/pr_nat.ma". include "ground/relocation/pr_ist.ma". (* TOTALITY CONDITION FOR PARTIAL RELOCATION MAPS ***************************) @@ -66,3 +67,12 @@ cases (pr_map_split_tl f2) #H2 lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by pr_pat_next/ ] qed-. + +(* Advanced constructions with pr_nat ***************************************) + +lemma is_pr_nat_dec (f) (l2): 𝐓❪f❫ → Decidable (∃l1. @↑❪l1,f❫ ≘ l2). +#f #l2 #Hf elim (is_pr_pat_dec … (↑l2) Hf) +[ * /3 width=2 by ex_intro, or_introl/ +| #H @or_intror * /3 width=2 by ex_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index a84e3e1a3..da49c6c48 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -35,13 +35,13 @@ table { [ "pr_sdj ( ? ∥ ? )" "pr_sdj_eq" "pr_sdj_isi" * ] [ "pr_sle ( ? ⊆ ? )" "pr_sle_eq" "pr_sle_pushs" "pr_sle_tls" "pr_sle_isi" "pr_sle_isd" "pr_sle_sle" * ] [ "pr_coafter ( ? ~⊚ ? ≘ ? )" "pr_coafter_eq" "pr_coafter_uni_pushs" "pr_coafter_pat_tls" "pr_coafter_nat_tls" "pr_coafter_nat_tls_pushs" "pr_coafter_isi" "pr_coafter_isu" "pr_coafter_ist_isi" "pr_coafter_ist_isf" "pr_coafter_coafter" "pr_coafter_coafter_ist" * ] - [ "pr_after ( ? ⊚ ? ≘ ? )" "pr_after_eq" "pr_after_uni" "pr_after_basic" "pr_after_pat" "pr_after_pat_tls" "pr_after_pat_uni_tls" "pr_after_nat_uni_tls" "pr_after_isi" "pr_after_isu" "pr_after_ist" "pr_after_ist_isi" "pr_after_after" "pr_after_after_ist" * ] + [ "pr_after ( ? ⊚ ? ≘ ? )" "pr_after_eq" "pr_after_uni" "pr_after_basic" "pr_after_pat" "pr_after_pat_tls" "pr_after_pat_uni_tls" "pr_after_nat" "pr_after_nat_uni_tls" "pr_after_isi" "pr_after_isu" "pr_after_ist" "pr_after_ist_isi" "pr_after_after" "pr_after_after_ist" * ] [ "pr_isd ( 𝛀❪?❫ )" "pr_isd_eq" "pr_isd_tl" "pr_isd_nexts" "pr_isd_tls" * ] [ "pr_ist ( 𝐓❪?❫ )" "pr_ist_tls" "pr_ist_isi" "pr_ist_ist" * ] [ "pr_isf ( 𝐅❪?❫ )" "pr_isf_eq" "pr_isf_tl" "pr_isf_pushs" "fr_isf_tls" "pr_ifs_uni" "pr_isf_isu" * ] [ "pr_fcla ( 𝐂❪?❫ ≘ ? )" "pr_fcla_eq" "fcla_uni" "pr_fcla_fcla" * ] [ "pr_isu ( 𝐔❪?❫ )" "pr_isu_tl" "pr_isu_uni" * ] - [ "pr_isi ( 𝐈❪?❫ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" * ] + [ "pr_isi ( 𝐈❪?❫ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ] [ "pr_nat ( @↑❪?,?❫ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ] [ "pr_pat ( @❪?,?❫ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ] [ "pr_basic ( 𝐛❨?,?❩ )" * ] diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index f019c66d6..e88d128d3 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -12,7 +12,14 @@ (* *) (**************************************************************************) -include "ground/relocation/nstream_after.ma". +include "ground/arith/nat_le_plus.ma". +include "ground/relocation/pr_compose.ma". +include "ground/relocation/pr_nat_uni.ma". +include "ground/relocation/pr_isi_nat.ma". +include "ground/relocation/pr_ist_ist.ma". +include "ground/relocation/pr_after_uni.ma". +include "ground/relocation/pr_after_nat.ma". +include "ground/relocation/pr_after_ist.ma". include "static_2/notation/relations/rliftstar_3.ma". include "static_2/notation/relations/rlift_3.ma". include "static_2/syntax/term.ma". @@ -25,7 +32,7 @@ include "static_2/syntax/term.ma". *) inductive lifts: pr_map → relation term ≝ | lifts_sort: ∀f,s. lifts f (⋆s) (⋆s) -| lifts_lref: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2) +| lifts_lref: ∀f,i1,i2. @↑❪i1,f❫ ≘ i2 → lifts f (#i1) (#i2) | lifts_gref: ∀f,l. lifts f (§l) (§l) | lifts_bind: ∀f,p,I,V1,V2,T1,T2. lifts f V1 V2 → lifts (⫯f) T1 T2 → @@ -81,7 +88,7 @@ lemma lifts_inv_sort1: ∀f,Y,s. ⇧*[f] ⋆s ≘ Y → Y = ⋆s. /2 width=4 by lifts_inv_sort1_aux/ qed-. fact lifts_inv_lref1_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀i1. X = #i1 → - ∃∃i2. @❪i1,f❫ ≘ i2 & Y = #i2. + ∃∃i2. @↑❪i1,f❫ ≘ i2 & Y = #i2. #f #X #Y * -f -X -Y [ #f #s #x #H destruct | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/ @@ -94,7 +101,7 @@ qed-. (* Basic_1: was: lift1_lref *) (* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *) lemma lifts_inv_lref1: ∀f,Y,i1. ⇧*[f] #i1 ≘ Y → - ∃∃i2. @❪i1,f❫ ≘ i2 & Y = #i2. + ∃∃i2. @↑❪i1,f❫ ≘ i2 & Y = #i2. /2 width=3 by lifts_inv_lref1_aux/ qed-. fact lifts_inv_gref1_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀l. X = §l → Y = §l. @@ -163,7 +170,7 @@ lemma lifts_inv_sort2: ∀f,X,s. ⇧*[f] X ≘ ⋆s → X = ⋆s. /2 width=4 by lifts_inv_sort2_aux/ qed-. fact lifts_inv_lref2_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀i2. Y = #i2 → - ∃∃i1. @❪i1,f❫ ≘ i2 & X = #i1. + ∃∃i1. @↑❪i1,f❫ ≘ i2 & X = #i1. #f #X #Y * -f -X -Y [ #f #s #x #H destruct | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/ @@ -176,7 +183,7 @@ qed-. (* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *) (* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *) lemma lifts_inv_lref2: ∀f,X,i2. ⇧*[f] X ≘ #i2 → - ∃∃i1. @❪i1,f❫ ≘ i2 & X = #i1. + ∃∃i1. @↑❪i1,f❫ ≘ i2 & X = #i1. /2 width=3 by lifts_inv_lref2_aux/ qed-. fact lifts_inv_gref2_aux: ∀f,X,Y. ⇧*[f] X ≘ Y → ∀l. Y = §l → X = §l. @@ -235,7 +242,7 @@ lemma lifts_inv_flat2: ∀f,I,V2,T2,X. ⇧*[f] X ≘ ⓕ[I]V2.T2 → lemma lifts_inv_atom1: ∀f,I,Y. ⇧*[f] ⓪[I] ≘ Y → ∨∨ ∃∃s. I = Sort s & Y = ⋆s - | ∃∃i,j. @❪i,f❫ ≘ j & I = LRef i & Y = #j + | ∃∃i,j. @↑❪i,f❫ ≘ j & I = LRef i & Y = #j | ∃∃l. I = GRef l & Y = §l. #f * #n #Y #H [ lapply (lifts_inv_sort1 … H) @@ -246,7 +253,7 @@ qed-. lemma lifts_inv_atom2: ∀f,I,X. ⇧*[f] X ≘ ⓪[I] → ∨∨ ∃∃s. X = ⋆s & I = Sort s - | ∃∃i,j. @❪i,f❫ ≘ j & X = #i & I = LRef j + | ∃∃i,j. @↑❪i,f❫ ≘ j & X = #i & I = LRef j | ∃∃l. X = §l & I = GRef l. #f * #n #X #H [ lapply (lifts_inv_sort2 … H) @@ -289,7 +296,7 @@ lemma lifts_inv_pair_xy_y: ∀I,T,V,f. ⇧*[f] ②[I]V.T ≘ T → ⊥. qed-. lemma lifts_inv_push_zero_sn (f): - ∀X. ⇧*[⫯f]#0 ≘ X → #0 = X. + ∀X. ⇧*[⫯f]#𝟎 ≘ X → #(𝟎) = X. #f #X #H elim (lifts_inv_lref1 … H) -H #i #Hi #H destruct lapply (pr_pat_inv_unit_push … Hi ???) -Hi // @@ -300,30 +307,34 @@ lemma lifts_inv_push_succ_sn (f) (i1): ∃∃i2. ⇧*[f]#i1 ≘ #i2 & #(↑i2) = X. #f #i1 #X #H elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct -elim (pr_pat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct +elim (pr_nat_inv_succ_push … Hij) -Hij [|*: // ] #i2 #Hi12 #H destruct /3 width=3 by lifts_lref, ex2_intro/ qed-. (* Inversion lemmas with uniform relocations ********************************) lemma lifts_inv_lref1_uni: ∀l,Y,i. ⇧[l] #i ≘ Y → Y = #(l+i). -#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H /4 width=4 by fr2_nat_mono, eq_f/ +#l #Y #i1 #H elim (lifts_inv_lref1 … H) -H +#i2 #H #H2 destruct +/4 width=4 by pr_nat_mono, eq_f/ qed-. lemma lifts_inv_lref2_uni: ∀l,X,i2. ⇧[l] X ≘ #i2 → - ∃∃i1. X = #i1 & i2 = l + i1. + ∃∃i1. X = #i1 & i1 + l = i2. #l #X #i2 #H elim (lifts_inv_lref2 … H) -H -/3 width=3 by pr_pat_inv_uni, ex2_intro/ +/3 width=3 by pr_nat_inv_uni, ex2_intro/ qed-. -lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(l + i) → X = #i. +lemma lifts_inv_lref2_uni_ge: ∀l,X,i. ⇧[l] X ≘ #(i+l) → X = #i. #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H -#i1 #H1 #H2 destruct /4 width=2 by eq_inv_nplus_bi_sn, eq_f, sym_eq/ +#i1 #H1 #H2 destruct +/4 width=2 by eq_inv_nplus_bi_dx, eq_f/ qed-. lemma lifts_inv_lref2_uni_lt: ∀l,X,i. ⇧[l] X ≘ #i → i < l → ⊥. #l #X #i2 #H elim (lifts_inv_lref2_uni … H) -H -#i1 #_ #H1 #H2 destruct /2 width=4 by nlt_ge_false/ +#i1 #_ #H1 #H2 destruct +/2 width=4 by nlt_ge_false/ qed-. (* Basic forward lemmas *****************************************************) @@ -331,7 +342,7 @@ qed-. (* Basic_2A1: includes: lift_inv_O2 *) lemma lifts_fwd_isid: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → 𝐈❪f❫ → T1 = T2. #f #T1 #T2 #H elim H -f -T1 -T2 -/4 width=3 by pr_isi_pat_des, pr_isi_push, eq_f2, eq_f/ +/4 width=3 by pr_isi_nat_des, pr_isi_push, eq_f2, eq_f/ qed-. (* Basic_2A1: includes: lift_fwd_pair1 *) @@ -381,18 +392,19 @@ lemma lifts_refl: ∀T,f. 𝐈❪f❫ → ⇧*[f] T ≘ T. qed. (* Basic_2A1: includes: lift_total *) -lemma lifts_total: ∀T1,f. ∃T2. ⇧*[f] T1 ≘ T2. +lemma lifts_total: ∀T1,f. 𝐓❪f❫ → ∃T2. ⇧*[f] T1 ≘ T2. #T1 elim T1 -T1 * -/3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/ -[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f -elim (IHV1 f) -IHV1 #V2 #HV12 -[ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/ +/3 width=2 by lifts_sort, lifts_gref, ex_intro/ +[ #i #f #Hf elim (Hf (↑i)) -Hf /3 width=2 by ex_intro, lifts_lref/ ] +[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f #Hf +elim (IHV1 f) -IHV1 // #V2 #HV12 +[ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by pr_ist_push, ex_intro, lifts_bind/ | elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/ ] qed-. -lemma lifts_push_zero (f): ⇧*[⫯f]#0 ≘ #0. -/2 width=1 by lifts_lref/ qed. +lemma lifts_push_zero (f): ⇧*[⫯f]#(𝟎) ≘ #(𝟎). +/3 width=2 by pr_nat_refl, lifts_lref/ qed. lemma lifts_push_lref (f) (i1) (i2): ⇧*[f]#i1 ≘ #i2 → ⇧*[⫯f]#(↑i1) ≘ #(↑i2). #f1 #i1 #i2 #H @@ -411,12 +423,12 @@ lemma lifts_split_trans: ∀f,T1,T2. ⇧*[f] T1 ≘ T2 → ∃∃T. ⇧*[f1] T1 ≘ T & ⇧*[f2] T ≘ T2. #f #T1 #T2 #H elim H -f -T1 -T2 [ /3 width=3 by lifts_sort, ex2_intro/ -| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_pat_des … Hi … Ht) -Hi -Ht +| #f #i1 #i2 #Hi #f1 #f2 #Ht elim (pr_after_nat_des … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht elim (IHV … Ht) elim (IHT (⫯f1) (⫯f2)) -IHV -IHT - /3 width=5 by lifts_bind, after_O2, ex2_intro/ + /3 width=7 by pr_after_refl, ex2_intro, lifts_bind/ | #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f1 #f2 #Ht elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht /3 width=5 by lifts_flat, ex2_intro/ @@ -425,17 +437,18 @@ qed-. (* Note: apparently, this was missing in Basic_2A1 *) lemma lifts_split_div: ∀f1,T1,T2. ⇧*[f1] T1 ≘ T2 → - ∀f2,f. f2 ⊚ f1 ≘ f → + ∀f2. 𝐓❪f2❫ → ∀f. f2 ⊚ f1 ≘ f → ∃∃T. ⇧*[f2] T2 ≘ T & ⇧*[f] T1 ≘ T. #f1 #T1 #T2 #H elim H -f1 -T1 -T2 [ /3 width=3 by lifts_sort, ex2_intro/ -| #f1 #i1 #i2 #Hi #f2 #f #Ht elim (pr_after_des_ist_pat … Hi … Ht) -Hi -Ht +| #f1 #i1 #i2 #Hi #f2 #Hf2 #f #Ht + elim (pr_after_des_ist_nat … Hi … Ht) -Hi -Ht /3 width=3 by lifts_lref, ex2_intro/ | /3 width=3 by lifts_gref, ex2_intro/ -| #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht - elim (IHV … Ht) elim (IHT (⫯f2) (⫯f)) -IHV -IHT - /3 width=5 by lifts_bind, after_O2, ex2_intro/ -| #f1 #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #f #Ht +| #f1 #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #Hf2 #f #Ht + elim (IHV … Ht) elim (IHT (⫯f2) … (⫯f)) -IHV -IHT + /3 width=7 by pr_ist_push, pr_after_refl, ex2_intro, lifts_bind/ +| #f1 #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f2 #Hf2 #f #Ht elim (IHV … Ht) elim (IHT … Ht) -IHV -IHT -Ht /3 width=5 by lifts_flat, ex2_intro/ ] @@ -443,18 +456,18 @@ qed-. (* Basic_1: includes: dnf_dec2 dnf_dec *) (* Basic_2A1: includes: is_lift_dec *) -lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2). +lemma is_lifts_dec: ∀T2,f. 𝐓❪f❫ → Decidable (∃T1. ⇧*[f] T1 ≘ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ] - #i2 #f elim (is_pr_pat_dec f i2) // + #i2 #f #Hf elim (is_pr_nat_dec f i2) // [ * /4 width=3 by lifts_lref, ex_intro, or_introl/ | #H @or_intror * #X #HX elim (lifts_inv_lref2 … HX) -HX /3 width=2 by ex_intro/ ] -| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f - [ elim (IHV2 f) -IHV2 - [ * #V1 #HV12 elim (IHT2 (⫯f)) -IHT2 +| * [ #p ] #I #V2 #T2 #IHV2 #IHT2 #f #Hf + [ elim (IHV2 f) -IHV2 // + [ * #V1 #HV12 elim (IHT2 (⫯f)) -IHT2 /2 width=1 by pr_ist_push/ [ * #T1 #HT12 @or_introl /3 width=2 by lifts_bind, ex_intro/ | -V1 #HT2 @or_intror * #X #H elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/ @@ -462,8 +475,8 @@ lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⇧*[f] T1 ≘ T2). | -IHT2 #HV2 @or_intror * #X #H elim (lifts_inv_bind2 … H) -H /3 width=2 by ex_intro/ ] - | elim (IHV2 f) -IHV2 - [ * #V1 #HV12 elim (IHT2 f) -IHT2 + | elim (IHV2 f) -IHV2 // + [ * #V1 #HV12 elim (IHT2 f) -IHT2 // [ * #T1 #HT12 /4 width=2 by lifts_flat, ex_intro, or_introl/ | -V1 #HT2 @or_intror * #X #H elim (lifts_inv_flat2 … H) -H /3 width=2 by ex_intro/ @@ -477,8 +490,8 @@ qed-. (* Properties with uniform relocation ***************************************) -lemma lifts_uni: ∀n1,n2,T,U. ⇧*[𝐔❨n1❩∘𝐔❨n2❩] T ≘ U → ⇧[n1+n2] T ≘ U. -/3 width=4 by lifts_eq_repl_back, after_inv_total/ qed. +lemma lifts_uni: ∀n1,n2,T,U. ⇧*[𝐮❨n2❩∘𝐮❨n1❩] T ≘ U → ⇧[n1+n2] T ≘ U. +/3 width=4 by lifts_eq_repl_back, pr_after_inv_total/ qed. (* Basic_2A1: removed theorems 14: lifts_inv_nil lifts_inv_cons -- 2.39.2