matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.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/substitution/lsubr.ma".
  16
  17 (* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************)
  18
  19 inductive lsubx: relation lenv ≝
  20 | lsubx_sort: ∀L. lsubx L (⋆)
  21 | lsubx_bind: ∀I,L1,L2,V. lsubx L1 L2 → lsubx (L1.ⓑ{I}V) (L2.ⓑ{I}V)
  22 | lsubx_abst: ∀L1,L2,V,W. lsubx L1 L2 → lsubx (L1.ⓓⓝW.V) (L2.ⓛW)
  23 .
  24
  25 interpretation
  26   "local environment refinement (extended reduction)"
  27   'CrSubEqT L1 L2 = (lsubx L1 L2).
  28
  29 (* Basic properties *********************************************************)
  30
  31 lemma lsubx_refl: ∀L. L ⓝ⊑ L.
  32 #L elim L -L // /2 width=1/
  33 qed.
  34
  35 (* Basic inversion lemmas ***************************************************)
  36
  37 fact lsubx_inv_atom1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → L1 = ⋆ → L2 = ⋆.
  38 #L1 #L2 * -L1 -L2 //
  39 [ #I #L1 #L2 #V #_ #H destruct
  40 | #L1 #L2 #V #W #_ #H destruct
  41 ]
  42 qed-.
  43
  44 lemma lsubx_inv_atom1: ∀L2. ⋆ ⓝ⊑ L2 → L2 = ⋆.
  45 /2 width=3 by lsubx_inv_atom1_aux/ qed-.
  46
  47 fact lsubx_inv_abst1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
  48                           L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
  49 #L1 #L2 * -L1 -L2
  50 [ #L #K1 #W #H destruct /2 width=1/
  51 | #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
  52 | #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
  53 ]
  54 qed-.
  55
  56 lemma lsubx_inv_abst1: ∀K1,L2,W. K1.ⓛW ⓝ⊑ L2 →
  57                        L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
  58 /2 width=3 by lsubx_inv_abst1_aux/ qed-.
  59
  60 fact lsubx_inv_abbr2_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
  61                           ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
  62 #L1 #L2 * -L1 -L2
  63 [ #L #K2 #W #H destruct
  64 | #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
  65 | #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
  66 ]
  67 qed-.
  68
  69 lemma lsubx_inv_abbr2: ∀L1,K2,W. L1 ⓝ⊑ K2.ⓓW →
  70                        ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
  71 /2 width=3 by lsubx_inv_abbr2_aux/ qed-.
  72
  73 (* Basic forward lemmas *****************************************************)
  74
  75 lemma lsubx_fwd_length: ∀L1,L2. L1 ⓝ⊑ L2 → |L2| ≤ |L1|.
  76 #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
  77 qed-.
  78
  79 lemma lsubx_fwd_lsubr: ∀L1,L2. L1 ⓝ⊑ L2 → L1 ⊑ L2.
  80 #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
  81 qed-.
  82
  83 lemma lsubx_fwd_ldrop2_bind: ∀L1,L2. L1 ⓝ⊑ L2 →
  84                              ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
  85                              (∃∃K1. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
  86                              ∃∃K1,V. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V.
  87 #L1 #L2 #H elim H -L1 -L2
  88 [ #L #I #K2 #W #i #H
  89   elim (ldrop_inv_atom1 … H) -H #H destruct
  90 | #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
  91   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
  92   [ /3 width=3/
  93   | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
  94   ]
  95 | #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
  96   elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
  97   [ /3 width=4/
  98   | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
  99   ]
 100 ]
 101 qed-.