]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/arity_eval.ma
made executable again
[helm.git] / matita / matita / lib / pts_dummy / arity_eval.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/arity.ma".
16 (*
17 (* ARITY ASSIGNMENT ***********************************************************)
18
19 (* the arity type *************************************************************)
20
21 (* arity type assigned to the term t in the environment E *)
22 let rec ata K t on t ≝  match t with
23    [ Sort _     ⇒ TOP
24    | Rel i      ⇒ nth i … K TOP
25    | App M N    ⇒ pred (ata K M) 
26    | Lambda N M ⇒ let C ≝ ata K N in FUN C (ata (C::K) M)
27    | Prod _ _   ⇒ TOP
28    | D M        ⇒ TOP (* ??? not so sure yet *)
29    ].
30
31 interpretation "arity type assignment" 'IInt1 t K = (ata K t).
32
33 lemma ata_app: ∀M,N,K. 〚App M N〛_[K] = pred (〚M〛_[K]).
34 // qed.
35
36 lemma ata_lambda: ∀M,N,K. 〚Lambda N M〛_[K] = FUN (〚N〛_[K]) (〚M〛_[〚N〛_[K]::K]).
37 // qed.
38
39 lemma ata_rel_lt: ∀H,K,i. (S i) ≤ |K| → 〚Rel i〛_[K @ H] = 〚Rel i〛_[K].
40 #H #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
41 #A #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
42 qed.
43
44 lemma ata_rel_ge: ∀H,K,i. (S i) ≰ |K| →
45                   〚Rel i〛_[K @ H] = 〚Rel (i-|K|)〛_[H].
46 #H #K elim K -K [ normalize // ]
47 #A #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
48 normalize #i #_ #Hie @IHK /2/
49 qed.
50
51 (* weakeing and thinning lemma for the arity type assignment *)
52 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
53 lemma ata_lift: ∀p,K,Kp. p = |Kp| → ∀t,k,Kk. k = |Kk| →
54                 〚lift t k p〛_[Kk @ Kp @ K] = 〚t〛_[Kk @ K].
55 #p #K #Kp #HKp #t elim t -t //
56    [ #i #k #Kk #HKk @(leb_elim (S i) k) #Hik
57      [ >(lift_rel_lt … Hik) >HKk in Hik #Hik
58        >(ata_rel_lt … Hik) >(ata_rel_lt … Hik) //
59      | >(lift_rel_ge … Hik) >HKk in Hik #Hik
60        >(ata_rel_ge … Hik) <associative_append
61        >(ata_rel_ge …) >length_append >HKp;
62        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
63      ]
64    | #M #N #IHM #_ #k #Kk #HKk >lift_app >ata_app /3/
65    | #N #M #IHN #IHM #k #Kk #HKk >lift_lambda >ata_lambda
66      >IHN // >(IHM … (? :: ?)) // >commutative_plus /2/ 
67    ]
68 qed.
69
70 (* substitution lemma for the arity type assignment *)
71 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
72 lemma ata_subst: ∀v,K,t,k,Kk. k = |Kk| → 
73                  〚t[k≝v]〛_[Kk @ K] = 〚t〛_[Kk @ 〚v〛_[K]::K].
74 #v #K #t elim t -t //
75    [ #i #k #Kk #HKk @(leb_elim (S i) k) #H1ik
76      [ >(subst_rel1 … H1ik) >HKk in H1ik #H1ik
77        >(ata_rel_lt … H1ik) >(ata_rel_lt … H1ik) //
78      | @(eqb_elim i k) #H2ik
79        [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HKk in H1ik #H1ik
80          >(ata_rel_ge … H1ik) <minus_n_n >(ata_lift ? ? ? ? ? ? ([])) //
81        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
82           >ata_rel_ge; [2: /2/ ] <(associative_append ? ? ([?]) ?)
83            >ata_rel_ge >length_append >commutative_plus;
84            [ <minus_plus // | <HKk -HKk Kk @not_le_to_not_le_S_S /3/ ]
85        ]
86      ]
87    | #M #N #IHM #_ #k #Kk #HKk >subst_app >ata_app /3/
88    | #N #M #IHN #IHM #k #Kk #HKk >subst_lambda > ata_lambda
89      >IHN // >commutative_plus >(IHM … (? :: ?)) /2/
90    ]
91 qed.
92
93 (* the arity ******************************************************************)
94
95 (* arity assigned to the term t in the environments E and K *)
96 let rec aa K E t on t ≝ match t with
97    [ Sort _     ⇒ sort
98    | Rel i      ⇒ nth i … E sort
99    | App M N    ⇒ aapp (〚N〛_[K]) (aa K E M) (aa K E N)
100    | Lambda N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
101    | Prod N M   ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
102    | D M        ⇒ sort (* ??? not so sure yet *)
103    ].
104
105 interpretation "arity assignment" 'IInt2 t E K = (aa K E t).
106
107 lemma aa_app: ∀M,N,E,K. 〚App M N〛_[E,K] = aapp (〚N〛_[K]) (〚M〛_[E,K]) (〚N〛_[E,K]).
108 // qed.
109
110 lemma aa_lambda: ∀N,M,E,K. 〚Lambda N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
111 // qed.
112
113 lemma aa_prod: ∀N,M,E,K. 〚Prod N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
114 // qed.
115
116 lemma aa_rel_lt: ∀K2,K1,D,E,i. (S i) ≤ |E| →
117                  〚Rel i〛_[E @ D, K1] = 〚Rel i〛_[E, K2].
118 #K1 #K1 #D #E elim E -E [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
119 #C #E #IHE #i elim i -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
120 qed.
121
122 lemma aa_rel_lt_id: ∀K,D,E,i. (S i) ≤ |E| →
123                     〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E, K].
124 #K @(aa_rel_lt K) qed.
125
126 lemma aa_rel_ge: ∀K2,K1,D,E,i. (S i) ≰ |E| →
127                  〚Rel i〛_[E @ D, K1] = 〚Rel (i-|E|)〛_[D, K2].
128 #K2 #K1 #D #E elim E -E [ normalize // ]
129 #C #E #IHE #i elim i -i [1: -IHE #Hie elim Hie -Hie #Hie elim (Hie ?) /2/ ]
130 normalize #i #_ #Hie @IHE /2/
131 qed.
132
133 lemma aa_rel_ge_id: ∀K,D,E,i. (S i) ≰ |E| →
134                     〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D, K].
135 #K @(aa_rel_ge K) qed.
136
137 (* weakeing and thinning lemma for the arity assignment *)
138 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
139 lemma aa_lift: ∀K,E1,E2. E1 ≅ E2 → ∀p,Kp,Ep. p=|Kp| → p = |Ep| →
140                ∀t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
141                〚lift t k p〛_[E1k @ Ep @ E1, Kk @ Kp @ K] ≅ 〚t〛_[E2k @ E2, Kk @ K].
142 #K #E1 #E2 #HE #p #Kp #Ep #HKp #HEp #t elim t -t /2 by invariant_sort/
143    [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #Hik
144      [ >(lift_rel_lt … Hik) >HE1k in Hik #Hik >(aa_rel_lt_id … Hik)
145        >(all2_length … HEk) in Hik #Hik >(aa_rel_lt_id … Hik) /2 by nth_sort_comp/
146      | >(lift_rel_ge … Hik) >HE1k in Hik #Hik <(associative_append … E1k)
147        >(aa_rel_ge_id …) >length_append >HEp; [2: @(arith3 … Hik) ]
148        >(all2_length … HEk) in Hik #Hik >(aa_rel_ge_id … Hik) >arith2;
149        [ /2 by nth_sort_comp/ | @not_lt_to_le /2/ ]
150      ]
151    | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_app >aa_app
152      >ata_lift /3/
153    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_lambda >aa_lambda
154      @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
155      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
156    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_prod >aa_prod
157      @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
158      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
159    ]
160 qed.
161
162 lemma aa_comp: ∀E1,E2. E1 ≅ E2 → ∀t,K. 〚t〛_[E1, K] ≅ 〚t〛_[E2, K].
163 #E1 #E2 #HE #t #K <(lift_0 t 0) in ⊢ (? % ?)
164 @(aa_lift … ([]) ([]) … ([]) ([]) ([])) //
165 qed.
166
167 (* the assigned arity is invariant *)
168 lemma aa_invariant: ∀t,E,K. !E → !〚t〛_[E, K].
169 /2/ qed.
170
171 (* substitution lemma for the arity assignment *)
172 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
173 lemma aa_subst: ∀K,E1,E2. E1 ≅ E2 →
174                 ∀v,t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
175                 〚t[k≝v]〛_[E1k@E1, Kk@K] ≅ 〚t〛_[E2k@〚v〛_[E2,K]::E2, Kk@〚v〛_[K]::K].
176 #K #E1 #E2 #HE #v #t elim t -t /2 by invariant_sort/
177    [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #H1ik
178      [ >(subst_rel1 … H1ik) >HE1k in H1ik #H1ik >(aa_rel_lt_id … H1ik)
179        >(all2_length … HEk) in H1ik #H1ik >(aa_rel_lt_id … H1ik) /2/
180      | @(eqb_elim i k) #H2ik
181        [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HE1k in H1ik #H1ik
182          >(all2_length … HEk) in H1ik #H1ik >(aa_rel_ge_id … H1ik) <minus_n_n
183          >HE1k in HKk #HKk -HE1k k  >(all2_length … HEk) in HKk #HKk
184          @(aa_lift … ([]) ([]) ([])) /3/
185        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
186          >(subst_rel3 … Hik) >aa_rel_ge_id; [2: /2/ ]
187          <(associative_append ? ? ([?]) ?) in ⊢ (? ? (? ? % ?))
188          >HE1k in Hik #Hik >(aa_rel_ge (Kk@K))
189          >length_append >commutative_plus <(all2_length … HEk);
190          [ <minus_plus /2/ | @not_le_to_not_le_S_S /3/ ]
191        ]
192      ]
193    | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_app >aa_app
194      >ata_subst /3/
195    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_lambda >aa_lambda
196      @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
197      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
198    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_prod >aa_prod
199      @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
200      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
201    ]
202 qed.
203
204 (* the assigned arity is constant *)
205 lemma aa_isc: ∀t,E,K. !E → all2 … isc E K → isc (〚t〛_[E,K]) (〚t〛_[K]).
206 #t elim t -t /2 by isc_sort/
207    [ #i #E #K #HE #H @(all2_nth … isc) //
208    | /3/
209    | #N #M #IHN #IHM #E #K #HE #H >aa_lambda >ata_lambda 
210
211
212
213 (*
214 const ? (〚v〛_[E1,K] (〚v〛_[K])) ≅ 〚v〛_[E1,K].
215
216 theorem aa_beta: ∀K,E1,E2. E1 ≅ E2 → ∀w,t,v. 〚v〛_[K] = 〚w〛_[K] →
217                  〚App (Lambda w t) v〛_[E1,K] ≅ 〚t[0≝v]〛_[E2,K].
218 #K #E1 #E2 #HE #w #t #v #H > aa_app >aa_lambda
219 @transitive_aeq; [3: @symmetric_aeq @(aa_subst … E1 … ([]) ([]) ([])) /2/ | skip ]
220 >H @aa_comp -H v; #C whd in ⊢ (? ? % ?)
221 *)
222
223 (*
224 axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 :: E2.
225
226 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
227 @A qed.
228 *)
229 *)