matita/matita/contribs/lambdadelta/basic_2A/etc/lpx_sn/llpx_sn.etc

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