]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/top/lenv_top.etc
- extended multiple substitutions now uses bounds in ynat (ie. they
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / top / lenv_top.etc
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 notation "hvbox( T1 𝟙 break term 46 T2 )"
16    non associative with precedence 45
17    for @{ 'RTop $T1 $T2 }.
18
19 include "basic_2/grammar/lenv_px.ma".
20
21 (* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
22
23 definition ttop: relation term ≝ λT1,T2. True.
24
25 definition ltop: relation lenv ≝ lpx ttop.
26
27 interpretation
28   "top reduction (environment)"
29   'RTop L1 L2 = (ltop L1 L2).
30
31 (* Basic properties *********************************************************)
32
33 lemma ltop_refl: reflexive … ltop.
34 /2 width=1/ qed.
35
36 lemma ltop_sym: symmetric … ltop.
37 /2 width=1/ qed.
38
39 lemma ltop_trans: transitive … ltop.
40 /2 width=3/ qed.
41
42 lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
43 /2 width=1/ qed.
44
45 (* Basic inversion lemmas ***************************************************)
46
47 lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
48 /2 width=2 by lpx_inv_atom1/ qed-.
49
50 lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
51                       ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
52 #K1 #I #V1 #L2 #H
53 elim (lpx_inv_pair1 … H) -H /2 width=4/
54 qed-.
55
56 lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
57 /2 width=2 by lpx_inv_atom2/ qed-.
58
59 lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
60                       ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
61 #L1 #K2 #I #V2 #H
62 elim (lpx_inv_pair2 … H) -H /2 width=4/
63 qed-.
64
65 (* Basic forward lemmas *****************************************************)
66
67 lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
68 /2 width=2 by lpx_fwd_length/ qed-.