feat(data/{seq,stream}): cons_injective2 (#15832)

Also some simple API lemmas for `nth`
I didn't change the style of the `stream/init` file.





Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>

src/data/seq/seq.lean

@@ -59,6 +59,16 @@ def nth : seq α → ℕ → option α := subtype.val
 @[ext] protected lemma ext {s t : seq α} (h : ∀ n : ℕ, s.nth n = t.nth n) : s = t :=
 subtype.eq $ funext h
 
+lemma cons_injective2 : function.injective2 (cons : α → seq α → seq α) :=
+λ x y s t h, ⟨by rw [←option.some_inj, ←nth_cons_zero, h, nth_cons_zero],
+  seq.ext $ λ n, by simp_rw [←nth_cons_succ x s n, h, nth_cons_succ]⟩
+
+lemma cons_left_injective (s : seq α) : function.injective (λ x, cons x s) :=
+cons_injective2.left _
+
+lemma cons_right_injective (x : α) : function.injective (cons x) :=
+cons_injective2.right _
+
 /-- A sequence has terminated at position `n` if the value at position `n` equals `none`. -/
 def terminated_at (s : seq α) (n : ℕ) : Prop := s.nth n = none
 

src/data/stream/init.lean

@@ -25,7 +25,7 @@ instance {α} [inhabited α] : inhabited (stream α) :=
 protected theorem eta (s : stream α) : head s :: tail s = s :=
 funext (λ i, begin cases i; refl end)
 
-theorem nth_zero_cons (a : α) (s : stream α) : nth (a :: s) 0 = a := rfl
+@[simp] theorem nth_zero_cons (a : α) (s : stream α) : nth (a :: s) 0 = a := rfl
 
 theorem head_cons (a : α) (s : stream α) : head (a :: s) = a := rfl
 
@@ -43,6 +43,8 @@ funext (λ i, begin unfold drop, rw nat.add_assoc end)
 
 theorem nth_succ (n : nat) (s : stream α) : nth s (succ n) = nth (tail s) n := rfl
 
+@[simp] lemma nth_succ_cons (n : nat) (s : stream α) (x : α) : nth (x :: s) n.succ = nth s n := rfl
+
 theorem drop_succ (n : nat) (s : stream α) : drop (succ n) s = drop n (tail s) := rfl
 
 @[simp] lemma head_drop {α} (a : stream α) (n : ℕ) : (a.drop n).head = a.nth n :=
@@ -51,6 +53,16 @@ by simp only [drop, head, nat.zero_add, stream.nth]
 @[ext] protected theorem ext {s₁ s₂ : stream α} : (∀ n, nth s₁ n = nth s₂ n) → s₁ = s₂ :=
 assume h, funext h
 
+lemma cons_injective2 : function.injective2 (cons : α → stream α → stream α) :=
+λ x y s t h, ⟨by rw [←nth_zero_cons x s, h, nth_zero_cons],
+  stream.ext (λ n, by rw [←nth_succ_cons n _ x, h, nth_succ_cons])⟩
+
+lemma cons_injective_left (s : stream α) : function.injective (λ x, cons x s) :=
+cons_injective2.left _
+
+lemma cons_injective_right (x : α) : function.injective (cons x) :=
+cons_injective2.right _
+
 theorem all_def (p : α → Prop) (s : stream α) : all p s = ∀ n, p (nth s n) := rfl
 
 theorem any_def (p : α → Prop) (s : stream α) : any p s = ∃ n, p (nth s n) := rfl