matita/matita/contribs/lambdadelta/basic_2/unfold/lcpss.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/unfold/cpss.ma".
  16
  17 (* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
  18
  19 inductive lcpss: relation lenv ≝
  20 | lcpss_atom: lcpss (⋆) (⋆)
  21 | lcpss_pair: ∀I,L1,L2,V1,V2. lcpss L1 L2 → L1 ⊢ V1 ▶* V2 →
  22               lcpss (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
  23 .
  24
  25 interpretation "parallel unfold (local environment, sn variant)"
  26    'PSubstStarSn L1 L2 = (lcpss L1 L2).
  27
  28 (* Basic inversion lemmas ***************************************************)
  29
  30 fact lcpss_inv_atom1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L1 = ⋆ → L2 = ⋆.
  31 #L1 #L2 * -L1 -L2
  32 [ //
  33 | #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
  34 ]
  35 qed-.
  36
  37 lemma lcpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆.
  38 /2 width=5 by lcpss_inv_atom1_aux/ qed-.
  39
  40 fact lcpss_inv_pair1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
  41                           ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
  42 #L1 #L2 * -L1 -L2
  43 [ #I #K1 #V1 #H destruct
  44 | #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K1 #W1 #H destruct /2 width=5/
  45 ]
  46 qed-.
  47
  48 lemma lcpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 →
  49                        ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
  50 /2 width=5 by lcpss_inv_pair1_aux/ qed-.
  51
  52 fact lcpss_inv_atom2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L2 = ⋆ → L1 = ⋆.
  53 #L1 #L2 * -L1 -L2
  54 [ //
  55 | #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
  56 ]
  57 qed-.
  58
  59 lemma lcpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆.
  60 /2 width=5 by lcpss_inv_atom2_aux/ qed-.
  61
  62 fact lcpss_inv_pair2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
  63                           ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
  64 #L1 #L2 * -L1 -L2
  65 [ #I #K1 #V1 #H destruct
  66 | #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K2 #W2 #H destruct /2 width=5/
  67 ]
  68 qed-.
  69
  70 lemma lcpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
  71                        ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
  72 /2 width=5 by lcpss_inv_pair2_aux/ qed-.
  73
  74 (* Basic properties *********************************************************)
  75
  76 lemma lcpss_refl: ∀L. L ⊢ ▶* L.
  77 #L elim L -L // /2 width=1/
  78 qed.
  79
  80 lemma lcpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
  81                     L1 @@ K1 ⊢ ▶* L2 @@ K2.
  82 #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
  83 qed.
  84
  85 (* Basic forward lemmas *****************************************************)
  86
  87 lemma lcpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|.
  88 #L1 #L2 #H elim H -L1 -L2 normalize //
  89 qed-.