]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
b71f25e5138b4877d49073a52009ebe56f38736f
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / lsubs_sfr.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/substitution/lsubs.ma".
16
17 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
18
19 (* bottom element of the refinement *)
20 definition sfr: nat → nat → predicate lenv ≝
21    λd,e. NF_sn … (lsubs d e) (lsubs d e …).
22
23 interpretation
24    "local environment full refinement (substitution)"
25    'SubEqBottom d e L = (sfr d e L).
26
27 (* Basic properties *********************************************************)
28
29 lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
30 #d #e #L #H
31 elim (lsubs_inv_atom2 … H) -H
32 [ #H destruct //
33 | * #H1 #H2 destruct //
34 ]
35 qed.
36
37 lemma sfr_OO: ∀L. ≽ [0, 0] L.
38 // qed.
39
40 lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
41 #L #V #e #HL #K #H
42 elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
43 lapply (HL … HLX) -HL -HLX /2 width=1/
44 qed.
45
46 lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
47 #L #V
48 @(sfr_abbr … 0) //
49 qed.
50
51 lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
52 #I #L #V #d #e #HL #K #H
53 elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
54 lapply (HL … HLX) -HL -HLX /2 width=1/
55 qed.
56
57 (* Basic inversion lemmas ***************************************************)
58
59 lemma sfr_inv_bind: ∀I,L,V,e. ≽ [0, e] L.ⓑ{I}V → 0 < e →
60                     ≽ [0, e - 1] L ∧ I = Abbr.
61 #I #L #V #e #HL #He
62 lapply (HL (L.ⓓV) ?) /2 width=1/ #H
63 elim (lsubs_inv_abbr2 … H ?) -H // #K #_ #H destruct
64 @conj // #L #HKL
65 lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
66 elim (lsubs_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
67 qed-.
68
69 lemma sfr_inv_skip: ∀I,L,V,d,e. ≽ [d, e] L.ⓑ{I}V → 0 < d → ≽ [d - 1, e] L.
70 #I #L #V #d #e #HL #Hd #K #HLK
71 lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
72 elim (lsubs_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
73 qed-.