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/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 d L1 L2 = (lleq d T L1 L2).
  27
  28 (* Basic inversion lemmas ***************************************************)
  29
  30 lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
  31                    ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
  32                 ) → (
  33                    ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
  34                 ) → (
  35                    ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
  36                    ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
  37                    K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
  38                 ) → (
  39                    ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
  40                 ) → (
  41                    ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
  42                 ) → (
  43                    ∀a,I,L1,L2,V,T,d.
  44                    L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
  45                    R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
  46                 ) → (
  47                    ∀I,L1,L2,V,T,d.
  48                    L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 →
  49                    R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
  50                 ) →
  51                 ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2.
  52 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim H -L1 -L2 -T -d /2 width=8 by/
  53 qed-.
  54
  55 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[ⓑ{a,I}V.T, d] L2 →
  56                      L1 ⋕[V, d] L2 ∧ L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V.
  57 /2 width=2 by llpx_sn_inv_bind/ qed-.
  58
  59 lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[ⓕ{I}V.T, d] L2 →
  60                      L1 ⋕[V, d] L2 ∧ L1 ⋕[T, d] L2.
  61 /2 width=2 by llpx_sn_inv_flat/ qed-.
  62
  63 (* Basic forward lemmas *****************************************************)
  64
  65 lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
  66 /2 width=4 by llpx_sn_fwd_length/ qed-.
  67
  68 lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
  69                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  70                       | yinj i < d
  71                       | ∃∃I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V &
  72                                      ⇩[i] L2 ≡ K2.ⓑ{I}V &
  73                                       K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
  74 #L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
  75 * /3 width=7 by or3_intro2, ex4_4_intro/
  76 qed-.
  77
  78 lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
  79                          ∃K2. ⇩[i] L2 ≡ K2.
  80 /2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-.
  81
  82 lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
  83                          ∃K1. ⇩[i] L1 ≡ K1.
  84 /2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-.
  85
  86 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
  87                         L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2.
  88 /2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
  89
  90 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d.
  91                         L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V.
  92 /2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
  93
  94 lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d.
  95                         L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[V, d] L2.
  96 /2 width=3 by llpx_sn_fwd_flat_sn/ qed-.
  97
  98 lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d.
  99                         L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[T, d] L2.
 100 /2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
 101
 102 (* Basic properties *********************************************************)
 103
 104 lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2.
 105 /2 width=1 by llpx_sn_sort/ qed.
 106
 107 lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2.
 108 /2 width=1 by llpx_sn_skip/ qed.
 109
 110 lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
 111                  ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
 112                  K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2.
 113 /2 width=9 by llpx_sn_lref/ qed.
 114
 115 lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ⋕[#i, d] L2.
 116 /2 width=1 by llpx_sn_free/ qed.
 117
 118 lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] L2.
 119 /2 width=1 by llpx_sn_gref/ qed.
 120
 121 lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
 122                  L1 ⋕[V, d] L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
 123                  L1 ⋕[ⓑ{a,I}V.T, d] L2.
 124 /2 width=1 by llpx_sn_bind/ qed.
 125
 126 lemma lleq_flat: ∀I,L1,L2,V,T,d.
 127                  L1 ⋕[V, d] L2 → L1 ⋕[T, d] L2 → L1 ⋕[ⓕ{I}V.T, d] L2.
 128 /2 width=1 by llpx_sn_flat/ qed.
 129
 130 lemma lleq_refl: ∀d,T. reflexive … (lleq d T).
 131 /2 width=1 by llpx_sn_refl/ qed.
 132
 133 lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ⋕[T, ∞] L2.
 134 /2 width=1 by llpx_sn_Y/ qed.
 135
 136 lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
 137 #d #T #L1 #L2 #H @(lleq_ind … H) -d -T -L1 -L2
 138 /2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
 139 qed-.
 140
 141 lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
 142                   ∀T,d,e. ⇧[d, e] T ≡ U →
 143                   dt ≤ d + e → L1 ⋕[U, d] L2.
 144 /2 width=6 by llpx_sn_ge_up/ qed-.
 145
 146 lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2.
 147 /2 width=3 by llpx_sn_ge/ qed-.
 148
 149 lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
 150                    L1 ⋕[ⓑ{a,I}V.T, 0] L2.
 151 /2 width=1 by llpx_sn_bind_O/ qed-.