matita/matita/contribs/lambda/subterms/carrier.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 "terms/relocating_substitution.ma".
  16 include "subterms/relocating_substitution.ma".
  17
  18 (* CARRIER (UNDERLYING TERM) ************************************************)
  19
  20 let rec carrier F on F ≝ match F with
  21 [ SVRef _ i   ⇒ #i
  22 | SAbst _ T   ⇒ 𝛌.(carrier T)
  23 | SAppl _ V T ⇒ @(carrier V).(carrier T)
  24 ].
  25
  26 interpretation "carrier (subterms)"
  27    'ProjectDown F = (carrier F).
  28
  29 notation "hvbox(⇓ term 46 F)"
  30    non associative with precedence 46
  31    for @{ 'ProjectDown $F }.
  32
  33 lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
  34 #j * normalize
  35 [ #b #i #H destruct /2 width=2/
  36 | #b #T #H destruct
  37 | #b #V #T #H destruct
  38 ]
  39 qed-.
  40
  41 lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
  42 #C * normalize
  43 [ #b #i #H destruct
  44 | #b #T #H destruct /2 width=4/
  45 | #b #V #T #H destruct
  46 ]
  47 qed-.
  48
  49 lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
  50                         ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
  51 #D #C * normalize
  52 [ #b #i #H destruct
  53 | #b #T #H destruct
  54 | #b #V #T #H destruct /2 width=6/
  55 ]
  56 qed-.
  57
  58 lemma carrier_lift: ∀h,F,d. ⇓ ↑[d, h] F = ↑[d, h] ⇓F.
  59 #h #F elim F -F normalize //
  60 qed.
  61
  62 lemma carrier_dsubst: ∀G,F,d. ⇓ [d ↙ G] F = [d ↙ ⇓G] ⇓F.
  63 #G #F elim F -F [2,3: normalize // ]
  64 #b #i #d elim (lt_or_eq_or_gt i d) #Hid
  65 [ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
  66 | destruct normalize //
  67 | >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
  68 ]
  69 qed.