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/dynamic/nta_drops.ma".
16 include "basic_2/dynamic/nta_cpms.ma".
17 include "basic_2/dynamic/nta_cpcs.ma".
18 include "basic_2/dynamic/nta_preserve.ma".
20 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
22 (* Advanced eliminators *****************************************************)
24 lemma nta_ind_rest_cnv (h) (Q:relation4 …):
25 (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
27 ⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] W ≘ U →
28 Q G K V W → Q G (K.ⓓV) (#0) U
30 (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
32 ⦃G,K⦄ ⊢ #i :[h] W → ⬆*[1] W ≘ U →
33 Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
36 ⦃G,K⦄ ⊢ V ![h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h] U →
37 Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
40 ⦃G,L⦄ ⊢ V :[h] W → ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U →
41 Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
43 (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U → Q G L (ⓝU.T) U
46 ⦃G,L⦄ ⊢ T :[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h] →
47 Q G L T U1 → Q G L T U2
49 ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U.
50 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #G #L #T
51 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
52 [ #s #HG #HL #HT #X #H destruct -IH
53 elim (nta_inv_sort_sn … H) -H #HUX #HX
55 | * [| #i ] #HG #HL #HT #X #H destruct
56 [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
57 [ #K #V #W #U #H #HVW #HWU #HUX #HX
58 lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
59 /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
60 | #K #W #U #H #HW #HWU #HUX #HX
61 lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
62 /3 width=4 by nta_ldec_cnv/
64 | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
65 /5 width=7 by nta_lref, fqu_fqup/
67 | #l #HG #HL #HT #U #H destruct -IH
68 elim (nta_inv_gref_sn … H)
69 | #p #I #V #T #HG #HL #HT #X #H destruct
70 elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
71 /4 width=5 by nta_bind_cnv/
72 | #V #T #HG #HL #HT #X #H destruct
73 elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
74 /4 width=9 by nta_appl/
75 | #U #T #HG #HL #HT #X #H destruct
76 elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
77 /4 width=4 by nta_cast/
81 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
82 (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
84 ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
85 Q G K V W → Q G (K.ⓓV) (#0) U
87 (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
89 ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
90 Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
93 ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
94 Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
97 ⦃G,L⦄ ⊢ V :*[h] W → ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U →
98 Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
101 ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
102 Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
104 (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
107 ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
108 Q G L T U1 → Q G L T U2
110 ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
111 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T
112 @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
113 [ #s #HG #HL #HT #X #H destruct -IH
114 elim (nta_inv_sort_sn … H) -H #HUX #HX
116 | * [| #i ] #HG #HL #HT #X #H destruct
117 [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
118 [ #K #V #W #U #H #HVW #HWU #HUX #HX
119 lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
120 /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
121 | #K #W #U #H #HW #HWU #HUX #HX
122 lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
123 /3 width=4 by nta_ldec_cnv/
125 | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
126 /5 width=7 by nta_lref, fqu_fqup/
128 | #l #HG #HL #HT #U #H destruct -IH
129 elim (nta_inv_gref_sn … H)
130 | #p #I #V #T #HG #HL #HT #X #H destruct
131 elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
132 /4 width=5 by nta_bind_cnv/
133 | #V #T #HG #HL #HT #X #H destruct
134 elim (nta_inv_pure_sn_cnv … H) -H *
135 [ #p #W #U #HVW #HTU #HUX #HX
136 /4 width=9 by nta_appl/
137 | #U #HTU #HVU #HUX #HX
138 /4 width=6 by nta_pure_cnv/
140 | #U #T #HG #HL #HT #X #H destruct
141 elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
142 /4 width=4 by nta_cast/
146 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
147 (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
149 ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
150 Q G K V W → Q G (K.ⓓV) (#0) U
152 (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
154 ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
155 Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
158 ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
159 Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
162 ⦃G,K⦄ ⊢ V :*[h] W → ⦃G,K.ⓛW⦄ ⊢ T :*[h] U →
163 Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ{p}W.T) (ⓐV.ⓛ{p}W.U)
166 ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
167 Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
169 (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
172 ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
173 Q G L T U1 → Q G L T U2
175 ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
176 #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
177 @(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
178 #p #G #L #V #W #T #U #HVW #HTU #_ #IHTU
179 lapply (nta_fwd_cnv_dx … HTU) #H
180 elim (cnv_inv_bind … H) -H #_ #HU
181 elim (cnv_nta_sn … HU) -HU #X #HUX
182 /4 width=2 by nta_appl_abst, nta_fwd_cnv_sn/