]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/subterms/carrier.ma
8936792e2eec1c0ab2ace0ba056d9a406b77156e
[helm.git] / 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.