matita/matita/contribs/lambdadelta/static_2/relocation/lifts_bind.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 "static_2/syntax/ext2.ma".
  16 include "static_2/relocation/lifts.ma".
  17
  18 (* GENERIC RELOCATION FOR BINDERS *******************************************)
  19
  20 definition liftsb: rtmap → relation bind ≝
  21            λf. ext2 (lifts f).
  22
  23 interpretation "generic relocation (binder for local environments)"
  24    'RLiftStar f I1 I2 = (liftsb f I1 I2).
  25
  26 interpretation "uniform relocation (binder for local environments)"
  27    'RLift i I1 I2 = (liftsb (uni i) I1 I2).
  28
  29 (* Basic_inversion lemmas **************************************************)
  30
  31 lemma liftsb_inv_unit_sn (f):
  32       ∀I,Z2. ⇧*[f] BUnit I ≘ Z2 → Z2 = BUnit I.
  33 /2 width=2 by ext2_inv_unit_sn/ qed-.
  34
  35 lemma liftsb_inv_pair_sn (f):
  36       ∀Z2,I,V1. ⇧*[f] BPair I V1 ≘ Z2 →
  37       ∃∃V2. ⇧*[f] V1 ≘ V2 & Z2 = BPair I V2.
  38 /2 width=1 by ext2_inv_pair_sn/ qed-.
  39
  40 lemma liftsb_inv_unit_dx (f):
  41       ∀I,Z1. ⇧*[f] Z1 ≘ BUnit I → Z1 = BUnit I.
  42 /2 width=2 by ext2_inv_unit_dx/ qed-.
  43
  44 lemma liftsb_inv_pair_dx (f):
  45       ∀Z1,I,V2. ⇧*[f] Z1 ≘ BPair I V2 →
  46       ∃∃V1. ⇧*[f] V1 ≘ V2 & Z1 = BPair I V1.
  47 /2 width=1 by ext2_inv_pair_dx/ qed-.
  48
  49 (* Basic properties *********************************************************)
  50
  51 lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⇧*[f] I1 ≘ I2).
  52 #I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
  53 qed-.
  54
  55 lemma liftsb_refl (f):  𝐈❪f❫ → reflexive … (liftsb f).
  56 /3 width=1 by lifts_refl, ext2_refl/ qed.
  57
  58 lemma liftsb_total: ∀I1,f. ∃I2. ⇧*[f] I1 ≘ I2.
  59 * [2: #I #T1 #f elim (lifts_total T1 f) ]
  60 /3 width=2 by ext2_unit, ext2_pair, ex_intro/
  61 qed-.
  62
  63 lemma liftsb_split_trans (f):
  64       ∀I1,I2. ⇧*[f] I1 ≘ I2 → ∀f1,f2. f2 ⊚ f1 ≘ f →
  65       ∃∃I. ⇧*[f1] I1 ≘ I & ⇧*[f2] I ≘ I2.
  66 #f #I1 #I2 * -I1 -I2 /2 width=3 by ext2_unit, ex2_intro/
  67 #I #V1 #V2 #HV12 #f1 #f2 #Hf elim (lifts_split_trans … HV12 … Hf) -f
  68 /3 width=3 by ext2_pair, ex2_intro/
  69 qed-.
  70
  71 (* Basic forward lemmas *****************************************************)
  72
  73 lemma liftsb_fwd_isid (f):
  74       ∀I1,I2. ⇧*[f] I1 ≘ I2 → 𝐈❪f❫ → I1 = I2.
  75 #f #I1 #I2 * -I1 -I2 /3 width=3 by lifts_fwd_isid, eq_f2/
  76 qed-.