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/grammar/aarity.ma".
16 include "basic_2/substitution/ldrop.ma".
18 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
20 inductive aaa: lenv → term → predicate aarity ≝
21 | aaa_sort: ∀L,k. aaa L (⋆k) ⓪
22 | aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
23 | aaa_abbr: ∀L,V,T,B,A.
24 aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓV. T) A
25 | aaa_abst: ∀L,V,T,B,A.
26 aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛV. T) (②B. A)
27 | aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
28 | aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓣV. T) A
31 interpretation "atomic arity assignment (term)"
32 'AtomicArity L T A = (aaa L T A).
34 (* Basic inversion lemmas ***************************************************)
36 fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪.
39 | #I #L #K #V #B #i #_ #_ #k #H destruct
40 | #L #V #T #B #A #_ #_ #k #H destruct
41 | #L #V #T #B #A #_ #_ #k #H destruct
42 | #L #V #T #B #A #_ #_ #k #H destruct
43 | #L #V #T #A #_ #_ #k #H destruct
47 lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ÷ A → A = ⓪.
50 fact aaa_inv_lref_aux: ∀L,T,A. L ⊢ T ÷ A → ∀i. T = #i →
51 ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
53 [ #L #k #i #H destruct
54 | #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
55 | #L #V #T #B #A #_ #_ #i #H destruct
56 | #L #V #T #B #A #_ #_ #i #H destruct
57 | #L #V #T #B #A #_ #_ #i #H destruct
58 | #L #V #T #A #_ #_ #i #H destruct
62 lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ÷ A →
63 ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
66 fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓓW. U →
67 ∃∃B. L ⊢ W ÷ B & L. ⓓW ⊢ U ÷ A.
69 [ #L #k #W #U #H destruct
70 | #I #L #K #V #B #i #_ #_ #W #U #H destruct
71 | #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=2/
72 | #L #V #T #B #A #_ #_ #W #U #H destruct
73 | #L #V #T #B #A #_ #_ #W #U #H destruct
74 | #L #V #T #A #_ #_ #W #U #H destruct
78 lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ÷ A →
79 ∃∃B. L ⊢ V ÷ B & L. ⓓV ⊢ T ÷ A.
82 fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓛW. U →
83 ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ U ÷ B2 & A = ②B1. B2.
85 [ #L #k #W #U #H destruct
86 | #I #L #K #V #B #i #_ #_ #W #U #H destruct
87 | #L #V #T #B #A #_ #_ #W #U #H destruct
88 | #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=5/
89 | #L #V #T #B #A #_ #_ #W #U #H destruct
90 | #L #V #T #A #_ #_ #W #U #H destruct
94 lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ÷ A →
95 ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ T ÷ B2 & A = ②B1. B2.
98 fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓐW. U →
99 ∃∃B. L ⊢ W ÷ B & L ⊢ U ÷ ②B. A.
101 [ #L #k #W #U #H destruct
102 | #I #L #K #V #B #i #_ #_ #W #U #H destruct
103 | #L #V #T #B #A #_ #_ #W #U #H destruct
104 | #L #V #T #B #A #_ #_ #W #U #H destruct
105 | #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
106 | #L #V #T #A #_ #_ #W #U #H destruct
110 lemma aaa_inv_appl: ∀L,V,T,A. L ⊢ ⓐV. T ÷ A →
111 ∃∃B. L ⊢ V ÷ B & L ⊢ T ÷ ②B. A.
114 fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓣW. U →
115 L ⊢ W ÷ A ∧ L ⊢ U ÷ A.
117 [ #L #k #W #U #H destruct
118 | #I #L #K #V #B #i #_ #_ #W #U #H destruct
119 | #L #V #T #B #A #_ #_ #W #U #H destruct
120 | #L #V #T #B #A #_ #_ #W #U #H destruct
121 | #L #V #T #B #A #_ #_ #W #U #H destruct
122 | #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
126 lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ÷ A →
127 L ⊢ W ÷ A ∧ L ⊢ T ÷ A.