From 8fe4dc148d50a0352313633bea61441bc817afbf Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Mon, 11 Oct 2021 13:51:08 +0200
Subject: [PATCH] partial update in static_2

+ propagating the ground library
+ one addition in ground
---
 .../lambdadelta/ground/arith/nat_pred_succ.ma |  4 ++
 .../lambdadelta/static_2/syntax/sd_d.ma       | 56 ++++++++++++-------
 .../lambdadelta/static_2/syntax/sd_lt.ma      | 15 ++---
 .../lambdadelta/static_2/syntax/sh_lt.ma      | 10 ++--
 .../lambdadelta/static_2/syntax/sh_nexts.ma   | 21 ++++---
 5 files changed, 67 insertions(+), 39 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index dafe17910..4a6e23b01 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -34,6 +34,10 @@ lemma pnpred_psucc (p): pnpred (psucc p) = nsucc (pnpred p).
 
 (* Constructions with nsucc *************************************************)
 
+lemma nsucc_pnpred (p):
+      ninj p = ↑(pnpred p).
+// qed.
+
 (*** pred_Sn pred_S *)
 lemma npred_succ (n): n = ↓↑n.
 * //
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 7c6f680e8..10620b0bf 100644
--- 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".
 
@@ -36,13 +38,16 @@ lemma deg_SO_inv_succ (h) (s) (s0):
       ∀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 𝟏.
+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
@@ -61,26 +66,31 @@ lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h →
 | #s0 #d *
   [ #n #H destruct
     <npred_succ @(nat_ind_succ … n) -n
-    [ @deg_SO_zero #n >(sh_nexts_succ_next h n s0) #H 
-      lapply (sh_nexts_inj … Hha ???) -H #H destruct
-    | #n @deg_SO_succ >sh_nexts_swap //
+    [ @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 >sh_nexts_swap #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 (pr_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/
@@ -89,11 +99,17 @@ qed.
 (* Properties with sd_d *****************************************************)
 
 lemma sd_d_SS (h):
-      ∀s,d. sd_d h s (↑↑d) = sd_d h (⫯[h]s) (↑d).
+      ∀s,d. sd_d h s (↑↑d) = sd_d h (⇡[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.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
index 23725dba7..24d4651b5 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma
@@ -20,13 +20,14 @@ include "static_2/syntax/sd_d.ma".
 (* Properties with sh_lt ****************************************************)
 
 lemma deg_SO_gt (h): sh_lt h →
-      ∀s1,s2. s1 < s2 → deg_SO h s1 s2 0.
-#h #Hh #s1 #s2 #Hs12 @deg_SO_zero * normalize
-[ #H destruct
+      ∀s1,s2. s1 < s2 → deg_SO h s1 s2 𝟎.
+#h #Hh #s1 #s2 #Hs12 @deg_SO_zero
+#n @(nat_ind_succ … n) -n
+[ <sh_nexts_zero #H destruct
   elim (nlt_inv_refl … Hs12)
-| #n #H
-  lapply (next_lt … Hh ((pr_next h)^n s2)) >H -H #H
-  lapply (nlt_trans … H Hs12) -s1 #H1
-  /3 width=5 by nlt_ge_false, nexts_le/ (* full auto too slow *)
+| #n #_ <sh_nexts_succ #H
+  lapply (sh_next_lt h Hh (⇡*[h,n]s2)) >H -H #H
+  lapply (nlt_trans … H … Hs12) -s1 #H1
+  /3 width=5 by nlt_ge_false, sh_nexts_le/ (* full auto too slow *)
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
index bfeab5905..6e078ad40 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma
@@ -27,7 +27,7 @@ record sh_lt (h): Prop ≝
 
 lemma sh_nexts_le (h): sh_lt h → ∀s,n. s ≤ ⇡*[h,n]s.
 #h #Hh #s #n @(nat_ind_succ … n) -n [ // ] #n #IH <sh_nexts_succ
-lapply (sh_next_lt … Hh ((sh_next h)^n s)) #H
+lapply (sh_next_lt … Hh (⇡*[h,n]s)) #H
 lapply (nle_nlt_trans … IH H) -IH -H /2 width=2 by nlt_des_le/
 qed.
 
@@ -50,7 +50,7 @@ lemma sh_lt_nexts_inv_lt (h): sh_lt h →
   [ <sh_nexts_zero #H
     elim (nlt_inv_refl s)
     /3 width=3 by sh_nexts_lt, nlt_trans/
-  | #n2 #_ <sh_nexts_succ <sh_nexts_succ >sh_nexts_swap >sh_nexts_swap #H
+  | #n2 #_ <sh_nexts_succ_next <sh_nexts_succ_next #H
     /3 width=2 by nlt_succ_bi/
   ]
 ]
@@ -68,7 +68,7 @@ lemma sh_lt_acyclic (h): sh_lt h → sh_acyclic h.
   [ <sh_nexts_zero #H -IH
     elim (nlt_inv_refl s) <H in ⊢ (??%); -H
     /2 width=1 by sh_nexts_lt/
-  | #n2 #_ <sh_nexts_succ <sh_nexts_succ >sh_nexts_swap >sh_nexts_swap #H
+  | #n2 #_ <sh_nexts_succ_next <sh_nexts_succ_next #H
     lapply (IH … H) -IH -H //
   ]
 ]
@@ -97,13 +97,13 @@ elim (nat_split_lt_ge s2 s1) #Hs
     [3: /3 width=1 by sh_next_lt, nlt_minus_bi_sn/ ]
     <nminus_minus_dx_refl_sn [2,4: /2 width=1 by nlt_des_le/ ] -Hs21
     [ * #n #H destruct
-      @or_introl @(ex_intro … (↑n)) <sh_nexts_succ >sh_nexts_swap //
+      @or_introl @(ex_intro … (↑n)) //
     | #H1 @or_intror * #n #H2 @H1 -H1 destruct
       generalize in match Hs12; -Hs12
       >(sh_nexts_zero h s1) in ⊢ (?%?→?); #H
       lapply (sh_lt_nexts_inv_lt … Hh … H) -H #H
       >(nlt_des_gen … H) -H
-      @(ex_intro … (↓n)) <sh_nexts_succ >sh_nexts_swap //
+      @(ex_intro … (↓n)) //
     ]
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
index 143e2dbb8..f9c69e429 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_nexts.ma
@@ -26,21 +26,28 @@ interpretation
 
 (* Basic constructions *)
 
-lemma sh_nexts_zero (h): ∀s. s = ⇡*[h,𝟎]s.
+lemma sh_nexts_zero (h):
+      ∀s. s = ⇡*[h,𝟎]s.
 // qed.
 
-lemma sh_nexts_unit (h): ⇡[h] ≐ ⇡*[h,𝟏].
+lemma sh_nexts_unit (h):
+      ∀s. ⇡[h]s = ⇡*[h,𝟏]s.
 // qed.
 
-lemma sh_nexts_succ (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,↑n].
-/2 width=1 by niter_succ/ qed.
+lemma sh_nexts_succ (h) (n):
+      ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,↑n]s.
+#h #n #s @(niter_succ … (⇡[h]))
+qed.
 
 (* Advanced constructions ****************************)
 
-lemma sh_nexts_swap (h) (n): ⇡[h] ∘ (⇡*[h,n]) ≐ ⇡*[h,n] ∘ ⇡[h].
-/2 width=1 by niter_appl/ qed.
+lemma sh_nexts_swap (h) (n):
+      ∀s. ⇡[h](⇡*[h,n]s) = ⇡*[h,n](⇡[h]s).
+#h #n #s @(niter_appl … (⇡[h]))
+qed.
 
 (* Helper constructions *****************************************************)
 
-lemma sh_nexts_succ_next (h) (n): ⇡*[h,n] ∘ (⇡[h]) ≐ ⇡*[h,↑n].
+lemma sh_nexts_succ_next (h) (n):
+      ∀s. ⇡*[h,n](⇡[h]s) = ⇡*[h,↑n]s.
 // qed.
-- 
2.39.2