matita/matita/lib/lambda-delta/substitution/tps_tps.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "lambda-delta/substitution/tps_split.ma".
  13
  14 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
  15
  16 (* Main properties **********************************************************)
  17
  18 lemma tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ≫ T → ∀T2. L ⊢ T [d, e] ≫ T2 →
  19                  L ⊢ T1 [d, e] ≫ T2.
  20 #L #T1 #T #d #e #H elim H -L T1 T d e
  21 [ //
  22 | //
  23 | #L #K #V #V1 #V2 #i #d #e #Hdi #Hide #HLK #_ #HV12 #IHV12 #T2 #HVT2
  24   lapply (drop_fwd_drop2 … HLK) #H
  25   elim (tps_inv_lift1_up … HVT2 … H … HV12 ? ? ?) -HVT2 H HV12 // normalize [2: /2/ ] #V #HV1 #HVT2
  26   @tps_subst [4,5,6,8: // |1,2,3: skip | /2/ ]
  27 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  28   elim (tps_inv_bind1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X;
  29   @tps_bind /2/ @IHT12 @(tps_leq_repl … HT2) /2/
  30 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  31   elim (tps_inv_flat1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
  32 ]
  33 qed.
  34
  35 axiom tps_conf: ∀L,T0,d,e,T1. L ⊢ T0 [d, e] ≫ T1 → ∀T2. L ⊢ T0 [d, e] ≫ T2 →
  36                   ∃∃T. L ⊢ T1 [d, e] ≫ T & L ⊢ T2 [d, e] ≫ T.
  37
  38 (*
  39       Theorem subst0_subst0: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
  40                              (u1,u:?; i:?) (subst0 i u u1 u2) ->
  41                              (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
  42
  43       Theorem subst0_subst0_back: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
  44                                   (u1,u:?; i:?) (subst0 i u u2 u1) ->
  45                                   (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t2 t)).
  46
  47 *)