matita/matita/lib/lambda-delta/reduction/pr_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 "lambda-delta/substitution/lift_main.ma".
  16 include "lambda-delta/substitution/subst_defs.ma".
  17 include "lambda-delta/reduction/pr_defs.ma".
  18
  19 lemma subst_pr: ∀d,e,L,T1,U2. L ⊢ ↓[d,e] T1 ≡ U2 → ∀T2. ↑[d,e] U2 ≡ T2 →
  20                 L ⊢ T1 ⇒ T2.
  21 #d #e #L #T1 #U2 #H elim H -H d e L T1 U2
  22 [ #L #k #d #e #X #HX
  23   lapply (lift_inv_sort1 … HX) -HX #HX destruct -X //
  24 | #L #i #d #e #Hid #X #HX
  25   lapply (lift_inv_lref1_lt … HX Hid) -HX #HX destruct -X //
  26 | #L #K #V #U1 #U2 #i #d #e #Hdi #Hide #HLK #_ #HU12 #IHVU1 #U #HU2
  27   lapply (lift_trans_be … HU12 … HU2 ? ?) // -HU12 HU2 U2 #HU1
  28   elim (lift_free … HU1 0 (d+e-i-1) ? ? ?) -HU1 // #U2 #HU12 >arith6 // #HU2
  29   @pr_delta [4,5,6: /2/ |1,2,3: skip ] (**) (* /2/ *)
  30 | #L #i #d #e #Hdei #X #HX
  31   lapply (lift_inv_lref1_ge … HX ?) -HX /2/ #HX destruct -X;
  32   >arith7 /2/
  33 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  34   elim (lift_inv_bind1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
  35 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
  36   elim (lift_inv_flat1 … HX) -HX #V #T #HV2 #HT2 #HX destruct -X /3/
  37 ]
  38 qed.
  39 (*
  40 lemma pr_subst_pr: ∀L,T1,T. L ⊢ T1 ⇒ T → ∀d,e,U. L ⊢ ↓[d,e] T ≡ U →
  41                    ∀T2. ↑[d,e] U ≡ T2 → L ⊢ T1 ⇒ T2.
  42 #L #T1 #T #H elim H -H L T1 T
  43 [ /2 width=5/
  44 | /2 width=5/
  45 | #L #I #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
  46   elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
  47   elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
  48   @pr_bind /2 width=5/ @IHT12
  49 | #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
  50   elim (subst_inv_flat1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
  51   elim (lift_inv_flat1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
  52   /3 width=5/
  53 | #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X2 #HX2 #X1 #HX1
  54   elim (subst_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #H destruct -X2;
  55   elim (lift_inv_bind1 … HX1) -HX1 #V4 #T4 #HV34 #HT34 #H destruct -X1;
  56   @pr_beta /2 width=5/ @IHT12
  57 | #L #K #V1 #V2 #V #i #HLK #HV12 #HV2 #IHV12 #d #e #U #HVU #U0 #HU0
  58   lapply (lift_free … HU0 0 (i + 1 + e) ? ? ?) //
  59
  60
  61   @pr_delta [4: // |1,2: skip |6:
  62 *)