matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq.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/lazyeq_4.ma".
  16 include "basic_2/multiple/llpx_sn.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 (* Basic inversion lemmas ***************************************************)
  21
  22 lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
  23                    ∀L1,L2,l,s. |L1| = |L2| → R l (⋆s) L1 L2
  24                 ) → (
  25                    ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → R l (#i) L1 L2
  26                 ) → (
  27                    ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i →
  28                    ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V →
  29                    K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R l (#i) L1 L2
  30                 ) → (
  31                    ∀L1,L2,l,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R l (#i) L1 L2
  32                 ) → (
  33                    ∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2
  34                 ) → (
  35                    ∀a,I,L1,L2,V,T,l.
  36                    L1 ≡[V, l]L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V →
  37                    R l V L1 L2 → R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
  38                 ) → (
  39                    ∀I,L1,L2,V,T,l.
  40                    L1 ≡[V, l]L2 → L1 ≡[T, l] L2 →
  41                    R l V L1 L2 → R l T L1 L2 → R l (ⓕ{I}V.T) L1 L2
  42                 ) →
  43                 ∀l,T,L1,L2. L1 ≡[T, l] L2 → R l T L1 L2.
  44 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #l #T #L1 #L2 #H elim H -L1 -L2 -T -l /2 width=8 by/
  45 qed-.
  46
  47 (* Basic forward lemmas *****************************************************)
  48
  49 lemma lleq_fwd_lref: ∀L1,L2,l,i. L1 ≡[#i, l] L2 →
  50                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
  51                       | yinj i < l
  52                       | ∃∃I,K1,K2,V. ⬇[i] L1 ≡ K1.ⓑ{I}V &
  53                                      ⬇[i] L2 ≡ K2.ⓑ{I}V &
  54                                       K1 ≡[V, yinj 0] K2 & l ≤ yinj i.
  55 #L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1 by or3_intro0, or3_intro1/
  56 * /3 width=7 by or3_intro2, ex4_4_intro/
  57 qed-.
  58
  59 lemma lleq_fwd_drop_sn: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K1,i. ⬇[i] L1 ≡ K1 →
  60                          ∃K2. ⬇[i] L2 ≡ K2.
  61 /2 width=7 by llpx_sn_fwd_drop_sn/ qed-.
  62
  63 lemma lleq_fwd_drop_dx: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K2,i. ⬇[i] L2 ≡ K2 →
  64                          ∃K1. ⬇[i] L1 ≡ K1.
  65 /2 width=7 by llpx_sn_fwd_drop_dx/ qed-.
  66
  67 (* Basic properties *********************************************************)
  68
  69 lemma lleq_lref: ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i →
  70                  ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V →
  71                  K1 ≡[V, 0] K2 → L1 ≡[#i, l] L2.
  72 /2 width=9 by llpx_sn_lref/ qed.