matita/matita/contribs/lambdadelta/basic_2/etc_2A1/cpr/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-.