1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/rt_computation/cpms_fpbg.ma".
16 include "basic_2/dynamic/cnv.ma".
18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
20 (* Inductive premises for the preservation results **************************)
22 definition IH_cnv_cpm_trans_lpr (h) (a): relation3 genv lenv term ≝
23 λG,L1,T1. ⦃G,L1⦄ ⊢ T1 ![h,a] →
24 ∀n,T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 →
25 ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 ![h,a].
27 definition IH_cnv_cpms_trans_lpr (h) (a): relation3 genv lenv term ≝
28 λG,L1,T1. ⦃G,L1⦄ ⊢ T1 ![h,a] →
29 ∀n,T2. ⦃G,L1⦄ ⊢ T1 ➡*[n,h] T2 →
30 ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ⦃G,L2⦄ ⊢ T2 ![h,a].
32 definition IH_cnv_cpm_conf_lpr (h) (a): relation3 genv lenv term ≝
33 λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
34 ∀n1,T1. ⦃G,L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G,L0⦄ ⊢ T0 ➡[n2,h] T2 →
35 ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ➡[h] L2 →
36 ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
38 definition IH_cnv_cpms_strip_lpr (h) (a): relation3 genv lenv term ≝
39 λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
40 ∀n1,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L0⦄ ⊢ T0 ➡[n2,h] T2 →
41 ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ➡[h] L2 →
42 ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
44 definition IH_cnv_cpms_conf_lpr (h) (a): relation3 genv lenv term ≝
45 λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
46 ∀n1,T1. ⦃G,L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L0⦄ ⊢ T0 ➡*[n2,h] T2 →
47 ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ➡[h] L2 →
48 ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
50 (* Auxiliary properties for preservation ************************************)
52 fact cnv_cpms_trans_lpr_sub (h) (a):
54 (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
55 ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_trans_lpr h a G1 L1 T1.
56 #h #a #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
57 @(cpms_ind_dx … H) -n -T2
58 /3 width=7 by fpbg_cpms_trans/
61 fact cnv_cpm_conf_lpr_sub (h) (a):
63 (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
64 ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_conf_lpr h a G1 L1 T1.
65 /3 width=8 by cpm_cpms/ qed-.
67 fact cnv_cpms_strip_lpr_sub (h) (a):
69 (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
70 ∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_strip_lpr h a G1 L1 T1.
71 /3 width=8 by cpm_cpms/ qed-.