matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.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 "basic_2/notation/relations/lazyeq_4.ma".
  16 include "basic_2/relocation/ldrop.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 inductive lleq: nat → term → relation lenv ≝
  21 | lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2
  22 | lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d →
  23              ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 →
  24              lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2
  25 | lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i →
  26              ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
  27              lleq 0 V K1 K2 → lleq d (#i) L1 L2
  28 | lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2
  29 | lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2
  30 | lleq_bind: ∀a,I,L1,L2,V,T,d.
  31              lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
  32              lleq d (ⓑ{a,I}V.T) L1 L2
  33 | lleq_flat: ∀I,L1,L2,V,T,d.
  34              lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2
  35 .
  36
  37 interpretation
  38    "lazy equivalence (local environment)"
  39    'LazyEq d T L1 L2 = (lleq d T L1 L2).
  40
  41 (* Basic_properties *********************************************************)
  42
  43 lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
  44 #d #T #L1 #L2 #H elim H -d -T -L1 -L2
  45 /2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
  46 qed-.
  47
  48 (* Note this is: "∀d,T. reflexive … (lleq d T)" *)
  49 axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L.
  50 (*
  51 #T #L @(f2_ind … rfw … L T) -L -T
  52 #n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/
  53 #i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/
  54 #HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/
  55 elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
  56 qed.
  57 *)
  58
  59 lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2.
  60 #L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1
  61 /4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/
  62 [ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *)
  63 | #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2)
  64   [ -d1 /3 width=10 by lleq_skip/
  65   | /3 width=7 by lleq_lref, transitive_le/
  66   ]
  67 ]
  68 qed-.
  69
  70 (* Basic inversion lemmas ***************************************************)
  71
  72 fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i →
  73                         ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  74                          | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
  75                                                 ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
  76                                                 K1 ⋕[d-i-1, V1] K2 &
  77                                                 K1 ⋕[d-i-1, V2] K2 &
  78                                                 i < d
  79                          | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
  80                                         ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
  81                                         K1 ⋕[0, V] K2 & d ≤ i.
  82 #d #X #L1 #L2 * -d -X -L1 -L2
  83 [ #L1 #L2 #d #k #_ #j #H destruct
  84 | #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/
  85 | #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/
  86 | #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
  87 | #L1 #L2 #d #p #_ #j #H destruct
  88 | #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
  89 | #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
  90 ]
  91 qed-.
  92
  93 lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
  94                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  95                       | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
  96                                              ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
  97                                              K1 ⋕[d-i-1, V1] K2 &
  98                                              K1 ⋕[d-i-1, V2] K2 &
  99                                              i < d
 100                       | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
 101                                      ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
 102                                      K1 ⋕[0, V] K2 & d ≤ i.
 103 /2 width=3 by lleq_inv_lref_aux/ qed-.
 104
 105 fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
 106                         L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
 107 #d #X #L1 #L2 * -d -X -L1 -L2
 108 [ #L1 #L2 #d #k #_ #b #J #W #U #H destruct
 109 | #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
 110 | #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct
 111 | #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct
 112 | #L1 #L2 #d #p #_ #b #J #W #U #H destruct
 113 | #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
 114 | #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct
 115 ]
 116 qed-.
 117
 118 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 →
 119                      L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
 120 /2 width=4 by lleq_inv_bind_aux/ qed-.
 121
 122 fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
 123                         L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
 124 #d #X #L1 #L2 * -d -X -L1 -L2
 125 [ #L1 #L2 #d #k #_ #J #W #U #H destruct
 126 | #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct
 127 | #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct
 128 | #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct
 129 | #L1 #L2 #d #p #_ #J #W #U #H destruct
 130 | #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct
 131 | #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/
 132 ]
 133 qed-.
 134
 135 lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 →
 136                      L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
 137 /2 width=4 by lleq_inv_flat_aux/ qed-.
 138
 139 (* Basic forward lemmas *****************************************************)
 140
 141 lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|.
 142 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
 143 [ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_
 144 | #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12
 145 ]
 146 lapply (ldrop_fwd_length … HLK1) -HLK1
 147 lapply (ldrop_fwd_length … HLK2) -HLK2
 148 normalize //
 149 qed-.
 150
 151 lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
 152                          ∃K2. ⇩[0, i] L2 ≡ K2.
 153 #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
 154 #HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
 155 qed-.
 156
 157 lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
 158                          ∃K1. ⇩[0, i] L1 ≡ K1.
 159 /3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.