matita/matita/contribs/lambdadelta/basic_2A/multiple/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_2A/notation/relations/lazyeq_4.ma".
  16 include "basic_2A/multiple/llpx_sn.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2.
  21
  22 definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq.
  23
  24 interpretation
  25    "lazy equivalence (local environment)"
  26    'LazyEq T l L1 L2 = (lleq l T L1 L2).
  27
  28 definition lleq_transitive: predicate (relation3 lenv term term) ≝
  29            λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R L1 T1 T2.
  30
  31 (* Basic inversion lemmas ***************************************************)
  32
  33 lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
  34                    ∀L1,L2,l,k. |L1| = |L2| → R l (⋆k) L1 L2
  35                 ) → (
  36                    ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → R l (#i) L1 L2
  37                 ) → (
  38                    ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i →
  39                    ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V →
  40                    K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R l (#i) L1 L2
  41                 ) → (
  42                    ∀L1,L2,l,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R l (#i) L1 L2
  43                 ) → (
  44                    ∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2
  45                 ) → (
  46                    ∀a,I,L1,L2,V,T,l.
  47                    L1 ≡[V, l]L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V →
  48                    R l V L1 L2 → R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
  49                 ) → (
  50                    ∀I,L1,L2,V,T,l.
  51                    L1 ≡[V, l]L2 → L1 ≡[T, l] L2 →
  52                    R l V L1 L2 → R l T L1 L2 → R l (ⓕ{I}V.T) L1 L2
  53                 ) →
  54                 ∀l,T,L1,L2. L1 ≡[T, l] L2 → R l T L1 L2.
  55 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #l #T #L1 #L2 #H elim H -L1 -L2 -T -l /2 width=8 by/
  56 qed-.
  57
  58 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 →
  59                      L1 ≡[V, l] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V.
  60 /2 width=2 by llpx_sn_inv_bind/ qed-.
  61
  62 lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 →
  63                      L1 ≡[V, l] L2 ∧ L1 ≡[T, l] L2.
  64 /2 width=2 by llpx_sn_inv_flat/ qed-.
  65
  66 (* Basic forward lemmas *****************************************************)
  67
  68 lemma lleq_fwd_length: ∀L1,L2,T,l. L1 ≡[T, l] L2 → |L1| = |L2|.
  69 /2 width=4 by llpx_sn_fwd_length/ qed-.
  70
  71 lemma lleq_fwd_lref: ∀L1,L2,l,i. L1 ≡[#i, l] L2 →
  72                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  73                       | yinj i < l
  74                       | ∃∃I,K1,K2,V. ⬇[i] L1 ≡ K1.ⓑ{I}V &
  75                                      ⬇[i] L2 ≡ K2.ⓑ{I}V &
  76                                       K1 ≡[V, yinj 0] K2 & l ≤ yinj i.
  77 #L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1 by or3_intro0, or3_intro1/
  78 * /3 width=7 by or3_intro2, ex4_4_intro/
  79 qed-.
  80
  81 lemma lleq_fwd_drop_sn: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K1,i. ⬇[i] L1 ≡ K1 →
  82                          ∃K2. ⬇[i] L2 ≡ K2.
  83 /2 width=7 by llpx_sn_fwd_drop_sn/ qed-.
  84
  85 lemma lleq_fwd_drop_dx: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K2,i. ⬇[i] L2 ≡ K2 →
  86                          ∃K1. ⬇[i] L1 ≡ K1.
  87 /2 width=7 by llpx_sn_fwd_drop_dx/ qed-.
  88
  89 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,l.
  90                         L1 ≡[ⓑ{a,I}V.T, l] L2 → L1 ≡[V, l] L2.
  91 /2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
  92
  93 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l.
  94                         L1 ≡[ⓑ{a,I}V.T, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V.
  95 /2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
  96
  97 lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l.
  98                         L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[V, l] L2.
  99 /2 width=3 by llpx_sn_fwd_flat_sn/ qed-.
 100
 101 lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,l.
 102                         L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[T, l] L2.
 103 /2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
 104
 105 (* Basic properties *********************************************************)
 106
 107 lemma lleq_sort: ∀L1,L2,l,k. |L1| = |L2| → L1 ≡[⋆k, l] L2.
 108 /2 width=1 by llpx_sn_sort/ qed.
 109
 110 lemma lleq_skip: ∀L1,L2,l,i. yinj i < l → |L1| = |L2| → L1 ≡[#i, l] L2.
 111 /2 width=1 by llpx_sn_skip/ qed.
 112
 113 lemma lleq_lref: ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i →
 114                  ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V →
 115                  K1 ≡[V, 0] K2 → L1 ≡[#i, l] L2.
 116 /2 width=9 by llpx_sn_lref/ qed.
 117
 118 lemma lleq_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, l] L2.
 119 /2 width=1 by llpx_sn_free/ qed.
 120
 121 lemma lleq_gref: ∀L1,L2,l,p. |L1| = |L2| → L1 ≡[§p, l] L2.
 122 /2 width=1 by llpx_sn_gref/ qed.
 123
 124 lemma lleq_bind: ∀a,I,L1,L2,V,T,l.
 125                  L1 ≡[V, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V →
 126                  L1 ≡[ⓑ{a,I}V.T, l] L2.
 127 /2 width=1 by llpx_sn_bind/ qed.
 128
 129 lemma lleq_flat: ∀I,L1,L2,V,T,l.
 130                  L1 ≡[V, l] L2 → L1 ≡[T, l] L2 → L1 ≡[ⓕ{I}V.T, l] L2.
 131 /2 width=1 by llpx_sn_flat/ qed.
 132
 133 lemma lleq_refl: ∀l,T. reflexive … (lleq l T).
 134 /2 width=1 by llpx_sn_refl/ qed.
 135
 136 lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ≡[T, ∞] L2.
 137 /2 width=1 by llpx_sn_Y/ qed.
 138
 139 lemma lleq_sym: ∀l,T. symmetric … (lleq l T).
 140 #l #T #L1 #L2 #H @(lleq_ind … H) -l -T -L1 -L2
 141 /2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
 142 qed-.
 143
 144 lemma lleq_ge_up: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 →
 145                   ∀T,l,m. ⬆[l, m] T ≡ U →
 146                   lt ≤ l + m → L1 ≡[U, l] L2.
 147 /2 width=6 by llpx_sn_ge_up/ qed-.
 148
 149 lemma lleq_ge: ∀L1,L2,T,l1. L1 ≡[T, l1] L2 → ∀l2. l1 ≤ l2 → L1 ≡[T, l2] L2.
 150 /2 width=3 by llpx_sn_ge/ qed-.
 151
 152 lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V →
 153                    L1 ≡[ⓑ{a,I}V.T, 0] L2.
 154 /2 width=1 by llpx_sn_bind_O/ qed-.
 155
 156 (* Advanceded properties on lazy pointwise extensions ************************)
 157
 158 lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) →
 159                      ∀L1,L2,T,l. L1 ≡[T, l] L2 → llpx_sn R l T L1 L2.
 160 /2 width=3 by llpx_sn_co/ qed-.