matita/matita/contribs/lambdadelta/basic_2/etc_2A1/delift/delift_alt.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 notation "hvbox( L ⊢ break ▼ ▼ * [ term 46 d , break term 46 e ] break term 46 T1 ≡ break term 46 T2 )"
  16    non associative with precedence 45
  17    for @{ 'TSubstAlt $L $T1 $d $e $T2 }.
  18
  19 include "basic_2/unfold/delift_lift.ma".
  20
  21 (* INVERSE BASIC TERM RELOCATION  *******************************************)
  22
  23 (* alternative definition of inverse basic term relocation *)
  24 inductive delifta: nat → nat → lenv → relation term ≝
  25 | delifta_sort   : ∀L,d,e,k. delifta d e L (⋆k) (⋆k)
  26 | delifta_lref_lt: ∀L,d,e,i. i < d → delifta d e L (#i) (#i)
  27 | delifta_lref_be: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
  28                    ⇩[0, i] L ≡ K. ⓓV1 → delifta 0 (d + e - i - 1) K V1 V2 →
  29                    ⇧[0, d] V2 ≡ W2 → delifta d e L (#i) W2
  30 | delifta_lref_ge: ∀L,d,e,i. d + e ≤ i → delifta d e L (#i) (#(i - e))
  31 | delifta_gref   : ∀L,d,e,p. delifta d e L (§p) (§p)
  32 | delifta_bind   : ∀L,a,I,V1,V2,T1,T2,d,e.
  33                    delifta d e L V1 V2 → delifta (d + 1) e (L. ⓑ{I} V2) T1 T2 →
  34                    delifta d e L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
  35 | delifta_flat   : ∀L,I,V1,V2,T1,T2,d,e.
  36                    delifta d e L V1 V2 → delifta d e L T1 T2 →
  37                    delifta d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
  38 .
  39
  40 interpretation "inverse basic relocation (term) alternative"
  41    'TSubstAlt L T1 d e T2 = (delifta d e L T1 T2).
  42
  43 (* Basic properties *********************************************************)
  44
  45 lemma delifta_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ ▼▼*[d, e] T1 ≡ T2 →
  46                            ∀L2. L2 ⊑ [d, e] L1 → L2 ⊢ ▼▼*[d, e] T1 ≡ T2.
  47 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/
  48 [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
  49   elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
  50 | /4 width=1/
  51 | /3 width=1/
  52 ]
  53 qed.
  54
  55 lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼▼*[d, e] T1 ≡ T2.
  56 #L #T1 @(f2_ind … fw … L T1) -L -T1 #n #IH #L *
  57 [ * #i #Hn #T2 #d #e #H destruct
  58   [ >(delift_inv_sort1 … H) -H //
  59   | elim (delift_inv_lref1 … H) -H * /2 width=1/
  60     #K #V1 #V2 #Hdi #Hide #HLK #HV12 #HVT2
  61     lapply (ldrop_pair2_fwd_fw … HLK) #H
  62     lapply (IH … HV12) // -H /2 width=6/
  63   | >(delift_inv_gref1 … H) -H //
  64   ]
  65 | * [ #a ] #I #V1 #T1 #Hn #X #d #e #H
  66   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
  67     lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V1) ?) -HT12 /2 width=1/ #HT12
  68     lapply (IH … HV12) -HV12 // #HV12
  69     lapply (IH … HT12) -IH -HT12 /2 width=1/ #HT12
  70     lapply (delifta_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
  71   | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
  72     lapply (IH … HV12) -HV12 //
  73     lapply (IH … HT12) -IH -HT12 // /2 width=1/
  74   ]
  75 ]
  76 qed.
  77
  78 (* Basic inversion lemmas ***************************************************)
  79
  80 lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
  81 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/
  82 qed-.
  83
  84 lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
  85                       (∀L,d,e,k. R d e L (⋆k) (⋆k)) →
  86                       (∀L,d,e,i. i < d → R d e L (#i) (#i)) →
  87                       (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
  88                        ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ ▼*[O, d + e - i - 1] V1 ≡ V2 →
  89                        ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
  90                       ) →
  91                       (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) →
  92                       (∀L,d,e,p. R d e L (§p) (§p)) →
  93                       (∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 →
  94                        L.ⓑ{I}V2 ⊢ ▼*[d + 1, e] T1 ≡ T2 → R d e L V1 V2 →
  95                        R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
  96                       ) →
  97                       (∀L,I,V1,V2,T1,T2,d,e. L ⊢ ▼*[d, e] V1 ≡ V2 →
  98                        L⊢ ▼*[d, e] T1 ≡ T2 → R d e L V1 V2 →
  99                        R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 100                       ) →
 101                       ∀d,e,L,T1,T2. L ⊢ ▼*[d, e] T1 ≡ T2 → R d e L T1 T2.
 102 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e
 103 // /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/
 104 qed-.