propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / rtmap_uni.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.ma
index 3195a8332a29091e1ce82ab66884e0507a141d23..4eb1e17b4963ed55727fd55b267b03aa5804cd25 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_uni.ma
@@ -13,48 +13,48 @@
 (**************************************************************************)
 
 include "ground/notation/functions/uniform_1.ma".
+include "ground/relocation/rtmap_nexts.ma".
 include "ground/relocation/rtmap_id.ma".
 include "ground/relocation/rtmap_isuni.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-rec definition uni (n:nat) on n: rtmap  ≝ match n with
-[ O   ⇒ 𝐈𝐝
-| S n ⇒ ↑(uni n)
-].
+definition uni (n) ≝ ↑*[n] 𝐈𝐝.
 
 interpretation "uniform relocation (rtmap)"
    'Uniform n = (uni n).
 
 (* Basic properties *********************************************************)
 
-lemma uni_zero: 𝐈𝐝 = 𝐔❨0❩.
+lemma uni_zero: 𝐈𝐝 = 𝐔❨𝟎❩.
 // qed.
 
 lemma uni_succ: ∀n. ↑𝐔❨n❩ = 𝐔❨↑n❩.
-// qed.
+/2 width=1 by nexts_S/ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ f.
-#f * /3 width=5 by eq_inv_pp, conj/
-#n <uni_succ #H elim (eq_inv_np … H) -H //
+lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
+#f #n @(nat_ind_succ … n) -n
+[ /3 width=5 by eq_inv_pp, conj/
+| #n #_ <uni_succ #H elim (eq_inv_np … H) -H //
+]
 qed-.
 
-lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 0 = n ∧ 𝐈𝐝 ≡ f.
+lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
 /3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
 
-lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 0 = n.
+lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 𝟎 = n.
 #n <id_rew #H elim (uni_inv_push_dx … H) -H //
 qed-.
 
-lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≡ 𝐔❨n❩ → 0 = n.
+lemma uni_inv_id_sn: ∀n.  𝐈𝐝 ≡ 𝐔❨n❩ → 𝟎 = n.
 /3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
 
 lemma uni_inv_next_dx: ∀f,n. 𝐔❨n❩ ≡ ↑f → ∃∃m. 𝐔❨m❩ ≡ f & ↑m = n.
-#f *
+#f #n @(nat_ind_succ … n) -n
 [ <uni_zero <id_rew #H elim (eq_inv_pn … H) -H //
-| #n <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
+| #n #_ <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
 ]
 qed-.
 
@@ -63,18 +63,19 @@ lemma uni_inv_next_sn: ∀f,n. ↑f ≡ 𝐔❨n❩ → ∃∃m. 𝐔❨m❩ ≡
 
 (* Properties with test for identity ****************************************)
 
-lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨0❩ ≡ f.
+lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨𝟎❩ ≡ f.
 /2 width=1 by eq_id_inv_isid/ qed-.
 
 (* Inversion lemmas with test for identity **********************************)
 
-lemma uni_inv_isid: ∀f. 𝐔❨0❩ ≡ f → 𝐈❪f❫.
+lemma uni_inv_isid: ∀f. 𝐔❨𝟎❩ ≡ f → 𝐈❪f❫.
 /2 width=1 by eq_id_isid/ qed-.
 
 (* Properties with finite colength assignment ***************************)
 
 lemma fcla_uni: ∀n. 𝐂❪𝐔❨n❩❫ ≘ n.
-#n elim n -n /2 width=1 by fcla_isid, fcla_next/
+#n @(nat_ind_succ … n) -n
+/2 width=1 by fcla_isid, fcla_next/
 qed.
 
 (* Properties with test for finite colength ***************************)
@@ -85,7 +86,8 @@ lemma isfin_uni: ∀n. 𝐅❪𝐔❨n❩❫.
 (* Properties with test for uniformity **************************************)
 
 lemma isuni_uni: ∀n. 𝐔❪𝐔❨n❩❫.
-#n elim n -n /3 width=3 by isuni_isid, isuni_next/
+#n @(nat_ind_succ … n) -n
+/3 width=3 by isuni_isid, isuni_next/
 qed.
 
 lemma uni_isuni: ∀f. 𝐔❪f❫ → ∃n. 𝐔❨n❩ ≡ f.
@@ -96,6 +98,8 @@ qed-.
 (* Inversion lemmas with test for uniformity ********************************)
 
 lemma uni_inv_isuni: ∀n,f. 𝐔❨n❩ ≡ f →  𝐔❪f❫.
-#n elim n -n /3 width=1 by uni_inv_isid, isuni_isid/
-#n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
+#n @(nat_ind_succ … n) -n
+[ /3 width=1 by uni_inv_isid, isuni_isid/
+| #n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
+]
 qed-.