]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_lprs.ma
update in ground, basic_2A and apps_2
[helm.git] / 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,0] 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,0] 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,0] L2 →
35                               ∀T1,T2. ❨G,L1❩ ⊢ T1 ➡*[h,0] 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,0] L2 →
44                              ∀T1,T2. ❨G,L1❩ ⊢ T1 ➡*[h,0] 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,0] L2 →
52                             ∀T1,T2. ❨G,L1❩ ⊢ T1 ➡[h,0] 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_bi_sn (h) (G) (L):
59       ∀p1,p2,W1,W2,T1,T2. ❨G,L❩ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
60       ∧∧ ❨G,L❩ ⊢ W1 ⬌*[h] W2 & ❨G,L.ⓛW1❩ ⊢ T1 ⬌*[h] T2 & p1 = p2.
61 #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #H
62 elim (cpcs_inv_cprs … H) -H #T #H1 #H2
63 elim (cpms_inv_abst_sn … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct
64 elim (cpms_inv_abst_sn … H2) -H2 #W #T #HW2 #HT2 #H destruct
65 lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
66 lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2
67 /4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/
68 qed-.
69
70 lemma cpcs_inv_abst_bi_dx (h) (G) (L):
71       ∀p1,p2,W1,W2,T1,T2. ❨G,L❩ ⊢ ⓛ[p1]W1.T1 ⬌*[h] ⓛ[p2]W2.T2 →
72       ∧∧ ❨G,L❩ ⊢ W1 ⬌*[h] W2 & ❨G,L.ⓛW2❩ ⊢ T1 ⬌*[h] T2 & p1 = p2.
73 #h #G #L #p1 #p2 #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12
74 #HT12 elim (cpcs_inv_abst_bi_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/
75 qed-.