matita/matita/contribs/lambdadelta/basic_2/syntax/voids.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/notation/functions/voidstar_2.ma".
  16 include "basic_2/syntax/lenv.ma".
  17
  18 (* EXTENSION OF A LOCAL ENVIRONMENT WITH EXCLUSION BINDERS ******************)
  19
  20 rec definition voids (L:lenv) (n:nat) on n: lenv ≝ match n with
  21 [ O ⇒ L | S m ⇒ (voids L m).ⓧ ].
  22
  23 interpretation "extension with exclusion binders (local environment)"
  24    'VoidStar n L = (voids L n).
  25
  26 (* Basic properties *********************************************************)
  27
  28 lemma voids_zero: ∀L. L = ⓧ*[0]L.
  29 // qed.
  30
  31 lemma voids_succ: ∀L,n. (ⓧ*[n]L).ⓧ = ⓧ*[⫯n]L.
  32 // qed.
  33
  34 (* Advanced properties ******************************************************)
  35
  36 lemma voids_next: ∀n,L. ⓧ*[n](L.ⓧ) = ⓧ*[⫯n]L.
  37 #n elim n -n //
  38 qed.
  39
  40 (* Basic inversion lemmas ***************************************************)
  41
  42 lemma voids_atom_inv: ∀K,n. ⓧ*[n]K = ⋆ → ∧∧ ⋆ = K & 0 = n.
  43 #K * /2 width=1 by conj/
  44 #n <voids_succ #H destruct
  45 qed-.
  46
  47 lemma voids_pair_inv: ∀I,K1,K2,V,n. ⓧ*[n]K1 = K2.ⓑ{I}V →
  48                       ∧∧ K2.ⓑ{I}V = K1 & 0 = n.
  49 #I #K1 #K2 #V * /2 width=1 by conj/
  50 #n <voids_succ #H destruct
  51 qed-.
  52
  53 (* Advanced inversion lemmas ************************************************)
  54
  55 lemma voids_inv_atom_sn: ∀n1,K2,n2. ⓧ*[n1]⋆ = ⓧ*[n2]K2 →
  56                          ∧∧ ⓧ*[n1-n2]⋆ = K2 & n2 ≤ n1.
  57 #n1 elim n1 -n1
  58 [ #K2 <voids_zero * /2 width=1 by conj/
  59   #n1 <voids_succ #H destruct
  60 | #n1 #IH #K2 *
  61   [ <voids_zero #H destruct /2 width=1 by conj/
  62   | #n2 <voids_succ <voids_succ >minus_S_S #H
  63     elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
  64     elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
  65   ]
  66 ]
  67 qed-.
  68
  69 lemma voids_inv_pair_sn: ∀I,V,n1,K1,K2,n2. ⓧ*[n1]K1.ⓑ{I}V = ⓧ*[n2]K2 →
  70                          ∧∧ ⓧ*[n1-n2]K1.ⓑ{I}V = K2 & n2 ≤ n1.
  71 #I #V #n1 elim n1 -n1
  72 [ #K1 #K2 <voids_zero * /2 width=1 by conj/
  73   #n1 <voids_succ #H destruct
  74 | #n1 #IH #K1 #K2 *
  75   [ <voids_zero #H destruct /2 width=1 by conj/
  76   | #n2 <voids_succ <voids_succ >minus_S_S #H
  77     elim (destruct_lbind_lbind_aux … H) -H #HK #_ (**) (* destruct lemma needed *)
  78     elim (IH … HK) -IH -HK #H #Hn destruct /3 width=1 by conj, le_S_S/
  79   ]
  80 ]
  81 qed-.
  82
  83 (* Main inversion properties ************************************************)
  84
  85 theorem voids_inj: ∀n. injective … (λL. ⓧ*[n]L).
  86 #n elim n -n //
  87 #n #IH #L1 #L2
  88 <voids_succ <voids_succ #H
  89 elim (destruct_lbind_lbind_aux … H) -H (**) (* destruct lemma needed *)
  90 /2 width=1 by/
  91 qed-.