matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.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/relocation/lifts.ma".
  16
  17 (* GENERIC RELOCATION FOR TERMS *********************************************)
  18
  19 (* Main properties **********************************************************)
  20
  21 (* Basic_1: includes: lift_gen_lift *)
  22 (* Basic_2A1: includes: lift_div_le lift_div_be *)
  23 theorem lifts_div: ∀T,T2,f2. ⬆*[f2] T2 ≡ T → ∀T1,f. ⬆*[f] T1 ≡ T →
  24                    ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] T1 ≡ T2.
  25 #T #T2 #f2 #H elim H -T -T2 -f2
  26 [ #s #f2 #T1 #f #H >(lifts_inv_sort2 … H) -T1 //
  27 | #i2 #i #f2 #Hi2 #T1 #f #H #f1 #Ht21 elim (lifts_inv_lref2 … H) -H
  28   #i1 #Hi1 #H destruct /3 width=6 by lifts_lref, after_fwd_at1/
  29 | #l #f2 #T1 #f #H >(lifts_inv_gref2 … H) -T1 //
  30 | #p #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H
  31   elim (lifts_inv_bind2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
  32   /4 width=3 by lifts_bind, after_O2/
  33 | #I #W2 #W #U2 #U #f2 #_ #_ #IHW #IHU #T1 #f #H
  34   elim (lifts_inv_flat2 … H) -H #W1 #U1 #HW1 #HU1 #H destruct
  35   /3 width=3 by lifts_flat/
  36 ]
  37 qed-.
  38
  39 (* Basic_1: was: lift1_lift1 (left to right) *)
  40 (* Basic_1: includes: lift_free (left to right) lift_d lift1_xhg (right to left) lift1_free (right to left) *)
  41 (* Basic_2A1: includes: lift_trans_be lift_trans_le lift_trans_ge lifts_lift_trans_le lifts_lift_trans *)
  42 theorem lifts_trans: ∀T1,T,f1. ⬆*[f1] T1 ≡ T → ∀T2,f2. ⬆*[f2] T ≡ T2 →
  43                      ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] T1 ≡ T2.
  44 #T1 #T #f1 #H elim H -T1 -T -f1
  45 [ #s #f1 #T2 #f2 #H >(lifts_inv_sort1 … H) -T2 //
  46 | #i1 #i #f1 #Hi1 #T2 #f2 #H #f #Ht21 elim (lifts_inv_lref1 … H) -H
  47   #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at/
  48 | #l #f1 #T2 #f2 #H >(lifts_inv_gref1 … H) -T2 //
  49 | #p #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H
  50   elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
  51   /4 width=3 by lifts_bind, after_O2/
  52 | #I #W1 #W #U1 #U #f1 #_ #_ #IHW #IHU #T2 #f2 #H
  53   elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
  54   /3 width=3 by lifts_flat/
  55 ]
  56 qed-.
  57
  58 (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *)
  59 theorem lifts_conf: ∀T,T1,f1. ⬆*[f1] T ≡ T1 → ∀T2,f. ⬆*[f] T ≡ T2 →
  60                     ∀f2. f2 ⊚ f1 ≡ f → ⬆*[f2] T1 ≡ T2.
  61 #T #T1 #f1 #H elim H -T -T1 -f1
  62 [ #s #f1 #T2 #f #H >(lifts_inv_sort1 … H) -T2 //
  63 | #i #i1 #f1 #Hi1 #T2 #f #H #f2 #Ht21 elim (lifts_inv_lref1 … H) -H
  64   #i2 #Hi2 #H destruct /3 width=6 by lifts_lref, after_fwd_at2/
  65 | #l #f1 #T2 #f #H >(lifts_inv_gref1 … H) -T2 //
  66 | #p #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H
  67   elim (lifts_inv_bind1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
  68   /4 width=3 by lifts_bind, after_O2/
  69 | #I #W #W1 #U #U1 #f1 #_ #_ #IHW #IHU #T2 #f #H
  70   elim (lifts_inv_flat1 … H) -H #W2 #U2 #HW2 #HU2 #H destruct
  71   /3 width=3 by lifts_flat/
  72 ]
  73 qed-.
  74
  75 (* Advanced proprerties *****************************************************)
  76
  77 (* Basic_2A1: includes: lift_inj *)
  78 lemma lifts_inj: ∀T1,U,f. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
  79 #T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝  … f)
  80 /3 width=6 by lifts_div, lifts_fwd_isid/
  81 qed-.
  82
  83 (* Basic_2A1: includes: lift_mono *)
  84 lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
  85 #T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝  … f)
  86 /3 width=6 by lifts_conf, lifts_fwd_isid/
  87 qed-.