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_cpms.ma".
16 include "basic_2/rt_equivalence/cpes.ma".
17 include "basic_2/dynamic/cnv.ma".
19 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
21 (* Properties with t-bound rt-equivalence for terms *************************)
23 lemma cnv_appl_cpes (h) (a) (G) (L):
25 ∀V. ❨G,L❩ ⊢ V ![h,a] → ∀T. ❨G,L❩ ⊢ T ![h,a] →
26 ∀W. ❨G,L❩ ⊢ V ⬌*[h,1,0] W →
27 ∀p,U. ❨G,L❩ ⊢ T ➡*[h,n] ⓛ[p]W.U → ❨G,L❩ ⊢ ⓐV.T ![h,a].
28 #h #a #G #L #n #Hn #V #HV #T #HT #W *
29 /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
32 lemma cnv_cast_cpes (h) (a) (G) (L):
33 ∀U. ❨G,L❩ ⊢ U ![h,a] →
34 ∀T. ❨G,L❩ ⊢ T ![h,a] → ❨G,L❩ ⊢ U ⬌*[h,0,1] T → ❨G,L❩ ⊢ ⓝU.T ![h,a].
35 #h #a #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
38 (* Inversion lemmas with t-bound rt-equivalence for terms *******************)
40 lemma cnv_inv_appl_cpes (h) (a) (G) (L):
41 ∀V,T. ❨G,L❩ ⊢ ⓐV.T ![h,a] →
42 ∃∃n,p,W,U. ad a n & ❨G,L❩ ⊢ V ![h,a] & ❨G,L❩ ⊢ T ![h,a] &
43 ❨G,L❩ ⊢ V ⬌*[h,1,0] W & ❨G,L❩ ⊢ T ➡*[h,n] ⓛ[p]W.U.
45 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
46 /3 width=7 by cpms_div, ex5_4_intro/
49 lemma cnv_inv_cast_cpes (h) (a) (G) (L):
50 ∀U,T. ❨G,L❩ ⊢ ⓝU.T ![h,a] →
51 ∧∧ ❨G,L❩ ⊢ U ![h,a] & ❨G,L❩ ⊢ T ![h,a] & ❨G,L❩ ⊢ U ⬌*[h,0,1] T.
53 elim (cnv_inv_cast … H) -H
54 /3 width=3 by cpms_div, and3_intro/
57 (* Eliminators with t-bound rt-equivalence for terms ************************)
59 lemma cnv_ind_cpes (h) (a) (Q:relation3 genv lenv term):
60 (∀G,L,s. Q G L (⋆s)) →
61 (∀I,G,K,V. ❨G,K❩ ⊢ V![h,a] → Q G K V → Q G (K.ⓑ[I]V) (#O)) →
62 (∀I,G,K,i. ❨G,K❩ ⊢ #i![h,a] → Q G K (#i) → Q G (K.ⓘ[I]) (#(↑i))) →
63 (∀p,I,G,L,V,T. ❨G,L❩ ⊢ V![h,a] → ❨G,L.ⓑ[I]V❩⊢T![h,a] →
64 Q G L V →Q G (L.ⓑ[I]V) T →Q G L (ⓑ[p,I]V.T)
66 (∀n,p,G,L,V,W,T,U. ad a n → ❨G,L❩ ⊢ V![h,a] → ❨G,L❩ ⊢ T![h,a] →
67 ❨G,L❩ ⊢ V ⬌*[h,1,0]W → ❨G,L❩ ⊢ T ➡*[h,n] ⓛ[p]W.U →
68 Q G L V → Q G L T → Q G L (ⓐV.T)
70 (∀G,L,U,T. ❨G,L❩⊢ U![h,a] → ❨G,L❩ ⊢ T![h,a] → ❨G,L❩ ⊢ U ⬌*[h,0,1] T →
71 Q G L U → Q G L T → Q G L (ⓝU.T)
73 ∀G,L,T. ❨G,L❩⊢ T![h,a] → Q G L T.
74 #h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
75 elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ]