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/notation/relations/exclaim_5.ma".
16 include "basic_2/rt_computation/cpms.ma".
18 (* NATIVE VALIDITY FOR TERMS ************************************************)
21 (* Basic_2A1: uses: snv *)
22 inductive nv (a) (h): relation3 genv lenv term ≝
23 | nv_sort: ∀G,L,s. nv a h G L (⋆s)
24 | nv_zero: ∀I,G,K,V. nv a h G K V → nv a h G (K.ⓑ{I}V) (#0)
25 | nv_lref: ∀I,G,K,i. nv a h G K (#i) → nv a h G (K.ⓘ{I}) (#↑i)
26 | nv_bind: ∀p,I,G,L,V,T. nv a h G L V → nv a h G (L.ⓑ{I}V) T → nv a h G L (ⓑ{p,I}V.T)
27 | nv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n = 1) → nv a h G L V → nv a h G L T →
28 ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → nv a h G L (ⓐV.T)
29 | nv_cast: ∀G,L,U,T,U0. nv a h G L U → nv a h G L T →
30 ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → nv a h G L (ⓝU.T)
33 interpretation "native validity (term)"
34 'Exclaim a h G L T = (nv a h G L T).
36 (* Basic inversion lemmas ***************************************************)
38 fact nv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
39 ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
40 #a #h #G #L #X * -G -L -X
41 [ #G #L #s #H destruct
42 | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
43 | #I #G #K #i #_ #H destruct
44 | #p #I #G #L #V #T #_ #_ #H destruct
45 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #H destruct
46 | #G #L #U #T #U0 #_ #_ #_ #_ #H destruct
50 lemma nv_inv_zero (a) (h): ∀G,L. ⦃G, L⦄ ⊢ #0 ![a, h] →
51 ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
52 /2 width=3 by nv_inv_zero_aux/ qed-.
54 fact nv_inv_lref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀i. X = #(↑i) →
55 ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
56 #a #h #G #L #X * -G -L -X
57 [ #G #L #s #j #H destruct
58 | #I #G #K #V #_ #j #H destruct
59 | #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/
60 | #p #I #G #L #V #T #_ #_ #j #H destruct
61 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #j #H destruct
62 | #G #L #U #T #U0 #_ #_ #_ #_ #j #H destruct
66 lemma nv_inv_lref (a) (h): ∀G,L,i. ⦃G, L⦄ ⊢ #↑i ![a, h] →
67 ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
68 /2 width=3 by nv_inv_lref_aux/ qed-.
70 fact nv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀l. X = §l → ⊥.
71 #a #h #G #L #X * -G -L -X
72 [ #G #L #s #l #H destruct
73 | #I #G #K #V #_ #l #H destruct
74 | #I #G #K #i #_ #l #H destruct
75 | #p #I #G #L #V #T #_ #_ #l #H destruct
76 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #l #H destruct
77 | #G #L #U #T #U0 #_ #_ #_ #_ #l #H destruct
81 (* Basic_2A1: uses: snv_inv_gref *)
82 lemma nv_inv_gref (a) (h): ∀G,L,l. ⦃G, L⦄ ⊢ §l ![a, h] → ⊥.
83 /2 width=8 by nv_inv_gref_aux/ qed-.
85 fact nv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] →
86 ∀p,I,V,T. X = ⓑ{p,I}V.T →
88 & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
89 #a #h #G #L #X * -G -L -X
90 [ #G #L #s #q #Z #X1 #X2 #H destruct
91 | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
92 | #I #G #K #i #_ #q #Z #X1 #X2 #H destruct
93 | #p #I #G #L #V #T #HV #HT #q #Z #X1 #X2 #H destruct /2 width=1 by conj/
94 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
95 | #G #L #U #T #U0 #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
99 (* Basic_2A1: uses: snv_inv_bind *)
100 lemma nv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] →
101 ∧∧ ⦃G, L⦄ ⊢ V ![a, h]
102 & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
103 /2 width=4 by nv_inv_bind_aux/ qed-.
105 fact nv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T →
106 ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
107 ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
108 #a #h #G #L #X * -L -X
109 [ #G #L #s #X1 #X2 #H destruct
110 | #I #G #K #V #_ #X1 #X2 #H destruct
111 | #I #G #K #i #_ #X1 #X2 #H destruct
112 | #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
113 | #n #p #G #L #V #W0 #T #U0 #Ha #HV #HT #HVW0 #HTU0 #X1 #X2 #H destruct /3 width=7 by ex5_4_intro/
114 | #G #L #U #T #U0 #_ #_ #_ #_ #X1 #X2 #H destruct
118 (* Basic_2A1: uses: snv_inv_appl *)
119 lemma nv_inv_appl (a) (h): ∀G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
120 ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
121 ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
122 /2 width=3 by nv_inv_appl_aux/ qed-.
124 fact nv_inv_cast_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀U,T. X = ⓝU.T →
125 ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
126 ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
127 #a #h #G #L #X * -G -L -X
128 [ #G #L #s #X1 #X2 #H destruct
129 | #I #G #K #V #_ #X1 #X2 #H destruct
130 | #I #G #K #i #_ #X1 #X2 #H destruct
131 | #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
132 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #X1 #X2 #H destruct
133 | #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
137 (* Basic_2A1: uses: snv_inv_appl *)
138 lemma nv_inv_cast (a) (h): ∀G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
139 ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
140 ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
141 /2 width=3 by nv_inv_cast_aux/ qed-.