matita/matita/contribs/lambdadelta/static_2/syntax/append_length.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 "ground/arith/nat_plus.ma".
  16 include "ground/arith/wf1_ind_nlt.ma".
  17 include "static_2/syntax/lenv_length.ma".
  18 include "static_2/syntax/append.ma".
  19
  20 (* APPEND FOR LOCAL ENVIRONMENTS ********************************************)
  21
  22 (* Properties with length for local environments ****************************)
  23
  24 lemma append_length: ∀L1,L2. |L1 + L2| = |L1| + |L2|.
  25 #L1 #L2 elim L2 -L2 //
  26 #L2 #I >append_bind >length_bind >length_bind //
  27 qed.
  28
  29 lemma ltail_length: ∀I,L. |ⓘ[I].L| = ↑|L|.
  30 #I #L >append_length //
  31 qed.
  32
  33 (* Advanced inversion lemmas on length for local environments ***************)
  34
  35 (* Basic_2A1: was: length_inv_pos_dx_ltail *)
  36 lemma length_inv_succ_dx_ltail: ∀L,n. |L| = ↑n →
  37                                 ∃∃I,K. |K| = n & L = ⓘ[I].K.
  38 #Y #n #H elim (length_inv_succ_dx … H) -H #I #L #Hn #HLK destruct
  39 elim (lenv_case_tail … L) [| * #K #J ] #H destruct
  40 /2 width=4 by ex2_2_intro/
  41 @(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *)
  42 >ltail_length >length_bind //
  43 qed-.
  44
  45 (* Basic_2A1: was: length_inv_pos_sn_ltail *)
  46 lemma length_inv_succ_sn_ltail: ∀L,n. ↑n = |L| →
  47                                 ∃∃I,K. n = |K| & L = ⓘ[I].K.
  48 #Y #n #H elim (length_inv_succ_sn … H) -H #I #L #Hn #HLK destruct
  49 elim (lenv_case_tail … L) [| * #K #J ] #H destruct
  50 /2 width=4 by ex2_2_intro/
  51 @(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *)
  52 >ltail_length >length_bind //
  53 qed-.
  54
  55 (* Inversion lemmas with length for local environments **********************)
  56
  57 (* Basic_2A1: was: append_inj_sn *)
  58 lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |K1| = |K2| →
  59                             ∧∧ L1 = L2 & K1 = K2.
  60 #K1 elim K1 -K1
  61 [ * /2 width=1 by conj/
  62   #K2 #I2 #L1 #L2 #_ >length_atom >length_bind
  63   #H elim (eq_inv_zero_nsucc … H)
  64 | #K1 #I1 #IH *
  65   [ #L1 #L2 #_ >length_atom >length_bind
  66     #H elim (eq_inv_nsucc_zero … H)
  67   | #K2 #I2 #L1 #L2 #H1 >length_bind >length_bind #H2
  68     lapply (eq_inv_nsucc_bi … H2) -H2 #H2
  69     elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *)
  70     elim (IH … H1) -IH -H1 /3 width=4 by conj/
  71   ]
  72 ]
  73 qed-.
  74
  75 (* Note: lemma 750 *)
  76 (* Basic_2A1: was: append_inj_dx *)
  77 lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| →
  78                             ∧∧ L1 = L2 & K1 = K2.
  79 #K1 elim K1 -K1
  80 [ * /2 width=1 by conj/
  81   #K2 #I2 #L1 #L2 >append_atom >append_bind #H destruct
  82   >length_bind >append_length #H
  83   elim (succ_nplus_refl_sn (|L2|) (|K2|) ?) //
  84 | #K1 #I1 #IH *
  85   [ #L1 #L2 >append_bind >append_atom #H destruct
  86     >length_bind >append_length #H
  87     elim (succ_nplus_refl_sn … H)
  88   | #K2 #I2 #L1 #L2 >append_bind >append_bind #H1 #H2
  89     elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *)
  90     elim (IH … H1) -IH -H1 /2 width=1 by conj/
  91   ]
  92 ]
  93 qed-.
  94
  95 (* Advanced inversion lemmas ************************************************)
  96
  97 lemma append_inj_dx: ∀L,K1,K2. L+K1 = L+K2 → K1 = K2.
  98 #L #K1 #K2 #H elim (append_inj_length_dx … H) -H //
  99 qed-.
 100
 101 lemma append_inv_refl_dx: ∀L,K. L+K = L → K = ⋆.
 102 #L #K #H elim (append_inj_dx … (⋆) … H) //
 103 qed-.
 104
 105 lemma append_inv_pair_dx: ∀I,L,K,V. L+K = L.ⓑ[I]V → K = ⋆.ⓑ[I]V.
 106 #I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ[I]V) … H) //
 107 qed-.
 108
 109 (* Basic eliminators ********************************************************)
 110
 111 (* Basic_1: was: c_tail_ind *)
 112 (* Basic_2A1: was: lenv_ind_alt *)
 113 lemma lenv_ind_tail: ∀Q:predicate lenv.
 114                      Q (⋆) → (∀I,L. Q L → Q (ⓘ[I].L)) → ∀L. Q L.
 115 #Q #IH1 #IH2 #L @(wf1_ind_nlt … length … L) -L #x #IHx * //
 116 #L #I -IH1 #H destruct
 117 elim (lenv_case_tail … L) [| * #K #J ]
 118 #H destruct /3 width=1 by/
 119 qed-.