matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn.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/xoa/ex_5_5.ma".
  16 include "ground_2/ynat/ynat_plus.ma".
  17 include "basic_2A/substitution/drop.ma".
  18
  19 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
  20
  21 inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝
  22 | llpx_sn_sort: ∀L1,L2,l,k. |L1| = |L2| → llpx_sn R l (⋆k) L1 L2
  23 | llpx_sn_skip: ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → llpx_sn R l (#i) L1 L2
  24 | llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,l,i. l ≤ yinj i →
  25                 ⬇[i] L1 ≡ K1.ⓑ{I}V1 → ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
  26                 llpx_sn R (yinj 0) V1 K1 K2 → R K1 V1 V2 → llpx_sn R l (#i) L1 L2
  27 | llpx_sn_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R l (#i) L1 L2
  28 | llpx_sn_gref: ∀L1,L2,l,p. |L1| = |L2| → llpx_sn R l (§p) L1 L2
  29 | llpx_sn_bind: ∀a,I,L1,L2,V,T,l.
  30                 llpx_sn R l V L1 L2 → llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
  31                 llpx_sn R l (ⓑ{a,I}V.T) L1 L2
  32 | llpx_sn_flat: ∀I,L1,L2,V,T,l.
  33                 llpx_sn R l V L1 L2 → llpx_sn R l T L1 L2 → llpx_sn R l (ⓕ{I}V.T) L1 L2
  34 .
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  38 fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 →
  39                            ∀a,I,V,T. X = ⓑ{a,I}V.T →
  40                            llpx_sn R l V L1 L2 ∧ llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
  41 #R #L1 #L2 #X #l * -L1 -L2 -X -l
  42 [ #L1 #L2 #l #k #_ #b #J #W #U #H destruct
  43 | #L1 #L2 #l #i #_ #_ #b #J #W #U #H destruct
  44 | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
  45 | #L1 #L2 #l #i #_ #_ #_ #b #J #W #U #H destruct
  46 | #L1 #L2 #l #p #_ #b #J #W #U #H destruct
  47 | #a #I #L1 #L2 #V #T #l #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
  48 | #I #L1 #L2 #V #T #l #_ #_ #b #J #W #U #H destruct
  49 ]
  50 qed-.
  51
  52 lemma llpx_sn_inv_bind: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
  53                         llpx_sn R l V L1 L2 ∧ llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
  54 /2 width=4 by llpx_sn_inv_bind_aux/ qed-.
  55
  56 fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 →
  57                            ∀I,V,T. X = ⓕ{I}V.T →
  58                            llpx_sn R l V L1 L2 ∧ llpx_sn R l T L1 L2.
  59 #R #L1 #L2 #X #l * -L1 -L2 -X -l
  60 [ #L1 #L2 #l #k #_ #J #W #U #H destruct
  61 | #L1 #L2 #l #i #_ #_ #J #W #U #H destruct
  62 | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #J #W #U #H destruct
  63 | #L1 #L2 #l #i #_ #_ #_ #J #W #U #H destruct
  64 | #L1 #L2 #l #p #_ #J #W #U #H destruct
  65 | #a #I #L1 #L2 #V #T #l #_ #_ #J #W #U #H destruct
  66 | #I #L1 #L2 #V #T #l #HV #HT #J #W #U #H destruct /2 width=1 by conj/
  67 ]
  68 qed-.
  69
  70 lemma llpx_sn_inv_flat: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 →
  71                         llpx_sn R l V L1 L2 ∧ llpx_sn R l T L1 L2.
  72 /2 width=4 by llpx_sn_inv_flat_aux/ qed-.
  73
  74 (* Basic forward lemmas *****************************************************)
  75
  76 lemma llpx_sn_fwd_length: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 → |L1| = |L2|.
  77 #R #L1 #L2 #T #l #H elim H -L1 -L2 -T -l //
  78 #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #HLK1 #HLK2 #_ #_ #HK12
  79 lapply (drop_fwd_length … HLK1) -HLK1
  80 lapply (drop_fwd_length … HLK2) -HLK2
  81 normalize //
  82 qed-.
  83
  84 lemma llpx_sn_fwd_drop_sn: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 →
  85                             ∀K1,i. ⬇[i] L1 ≡ K1 → ∃K2. ⬇[i] L2 ≡ K2.
  86 #R #L1 #L2 #T #l #H #K1 #i #HLK1 lapply (llpx_sn_fwd_length … H) -H
  87 #HL12 lapply (drop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by drop_O1_le/
  88 qed-.
  89
  90 lemma llpx_sn_fwd_drop_dx: ∀R,L1,L2,T,l. llpx_sn R l T L1 L2 →
  91                             ∀K2,i. ⬇[i] L2 ≡ K2 → ∃K1. ⬇[i] L1 ≡ K1.
  92 #R #L1 #L2 #T #l #H #K2 #i #HLK2 lapply (llpx_sn_fwd_length … H) -H
  93 #HL12 lapply (drop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by drop_O1_le/
  94 qed-.
  95
  96 fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → ∀i. X = #i →
  97                            ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  98                             | yinj i < l
  99                             | ∃∃I,K1,K2,V1,V2. ⬇[i] L1 ≡ K1.ⓑ{I}V1 &
 100                                                ⬇[i] L2 ≡ K2.ⓑ{I}V2 &
 101                                                llpx_sn R (yinj 0) V1 K1 K2 &
 102                                                R K1 V1 V2 & l ≤ yinj i.
 103 #R #L1 #L2 #X #l * -L1 -L2 -X -l
 104 [ #L1 #L2 #l #k #_ #j #H destruct
 105 | #L1 #L2 #l #i #_ #Hil #j #H destruct /2 width=1 by or3_intro1/
 106 | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #Hli #HLK1 #HLK2 #HK12 #HV12 #j #H destruct
 107   /3 width=9 by or3_intro2, ex5_5_intro/
 108 | #L1 #L2 #l #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
 109 | #L1 #L2 #l #p #_ #j #H destruct
 110 | #a #I #L1 #L2 #V #T #l #_ #_ #j #H destruct
 111 | #I #L1 #L2 #V #T #l #_ #_ #j #H destruct
 112 ]
 113 qed-.
 114
 115 lemma llpx_sn_fwd_lref: ∀R,L1,L2,l,i. llpx_sn R l (#i) L1 L2 →
 116                         ∨∨ |L1| ≤ i ∧ |L2| ≤ i
 117                          | yinj i < l
 118                          | ∃∃I,K1,K2,V1,V2. ⬇[i] L1 ≡ K1.ⓑ{I}V1 &
 119                                             ⬇[i] L2 ≡ K2.ⓑ{I}V2 &
 120                                             llpx_sn R (yinj 0) V1 K1 K2 &
 121                                             R K1 V1 V2 & l ≤ yinj i.
 122 /2 width=3 by llpx_sn_fwd_lref_aux/ qed-.
 123
 124 lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
 125                            llpx_sn R l V L1 L2.
 126 #R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H //
 127 qed-.
 128
 129 lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
 130                            llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
 131 #R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H //
 132 qed-.
 133
 134 lemma llpx_sn_fwd_flat_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 →
 135                            llpx_sn R l V L1 L2.
 136 #R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H //
 137 qed-.
 138
 139 lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,l. llpx_sn R l (ⓕ{I}V.T) L1 L2 →
 140                            llpx_sn R l T L1 L2.
 141 #R #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_flat … H) -H //
 142 qed-.
 143
 144 lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,l. llpx_sn R l (②{I}V.T) L1 L2 →
 145                            llpx_sn R l V L1 L2.
 146 #R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
 147 qed-.
 148
 149 (* Basic properties *********************************************************)
 150
 151 lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,l. llpx_sn R l T L L.
 152 #R #HR #T #L @(f2_ind … rfw … L T) -L -T
 153 #x #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
 154 #i #Hx elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
 155 #HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
 156 elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
 157 qed-.
 158
 159 lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
 160 #R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
 161 #x #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
 162 #a #I #V1 #T1 #Hx #L2 #HL12
 163 @llpx_sn_bind /2 width=1 by/ (**) (* explicit constructor *)
 164 @IH -IH // normalize /2 width=1 by eq_f2/
 165 qed-.
 166
 167 lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,m. ⬆[l, m] T ≡ U →
 168                      lt ≤ l + m → llpx_sn R l U L1 L2.
 169 #R #L1 #L2 #U #lt #H elim H -L1 -L2 -U -lt
 170 [ #L1 #L2 #lt #k #HL12 #X #l #m #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/
 171 | #L1 #L2 #lt #i #HL12 #Hilt #X #l #m #H #Hltlm
 172   elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12
 173   elim (ylt_yle_false … Hilt) -Hilt
 174   @(yle_trans … Hltlm) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *)
 175 | #I #L1 #L2 #K1 #K2 #W1 #W2 #lt #i #Hlti #HLK1 #HLK2 #HW1 #HW12 #_ #X #l #m #H #_
 176   elim (lift_inv_lref2 … H) -H * #Hil #H destruct
 177   [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
 178     lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
 179     normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/
 180   | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/
 181   ]
 182 | /2 width=1 by llpx_sn_free/
 183 | #L1 #L2 #lt #p #HL12 #X #l #m #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/
 184 | #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct
 185   elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct
 186   @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *)
 187   @(IHT … HTU) /2 width=1 by yle_succ/
 188 | #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct
 189   elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct
 190   /3 width=4 by llpx_sn_flat/
 191 ]
 192 qed-.
 193
 194 (**) (* the minor premise comes first *)
 195 lemma llpx_sn_ge: ∀R,L1,L2,T,l1,l2. l1 ≤ l2 →
 196                   llpx_sn R l1 T L1 L2 → llpx_sn R l2 T L1 L2.
 197 #R #L1 #L2 #T #l1 #l2 * -l1 -l2 (**) (* destructed yle *)
 198 /3 width=6 by llpx_sn_ge_up, llpx_sn_Y, llpx_sn_fwd_length, yle_inj/
 199 qed-.
 200
 201 lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 →
 202                       llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
 203                       llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2.
 204 /3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-.
 205
 206 lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
 207                   ∀L1,L2,T,l. llpx_sn R1 l T L1 L2 → llpx_sn R2 l T L1 L2.
 208 #R1 #R2 #HR12 #L1 #L2 #T #l #H elim H -L1 -L2 -T -l
 209 /3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
 210 qed-.