]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / aaa.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "ground/xoa/ex_2_3.ma".
16 include "ground/xoa/ex_3_2.ma".
17 include "static_2/notation/relations/atomicarity_4.ma".
18 include "static_2/syntax/aarity.ma".
19 include "static_2/syntax/lenv.ma".
20 include "static_2/syntax/genv.ma".
21
22 (* ATONIC ARITY ASSIGNMENT FOR TERMS ****************************************)
23
24 (* activate genv *)
25 inductive aaa: relation4 genv lenv term aarity ≝
26 | aaa_sort: ∀G,L,s. aaa G L (⋆s) (⓪)
27 | aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ[I]V) (#0) B
28 | aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ[I]) (#↑i) A
29 | aaa_abbr: ∀p,G,L,V,T,B,A.
30             aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ[p]V.T) A
31 | aaa_abst: ∀p,G,L,V,T,B,A.
32             aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ[p]V.T) (②B.A)
33 | aaa_appl: ∀G,L,V,T,B,A. aaa G L V B → aaa G L T (②B.A) → aaa G L (ⓐV.T) A
34 | aaa_cast: ∀G,L,V,T,A. aaa G L V A → aaa G L T A → aaa G L (ⓝV.T) A
35 .
36
37 interpretation "atomic arity assignment (term)"
38    'AtomicArity G L T A = (aaa G L T A).
39
40 (* Basic inversion lemmas ***************************************************)
41
42 fact aaa_inv_sort_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
43 #G #L #T #A * -G -L -T -A //
44 [ #I #G #L #V #B #_ #s #H destruct
45 | #I #G #L #A #i #_ #s #H destruct
46 | #p #G #L #V #T #B #A #_ #_ #s #H destruct
47 | #p #G #L #V #T #B #A #_ #_ #s #H destruct
48 | #G #L #V #T #B #A #_ #_ #s #H destruct
49 | #G #L #V #T #A #_ #_ #s #H destruct
50 ]
51 qed-.
52
53 lemma aaa_inv_sort: ∀G,L,A,s. ❨G,L❩ ⊢ ⋆s ⁝ A → A = ⓪.
54 /2 width=6 by aaa_inv_sort_aux/ qed-.
55
56 fact aaa_inv_zero_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → T = #0 →
57                        ∃∃I,K,V. L = K.ⓑ[I]V & ❨G,K❩ ⊢ V ⁝ A.
58 #G #L #T #A * -G -L -T -A /2 width=5 by ex2_3_intro/
59 [ #G #L #s #H destruct
60 | #I #G #L #A #i #_ #H destruct
61 | #p #G #L #V #T #B #A #_ #_ #H destruct
62 | #p #G #L #V #T #B #A #_ #_ #H destruct
63 | #G #L #V #T #B #A #_ #_ #H destruct
64 | #G #L #V #T #A #_ #_ #H destruct
65 ]
66 qed-.
67
68 lemma aaa_inv_zero: ∀G,L,A. ❨G,L❩ ⊢ #0 ⁝ A →
69                     ∃∃I,K,V. L = K.ⓑ[I]V & ❨G,K❩ ⊢ V ⁝ A.
70 /2 width=3 by aaa_inv_zero_aux/ qed-.
71
72 fact aaa_inv_lref_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀i. T = #(↑i) →
73                        ∃∃I,K. L = K.ⓘ[I] & ❨G,K❩ ⊢ #i ⁝ A.
74 #G #L #T #A * -G -L -T -A
75 [ #G #L #s #j #H destruct
76 | #I #G #L #V #B #_ #j #H destruct
77 | #I #G #L #A #i #HA #j #H destruct /2 width=4 by ex2_2_intro/
78 | #p #G #L #V #T #B #A #_ #_ #j #H destruct
79 | #p #G #L #V #T #B #A #_ #_ #j #H destruct
80 | #G #L #V #T #B #A #_ #_ #j #H destruct
81 | #G #L #V #T #A #_ #_ #j #H destruct
82 ]
83 qed-.
84
85 lemma aaa_inv_lref: ∀G,L,A,i. ❨G,L❩ ⊢ #↑i ⁝ A →
86                     ∃∃I,K. L = K.ⓘ[I] & ❨G,K❩ ⊢ #i ⁝ A.
87 /2 width=3 by aaa_inv_lref_aux/ qed-.
88
89 fact aaa_inv_gref_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀l. T = §l → ⊥.
90 #G #L #T #A * -G -L -T -A
91 [ #G #L #s #k #H destruct
92 | #I #G #L #V #B #_ #k #H destruct
93 | #I #G #L #A #i #_ #k #H destruct
94 | #p #G #L #V #T #B #A #_ #_ #k #H destruct
95 | #p #G #L #V #T #B #A #_ #_ #k #H destruct
96 | #G #L #V #T #B #A #_ #_ #k #H destruct
97 | #G #L #V #T #A #_ #_ #k #H destruct
98 ]
99 qed-.
100
101 lemma aaa_inv_gref: ∀G,L,A,l. ❨G,L❩ ⊢ §l ⁝ A → ⊥.
102 /2 width=7 by aaa_inv_gref_aux/ qed-.
103
104 fact aaa_inv_abbr_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀p,W,U. T = ⓓ[p]W.U →
105                        ∃∃B. ❨G,L❩ ⊢ W ⁝ B & ❨G,L.ⓓW❩ ⊢ U ⁝ A.
106 #G #L #T #A * -G -L -T -A
107 [ #G #L #s #q #W #U #H destruct
108 | #I #G #L #V #B #_ #q #W #U #H destruct
109 | #I #G #L #A #i #_ #q #W #U #H destruct
110 | #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=2 by ex2_intro/
111 | #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
112 | #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
113 | #G #L #V #T #A #_ #_ #q #W #U #H destruct
114 ]
115 qed-.
116
117 lemma aaa_inv_abbr: ∀p,G,L,V,T,A. ❨G,L❩ ⊢ ⓓ[p]V.T ⁝ A →
118                     ∃∃B. ❨G,L❩ ⊢ V ⁝ B & ❨G,L.ⓓV❩ ⊢ T ⁝ A.
119 /2 width=4 by aaa_inv_abbr_aux/ qed-.
120
121 fact aaa_inv_abst_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀p,W,U. T = ⓛ[p]W.U →
122                        ∃∃B1,B2. ❨G,L❩ ⊢ W ⁝ B1 & ❨G,L.ⓛW❩ ⊢ U ⁝ B2 & A = ②B1.B2.
123 #G #L #T #A * -G -L -T -A
124 [ #G #L #s #q #W #U #H destruct
125 | #I #G #L #V #B #_ #q #W #U #H destruct
126 | #I #G #L #A #i #_ #q #W #U #H destruct
127 | #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
128 | #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=5 by ex3_2_intro/
129 | #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
130 | #G #L #V #T #A #_ #_ #q #W #U #H destruct
131 ]
132 qed-.
133
134 lemma aaa_inv_abst: ∀p,G,L,W,T,A. ❨G,L❩ ⊢ ⓛ[p]W.T ⁝ A →
135                     ∃∃B1,B2. ❨G,L❩ ⊢ W ⁝ B1 & ❨G,L.ⓛW❩ ⊢ T ⁝ B2 & A = ②B1.B2.
136 /2 width=4 by aaa_inv_abst_aux/ qed-.
137
138 fact aaa_inv_appl_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
139                        ∃∃B. ❨G,L❩ ⊢ W ⁝ B & ❨G,L❩ ⊢ U ⁝ ②B.A.
140 #G #L #T #A * -G -L -T -A
141 [ #G #L #s #W #U #H destruct
142 | #I #G #L #V #B #_ #W #U #H destruct
143 | #I #G #L #A #i #_ #W #U #H destruct
144 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
145 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
146 | #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3 by ex2_intro/
147 | #G #L #V #T #A #_ #_ #W #U #H destruct
148 ]
149 qed-.
150
151 lemma aaa_inv_appl: ∀G,L,V,T,A. ❨G,L❩ ⊢ ⓐV.T ⁝ A →
152                     ∃∃B. ❨G,L❩ ⊢ V ⁝ B & ❨G,L❩ ⊢ T ⁝ ②B.A.
153 /2 width=3 by aaa_inv_appl_aux/ qed-.
154
155 fact aaa_inv_cast_aux: ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
156                        ❨G,L❩ ⊢ W ⁝ A ∧ ❨G,L❩ ⊢ U ⁝ A.
157 #G #L #T #A * -G -L -T -A
158 [ #G #L #s #W #U #H destruct
159 | #I #G #L #V #B #_ #W #U #H destruct
160 | #I #G #L #A #i #_ #W #U #H destruct
161 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
162 | #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
163 | #G #L #V #T #B #A #_ #_ #W #U #H destruct
164 | #G #L #V #T #A #HV #HT #W #U #H destruct /2 width=1 by conj/
165 ]
166 qed-.
167
168 lemma aaa_inv_cast: ∀G,L,W,T,A. ❨G,L❩ ⊢ ⓝW.T ⁝ A →
169                     ❨G,L❩ ⊢ W ⁝ A ∧ ❨G,L❩ ⊢ T ⁝ A.
170 /2 width=3 by aaa_inv_cast_aux/ qed-.