matita/matita/contribs/lambdadelta/basic_2A/etc/cpr/tpss_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 T1 break ▶ ▶ * [ term 46 d , break term 46 e ] break term 46 T2 )"
  16    non associative with precedence 45
  17    for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
  18
  19 include "basic_2/unfold/tpss_lift.ma".
  20
  21 (* PARALLEL UNFOLD ON TERMS *************************************************)
  22
  23 (* alternative definition of tpss *)
  24 inductive tpssa: nat → nat → lenv → relation term ≝
  25 | tpssa_atom : ∀L,I,d,e. tpssa d e L (⓪{I}) (⓪{I})
  26 | tpssa_subst: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
  27                ⇩[0, i] L ≡ K. ⓓV1 → tpssa 0 (d + e - i - 1) K V1 V2 →
  28                ⇧[0, i + 1] V2 ≡ W2 → tpssa d e L (#i) W2
  29 | tpssa_bind : ∀L,a,I,V1,V2,T1,T2,d,e.
  30                tpssa d e L V1 V2 → tpssa (d + 1) e (L. ⓑ{I} V2) T1 T2 →
  31                tpssa d e L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
  32 | tpssa_flat : ∀L,I,V1,V2,T1,T2,d,e.
  33                tpssa d e L V1 V2 → tpssa d e L T1 T2 →
  34                tpssa d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
  35 .
  36
  37 interpretation "parallel unfold (term) alternative"
  38    'PSubstStarAlt L T1 d e T2 = (tpssa d e L T1 T2).
  39
  40 (* Basic properties *********************************************************)
  41
  42 lemma tpssa_lsubr_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶▶* [d, e] T2 →
  43                          ∀L2. L2 ⊑ [d, e] L1 → L2 ⊢ T1 ▶▶* [d, e] T2.
  44 #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
  45 [ //
  46 | #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
  47   elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
  48 | /4 width=1/
  49 | /3 width=1/
  50 ]
  51 qed.
  52
  53 lemma tpssa_refl: ∀T,L,d,e. L ⊢ T ▶▶* [d, e] T.
  54 #T elim T -T //
  55 #I elim I -I /2 width=1/
  56 qed.
  57
  58 lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 ▶▶* [d, e] T →
  59                        ∀T2. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
  60 #L #T1 #T #d #e #H elim H -L -T1 -T -d -e
  61 [ #L #I #d #e #X #H
  62   elim (tps_inv_atom1 … H) -H // * /2 width=6/
  63 | #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H
  64   lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
  65   lapply (tps_weak … H 0 (d+e) ? ?) -H // #H
  66   elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
  67 | #L #a #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
  68   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
  69   lapply (tps_lsubr_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
  70   lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
  71   lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
  72   lapply (tpssa_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
  73 | #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
  74   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
  75 ]
  76 qed.
  77
  78 lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → L ⊢ T1 ▶▶* [d, e] T2.
  79 #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/
  80 qed.
  81
  82 (* Basic inversion lemmas ***************************************************)
  83
  84 lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
  85 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
  86 qed-.
  87
  88 lemma tpss_ind_alt: ∀R:nat→nat→lenv→relation term.
  89                     (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
  90                     (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
  91                      ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▶* [O, d + e - i - 1] V2 →
  92                      ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L (#i) W2
  93                     ) →
  94                     (∀L,a,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
  95                      L.ⓑ{I}V2 ⊢ T1 ▶* [d + 1, e] T2 → R d e L V1 V2 →
  96                      R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
  97                     ) →
  98                     (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▶* [d, e] V2 →
  99                      L ⊢ T1 ▶* [d, e] T2 → R d e L V1 V2 →
 100                      R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
 101                     ) →
 102                     ∀d,e,L,T1,T2. L ⊢ T1 ▶* [d, e] T2 → R d e L T1 T2.
 103 #R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e
 104 // /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/
 105 qed-.