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_equivalence/cpes.ma".
16 include "basic_2/dynamic/cnv_aaa.ma".
18 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
20 (* Properties with t-bound rt-equivalence for terms *************************)
22 lemma cnv_appl_cpes (a) (h) (G) (L):
24 ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] →
25 ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W →
26 ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h].
27 #a #h #G #L #n #Hn #V #HV #T #HT #W *
28 /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
31 lemma cnv_cast_cpes (a) (h) (G) (L):
32 ∀U. ⦃G, L⦄ ⊢ U ![a, h] →
33 ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G, L⦄ ⊢ ⓝU.T ![a, h].
34 #a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
37 (* Inversion lemmas with t-bound rt-equivalence for terms *******************)
39 lemma cnv_inv_appl_cpes (a) (h) (G) (L):
40 ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
41 ∃∃n,p,W,U. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
42 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
44 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
45 /3 width=7 by cpms_div, ex5_4_intro/
48 lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L):
49 ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![yinj a, h] →
50 ∃∃p,W,U. ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
51 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W.U.
53 elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU
54 /3 width=7 by cpms_div, ex4_3_intro/
57 lemma cnv_inv_cast_cpes (a) (h) (G) (L):
58 ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
59 ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
61 elim (cnv_inv_cast … H) -H
62 /3 width=3 by cpms_div, and3_intro/
65 (* Eliminators with t-bound rt-equivalence for terms ************************)
67 lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term):
68 (∀G,L,s. Q G L (⋆s)) →
69 (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) →
70 (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) →
71 (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
72 Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
74 (∀n,p,G,L,V,W,T,U. yinj n < a → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
75 ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U →
76 Q G L V → Q G L T → Q G L (ⓐV.T)
78 (∀G,L,U,T. ⦃G,L⦄⊢ U![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T →
79 Q G L U → Q G L T → Q G L (ⓝU.T)
81 ∀G,L,T. ⦃G,L⦄⊢ T![a,h] → Q G L T.
82 #a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
83 elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ]