matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.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/grammar/genv.ma".
  16
  17 (* GLOBAL ENVIRONMENT SLICING ***********************************************)
  18
  19 inductive gdrop (e:nat): relation genv ≝
  20 | gdrop_gt: ∀G. |G| ≤ e → gdrop e G (⋆)
  21 | gdrop_eq: ∀G. |G| = e + 1 → gdrop e G G
  22 | gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. ⓑ{I} V) G2
  23 .
  24
  25 interpretation "global slicing"
  26    'RDrop e G1 G2 = (gdrop e G1 G2).
  27
  28 (* basic inversion lemmas ***************************************************)
  29
  30 lemma gdrop_inv_gt: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
  31 #G1 #G2 #e * -G1 -G2 //
  32 [ #G #H >H -H >commutative_plus #H
  33   lapply (le_plus_to_le_r … 0 H) -H #H
  34   lapply (le_n_O_to_eq … H) -H #H destruct
  35 | #I #G1 #G2 #V #H1 #_ #H2
  36   lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 normalize in ⊢ (? % ? → ?); >commutative_plus #H
  37   lapply (lt_plus_to_lt_l … 0 H) -H #H
  38   elim (lt_zero_false … H)
  39 ]
  40 qed-.
  41
  42 lemma gdrop_inv_eq: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
  43 #G1 #G2 #e * -G1 -G2 //
  44 [ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H
  45   lapply (le_plus_to_le_r … 0 H) -H #H
  46   lapply (le_n_O_to_eq … H) -H #H destruct
  47 | #I #G1 #G2 #V #H1 #_ normalize #H2
  48   <(injective_plus_l … H2) in H1; -H2 #H
  49   elim (lt_refl_false … H)
  50 ]
  51 qed-.
  52
  53 fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. ⓑ{I} V →
  54                        e < |G1| → ⇩[e] G1 ≡ G2.
  55 #I #G #G1 #G2 #V #e * -G -G2
  56 [ #G #H1 #H destruct #H2
  57   lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
  58   lapply (lt_plus_to_lt_l … 0 H) -H #H
  59   elim (lt_zero_false … H)
  60 | #G #H1 #H2 destruct >(injective_plus_l … H1) -H1 #H
  61   elim (lt_refl_false … H)
  62 | #J #G #G2 #W #_ #HG2 #H destruct //
  63 ]
  64 qed.
  65
  66 lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
  67                     ⇩[e] G1. ⓑ{I} V ≡ G2 → e < |G1| → ⇩[e] G1 ≡ G2.
  68 /2 width=5/ qed-.
  69
  70 (* Basic properties *********************************************************)
  71
  72 lemma gdrop_total: ∀e,G1. ∃G2. ⇩[e] G1 ≡ G2.
  73 #e #G1 elim G1 -G1 /3 width=2/
  74 #I #V #G1 * #G2 #HG12
  75 elim (lt_or_eq_or_gt e (|G1|)) #He
  76 [ /3 width=2/
  77 | destruct /3 width=2/
  78 | @ex_intro [2: @gdrop_gt normalize /2 width=1/ | skip ] (**) (* explicit constructor *)
  79 ]
  80 qed.