matita/matita/contribs/lambdadelta/basic_2A/substitution/gget.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_2A/notation/relations/rdrop_3.ma".
  16 include "basic_2A/grammar/genv.ma".
  17
  18 (* GLOBAL ENVIRONMENT READING ***********************************************)
  19
  20 inductive gget (m:nat): relation genv ≝
  21 | gget_gt: ∀G. |G| ≤ m → gget m G (⋆)
  22 | gget_eq: ∀G. |G| = m + 1 → gget m G G
  23 | gget_lt: ∀I,G1,G2,V. m < |G1| → gget m G1 G2 → gget m (G1. ⓑ{I} V) G2
  24 .
  25
  26 interpretation "global reading"
  27    'RDrop m G1 G2 = (gget m G1 G2).
  28
  29 (* basic inversion lemmas ***************************************************)
  30
  31 lemma gget_inv_gt: ∀G1,G2,m. ⬇[m] G1 ≡ G2 → |G1| ≤ m → G2 = ⋆.
  32 #G1 #G2 #m * -G1 -G2 //
  33 [ #G #H >H -H >commutative_plus #H (**) (* lemma needed here *)
  34   lapply (le_plus_to_le_r … 0 H) -H #H
  35   lapply (le_n_O_to_eq … H) -H #H destruct
  36 | #I #G1 #G2 #V #H1 #_ #H2
  37   lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 normalize in ⊢ (? % ? → ?); >commutative_plus #H
  38   lapply (lt_plus_to_lt_l … 0 H) -H #H
  39   elim (lt_zero_false … H)
  40 ]
  41 qed-.
  42
  43 lemma gget_inv_eq: ∀G1,G2,m. ⬇[m] G1 ≡ G2 → |G1| = m + 1 → G1 = G2.
  44 #G1 #G2 #m * -G1 -G2 //
  45 [ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H (**) (* lemma needed here *)
  46   lapply (le_plus_to_le_r … 0 H) -H #H
  47   lapply (le_n_O_to_eq … H) -H #H destruct
  48 | #I #G1 #G2 #V #H1 #_ normalize #H2
  49   <(injective_plus_l … H2) in H1; -H2 #H
  50   elim (lt_refl_false … H)
  51 ]
  52 qed-.
  53
  54 fact gget_inv_lt_aux: ∀I,G,G1,G2,V,m. ⬇[m] G ≡ G2 → G = G1. ⓑ{I} V →
  55                       m < |G1| → ⬇[m] G1 ≡ G2.
  56 #I #G #G1 #G2 #V #m * -G -G2
  57 [ #G #H1 #H destruct #H2
  58   lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
  59   lapply (lt_plus_to_lt_l … 0 H) -H #H
  60   elim (lt_zero_false … H)
  61 | #G #H1 #H2 destruct >(injective_plus_l … H1) -H1 #H
  62   elim (lt_refl_false … H)
  63 | #J #G #G2 #W #_ #HG2 #H destruct //
  64 ]
  65 qed-.
  66
  67 lemma gget_inv_lt: ∀I,G1,G2,V,m.
  68                     ⬇[m] G1. ⓑ{I} V ≡ G2 → m < |G1| → ⬇[m] G1 ≡ G2.
  69 /2 width=5 by gget_inv_lt_aux/ qed-.
  70
  71 (* Basic properties *********************************************************)
  72
  73 lemma gget_total: ∀m,G1. ∃G2. ⬇[m] G1 ≡ G2.
  74 #m #G1 elim G1 -G1 /3 width=2 by gget_gt, ex_intro/
  75 #I #V #G1 * #G2 #HG12
  76 elim (lt_or_eq_or_gt m (|G1|)) #Hm
  77 [ /3 width=2 by gget_lt, ex_intro/
  78 | destruct /3 width=2 by gget_eq, ex_intro/
  79 | @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
  80 ]
  81 qed-.