]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2A/static/sd.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / static / sd.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_2A/static/sh.ma".
16
17 (* SORT DEGREE **************************************************************)
18
19 (* sort degree specification *)
20 record sd (h:sh): Type[0] ≝ {
21    deg      : relation nat;                            (* degree of the sort *)
22    deg_total: ∀k. ∃d. deg k d;                         (* functional relation axioms *)
23    deg_mono : ∀k,d1,d2. deg k d1 → deg k d2 → d1 = d2;
24    deg_next : ∀k,d. deg k d → deg (next h k) (d - 1)   (* compatibility condition *)
25 }.
26
27 (* Notable specifications ***************************************************)
28
29 definition deg_O: relation nat ≝ λk,d. d = 0.
30
31 definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
32 /2 width=2 by le_n_O_to_eq, le_n, ex_intro/ defined.
33
34 inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝
35 | deg_SO_pos : ∀d0. (next h)^d0 k0 = k → deg_SO h k k0 (d0 + 1)
36 | deg_SO_zero: ((∃d0. (next h)^d0 k0 = k) → ⊥) → deg_SO h k k0 0
37 .
38
39 fact deg_SO_inv_pos_aux: ∀h,k,k0,d0. deg_SO h k k0 d0 → ∀d. d0 = d + 1 →
40                          (next h)^d k0 = k.
41 #h #k #k0 #d0 * -d0
42 [ #d0 #Hd0 #d #H
43   lapply (injective_plus_l … H) -H #H destruct //
44 | #_ #d0 <plus_n_Sm #H destruct
45 ]
46 qed.
47
48 lemma deg_SO_inv_pos: ∀h,k,k0,d0. deg_SO h k k0 (d0 + 1) → (next h)^d0 k0 = k.
49 /2 width=3 by deg_SO_inv_pos_aux/ qed-.
50
51 lemma deg_SO_refl: ∀h,k. deg_SO h k k 1.
52 #h #k @(deg_SO_pos … 0 ?) //
53 qed.
54
55 lemma deg_SO_gt: ∀h,k1,k2. k1 < k2 → deg_SO h k1 k2 0.
56 #h #k1 #k2 #HK12 @deg_SO_zero * #d elim d -d normalize
57 [ #H destruct
58   elim (lt_refl_false … HK12)
59 | #d #_ #H
60   lapply (next_lt h ((next h)^d k2)) >H -H #H
61   lapply (transitive_lt … H HK12) -k1 #H1
62   lapply (nexts_le h k2 d) #H2
63   lapply (le_to_lt_to_lt … H2 H1) -h -d #H
64   elim (lt_refl_false … H)
65 ]
66 qed.
67
68 definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
69 [ #k0
70   lapply (nexts_dec h k0 k) *
71   [ * /3 width=2 by deg_SO_pos, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ]
72 | #K0 #d1 #d2 * [ #d01 ] #H1 * [1,3: #d02 ] #H2 //
73   [ < H2 in H1; -H2 #H
74     lapply (nexts_inj … H) -H #H destruct //
75   | elim H1 /2 width=2 by ex_intro/
76   | elim H2 /2 width=2 by ex_intro/
77   ]
78 | #k0 #d0 *
79   [ #d #H destruct elim d -d normalize
80     /2 width=1 by deg_SO_gt, deg_SO_pos, next_lt/
81   | #H1 @deg_SO_zero * #d #H2 destruct
82     @H1 -H1 @(ex_intro … (S d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *)
83   ]
84 ]
85 defined.
86
87 let rec sd_d (h:sh) (k:nat) (d:nat) on d : sd h ≝
88    match d with
89    [ O   ⇒ sd_O h
90    | S d ⇒ match d with
91            [ O ⇒ sd_SO h k
92            | _ ⇒ sd_d h (next h k) d
93            ]
94    ].
95
96 (* Basic inversion lemmas ***************************************************)
97
98 lemma deg_inv_pred: ∀h,g,k,d. deg h g (next h k) (d+1) → deg h g k (d+2).
99 #h #g #k #d #H1
100 elim (deg_total h g k) #d0 #H0
101 lapply (deg_next … H0) #H2
102 lapply (deg_mono … H1 H2) -H1 -H2 #H
103 <(associative_plus d 1 1) >H <plus_minus_m_m /2 width=3 by transitive_le/
104 qed-.
105
106 lemma deg_inv_prec: ∀h,g,k,d,d0. deg h g ((next h)^d k) (d0+1) → deg h g k (d+d0+1).
107 #h #g #k #d @(nat_ind_plus … d) -d //
108 #d #IHd #d0 >iter_SO #H
109 lapply (deg_inv_pred … H) -H <(associative_plus d0 1 1) #H
110 lapply (IHd … H) -IHd -H //
111 qed-.
112
113 (* Basic properties *********************************************************)
114
115 lemma deg_iter: ∀h,g,k,d1,d2. deg h g k d1 → deg h g ((next h)^d2 k) (d1-d2).
116 #h #g #k #d1 #d2 @(nat_ind_plus … d2) -d2  [ <minus_n_O // ]
117 #d2 #IHd2 #Hkd1 >iter_SO <minus_plus /3 width=1 by deg_next/
118 qed.
119
120 lemma deg_next_SO: ∀h,g,k,d. deg h g k (d+1) → deg h g (next h k) d.
121 #h #g #k #d #Hkd
122 lapply (deg_next … Hkd) -Hkd <minus_plus_m_m //
123 qed-.
124
125 lemma sd_d_SS: ∀h,k,d. sd_d h k (d + 2) = sd_d h (next h k) (d + 1).
126 #h #k #d <plus_n_Sm <plus_n_Sm //
127 qed.
128
129 lemma sd_d_correct: ∀h,d,k. deg h (sd_d h k d) k d.
130 #h #d @(nat_ind_plus … d) -d // #d @(nat_ind_plus … d) -d /3 width=1 by deg_inv_pred/
131 qed.