matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.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/lazyeqalt_4.ma".
  16 include "basic_2/substitution/lleq_lleq.ma".
  17
  18 inductive lleqa: relation4 ynat term lenv lenv ≝
  19 | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
  20 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2
  21 | lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
  22               ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
  23               lleqa (yinj 0) V K1 K2 → lleqa d (#i) L1 L2
  24 | lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2
  25 | lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2
  26 | lleqa_bind: ∀a,I,L1,L2,V,T,d.
  27               lleqa d V L1 L2 → lleqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
  28               lleqa d (ⓑ{a,I}V.T) L1 L2
  29 | lleqa_flat: ∀I,L1,L2,V,T,d.
  30               lleqa d V L1 L2 → lleqa d T L1 L2 → lleqa d (ⓕ{I}V.T) L1 L2
  31 .
  32
  33 interpretation
  34    "lazy equivalence (local environment) alternative"
  35    'LazyEqAlt T d L1 L2 = (lleqa d T L1 L2).
  36
  37 (* Main inversion lemmas ****************************************************)
  38
  39 theorem lleqa_inv_lleq: ∀L1,L2,T,d. L1 ⋕⋕[T, d] L2 → L1 ⋕[T, d] L2.
  40 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
  41 /2 width=8 by lleq_flat, lleq_bind, lleq_gref, lleq_free, lleq_lref, lleq_skip, lleq_sort/
  42 qed-.
  43
  44 (* Main properties **********************************************************)
  45
  46 theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2.
  47 #L1 #T @(f2_ind … rfw … L1 T) -L1 -T
  48 #n #IH #L1 * * /3 width=3 by lleqa_gref, lleqa_sort, lleq_fwd_length/
  49 [ #i #Hn #L2 #d #H elim (lleq_fwd_lref … H) [ * || * ]
  50   /4 width=9 by lleqa_free, lleqa_lref, lleqa_skip, lleq_fwd_length, ldrop_fwd_rfw/
  51 | #a #I #V #T #Hn #L2 #d #H elim (lleq_inv_bind … H) -H /3 width=1 by lleqa_bind/
  52 | #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/
  53 ]
  54 qed.
  55
  56 (* Advanced eliminators *****************************************************)
  57
  58 lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. (
  59                        ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
  60                     ) → (
  61                        ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
  62                     ) → (
  63                        ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
  64                        ⇩[O, i] L1 ≡ K1.ⓑ{I1}V → ⇩[O, i] L2 ≡ K2.ⓑ{I2}V →
  65                        K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
  66                     ) → (
  67                        ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
  68                     ) → (
  69                        ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
  70                     ) → (
  71                        ∀a,I,L1,L2,V,T,d.
  72                        L1 ⋕[V, d]L2 → L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V →
  73                        R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
  74                     ) → (
  75                        ∀I,L1,L2,V,T,d.
  76                        L1 ⋕[V, d]L2 → L1 ⋕[T, d] L2 →
  77                        R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
  78                     ) →
  79                     ∀d,T,L1,L2. L1 ⋕[T, d] L2 → R d T L1 L2.
  80 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim (lleq_lleqa … H) -H
  81 /3 width=9 by lleqa_inv_lleq/
  82 qed-.
  83
  84 (* Advanced inversion lemmas ************************************************)
  85
  86 fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 →
  87                      ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
  88                      K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
  89 #L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0
  90 /2 width=1 by lleq_gref, lleq_free, lleq_sort/
  91 [ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V #HLK1 #HLK2 #HV destruct
  92   elim (yle_split_eq i d) /2 width=1 by lleq_skip, ylt_fwd_succ2/ -HL12 -Hid
  93   #H destruct /2 width=8 by lleq_lref/
  94 | #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct
  95   /3 width=8 by lleq_lref, yle_pred_sn/
  96 | #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
  97   /4 width=7 by lleq_bind, ldrop_ldrop/
  98 | #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
  99   /3 width=7 by lleq_flat/
 100 ]
 101 qed-.
 102
 103 lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 →
 104                   ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
 105                   K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
 106 /2 width=7 by lleq_inv_S_aux/ qed-.
 107
 108 lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 →
 109                        L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V.
 110 #a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H
 111 /3 width=7 by ldrop_pair, conj, lleq_inv_S/
 112 qed-.
 113
 114 (* Advanced properties ******************************************************)
 115
 116 lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2.
 117 #L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1
 118 /4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/
 119 [ /3 width=3 by lleq_skip, ylt_yle_trans/
 120 | #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2)
 121   [ lapply (lleq_fwd_length … HV) #HK12 #Hid2
 122     lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
 123     normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/
 124   | /3 width=8 by lleq_lref, yle_trans/
 125   ]
 126 ]
 127 qed-.
 128
 129 lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[V, 0] L2 → L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
 130                    L1 ⋕[ⓑ{a,I}V.T, 0] L2.
 131 /3 width=3 by lleq_ge, lleq_bind/ qed.
 132
 133 lemma lleq_bind_repl_SO: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
 134                          ∀J,W. L1.ⓑ{J}W ⋕[T, 1] L2.ⓑ{J}W.
 135 #I #L1 #L2 #V #T #HT #J #W lapply (lleq_ge … HT 1 ?) // -HT
 136 #HT @(lleq_lsuby_repl … HT) /2 width=1 by lsuby_succ/ (**) (* full auto fails *)
 137 qed-.
 138
 139 lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V →
 140                         ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W.
 141 /3 width=7 by lleq_bind_repl_SO, lleq_inv_S/ qed-.