(* RELOCATION N-STREAM ******************************************************)
-let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
* #n #f cases i -i
[ @n
| #i lapply (apply i f) -apply -i -f
- #i @(⫯(n+i))
+ #i @(â\86\91(n+i))
]
defined.
(* Specific properties on at ************************************************)
-lemma at_O1: â\88\80i2,f. @â¦\830, i2@fâ¦\84 â\89¡ i2.
+lemma at_O1: â\88\80i2,f. @â\9dª0, i2⨮fâ\9d« â\89\98 i2.
#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
qed.
-lemma at_S1: â\88\80n,f,i1,i2. @â¦\83i1, fâ¦\84 â\89¡ i2 â\86\92 @â¦\83⫯i1, n@fâ¦\84 â\89¡ ⫯(n+i2).
+lemma at_S1: â\88\80n,f,i1,i2. @â\9dªi1, fâ\9d« â\89\98 i2 â\86\92 @â\9dªâ\86\91i1, n⨮fâ\9d« â\89\98 â\86\91(n+i2).
#n elim n -n /3 width=7 by at_push, at_next/
qed.
-lemma at_total: â\88\80i1,f. @â¦\83i1, fâ¦\84 â\89¡ f@â\9d´i1â\9dµ.
+lemma at_total: â\88\80i1,f. @â\9dªi1, fâ\9d« â\89\98 f@â\9d¨i1â\9d©.
#i1 elim i1 -i1
[ * // | #i #IH * /3 width=1 by at_S1/ ]
qed.
-lemma at_istot: â\88\80f. ð\9d\90\93â¦\83fâ¦\84.
+lemma at_istot: â\88\80f. ð\9d\90\93â\9dªfâ\9d«.
/2 width=2 by ex_intro/ qed.
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i.
-#f #i1 #i #n #m #H elim m -m /2 width=5 by at_next/
+lemma at_plus2: ∀f,i1,i,n,m. @❪i1, n⨮f❫ ≘ i → @❪i1, (m+n)⨮f❫ ≘ m+i.
+#f #i1 #i #n #m #H elim m -m //
+#m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
qed.
(* Specific inversion lemmas on at ******************************************)
-lemma at_inv_O1: â\88\80f,n,i2. @â¦\830, n@fâ¦\84 â\89¡ i2 → n = i2.
+lemma at_inv_O1: â\88\80f,n,i2. @â\9dª0, n⨮fâ\9d« â\89\98 i2 → n = i2.
#f #n elim n -n /2 width=6 by at_inv_ppx/
#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 /3 width=1 by eq_f/
qed-.
-lemma at_inv_S1: â\88\80f,n,j1,i2. @â¦\83⫯j1, n@fâ¦\84 â\89¡ i2 →
- â\88\83â\88\83j2. @â¦\83j1, fâ¦\84 â\89¡ j2 & ⫯(n+j2) = i2.
+lemma at_inv_S1: â\88\80f,n,j1,i2. @â\9dªâ\86\91j1, n⨮fâ\9d« â\89\98 i2 →
+ â\88\83â\88\83j2. @â\9dªj1, fâ\9d« â\89\98 j2 & â\86\91(n+j2) = i2.
#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
#i2 #Hi * -j2 /2 width=3 by ex2_intro/
qed-.
-lemma at_inv_total: â\88\80f,i1,i2. @â¦\83i1, fâ¦\84 â\89¡ i2 â\86\92 f@â\9d´i1â\9dµ = i2.
+lemma at_inv_total: â\88\80f,i1,i2. @â\9dªi1, fâ\9d« â\89\98 i2 â\86\92 f@â\9d¨i1â\9d© = i2.
/2 width=6 by at_mono/ qed-.
(* Spercific forward lemmas on at *******************************************)
-lemma at_increasing_plus: â\88\80f,n,i1,i2. @â¦\83i1, n@fâ¦\84 â\89¡ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: â\88\80f,n,i1,i2. @â\9dªi1, n⨮fâ\9d« â\89\98 i2 → i1 + n ≤ i2.
#f #n *
[ #i2 #H <(at_inv_O1 … H) -i2 //
| #i1 #i2 #H elim (at_inv_S1 … H) -H
]
qed-.
-lemma at_fwd_id: â\88\80f,n,i. @â¦\83i, n@fâ¦\84 â\89¡ i → 0 = n.
+lemma at_fwd_id: â\88\80f,n,i. @â\9dªi, n⨮fâ\9d« â\89\98 i → 0 = n.
#f #n #i #H elim (at_fwd_id_ex … H) -H
#g #H elim (push_inv_seq_dx … H) -H //
qed-.
(* Basic properties *********************************************************)
-lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❴i❵ = f2@❴i❵).
+lemma apply_O1: ∀n,f. (n⨮f)@❨0❩ = n.
+// qed.
+
+lemma apply_S1: ∀n,f,i. (n⨮f)@❨↑i❩ = ↑(n+f@❨i❩).
+// qed.
+
+lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
elim (eq_inv_seq_aux … H) -H normalize //
#Hn #Hf /4 width=1 by eq_f2, eq_f/
qed.
-lemma apply_S1: ∀f,i. (⫯f)@❴i❵ = ⫯(f@❴i❵).
+lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
* #n #f * //
qed.
(* Main inversion lemmas ****************************************************)
-(*
-lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
- j1 = j2 → f1 ≗ f2 → i1 = i2.
-/2 width=6 by at_inj/ qed-.
-*)
+
+theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+/2 width=4 by at_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+* #n1 #f1 * #n2 #f2 #Hf @eq_seq
+[ @(Hf 0)
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+ lapply (Hf 0) >apply_O1 >apply_O1 #H destruct
+ lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
+ /3 width=2 by injective_plus_r, injective_S/
+]
+qed-.