partial update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
index 296322e61a8f173698ce3a0f2a439130d2b91298..10620b0bf19f96e8393fd81af2fdef640a708daa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/generated/pull_2.ma".
+include "ground/arith/pnat_pred.ma".
 include "static_2/syntax/sh_props.ma".
 include "static_2/syntax/sd.ma".
 
@@ -19,67 +21,76 @@ include "static_2/syntax/sd.ma".
 
 (* Basic_2A1: includes: deg_SO_pos *)
 inductive deg_SO (h) (s) (s0): predicate nat ≝
-| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n)
-| deg_SO_zero: (∀n. (next h)^n s0 = s → ⊥) → deg_SO h s s0 0
+| deg_SO_succ : ∀n. ⇡*[h,n]s0 = s → deg_SO h s s0 (↑n)
+| deg_SO_zero: (∀n. ⇡*[h,n]s0 = s → ⊥) → deg_SO h s s0 𝟎
 .
 
 fact deg_SO_inv_succ_aux (h) (s) (s0):
-     ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → (next h)^n s0 = s.
+     ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → ⇡*[h,n]s0 = s.
 #h #s #s0 #n0 * -n0
 [ #n #Hn #x #H destruct //
-| #_ #x #H destruct
+| #_ #x #H elim (eq_inv_zero_nsucc … H)
 ]
 qed-.
 
 (* Basic_2A1: was: deg_SO_inv_pos *)
 lemma deg_SO_inv_succ (h) (s) (s0):
-      ∀n. deg_SO h s s0 (↑n) → (next h)^n s0 = s.
+      ∀n. deg_SO h s s0 (↑n) → ⇡*[h,n]s0 = s.
 /2 width=3 by deg_SO_inv_succ_aux/ qed-.
 
-lemma deg_SO_refl (h) (s): deg_SO h s s 1.
-#h #s @(deg_SO_succ … 0 ?) //
+lemma deg_SO_refl (h) (s):
+      deg_SO h s s 𝟏.
+#h #s @(deg_SO_succ … 𝟎 ?) //
 qed.
 
-definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s).
+definition sd_SO (h) (s):
+           sd ≝ mk_sd (deg_SO h s).
 
-lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
+lemma sd_SO_props (h) (s):
+      sh_decidable h → sh_acyclic h →
       sd_props h (sd_SO h s).
 #h #s #Hhd #Hha
 @mk_sd_props
 [ #s0
-  elim (nexts_dec … Hhd s0 s) -Hhd
+  elim (sh_nexts_dec … Hhd s0 s) -Hhd
   [ * /3 width=2 by deg_SO_succ, ex_intro/
   | /5 width=2 by deg_SO_zero, ex_intro/
   ]
 | #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2
   [ < H2 in H1; -H2 #H
-    lapply (nexts_inj … Hha … H) -H #H destruct //
+    lapply (sh_nexts_inj … Hha … H) -H #H destruct //
   | elim H1 /2 width=2 by ex_intro/
   | elim H2 /2 width=2 by ex_intro/
   | //
   ]
 | #s0 #d *
-  [ #n #H destruct cases n -n normalize
-    [ @deg_SO_zero #n >iter_n_Sm #H
-      lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct
-    | #n @deg_SO_succ >iter_n_Sm //
+  [ #n #H destruct
+    <npred_succ @(nat_ind_succ … n) -n
+    [ @deg_SO_zero #n >sh_nexts_succ_next #H
+      lapply (sh_nexts_inj … Hha … H) -H #H
+      elim (eq_inv_nsucc_zero … H)
+    | #n #_ /2 width=1 by deg_SO_succ/
     ]
-  | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct
+  | #H0 @deg_SO_zero #n >sh_nexts_succ_next #H destruct
     /2 width=2 by/
   ]
 ]
 qed.
 
-rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝
-   match d with
-   [ O   ⇒ sd_O
-   | S d ⇒ match d with
-           [ O ⇒ sd_SO h s
-           | _ ⇒ sd_d h (next h s) d
-           ]
-   ].
+rec definition sd_d_pnat (h) (s) (d) on d: sd ≝
+match d with
+[ punit   ⇒ sd_SO h s
+| psucc d ⇒ sd_d_pnat h (⇡[h]s) d
+].
 
-lemma sd_d_props (h) (s) (d): sh_decidable h → sh_acyclic h →
+definition sd_d (h) (s) (d): sd ≝
+match d with
+[ nzero  ⇒ sd_O
+| ninj d ⇒ sd_d_pnat h s d
+].
+
+lemma sd_d_props (h) (s) (d):
+      sh_decidable h → sh_acyclic h →
       sd_props h (sd_d h s d).
 #h @pull_2 * [ // ]
 #d elim d -d /2 width=1 by sd_SO_props/
@@ -88,11 +99,17 @@ qed.
 (* Properties with sd_d *****************************************************)
 
 lemma sd_d_SS (h):
-      â\88\80s,d. sd_d h s (â\86\91â\86\91d) = sd_d h (⫯[h]s) (↑d).
+      â\88\80s,d. sd_d h s (â\86\91â\86\91d) = sd_d h (â\87¡[h]s) (↑d).
 // qed.
 
-lemma sd_d_correct (h): sh_decidable h → sh_acyclic h →
+lemma sd_d_correct (h):
+      sh_decidable h → sh_acyclic h →
       ∀s,d. deg (sd_d h s d) s d.
-#h #Hhd #Hha @pull_2 #d elim d -d [ // ]
-#d elim d -d /3 width=3 by deg_inv_pred, sd_d_props/
+#h #Hhd #Hha @pull_2 * [ // ]
+#d elim d -d [ // ] #d #IH #s
+>(npsucc_pred d) in ⊢ (???%);
+@(deg_inv_pred h)
+[ /2 width=1 by sd_d_props/
+| <nsucc_pnpred //
+]
 qed.