]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
059fe374fc9e88d75835cb505f7db2d961789764
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas.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 "basic_2/notation/relations/colonstar_7.ma".
16 include "basic_2/dynamic/cnv.ma".
17
18 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
19
20 definition ntas (h) (a) (n) (G) (L): relation term ≝ λT,U.
21            ∃∃U0. ❨G,L❩ ⊢ U ![h,a] & ❨G,L❩ ⊢ T ![h,a] & ❨G,L❩ ⊢ U ➡*[h,0] U0 & ❨G,L❩ ⊢ T ➡*[h,n] U0.
22
23 interpretation "iterated native type assignment (term)"
24    'ColonStar h a n G L T U = (ntas h a n G L T U).
25
26 (* Basic properties *********************************************************)
27
28 lemma ntas_intro (h) (a) (n) (G) (L):
29       ∀U. ❨G,L❩ ⊢ U ![h,a] → ∀T. ❨G,L❩ ⊢ T ![h,a] →
30       ∀U0. ❨G,L❩ ⊢ U ➡*[h,0] U0 → ❨G,L❩ ⊢ T ➡*[h,n] U0 → ❨G,L❩ ⊢ T :*[h,a,n] U.
31 /2 width=3 by ex4_intro/ qed.
32
33 lemma ntas_refl (h) (a) (G) (L):
34       ∀T. ❨G,L❩ ⊢ T ![h,a] → ❨G,L❩ ⊢ T :*[h,a,0] T.
35 /2 width=3 by ntas_intro/ qed.
36
37 lemma ntas_sort (h) (a) (n) (G) (L):
38       ∀s. ❨G,L❩ ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
39 #h #a #n #G #L #s
40 /2 width=3 by ntas_intro, cnv_sort, cpms_sort/
41 qed.
42
43 lemma ntas_bind_cnv (h) (a) (n) (G) (K):
44       ∀V. ❨G,K❩ ⊢ V ![h,a] →
45       ∀I,T,U. ❨G,K.ⓑ[I]V❩ ⊢ T :*[h,a,n] U →
46       ∀p. ❨G,K❩ ⊢ ⓑ[p,I]V.T :*[h,a,n] ⓑ[p,I]V.U.
47 #h #a #n #G #K #V #HV #I #T #U
48 * #X #HU #HT #HUX #HTX #p
49 /3 width=5 by ntas_intro, cnv_bind, cpms_bind_dx/
50 qed.
51
52 (* Basic_forward lemmas *****************************************************)
53
54 lemma ntas_fwd_cnv_sn (h) (a) (n) (G) (L):
55       ∀T,U. ❨G,L❩ ⊢ T :*[h,a,n] U → ❨G,L❩ ⊢ T ![h,a].
56 #h #a #n #G #L #T #U
57 * #X #_ #HT #_ #_ //
58 qed-.
59
60 (* Note: this is ntas_fwd_correct_cnv *)
61 lemma ntas_fwd_cnv_dx (h) (a) (n) (G) (L):
62       ∀T,U. ❨G,L❩ ⊢ T :*[h,a,n] U → ❨G,L❩ ⊢ U ![h,a].
63 #h #a #n #G #L #T #U
64 * #X #HU #_ #_ #_ //
65 qed-.