matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma

   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 include "basic_2/unfold/delift_lift.ma".
  16 include "apps_2/functional/lift.ma".
  17
  18 (* CORE SUBSTITUTION ********************************************************)
  19
  20 let rec fsubst W d U on U ≝ match U with
  21 [ TAtom I     ⇒ match I with
  22   [ Sort _ ⇒ U
  23   | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
  24   | GRef _ ⇒ U
  25   ]
  26 | TPair I V T ⇒ match I with
  27   [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
  28   | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
  29   ]
  30 ].
  31
  32 interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
  33
  34 (* Main properties **********************************************************)
  35
  36 theorem fsubst_delift: ∀K,V,T,L,d.
  37                        ⇩[0, d] L ≡ K. ⓓV → L ⊢ T ▼*[d, 1] ≡ [d ← V] T.
  38 #K #V #T elim T -T
  39 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
  40   elim (lt_or_eq_or_gt i d) #Hid
  41   [ -HLK >(tri_lt ?????? Hid) /3 width=3/
  42   | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *)
  43   | -HLK >(tri_gt ?????? Hid) /3 width=3/
  44   ]
  45 | * /3 width=1/ /4 width=1/
  46 ]
  47 qed.
  48
  49 (* Main inversion properties ************************************************)
  50
  51 theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
  52                            L ⊢ T1 ▼*[d, 1] ≡ T2 → [d ← V] T1 = T2.
  53 #K #V #T1 elim T1 -T1
  54 [ * #i #L #T2 #d #HLK #H
  55   [ -HLK >(delift_inv_sort1 … H) -H //
  56   | elim (lt_or_eq_or_gt i d) #Hid normalize
  57     [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
  58     | destruct
  59       elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
  60       lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
  61       >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
  62     | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
  63     ]
  64   | -HLK >(delift_inv_gref1 … H) -H //
  65   ]
  66 | * #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
  67   [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
  68     <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
  69   | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
  70     <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
  71   ]
  72 ]
  73 qed-.