matita/matita/contribs/lambdadelta/basic_2/relocation/drops_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_2/relocation/rtmap_isfin.ma".
  16 include "basic_2/grammar/lenv_length.ma".
  17 include "basic_2/relocation/drops.ma".
  18
  19 (* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
  20
  21 (* Forward lemmas with length for local environments ************************)
  22
  23 (* Basic_2A1: includes: drop_fwd_length_le4 *)
  24 lemma drops_fwd_length_le4: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → |L2| ≤ |L1|.
  25 #L1 #L2 #c #f #H elim H -L1 -L2 -f /2 width=1 by le_S, le_S_S/
  26 qed-.
  27
  28 (* Basic_2A1: includes: drop_fwd_length_eq1 *)
  29 theorem drops_fwd_length_eq1: ∀L1,K1,c1,c2,f. ⬇*[c1, f] L1 ≡ K1 →
  30                               ∀L2,K2. ⬇*[c2, f] L2 ≡ K2 →
  31                               |L1| = |L2| → |K1| = |K2|.
  32 #L1 #K1 #c1 #c2 #f #HLK1 elim HLK1 -L1 -K1 -f
  33 [ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
  34   #H destruct elim (drops_inv_atom1 … HLK2) -HLK2 //
  35 | #I1 #L1 #K1 #V1 #f #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
  36   #I2 #L2 #V2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
  37   #HLK2 @(IH … HLK2 H12) (**) (* auto fails *)
  38 | #I1 #L1 #K1 #V1 #V2 #f #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
  39   #I2 #L2 #V2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
  40   #K2 #W2 #HLK2 #_ #H destruct
  41   lapply (IH … HLK2 H12) -f /2 width=1 by/ (**) (* full auto fails *)
  42 ]
  43 qed-.
  44
  45 (* forward lemmas with finite colength assignment ***************************)
  46
  47 lemma drops_fwd_fcla: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
  48                       ∃∃n. 𝐂⦃f⦄ ≡ n & |L1| = |L2| + n.
  49 #L1 #L2 #f #H elim H -L1 -L2 -f
  50 [ /4 width=3 by fcla_isid, ex2_intro/
  51 | #I #L1 #L2 #V #f #_ * /3 width=3 by fcla_next, ex2_intro, eq_f/
  52 | #I #L1 #L2 #V1 #V2 #f #_ #_ * /3 width=3 by fcla_push, ex2_intro/
  53 ]
  54 qed-.
  55
  56 (* Basic_2A1: includes: drop_fwd_length *)
  57 lemma drops_fcla_fwd: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
  58                       |L1| = |L2| + n.
  59 #l1 #l2 #f #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
  60 #m #Hm #H <(fcla_mono … Hm … Hn) -f //
  61 qed-.
  62
  63 lemma drops_fwd_fcla_le2: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
  64                           ∃∃n. 𝐂⦃f⦄ ≡ n & n ≤ |L1|.
  65 #L1 #L2 #f #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
  66 qed-.
  67
  68 (* Basic_2A1: includes: drop_fwd_length_le2 *)
  69 lemma drops_fcla_fwd_le2: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
  70                           n ≤ |L1|.
  71 #L1 #L2 #f #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
  72 #m #Hm #H <(fcla_mono … Hm … Hn) -f //
  73 qed-.
  74
  75 lemma drops_fwd_fcla_lt2: ∀L1,I2,K2,V2,f. ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 →
  76                           ∃∃n. 𝐂⦃f⦄ ≡ n & n < |L1|.
  77 #L1 #I2 #K2 #V2 #f #H elim (drops_fwd_fcla … H) -H
  78 #n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
  79 qed-.
  80
  81 (* Basic_2A1: includes: drop_fwd_length_lt2 *)
  82 lemma drops_fcla_fwd_lt2: ∀L1,I2,K2,V2,f,n.
  83                           ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 → 𝐂⦃f⦄ ≡ n →
  84                           n < |L1|.
  85 #L1 #I2 #K2 #V2 #f #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
  86 #m #Hm #H <(fcla_mono … Hm … Hn) -f //
  87 qed-.
  88
  89 (* Basic_2A1: includes: drop_fwd_length_lt4 *)
  90 lemma drops_fcla_fwd_lt4: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n → 0 < n →
  91                           |L2| < |L1|.
  92 #L1 #L2 #f #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
  93 /2 width=1 by lt_minus_to_plus_r/ qed-.
  94
  95 (* Basic_2A1: includes: drop_inv_length_eq *)
  96 lemma drops_inv_length_eq: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → |L1| = |L2| → 𝐈⦃f⦄.
  97 #L1 #L2 #f #H #HL12 elim (drops_fwd_fcla … H) -H
  98 #n #Hn <HL12 -L2 #H lapply (discr_plus_x_xy … H) -H
  99 /2 width=3 by fcla_inv_xp/
 100 qed-.
 101
 102 (* Basic_2A1: includes: drop_fwd_length_eq2 *)
 103 theorem drops_fwd_length_eq2: ∀L1,L2,K1,K2,f. ⬇*[Ⓣ, f] L1 ≡ K1 → ⬇*[Ⓣ, f] L2 ≡ K2 →
 104                               |K1| = |K2| → |L1| = |L2|.
 105 #L1 #L2 #K1 #K2 #f #HLK1 #HLK2 #HL12
 106 elim (drops_fwd_fcla … HLK1) -HLK1 #n1 #Hn1 #H1 >H1 -L1
 107 elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
 108 <(fcla_mono … Hn2 … Hn1) -f //
 109 qed-.
 110
 111 theorem drops_conf_div: ∀L1,L2,f1,f2. ⬇*[Ⓣ, f1] L1 ≡ L2 → ⬇*[Ⓣ, f2] L1 ≡ L2 →
 112                         ∃∃n. 𝐂⦃f1⦄ ≡ n & 𝐂⦃f2⦄ ≡ n.
 113 #L1 #L2 #f1 #f2 #H1 #H2
 114 elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
 115 elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
 116 lapply (injective_plus_r … H) -L2 #H destruct /2 width=3 by ex2_intro/
 117 qed-.
 118
 119 theorem drops_conf_div_fcla: ∀L1,L2,f1,f2,n1,n2.
 120                              ⬇*[Ⓣ, f1] L1 ≡ L2 → ⬇*[Ⓣ, f2] L1 ≡ L2 → 𝐂⦃f1⦄ ≡ n1 → 𝐂⦃f2⦄ ≡ n2 →
 121                              n1 = n2.
 122 #L1 #L2 #f1 #f2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
 123 lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1
 124 lapply (drops_fcla_fwd … Hf2 Hn2) -f2 >H1 -L1
 125 /2 width=1 by injective_plus_r/
 126 qed-.