matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.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/lenv_length.ma".
  16
  17 (* LOCAL ENVIRONMENTS *******************************************************)
  18
  19 let rec append L K on K ≝ match K with
  20 [ LAtom       ⇒ L
  21 | LPair K I V ⇒ (append L K). ⓑ{I} V
  22 ].
  23
  24 interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
  25
  26 (* Basic properties *********************************************************)
  27
  28 lemma append_atom_sn: ∀L. ⋆ @@ L = L.
  29 #L elim L -L normalize //
  30 qed.
  31
  32 lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
  33 #L1 #L2 elim L2 -L2 normalize //
  34 qed.
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  38 axiom discr_lpair_append_xy_x: ∀I,L,K,V. (L @@ K).ⓑ{I}V = L → ⊥.
  39 (*
  40 #I #L #K #V #H
  41 lapply (refl … (|L|)) <H in ⊢ (? ? % ? → ?); -H
  42 normalize >append_length -I -V #H
  43 *)
  44 lemma append_inv_sn: ∀L1,L2,L. L1 @@ L = L2 @@ L → L1 = L2.
  45 #L1 #L2 #L elim L -L normalize //
  46 #L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
  47 qed.
  48
  49 (* Note: lemma 750 *)
  50 lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2.
  51 #L1 elim L1 -L1
  52 [ * normalize //
  53   #L2 #I2 #V2 #L #H
  54   elim (discr_lpair_append_xy_x I2 L L2 V2 ?) //
  55 | #L1 #I1 #V1 #IHL1 * normalize
  56   [ #L #H -IHL1 elim (discr_lpair_append_xy_x … H)
  57   | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *)
  58     -H >e0 /3 width=2/
  59   ]
  60 ]
  61 qed.