matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.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/rt_computation/lprs_cprs.ma".
  16 include "basic_2/rt_equivalence/cpcs_cprs.ma".
  17
  18 (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
  19
  20 (* Properties with parallel r-computation for full local environments *******)
  21
  22 lemma lpr_cpcs_trans (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h] L2 →
  23                               ∀T1,T2. ❪G,L2❫ ⊢ T1 ⬌*[h] T2 → ❪G,L1❫ ⊢ T1 ⬌*[h] T2.
  24 #h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
  25  /4 width=5 by cprs_div, lpr_cpms_trans/
  26 qed-.
  27
  28 lemma lprs_cpcs_trans (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡*[h] L2 →
  29                                ∀T1,T2. ❪G,L2❫ ⊢ T1 ⬌*[h] T2 → ❪G,L1❫ ⊢ T1 ⬌*[h] T2.
  30 #h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
  31 /4 width=5 by cprs_div, lprs_cpms_trans/
  32 qed-.
  33
  34 lemma lprs_cprs_conf (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡*[h] L2 →
  35                               ∀T1,T2. ❪G,L1❫ ⊢ T1 ➡*[h] T2 → ❪G,L2❫ ⊢ T1 ⬌*[h] T2.
  36 #h #G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1
  37 /2 width=3 by cprs_div/
  38 qed-.
  39
  40 (* Basic_1: was: pc3_wcpr0_t *)
  41 (* Basic_1: note: pc3_wcpr0_t should be renamed *)
  42 (* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *)
  43 lemma lpr_cprs_conf (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h] L2 →
  44                              ∀T1,T2. ❪G,L1❫ ⊢ T1 ➡*[h] T2 → ❪G,L2❫ ⊢ T1 ⬌*[h] T2.
  45 #h #G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1
  46 /2 width=3 by cprs_div/
  47 qed-.
  48
  49 (* Basic_1: was only: pc3_pr0_pr2_t *)
  50 (* Basic_1: note: pc3_pr0_pr2_t should be renamed *)
  51 lemma lpr_cpr_conf (h) (G): ∀L1,L2. ❪G,L1❫ ⊢ ➡[h] L2 →
  52                             ∀T1,T2. ❪G,L1❫ ⊢ T1 ➡[h] T2 → ❪G,L2❫ ⊢ T1 ⬌*[h] T2.
  53 /3 width=5 by lpr_cprs_conf, cpm_cpms/ qed-.
  54
  55 (* Advanced inversion lemmas ************************************************)
  56
  57 (* Note: there must be a proof suitable for lfpr *)
  58 lemma cpcs_inv_abst_sn (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
  59                                     ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
  60 #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H
  61 elim (cpcs_inv_cprs … H) -H #T #H1 #H2
  62 elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
  63 elim (cpms_inv_abst_sn … H2) -H2 #W #T #HW2 #HT2 #H destruct
  64 lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
  65 lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
  66 /4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
  67 qed-.
  68
  69 lemma cpcs_inv_abst_dx (h) (G) (L): ∀p1,p2,W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
  70                                    ∧∧ ❪G,L❫ ⊢ W1 ⬌*[h] W2 & ❪G,L.ⓛW2❫ ⊢ T1 ⬌*[h] T2 & p1 = p2.
  71 #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
  72 #HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
  73 qed-.