matita/matita/contribs/lambdadelta/basic_2/substitution/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/substitution/cpys.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 definition lleq: relation4 nat term lenv lenv ≝
  21                  λd,T,L1,L2. |L1| = |L2| ∧
  22                              (∀U. ⦃⋆, L1⦄ ⊢ T ▶*×[d, ∞] U ↔ ⦃⋆, L2⦄ ⊢ T ▶*×[d, ∞] U).
  23
  24 interpretation
  25    "lazy equivalence (local environment)"
  26    'LazyEq T d L1 L2 = (lleq d T L1 L2).
  27
  28 (* Basic properties *********************************************************)
  29
  30 lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] L2.
  31 #L1 #L2 #d #k #HL12 @conj // -HL12
  32 #U @conj #H >(cpys_inv_sort1 … H) -H //
  33 qed.
  34
  35 lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] L2.
  36 #L1 #L2 #d #k #HL12 @conj // -HL12
  37 #U @conj #H >(cpys_inv_gref1 … H) -H //
  38 qed.
  39
  40 lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
  41                  L1 ⋕[V, d] L2 → L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V →
  42                  L1 ⋕[ⓑ{a,I}V.T, d] L2.
  43 #a #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
  44 #X @conj #H elim (cpys_inv_bind1 … H) -H
  45 #W #U #HVW #HTU #H destruct
  46 elim (IHV W) -IHV #H1VW #H1WV
  47 elim (IHT U) -IHT #H1TU #H1UT
  48 @cpys_bind /2 width=1 by/ -HVW -H1VW -H1WV
  49 [ @(lsuby_cpys_trans … (L2.ⓑ{I}V))
  50 | @(lsuby_cpys_trans … (L1.ⓑ{I}V))
  51 ] /4 width=5 by lsuby_cpys_trans, lsuby_succ/ (**) (* full auto too slow *)
  52 qed.
  53
  54 lemma lleq_flat: ∀I,L1,L2,V,T,d.
  55                  L1 ⋕[V, d] L2 → L1 ⋕[T, d] L2 → L1 ⋕[ⓕ{I}V.T, d] L2.
  56 #I #L1 #L2 #V #T #d * #HL12 #IHV * #_ #IHT @conj // -HL12
  57 #X @conj #H elim (cpys_inv_flat1 … H) -H
  58 #W #U #HVW #HTU #H destruct
  59 elim (IHV W) -IHV elim (IHT U) -IHT
  60 /3 width=1 by cpys_flat/
  61 qed.
  62
  63 (* Basic forward lemmas *****************************************************)
  64
  65 lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
  66 #L1 #L2 #T #d * //
  67 qed-.
  68
  69 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
  70                         L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2.
  71 #a #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12
  72 #U elim (H (ⓑ{a,I}U.T)) -H
  73 #H1 #H2 @conj
  74 #H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2
  75 /2 width=1 by cpys_bind/ -H
  76 #H elim (cpys_inv_bind1 … H) -H
  77 #X #Y #H1 #H2 #H destruct //
  78 qed-.
  79
  80 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d.
  81                         L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V.
  82 #a #I #L1 #L2 #V #T #d * #HL12 #H @conj [ normalize // ] -HL12
  83 #U elim (H (ⓑ{a,I}V.U)) -H
  84 #H1 #H2 @conj
  85 #H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2
  86 /2 width=1 by cpys_bind/ -H
  87 #H elim (cpys_inv_bind1 … H) -H
  88 #X #Y #H1 #H2 #H destruct //
  89 qed-.
  90
  91 lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d.
  92                         L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[V, d] L2.
  93 #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12
  94 #U elim (H (ⓕ{I}U.T)) -H
  95 #H1 #H2 @conj
  96 #H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2
  97 /2 width=1 by cpys_flat/ -H
  98 #H elim (cpys_inv_flat1 … H) -H
  99 #X #Y #H1 #H2 #H destruct //
 100 qed-.
 101
 102 lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d.
 103                         L1 ⋕[ⓕ{I}V.T, d] L2 → L1 ⋕[T, d] L2.
 104 #I #L1 #L2 #V #T #d * #HL12 #H @conj // -HL12
 105 #U elim (H (ⓕ{I}V.U)) -H
 106 #H1 #H2 @conj
 107 #H [ lapply (H1 ?) | lapply (H2 ?) ] -H1 -H2
 108 /2 width=1 by cpys_flat/ -H
 109 #H elim (cpys_inv_flat1 … H) -H
 110 #X #Y #H1 #H2 #H destruct //
 111 qed-.
 112
 113 (* Basic inversion lemmas ***************************************************)
 114
 115 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[ⓑ{a,I}V.T, d] L2 →
 116                      L1 ⋕[V, d] L2 ∧ L1.ⓑ{I}V ⋕[T, d+1] L2.ⓑ{I}V.
 117 /3 width=4 by lleq_fwd_bind_sn, lleq_fwd_bind_dx, conj/ qed-.
 118
 119 lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[ⓕ{I}V.T, d] L2 →
 120                      L1 ⋕[V, d] L2 ∧ L1 ⋕[T, d] L2.
 121 /3 width=3 by lleq_fwd_flat_sn, lleq_fwd_flat_dx, conj/ qed-.