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_3.ma".
  16 include "basic_2/relocation/ldrop.ma".
  17
  18 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
  19
  20 inductive lleq: term → relation lenv ≝
  21 | lleq_sort: ∀L1,L2,k. |L1| = |L2| → lleq (⋆k) L1 L2
  22 | lleq_lref: ∀I,L1,L2,K1,K2,V,i.
  23              ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
  24              lleq V K1 K2 → lleq (#i) L1 L2
  25 | lleq_free: ∀L1,L2,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq (#i) L1 L2
  26 | lleq_gref: ∀L1,L2,p. |L1| = |L2| → lleq (§p) L1 L2
  27 | lleq_bind: ∀a,I,L1,L2,V,T.
  28              lleq V L1 L2 → lleq T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
  29              lleq (ⓑ{a,I}V.T) L1 L2
  30 | lleq_flat: ∀I,L1,L2,V,T.
  31              lleq V L1 L2 → lleq T L1 L2 → lleq (ⓕ{I}V.T) L1 L2
  32 .
  33
  34 interpretation
  35    "lazy equivalence (local environment)"
  36    'LazyEq T L1 L2 = (lleq T L1 L2).
  37
  38 (* Basic_properties *********************************************************)
  39
  40 lemma lleq_sym: ∀T. symmetric … (lleq T).
  41 #T #L1 #L2 #H elim H -T -L1 -L2
  42 /2 width=7 by lleq_sort, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
  43 qed-.
  44
  45 lemma lleq_refl: ∀T. reflexive … (lleq T).
  46 #T #L @(f2_ind … rfw … L T)
  47 #n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/
  48 #i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/
  49 #HiL elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
  50 qed.
  51
  52 (* Basic inversion lemmas ***************************************************)
  53
  54 fact lleq_inv_lref_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀i. X = #i →
  55                         (|L1| ≤ i ∧ |L2| ≤ i) ∨
  56                         ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
  57                                      ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
  58                                      K1 ⋕[V] K2.
  59 #X #L1 #L2 * -X -L1 -L2
  60 [ #L1 #L2 #k #_ #j #H destruct
  61 | #I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
  62 | #L1 #L2 #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or_introl, conj/
  63 | #L1 #L2 #p #_ #j #H destruct
  64 | #a #I #L1 #L2 #V #T #_ #_ #j #H destruct
  65 | #I #L1 #L2 #V #T #_ #_ #j #H destruct
  66 ]
  67 qed-.
  68
  69 lemma lleq_inv_lref: ∀L1,L2,i. L1 ⋕[#i] L2 →
  70                      (|L1| ≤ i ∧ |L2| ≤ i) ∨
  71                      ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
  72                                   ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
  73                                   K1 ⋕[V] K2.
  74 /2 width=3 by lleq_inv_lref_aux/ qed-.
  75
  76 fact lleq_inv_bind_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
  77                         L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V.
  78 #X #L1 #L2 * -X -L1 -L2
  79 [ #L1 #L2 #k #_ #b #J #W #U #H destruct
  80 | #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #b #J #W #U #H destruct
  81 | #L1 #L2 #i #_ #_ #_ #b #J #W #U #H destruct
  82 | #L1 #L2 #p #_ #b #J #W #U #H destruct
  83 | #a #I #L1 #L2 #V #T #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
  84 | #I #L1 #L2 #V #T #_ #_ #b #J #W #U #H destruct
  85 ]
  86 qed-.
  87
  88 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T. L1 ⋕[ ⓑ{a,I}V.T] L2 →
  89                      L1 ⋕[V] L2 ∧ L1.ⓑ{I}V ⋕[T] L2.ⓑ{I}V.
  90 /2 width=4 by lleq_inv_bind_aux/ qed-.
  91
  92 fact lleq_inv_flat_aux: ∀X,L1,L2. L1 ⋕[X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
  93                         L1 ⋕[V] L2 ∧ L1 ⋕[T] L2.
  94 #X #L1 #L2 * -X -L1 -L2
  95 [ #L1 #L2 #k #_ #J #W #U #H destruct
  96 | #I #L1 #L2 #K1 #K2 #V #i #_ #_ #_ #J #W #U #H destruct
  97 | #L1 #L2 #i #_ #_ #_ #J #W #U #H destruct
  98 | #L1 #L2 #p #_ #J #W #U #H destruct
  99 | #a #I #L1 #L2 #V #T #_ #_ #J #W #U #H destruct
 100 | #I #L1 #L2 #V #T #HV #HT #J #W #U #H destruct /2 width=1 by conj/
 101 ]
 102 qed-.
 103
 104 lemma lleq_inv_flat: ∀I,L1,L2,V,T. L1 ⋕[ ⓕ{I}V.T] L2 →
 105                      L1 ⋕[V] L2 ∧ L1 ⋕[T] L2.
 106 /2 width=4 by lleq_inv_flat_aux/ qed-.
 107
 108 (* Basic forward lemmas *****************************************************)
 109
 110 lemma lleq_fwd_length: ∀L1,L2,T. L1 ⋕[T] L2 → |L1| = |L2|.
 111 #L1 #L2 #T #H elim H -L1 -L2 -T //
 112 #I #L1 #L2 #K1 #K2 #V #i #HLK1 #HLK2 #_ #IHK12
 113 lapply (ldrop_fwd_length … HLK1) -HLK1
 114 lapply (ldrop_fwd_length … HLK2) -HLK2
 115 normalize //
 116 qed-.
 117
 118 lemma lleq_fwd_ldrop_sn: ∀L1,L2,T. L1 ⋕[T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
 119                          ∃K2. ⇩[0, i] L2 ≡ K2.
 120 #L1 #L2 #T #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
 121 #HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/ (**) (* full auto fails *)
 122 qed-.