matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.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/tpss_lift.ma".
  16 include "basic_2/unfold/delift.ma".
  17
  18 (* DELIFT ON TERMS **********************************************************)
  19
  20 (* Advanced forward lemmas **************************************************)
  21
  22 lemma delift_fwd_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → i < d → U2 = #i.
  23 #L #U2 #i #d #e * #U #HU #HU2 #Hid
  24 elim (tpss_inv_lref1 … HU) -HU
  25 [ #H destruct >(lift_inv_lref2_lt … HU2) //
  26 | * #K #V1 #V2 #Hdi
  27   lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
  28   elim (lt_refl_false … Hi)
  29 ]
  30 qed-.
  31
  32 lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
  33                            d ≤ i → i < d + e →
  34                            ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
  35                                       K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
  36                                       ⇧[0, d] V2 ≡ U2.
  37 #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
  38 elim (tpss_inv_lref1 … HU) -HU
  39 [ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
  40 | * #K #V1 #V #_ #_ #HLK #HV1 #HVU
  41   elim (lift_div_be … HVU … HU2 ? ?) -U // /2 width=1/ /3 width=6/
  42 ]
  43 qed-.
  44
  45 lemma delift_fwd_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 →
  46                            d + e ≤ i → U2 = #(i - e).
  47 #L #U2 #i #d #e * #U #HU #HU2 #Hdei
  48 elim (tpss_inv_lref1 … HU) -HU
  49 [ #H destruct >(lift_inv_lref2_ge … HU2) //
  50 | * #K #V1 #V2 #_ #Hide
  51   lapply (lt_to_le_to_lt … Hide Hdei) -Hide -Hdei #Hi
  52   elim (lt_refl_false … Hi)
  53 ]
  54 qed-.