1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "static_2/syntax/lenv_length.ma".
16 include "static_2/relocation/drops.ma".
18 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
20 (* Forward lemmas with length for local environments ************************)
22 (* Basic_2A1: includes: drop_fwd_length_le4 *)
23 lemma drops_fwd_length_le4: ∀b,f,L1,L2. ⇩*[b,f] L1 ≘ L2 → |L2| ≤ |L1|.
24 #b #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by nle_succ_dx, nle_succ_bi/
27 (* Basic_2A1: includes: drop_fwd_length_eq1 *)
28 theorem drops_fwd_length_eq1: ∀b1,b2,f,L1,K1. ⇩*[b1,f] L1 ≘ K1 →
29 ∀L2,K2. ⇩*[b2,f] L2 ≘ K2 →
30 |L1| = |L2| → |K1| = |K2|.
31 #b1 #b2 #f #L1 #K1 #HLK1 elim HLK1 -f -L1 -K1
32 [ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
33 #H destruct elim (drops_inv_atom1 … HLK2) -HLK2 //
34 | #f #I1 #L1 #K1 #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
35 #I2 #L2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
36 #HLK2 @(IH … HLK2 H12) (**) (* auto fails *)
37 | #f #I1 #I2 #L1 #K1 #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
38 #I2 #L2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
39 #I2 #K2 #HLK2 #_ #H destruct
40 lapply (IH … HLK2 H12) -f >length_bind >length_bind /2 width=1 by/ (**) (* full auto fails *)
44 (* forward lemmas with finite colength assignment ***************************)
46 lemma drops_fwd_fcla: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
47 ∃∃n. 𝐂❨f❩ ≘ n & |L1| = |L2| + n.
48 #f #L1 #L2 #H elim H -f -L1 -L2
49 [ /4 width=3 by pr_fcla_isi, ex2_intro/
50 | #f #I #L1 #L2 #_ * >length_bind /3 width=3 by pr_fcla_next, ex2_intro, eq_f/
51 | #f #I1 #I2 #L1 #L2 #_ #_ * >length_bind >length_bind /3 width=3 by pr_fcla_push, ex2_intro/
55 (* Basic_2A1: includes: drop_fwd_length *)
56 lemma drops_fcla_fwd: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n →
58 #f #l1 #l2 #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
59 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
62 lemma drops_fwd_fcla_le2: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
63 ∃∃n. 𝐂❨f❩ ≘ n & n ≤ |L1|.
64 #f #L1 #L2 #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
67 (* Basic_2A1: includes: drop_fwd_length_le2 *)
68 lemma drops_fcla_fwd_le2: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n →
70 #f #L1 #L2 #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
71 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
74 lemma drops_fwd_fcla_lt2: ∀f,L1,I2,K2. ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] →
75 ∃∃n. 𝐂❨f❩ ≘ n & n < |L1|.
76 #f #L1 #I2 #K2 #H elim (drops_fwd_fcla … H) -H
77 #n #Hf #H >H -L1 /3 width=3 by nle_succ_bi, ex2_intro/
80 (* Basic_2A1: includes: drop_fwd_length_lt2 *)
81 lemma drops_fcla_fwd_lt2: ∀f,L1,I2,K2,n.
82 ⇩*[Ⓣ,f] L1 ≘ K2.ⓘ[I2] → 𝐂❨f❩ ≘ n →
84 #f #L1 #I2 #K2 #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
85 #k #Hm #H <(pr_fcla_mono … Hm … Hn) -f //
88 (* Basic_2A1: includes: drop_fwd_length_lt4 *)
89 lemma drops_fcla_fwd_lt4: ∀f,L1,L2,n. ⇩*[Ⓣ,f] L1 ≘ L2 → 𝐂❨f❩ ≘ n → 0 < n →
91 #f #L1 #L2 #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
92 /2 width=1 by nlt_inv_minus_dx/ qed-.
94 (* Basic_2A1: includes: drop_inv_length_eq *)
95 lemma drops_inv_length_eq: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 → |L1| = |L2| → 𝐈❨f❩.
96 #f #L1 #L2 #H #HL12 elim (drops_fwd_fcla … H) -H
97 #n #Hn <HL12 -L2 #H lapply (nplus_refl_sn … H) -H
98 /2 width=3 by pr_fcla_inv_zero/
101 (* Basic_2A1: includes: drop_fwd_length_eq2 *)
102 theorem drops_fwd_length_eq2: ∀f,L1,L2,K1,K2. ⇩*[Ⓣ,f] L1 ≘ K1 → ⇩*[Ⓣ,f] L2 ≘ K2 →
103 |K1| = |K2| → |L1| = |L2|.
104 #f #L1 #L2 #K1 #K2 #HLK1 #HLK2 #HL12
105 elim (drops_fwd_fcla … HLK1) -HLK1 #n1 #Hn1 #H1 >H1 -L1
106 elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
107 <(pr_fcla_mono … Hn2 … Hn1) -f //
110 theorem drops_conf_div: ∀f1,f2,L1,L2. ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 →
111 ∃∃n. 𝐂❨f1❩ ≘ n & 𝐂❨f2❩ ≘ n.
112 #f1 #f2 #L1 #L2 #H1 #H2
113 elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
114 elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
115 lapply (eq_inv_nplus_bi_sn … H) -L2 #H destruct /2 width=3 by ex2_intro/
118 theorem drops_conf_div_fcla: ∀f1,f2,L1,L2,n1,n2.
119 ⇩*[Ⓣ,f1] L1 ≘ L2 → ⇩*[Ⓣ,f2] L1 ≘ L2 → 𝐂❨f1❩ ≘ n1 → 𝐂❨f2❩ ≘ n2 →
121 #f1 #f2 #L1 #L2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
122 lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1
123 lapply (drops_fcla_fwd … Hf2 Hn2) -f2 >H1 -L1
124 /2 width=1 by eq_inv_nplus_bi_sn/