partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / sd.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma
index 533a79e05bc91ce73cce3c3391f94d6088c76f14..cd62fb439da88207b1194c78f9494b5cc3634acd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma
@@ -12,7 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "static_2/syntax/sh.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_minus.ma".
+include "ground/arith/nat_lt_pred.ma".
+include "static_2/syntax/sh_nexts.ma".
 
 (* SORT DEGREE **************************************************************)
 
@@ -28,41 +31,46 @@ record sd_props (h) (o): Prop ≝ {
    deg_total: ∀s. ∃d. deg o s d;
    deg_mono : ∀s,d1,d2. deg o s d1 → deg o s d2 → d1 = d2;
 (* compatibility condition *)
-   deg_next : â\88\80s,d. deg o s d â\86\92 deg o (⫯[h]s) (↓d)
+   deg_next : â\88\80s,d. deg o s d â\86\92 deg o (â\87¡[h]s) (↓d)
 }.
 
 (* Notable specifications ***************************************************)
 
-definition deg_O: relation nat ≝ λs,d. d = 0.
+definition deg_O: relation nat ≝ λs,d. d = 𝟎.
 
 definition sd_O: sd ≝ mk_sd deg_O.
 
 lemma sd_O_props (h): sd_props h sd_O ≝ mk_sd_props ….
-/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ qed.
+/2 width=2 by nle_inv_zero_dx, nle_refl, ex_intro/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 lemma deg_inv_pred (h) (o): sd_props h o →
-      â\88\80s,d. deg o (⫯[h]s) (↑d) → deg o s (↑↑d).
+      â\88\80s,d. deg o (â\87¡[h]s) (↑d) → deg o s (↑↑d).
 #h #o #Ho #s #d #H1
 elim (deg_total … Ho s) #d0 #H0
 lapply (deg_next … Ho … H0) #H2
-lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H >S_pred
-/2 width=2 by ltn_to_ltO/
+lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H <nlt_des_gen
+/2 width=2 by nlt_des_lt_zero_sn/
 qed-.
 
 lemma deg_inv_prec (h) (o): sd_props h o →
-      ∀s,n,d. deg o ((next h)^n s) (↑d) → deg o s (↑(d+n)).
-#h #o #H0 #s #n elim n -n normalize /3 width=3 by deg_inv_pred/
+      ∀s,n,d. deg o (⇡*[h,n]s) (↑d) → deg o s (↑(d+n)).
+#h #o #H0 #s #n @(nat_ind_succ … n) -n [ // ]
+#n #IH #d <sh_nexts_succ
+#H <nplus_succ_shift
+@IH -IH @(deg_inv_pred … H0) // (**) (* auto fails *)
 qed-.
 
 (* Basic properties *********************************************************)
 
 lemma deg_iter (h) (o): sd_props h o →
-      ∀s,d,n. deg o s d → deg o ((next h)^n s) (d-n).
-#h #o #Ho #s #d #n elim n -n normalize /3 width=1 by deg_next/
+      ∀s,d,n. deg o s d → deg o (⇡*[h,n]s) (d-n).
+#h #o #Ho #s #d #n @(nat_ind_succ … n) -n [ // ]
+#n #IH #H <nminus_succ_dx <sh_nexts_succ
+/3 width=1 by deg_next/
 qed.
 
 lemma deg_next_SO (h) (o): sd_props h o →
-      ∀s,d. deg o s (↑d) → deg o (next h s) d.
+      ∀s,d. deg o s (↑d) → deg o (⇡[h]s) d.
 /2 width=1 by deg_next/ qed-.