X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Frelocation%2Flifts.ma;h=4ec47cc91e47a93787cc259b65cc02b62541d386;hb=f308429a0fde273605a2330efc63268b4ac36c99;hp=56f69a641cb0256fb81e110d56a1cb7e4970d9f1;hpb=ff612dc35167ec0c145864c9aa8ae5e1ebe20a48;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma index 56f69a641..4ec47cc91 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma @@ -1,4 +1,3 @@ - (**************************************************************************) (* ___ *) (* ||M|| *) @@ -25,7 +24,7 @@ include "static_2/syntax/term.ma". *) inductive lifts: rtmap → 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 → @@ -57,6 +56,14 @@ definition deliftable2_bi: predicate (relation term) ≝ λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 → ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2. +definition liftable2_dx: predicate (relation term) ≝ + λR. ∀T1,T2. R T1 T2 → ∀f,U2. ⬆*[f] T2 ≘ U2 → + ∃∃U1. ⬆*[f] T1 ≘ U1 & R U1 U2. + +definition deliftable2_dx: predicate (relation term) ≝ + λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 → + ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2. + (* Basic inversion lemmas ***************************************************) fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → Y = ⋆s. @@ -73,7 +80,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/ @@ -86,7 +93,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. @@ -155,7 +162,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/ @@ -168,7 +175,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. @@ -227,7 +234,7 @@ lemma lifts_inv_flat2: ∀f:rtmap. ∀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) @@ -238,7 +245,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) @@ -330,6 +337,16 @@ qed-. (* Basic properties *********************************************************) +lemma liftable2_sn_dx (R): symmetric … R → liftable2_sn R → liftable2_dx R. +#R #H2R #H1R #T1 #T2 #HT12 #f #U2 #HTU2 +elim (H1R … T1 … HTU2) -H1R /3 width=3 by ex2_intro/ +qed-. + +lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R. +#R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2 +elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/ +qed-. + lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2). #T1 #T2 #f1 #H elim H -T1 -T2 -f1 /4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/ @@ -357,7 +374,16 @@ elim (IHV1 f) -IHV1 #V2 #HV12 ] qed-. -lemma lift_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i). +lemma lifts_push_zero (f): ⬆*[⫯f]#0 ≘ #0. +/2 width=1 by lifts_lref/ qed. + +lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2). +#f1 #i1 #i2 #H +elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct +/3 width=7 by lifts_lref, at_push/ +qed. + +lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i). #l elim l -l /2 width=1 by lifts_lref/ qed.