propagating the arithmetics library, partial commit

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.ma
index 41871b15cfc56433ff894d1e4b33b79051a300a6..ddb1819a57a956d36b3febaf45f8d84d401546f6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_at.ma
@@ -13,12 +13,14 @@
 (**************************************************************************)
 
 include "ground/notation/relations/rat_3.ma".
-include "ground/relocation/rtmap_uni.ma".
+include "ground/arith/pnat_plus.ma".
+include "ground/arith/pnat_lt_pred.ma".
+include "ground/relocation/rtmap_id.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-coinductive at: rtmap → relation nat ≝
-| at_refl: ∀f,g,j1,j2. ⫯f = g → 0 = j1 → 0 = j2 → at g j1 j2
+coinductive at: relation3 rtmap pnat pnat ≝
+| at_refl: ∀f,g,j1,j2. ⫯f = g → 𝟏 = j1 → 𝟏 = j2 → at g j1 j2
 | at_push: ∀f,i1,i2. at f i1 i2 → ∀g,j1,j2. ⫯f = g → ↑i1 = j1 → ↑i2 = j2 → at g j1 j2
 | at_next: ∀f,i1,i2. at f i1 i2 → ∀g,j2. ↑f = g → ↑i2 = j2 → at g i1 j2
 .
@@ -32,7 +34,7 @@ definition H_at_div: relation4 rtmap rtmap rtmap rtmap ≝ λf2,g2,f1,g1.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma at_inv_ppx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. 0 = i1 → ⫯g = f → 0 = i2.
+lemma at_inv_ppx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
 #f #i1 #i2 * -f -i1 -i2 //
 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
@@ -59,14 +61,16 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
+alias symbol "UpArrow" (instance 3) = "successor (positive integers)".
 lemma at_inv_ppn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
-                  ∀g,j2. 0 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+                  ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
 #H destruct
 qed-.
 
+alias symbol "UpArrow" (instance 7) = "successor (positive integers)".
 lemma at_inv_npp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
-                  ∀g,j1. ↑j1 = i1 → ⫯g = f → 0 = i2 → ⊥.
+                  ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct
 qed-.
@@ -78,7 +82,7 @@ lemma at_inv_npn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
 qed-.
 
 lemma at_inv_xnp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
-                  ∀g. ↑g = f → 0 = i2 → ⊥.
+                  ∀g. ↑g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
 #x2 #Hg * -i2 #H destruct
 qed-.
@@ -89,12 +93,12 @@ lemma at_inv_xnn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
-lemma at_inv_pxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 0 = i1 → 0 = i2 → ∃g. ⫯g = f.
+lemma at_inv_pxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
 #f elim (pn_split … f) * /2 width=2 by ex_intro/
 #g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
 qed-.
 
-lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 0 = i1 → ↑j2 = i2 →
+lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
                   ∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
 #f elim (pn_split … f) *
 #g #H #i1 #i2 #Hf #j2 #H1 #H2
@@ -103,8 +107,9 @@ lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 0 = i1 → ↑j2 = i
 ]
 qed-.
 
+alias symbol "UpArrow" (instance 5) = "successor (positive integers)".
 lemma at_inv_nxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
-                  ∀j1. ↑j1 = i1 → 0 = i2 → ⊥.
+                  ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
 #f elim (pn_split f) *
 #g #H #i1 #i2 #Hf #j1 #H1 #H2
 [ elim (at_inv_npp … Hf … H1 H H2)
@@ -121,15 +126,15 @@ qed-.
 
 (* Note: the following inversion lemmas must be checked *)
 lemma at_inv_xpx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f →
-                  (0 = i1 ∧ 0 = i2) ∨
-                  ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+                  ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
+                   | ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
 #f * [2: #i1 ] #i2 #Hf #g #H
 [ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 | >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
 ]
 qed-.
 
-lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 0 = i2 → 0 = i1.
+lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
 #f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
 #j1 #j2 #_ #_ * -i2 #H destruct
 qed-.
@@ -142,8 +147,8 @@ lemma at_inv_xpn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2
 ]
 qed-.
 
-lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 0 = i2 →
-                  ∃∃g. 0 = i1 & ⫯g = f.
+lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i2 →
+                  ∃∃g. 𝟏 = i1 & ⫯g = f.
 #f elim (pn_split f) *
 #g #H #i1 #i2 #Hf #H2
 [ /3 width=6 by at_inv_xpp, ex2_intro/
@@ -168,21 +173,21 @@ lemma at_increasing: ∀i2,i1,f. @❪i1,f❫ ≘ i2 → i1 ≤ i2.
 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
 | #i2 #IH * //
   #i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ]
-  /3 width=2 by le_S_S, le_S/
+  /3 width=2 by ple_succ_bi, ple_succ_dx/
 ]
 qed-.
 
 lemma at_increasing_strict: ∀g,i1,i2. @❪i1,g❫ ≘ i2 → ∀f. ↑f = g →
                             i1 < i2 ∧ @❪i1,f❫ ≘ ↓i2.
 #g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
-/4 width=2 by conj, at_increasing, le_S_S/
+/4 width=2 by conj, at_increasing, ple_succ_bi/
 qed-.
 
 lemma at_fwd_id_ex: ∀f,i. @❪i,f❫ ≘ i → ∃g. ⫯g = f.
 #f elim (pn_split f) * /2 width=2 by ex_intro/
 #g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
-#H elim (lt_le_false … H) -H //
+#H elim (plt_ge_false … H) -H //
 qed-.
 
 (* Basic properties *********************************************************)
@@ -205,20 +210,20 @@ lemma at_le_ex: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀i1. i1 ≤ i2 →
 [ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
   #g [ #x2 ] #Hg [ #H2 ] #H0
   [ * /3 width=3 by at_refl, ex2_intro/
-    #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12
+    #i1 #Hi12 destruct lapply (ple_inv_succ_bi … Hi12) -Hi12
     #Hi12 elim (IH … Hg … Hi12) -x2 -IH
-    /3 width=7 by at_push, ex2_intro, le_S_S/
+    /3 width=7 by at_push, ex2_intro, ple_succ_bi/
   | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2
-    /3 width=5 by at_next, ex2_intro, le_S_S/
+    /3 width=5 by at_next, ex2_intro, ple_succ_bi/
   ]
 | elim (at_inv_xxp … Hf) -Hf //
-  #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12)
+  #g * -i2 #H2 #i1 #Hi12 <(ple_inv_unit_dx … Hi12)
   /3 width=3 by at_refl, ex2_intro/
 ]
 qed-.
 
 lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @❪i2,f❫ ≘ i2 → @❪i1,f❫ ≘ i1.
-#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
+#i1 #i2 #H @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ]
 #f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
 qed-.
 
@@ -228,14 +233,14 @@ theorem at_monotonic: ∀j2,i2,f. @❪i2,f❫ ≘ j2 → ∀j1,i1. @❪i1,f❫ 
                       i1 < i2 → j1 < j2.
 #j2 elim j2 -j2
 [ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
-  #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi //
+  #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi //
 | #j2 #IH #i2 #f #H2f * //
-  #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi)
-  #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ]
+  #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi)
+  #_ #Hi2 elim (at_inv_nxn … H2f (↓i2)) -H2f [1,3: * |*: // ]
   #g #H2g #H
   [ elim (at_inv_xpn … H1f … H) -f
-    /4 width=8 by lt_S_S_to_lt, lt_S_S/
-  | /4 width=8 by at_inv_xnn, lt_S_S/
+    /4 width=8 by plt_inv_succ_bi, plt_succ_bi/
+  | /4 width=8 by at_inv_xnn, plt_succ_bi/
   ]
 ]
 qed-.
@@ -244,17 +249,17 @@ theorem at_inv_monotonic: ∀j1,i1,f. @❪i1,f❫ ≘ j1 → ∀j2,i2. @❪i2,f
                           j1 < j2 → i1 < i2.
 #j1 elim j1 -j1
 [ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
-  #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj
-  #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f //
+  #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj
+  #H22 elim (at_inv_xpn … H2f … (↓j2) H) -f //
 | #j1 #IH *
   [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ]
-    #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
+    #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
     /3 width=7 by at_inv_xnn/
-  | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
-    #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
+  | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
+    #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
     #g #Hg #H
-    [ elim (at_inv_xpn … H2f … H H22) -f -H22
-      /3 width=7 by lt_S_S/
+    [ elim (at_inv_xpn … H2f … (↓j2) H) -f
+      /3 width=7 by plt_succ_bi/
     | /3 width=7 by at_inv_xnn/
     ]
   ]
@@ -262,13 +267,13 @@ theorem at_inv_monotonic: ∀j1,i1,f. @❪i1,f❫ ≘ j1 → ∀j2,i2. @❪i2,f
 qed-.
 
 theorem at_mono: ∀f,i,i1. @❪i,f❫ ≘ i1 → ∀i2. @❪i,f❫ ≘ i2 → i2 = i1.
-#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
+#f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
+#Hi elim (plt_ge_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
 qed-.
 
 theorem at_inj: ∀f,i1,i. @❪i1,f❫ ≘ i → ∀i2. @❪i2,f❫ ≘ i → i1 = i2.
-#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
+#f #i1 #i #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
+#Hi elim (plt_ge_false i i) /2 width=6 by at_monotonic/
 qed-.
 
 theorem at_div_comm: ∀f2,g2,f1,g1.
@@ -312,17 +317,19 @@ theorem at_div_pn: ∀f2,g2,f1,g1.
 
 (* Properties on tls ********************************************************)
 
-lemma at_pxx_tls: ∀n,f. @❪0,f❫ ≘ n → @❪0,⫱*[n]f❫ ≘ 0.
-#n elim n -n //
+(* Note: this requires ↑ on first n *)
+lemma at_pxx_tls: ∀n,f. @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫱*[n]f❫ ≘ 𝟏.
+#n @(nat_ind_succ … n) -n //
 #n #IH #f #Hf
 cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
 <tls_xn /2 width=1 by/
 qed.
 
-lemma at_tls: ∀i2,f. ⫯⫱*[↑i2]f ≡ ⫱*[i2]f → ∃i1. @❪i1,f❫ ≘ i2.
-#i2 elim i2 -i2
+(* Note: this requires ↑ on third n2 *)
+lemma at_tls: ∀n2,f. ⫯⫱*[↑n2]f ≡ ⫱*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
+#n2 @(nat_ind_succ … n2) -n2
 [ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
-| #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
+| #n2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
   elim (IH … H) -IH -H #i1 #Hf
   elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/
 ]
@@ -330,8 +337,9 @@ qed-.
 
 (* Inversion lemmas with tls ************************************************)
 
-lemma at_inv_nxx: ∀n,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪0,g❫ ≘ n →
-                  ∃∃i2. @❪i1,⫱*[↑n]g❫ ≘ i2 & ↑(n+i2) = j2.
+(* Note: this does not require ↑ on second and third p *)
+lemma at_inv_nxx: ∀p,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪𝟏,g❫ ≘ p →
+                  ∃∃i2. @❪i1,⫱*[p]g❫ ≘ i2 & p+i2 = j2.
 #n elim n -n
 [ #g #i1 #j2 #Hg #H
   elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
@@ -345,11 +353,12 @@ lemma at_inv_nxx: ∀n,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪0,g❫ ≘ n →
 ]
 qed-.
 
-lemma at_inv_tls: ∀i2,i1,f. @❪i1,f❫ ≘ i2 → ⫯⫱*[↑i2]f ≡ ⫱*[i2]f.
-#i2 elim i2 -i2
+(* Note: this requires ↑ on first n2 *)
+lemma at_inv_tls: ∀n2,i1,f. @❪i1,f❫ ≘ ↑n2 → ⫯⫱*[↑n2]f ≡ ⫱*[n2]f.
+#n2 @(nat_ind_succ … n2) -n2
 [ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
   /2 width=1 by eq_refl/
-| #i2 #IH #i1 #f #Hf
+| #n2 #IH #i1 #f #Hf
   elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
   [ #g #j1 #Hg #H1 #H2 | #g #Hg #Ho ] destruct
   <tls_xn /2 width=2 by/
@@ -371,7 +380,7 @@ lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈❪f❫ → @❪i1,f❫ ≘ i2 → i1 =
 (* Advanced properties on isid **********************************************)
 
 corec lemma isid_at: ∀f. (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.
-#f #Hf lapply (Hf 0)
+#f #Hf lapply (Hf (𝟏))
 #H cases (at_fwd_id_ex … H) -H
 #g #H @(isid_push … H) /3 width=7 by at_inv_npn/
 qed-.
@@ -399,14 +408,3 @@ qed-.
 
 theorem at_div_id_sn: ∀f. H_at_div 𝐈𝐝 f f 𝐈𝐝.
 /3 width=6 by at_div_id_dx, at_div_comm/ qed-.
-
-(* Properties with uniform relocations **************************************)
-
-lemma at_uni: ∀n,i. @❪i,𝐔❨n❩❫ ≘ n+i.
-#n elim n -n /2 width=5 by at_next/
-qed.
-
-(* Inversion lemmas with uniform relocations ********************************)
-
-lemma at_inv_uni: ∀n,i,j. @❪i,𝐔❨n❩❫ ≘ j → j = n+i.
-/2 width=4 by at_mono/ qed-.