]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy_new/arity.ma
almost there
[helm.git] / matita / matita / lib / pts_dummy_new / arity.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 "pts_dummy/ext.ma".
16 (*
17 (* ARITIES ********************************************************************)
18
19 (* An arity is a normal term representing the functional structure of a term.
20  * Arities can be freely applied as lon as the result is typable in λ→.
21  * we encode an arity with a family of meta-linguistic functions typed by λ→
22  * Such a family contains one member for each type of λ→ 
23  *)
24
25 (* type of arity members ******************************************************)
26
27 (* the type of an arity member *)
28 inductive MEM: Type[0] ≝
29    | TOP: MEM
30    | FUN: MEM → MEM → MEM
31 .
32
33 definition pred ≝ λC. match C with
34    [ TOP     ⇒ TOP
35    | FUN _ A ⇒ A
36    ].
37
38 definition decidable_MEq: ∀C1,C2:MEM. (C1 = C2) + (C1 ≠ C2).
39 #C1 (elim C1) -C1
40    [ #C2 elim C2 -C2
41      [ /2/
42      | #B2 #A2 #_ #_ @inr @nmk #false destruct
43      ]
44    | #B1 #A1 #IHB1 #IHA1 #C2 elim C2 -C2
45      [ @inr @nmk #false destruct
46      | #B2 #A2 #_ #_ elim (IHB1 B2) -IHB1 #HB
47        [ elim (IHA1 A2) - IHA1 #HA
48          [ /2/ | @inr @nmk #false destruct elim HA /2/ ]
49        | @inr @nmk #false destruct elim HB /2/
50    ]
51 qed.
52
53 lemma fun_neq_sym: ∀A,C,B. pred C ≠ A → C ≠ FUN B A.
54 #A #C #B #HA elim HA -HA #HA @nmk #H @HA -HA >H //
55 qed. 
56
57 (* arity members **************************************************************)
58
59 (* the arity members of type TOP *)
60 inductive Top: Type[0] ≝
61    | SORT: Top
62
63
64 (* the arity members of type A *)
65 let rec Mem A ≝ match A with
66    [ TOP     ⇒ Top
67    | FUN B A ⇒ Mem B → Mem A
68    ].
69
70 (* the members of the arity "sort" *)
71 let rec sort_mem A ≝ match A return λA. Mem A with
72    [ TOP     ⇒ SORT
73    | FUN B A ⇒ λ_.sort_mem A
74    ]. 
75
76 (* arities ********************************************************************)
77
78 (* the type of arities *)
79 definition Arity ≝ ∀A. Mem A.
80
81 (* the arity "sort" *)
82 definition sort ≝ λA. sort_mem A.
83
84 (* the arity "constant" *)
85 definition const: ∀B. Mem B → Arity.
86 #B #x #A. elim (decidable_MEq B A) #H [ elim H @x | @(sort_mem A) ]
87 qed.
88
89 (* application of arities *)
90 definition aapp: MEM → Arity → Arity → Arity  ≝ λB,a,b,C. a (FUN B C) (b B).
91
92 (* abstraction of arities *)
93 definition aabst: (Arity → Arity) → Arity ≝
94    λf,C. match C return λC. Mem C with
95    [ TOP     ⇒ sort_mem TOP
96    | FUN B A ⇒ λx. f (const B x) A
97    ].
98
99 (* extensional equality of arity members **************************************)
100
101 (* Extensional equality of arity members (extensional equalty of functions).
102  * The functions may not respect extensional equality so reflexivity fails
103  * in general but may hold for specific arity members.
104  *)
105 let rec ameq A ≝ match A return λA. Mem A → Mem A → Prop with
106    [ TOP     ⇒ λa1,a2. a1 = a2
107    | FUN B A ⇒ λa1,a2. ∀b1,b2. ameq B b1 b2 → ameq A (a1 b1) (a2 b2)
108    ].
109
110 interpretation
111    "extensional equality (arity member)"
112    'Eq1 A a1 a2 = (ameq A a1 a2).
113
114 (* reflexivity of extensional equality for an arity member *)
115 definition invariant_mem ≝ λA,m. m ≅^A m.
116
117 interpretation
118    "invariance (arity member)"
119    'Invariant1 a A = (invariant_mem A a).
120
121
122 interpretation
123    "invariance (arity member with implicit type)"
124    'Invariant a = (invariant_mem ? a).
125
126 lemma symmetric_ameq: ∀A. symmetric ? (ameq A).
127 #A elim A -A /4/
128 qed.
129
130 lemma transitive_ameq: ∀A. transitive ? (ameq A).
131 #A elim A -A /5/
132 qed.
133
134 lemma invariant_sort_mem: ∀A. ! sort_mem A.
135 #A elim A normalize //
136 qed.
137
138 axiom const_eq: ∀A,x. const A x A ≅^A x.
139
140 axiom const_neq: ∀A,B,x. A ≠ B → const A x B ≅^B (sort_mem B).
141
142 (* extensional equality of arities ********************************************)
143
144 definition aeq: Arity → Arity → Prop ≝ λa1,a2. ∀A. a1 A ≅^A a2 A.
145
146 interpretation
147    "extensional equality (arity)"
148    'Eq a1 a2 = (aeq a1 a2).
149
150 definition invariant: Arity → Prop ≝ λa. a ≅ a.
151
152 interpretation
153    "invariance (arity)"
154    'Invariant a = (invariant a).
155
156 lemma symmetric_aeq: symmetric … aeq.
157 /2/ qed.
158
159 lemma transitive_aeq: transitive … aeq.
160 /2/ qed.
161
162 lemma const_comp: ∀A,x1,x2. x1 ≅^A x2 → const … x1 ≅ const … x2.
163 #A #x1 #x2 #Hx #C elim (decidable_MEq A C) #H
164    [ <H @transitive_ameq; [2: @const_eq | skip ]
165         @transitive_ameq; [2: @Hx | skip ]
166         @symmetric_ameq //
167    | @transitive_ameq; [2: @(const_neq … H) | skip ]
168      @transitive_ameq; [2: @invariant_sort_mem | skip ]
169      @symmetric_ameq /2/
170    ]
171 qed.
172
173 lemma aapp_comp: ∀C,a1,a2,b1,b2. a1 ≅ a2 → b1 ≅ b2 → aapp C a1 b1 ≅ aapp C a2 b2.
174 #C #a1 #a2 #b1 #b2 #Ha #Hb #D @(Ha (FUN C D)) //
175 qed.
176
177 lemma aabst_comp: ∀f1,f2. (∀a1,a2. a1 ≅ a2 → f1 a1 ≅ f2 a2) →
178                   aabst f1 ≅ aabst f2.
179 #f1 #f2 #H #C elim C -C // #B #A #_ #_ #b1 #b2 #Hb @H /2/
180 qed.
181
182 lemma invariant_sort: ! sort.
183 normalize //
184 qed.
185
186 (* "is a constant arity" *)
187 definition isc ≝ λa,A. const ? (a A) ≅ a.
188
189 lemma isc_sort: ∀A. isc sort A.
190 #A #C elim (decidable_MEq A C) #H [ <H // | /2 by const_neq/ ].
191 qed.
192
193 lemma isc_aapp: ∀B,A,b,a. ! b B → isc a A → isc (aapp B a b) (pred A).
194 #B #A #b #a #Hb #Ha #C elim (decidable_MEq (pred A) C) #H [ >H // ]
195 @transitive_ameq; [2: @(const_neq … H) | skip ]
196 lapply (transitive_ameq ????? (Ha (FUN B C))) -Ha [3: #Ha @Ha // |2: skip ]
197 @symmetric_ameq @const_neq /2/
198 qed.
199
200 (* extensional equality of arity contexts *************************************)
201
202 definition aceq ≝ λE1,E2. all2 … aeq E1 E2.
203
204 interpretation
205    "extensional equality (arity context)"
206    'Eq E1 E2 = (aceq E1 E2).
207
208 definition invariant_env: list Arity → Prop ≝ λE. E ≅ E.
209
210 interpretation
211    "invariance (arity context)"
212    'Invariant E = (invariant_env E).
213
214 lemma symmetric_aceq: symmetric … aceq.
215 /2/ qed.
216
217 lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
218                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
219 #E1 #E2 #H #i @(all2_nth … aeq) //
220 qed.
221 *)