include "ground_2/notation/functions/identity_0.ma".
include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/nstream_lift.ma".
include "ground_2/relocation/nstream_after.ma".
(* RELOCATION N-STREAM ******************************************************)
(* Basic properties on isid *************************************************)
+lemma isid_eq_repl_back: eq_stream_repl_back … isid.
+/2 width=3 by eq_stream_canc_sn/ qed-.
+
+lemma isid_eq_repl_fwd: eq_stream_repl_fwd … isid.
+/3 width=3 by isid_eq_repl_back, eq_stream_repl_sym/ qed-.
+
lemma isid_id: 𝐈⦃𝐈𝐝⦄.
// qed.
(* Basic inversion lemmas on isid *******************************************)
-lemma isid_inv_seq: ∀f,a. 𝐈⦃a@f⦄ → 𝐈⦃f⦄ ∧ a = 0.
-#f #a normalize >id_unfold in ⊢ (???%→?);
+lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ n = 0.
+#f #n normalize >id_unfold in ⊢ (???%→?);
#H elim (eq_stream_inv_seq ????? H) -H /2 width=1 by conj/
qed-.
lemma isid_inv_push: ∀f. 𝐈⦃↑f⦄ → 𝐈⦃f⦄.
-* #a #f #H elim (isid_inv_seq … H) -H //
+* #n #f #H elim (isid_inv_seq … H) -H //
qed-.
lemma isid_inv_next: ∀f. 𝐈⦃⫯f⦄ → ⊥.
-* #a #f #H elim (isid_inv_seq … H) -H
+* #n #f #H elim (isid_inv_seq … H) -H
#_ #H destruct
qed-.
+lemma isid_inv_gen: ∀f. 𝐈⦃f⦄ → ∃∃g. 𝐈⦃g⦄ & f = ↑g.
+* #n #f #H elim (isid_inv_seq … H) -H
+#Hf #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≐ f2.
+/2 width=3 by eq_stream_canc_dx/ qed-.
+
(* inversion lemmas on at ***************************************************)
let corec id_inv_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → f ≐ 𝐈𝐝 ≝ ?.
-* #a #f #Ht lapply (Ht 0)
+* #n #f #Ht lapply (Ht 0)
#H lapply (at_inv_O1 … H) -H
#H0 >id_unfold @eq_seq
-[ cases H0 -a //
+[ cases H0 -n //
| @id_inv_at -id_inv_at
- #i lapply (Ht (⫯i)) -Ht cases H0 -a
+ #i lapply (Ht (⫯i)) -Ht cases H0 -n
#H elim (at_inv_SOx … H) -H //
]
qed-.
lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
#i elim i -i
-[ * #a #f #H elim (isid_inv_seq … H) -H //
-| #i #IH * #a #f #H elim (isid_inv_seq … H) -H
+[ * #n #f #H elim (isid_inv_seq … H) -H //
+| #i #IH * #n #f #H elim (isid_inv_seq … H) -H
/3 width=1 by at_S1/
]
qed-.
#i2 #i #Hi2 lapply (at_total i2 f1)
#H0 lapply (at_increasing … H0)
#Ht1 lapply (after_fwd_at2 … (f1@❴i2❵) … H0 … Ht)
-/3 width=7 by at_repl_back, at_mono, at_id_le/
+/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
qed.
(* Inversion lemmas on after ************************************************)
let corec isid_after_sn: ∀f1,f2. 𝐈⦃f1⦄ → f1 ⊚ f2 ≡ f2 ≝ ?.
-* #a1 #f1 * * [ | #a2 ] #f2 #H cases (isid_inv_seq … H) -H
-#Ht1 #H1
-[ @(after_zero … H1) -H1 /2 width=1 by/
-| @(after_skip … H1) -H1 /2 width=5 by/
-]
+* #n1 #f1 * * [ | #n2 ] #f2 #H cases (isid_inv_seq … H) -H
+/3 width=7 by after_push, after_refl/
qed-.
let corec isid_after_dx: ∀f2,f1. 𝐈⦃f2⦄ → f1 ⊚ f2 ≡ f1 ≝ ?.
-* #a2 #f2 * *
+* #n2 #f2 * *
[ #f1 #H cases (isid_inv_seq … H) -H
- #Ht2 #H2 @(after_zero … H2) -H2 /2 width=1 by/
-| #a1 #f1 #H @(after_drop … a1 a1) /2 width=5 by/
+ /3 width=7 by after_refl/
+| #n1 #f1 #H @after_next [4,5: // |1,2: skip ] /2 width=1 by/
]
qed-.
lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≐ f.
-/3 width=4 by isid_after_sn, after_mono/
+/3 width=8 by isid_after_sn, after_mono/
qed-.
lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≐ f.
-/3 width=4 by isid_after_dx, after_mono/
+/3 width=8 by isid_after_dx, after_mono/
qed-.
(*
lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.