]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma
update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_preserve.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/dynamic/cnv_cpms_conf.ma".
16
17 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
18
19 (* Main preservation properties *********************************************)
20
21 (* Basic_2A1: uses: snv_preserve *)
22 lemma cnv_preserve (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] →
23                             ∧∧ IH_cnv_cpms_conf_lpr a h G L T
24                              & IH_cnv_cpm_trans_lpr a h G L T.
25 #a #h #G #L #T #HT
26 letin o ≝ (sd_O h)
27 lapply (cnv_fwd_fsb … o … HT) -HT #H
28 @(fsb_ind_fpbg … H) -G -L -T #G #L #T #_ #IH
29 @conj [ letin aux ≝ cnv_cpms_conf_lpr_aux | letin aux ≝ cnv_cpm_trans_lpr_aux ]
30 @(aux … o … G L T) // #G0 #L0 #T0 #H
31 elim (IH … H) -IH -H //
32 qed-.
33
34 theorem cnv_cpms_conf_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_conf_lpr a h G L T.
35 #a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=1 by/
36 qed-.
37
38 (* Basic_2A1: uses: snv_cpr_lpr *)
39 theorem cnv_cpm_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpm_trans_lpr a h G L T.
40 #a #h #G #L #T #HT elim (cnv_preserve … HT) /2 width=2 by/
41 qed-.
42
43 (* Advanced preservation properties *****************************************)
44
45 lemma cnv_cpms_conf (a) (h) (G) (L):
46       ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] →
47       ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*[n2,h] T2 →
48       ∃∃T. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L⦄ ⊢ T2 ➡*[n1-n2,h] T.
49 /2 width=8 by cnv_cpms_conf_lpr/ qed-.
50
51 (* Basic_2A1: uses: snv_cprs_lpr *)
52 lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T.
53 #a #h #G #L1 #T1 #HT1 #n #T2 #H
54 @(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/
55 qed-.
56
57 lemma cnv_cpm_trans (a) (h) (G) (L):
58       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
59       ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
60 /2 width=6 by cnv_cpm_trans_lpr/ qed-.
61
62 (* Note: this is the preservation property *)
63 lemma cnv_cpms_trans (a) (h) (G) (L):
64       ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
65       ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
66 /2 width=6 by cnv_cpms_trans_lpr/ qed-.
67
68 lemma cnv_lpr_trans (a) (h) (G):
69       ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h].
70 /2 width=6 by cnv_cpm_trans_lpr/ qed-.
71
72 lemma cnv_lprs_trans (a) (h) (G):
73       ∀L1,T. ⦃G,L1⦄ ⊢ T ![a,h] → ∀L2. ⦃G,L1⦄ ⊢ ➡*[h] L2 → ⦃G,L2⦄ ⊢ T ![a,h].
74 #a #h #G #L1 #T #HT #L2 #H
75 @(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/
76 qed-.