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/static/sh.ma".
17 (* SORT DEGREE **************************************************************)
19 (* sort degree specification *)
20 record sd (h:sh): Type[0] ≝ {
21 deg : relation nat; (* degree of the sort *)
22 deg_total: ∀k. ∃l. deg k l; (* functional relation axioms *)
23 deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2;
24 deg_next : ∀k,l. deg k l → deg (next h k) (l - 1) (* compatibility condition *)
27 (* Notable specifications ***************************************************)
29 definition deg_O: relation nat ≝ λk,l. l = 0.
31 definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O ….
32 // /2 width=1/ /2 width=2/ qed.
34 inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝
35 | deg_SO_pos : ∀l0. (next h)^l0 k0 = k → deg_SO h k k0 (l0 + 1)
36 | deg_SO_zero: ((∃l0. (next h)^l0 k0 = k) → ⊥) → deg_SO h k k0 0
39 fact deg_SO_inv_pos_aux: ∀h,k,k0,l0. deg_SO h k k0 l0 → ∀l. l0 = l + 1 →
43 lapply (injective_plus_l … H) -H #H destruct //
44 | #_ #l0 <plus_n_Sm #H destruct
48 lemma deg_SO_inv_pos: ∀h,k,k0,l0. deg_SO h k k0 (l0 + 1) → (next h)^l0 k0 = k.
51 lemma deg_SO_refl: ∀h,k. deg_SO h k k 1.
52 #h #k @(deg_SO_pos … 0 ?) //
55 lemma deg_SO_gt: ∀h,k1,k2. k1 < k2 → deg_SO h k1 k2 0.
56 #h #k1 #k2 #HK12 @deg_SO_zero * #l elim l -l normalize
58 elim (lt_refl_false … HK12)
60 lapply (next_lt h ((next h)^l k2)) >H -H #H
61 lapply (transitive_lt … H HK12) -k1 #H1
62 lapply (nexts_le h k2 l) #H2
63 lapply (le_to_lt_to_lt … H2 H1) -h -l #H
64 elim (lt_refl_false … H)
67 definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
69 lapply (nexts_dec h k0 k) * [ * /3 width=2/ | /4 width=2/ ]
70 | #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 //
72 lapply (nexts_inj … H) -H #H destruct //
77 [ #l #H destruct elim l -l normalize /2 width=1/
78 | #H1 @deg_SO_zero * #l #H2 destruct
79 @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *)
84 let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
89 | _ ⇒ sd_l h (next h k) l
93 (* Basic inversion lemmas ***************************************************)
95 lemma deg_inv_pred: ∀h,g,k,l. deg h g (next h k) (l+1) → deg h g k (l+2).
97 elim (deg_total h g k) #l0 #H0
98 lapply (deg_next … H0) #H2
99 lapply (deg_mono … H1 H2) -H1 -H2 #H
100 <(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
103 lemma deg_inv_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
104 #h #g #k #l @(nat_ind_plus … l) -l //
105 #l #IHl #l0 >iter_SO #H
106 lapply (deg_inv_pred … H) -H <(associative_plus l0 1 1) #H
107 lapply (IHl … H) -IHl -H //
110 (* Basic properties *********************************************************)
112 lemma deg_iter: ∀h,g,k,l1,l2. deg h g k l1 → deg h g ((next h)^l2 k) (l1-l2).
113 #h #g #k #l1 #l2 @(nat_ind_plus … l2) -l2 [ <minus_n_O // ]
114 #l2 #IHl2 #Hkl1 >iter_SO <minus_plus /3 width=1/
117 lemma deg_next_SO: ∀h,g,k,l. deg h g k (l+1) → deg h g (next h k) l.
119 lapply (deg_next … Hkl) -Hkl <minus_plus_m_m //
122 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
123 #h #k #l <plus_n_Sm <plus_n_Sm //
126 lemma sd_l_correct: ∀h,l,k. deg h (sd_l h k l) k l.
127 #h #l @(nat_ind_plus … l) -l // #l @(nat_ind_plus … l) -l // /3 width=1 by deg_inv_pred/