matita/matita/contribs/lambdadelta/basic_2A/etc/lleq_alt/lleq_alt.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 "basic_2/notation/relations/lazyeqalt_4.ma".
  16 include "basic_2/substitution/lleq_lleq.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 (* Note: alternative definition of lleq *)
  21 inductive lleqa: relation4 ynat term lenv lenv ≝
  22 | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
  23 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2
  24 | lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
  25               ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
  26               lleqa (yinj 0) V K1 K2 → lleqa d (#i) L1 L2
  27 | lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2
  28 | lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2
  29 | lleqa_bind: ∀a,I,L1,L2,V,T,d.
  30               lleqa d V L1 L2 → lleqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
  31               lleqa d (ⓑ{a,I}V.T) L1 L2
  32 | lleqa_flat: ∀I,L1,L2,V,T,d.
  33               lleqa d V L1 L2 → lleqa d T L1 L2 → lleqa d (ⓕ{I}V.T) L1 L2
  34 .
  35
  36 interpretation
  37    "lazy equivalence (local environment) alternative"
  38    'LazyEqAlt T d L1 L2 = (lleqa d T L1 L2).
  39
  40 (* Main inversion lemmas ****************************************************)
  41
  42 theorem lleqa_inv_lleq: ∀L1,L2,T,d. L1 ⋕⋕[T, d] L2 → L1 ⋕[T, d] L2.
  43 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
  44 /2 width=8 by lleq_flat, lleq_bind, lleq_gref, lleq_free, lleq_lref, lleq_skip, lleq_sort/
  45 qed-.
  46
  47 (* Main properties **********************************************************)
  48
  49 theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2.
  50 #L1 #T @(f2_ind … rfw … L1 T) -L1 -T
  51 #n #IH #L1 * * /3 width=3 by lleqa_gref, lleqa_sort, lleq_fwd_length/
  52 [ #i #Hn #L2 #d #H elim (lleq_fwd_lref … H) [ * || * ]
  53   /4 width=9 by lleqa_free, lleqa_lref, lleqa_skip, lleq_fwd_length, ldrop_fwd_rfw/
  54 | #a #I #V #T #Hn #L2 #d #H elim (lleq_inv_bind … H) -H /3 width=1 by lleqa_bind/
  55 | #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/
  56 ]
  57 qed.
  58
  59 (* Advanced eliminators *****************************************************)
  60
  61 lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. (
  62                        ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
  63                     ) → (
  64                        ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
  65                     ) → (
  66                        ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
  67                        ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
  68                        K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
  69                     ) → (
  70                        ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
  71                     ) → (
  72                        ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
  73                     ) → (
  74                        ∀a,I,L1,L2,V,T,d.
  75                        L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
  76                        R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
  77                     ) → (
  78                        ∀I,L1,L2,V,T,d.
  79                        L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 →
  80                        R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
  81                     ) →
  82                     ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2.
  83 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H
  84 /3 width=9 by lleqa_inv_lleq/
  85 qed-.