(* Constructions with nsucc *************************************************)
+lemma nsucc_pnpred (p):
+ ninj p = ↑(pnpred p).
+// qed.
+
(*** pred_Sn pred_S *)
lemma npred_succ (n): n = ↓↑n.
* //
(* *)
(**************************************************************************)
+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".
∀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
| #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/
(* 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.
(* 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.
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.
[ <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/
]
]
[ <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 //
]
]
[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)) //
]
]
]
(* 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.
projects / helm.git / commitdiff