internlm/Lean-Github huggingface dataset:
Theorem: Stream'.take_append_drop_take
Proof state before:
α : Type u_1
σ : Stream' α
i j : ℕ
⊢ (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
Tactic:
induction' i with i ih generalizing j σ
Proof state after:
case zero
α : Type u_1
σ✝ : Stream' α
j✝ : ℕ
σ : Stream' α
j : ℕ
⊢ (take Nat.zero σ ++ take j fun i => σ (i + Nat.zero)) = take (Nat.zero + j) σ

case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take (Nat.succ i) σ ++ take j fun i_1 => σ (i_1 + Nat.succ i)) = take (Nat.succ i + j) σ
Theorem: Stream'.take_append_drop_take
Proof state before:
case zero
α : Type u_1
σ✝ : Stream' α
j✝ : ℕ
σ : Stream' α
j : ℕ
⊢ (take Nat.zero σ ++ take j fun i => σ (i + Nat.zero)) = take (Nat.zero + j) σ
Tactic:
simp [take]
Proof state after:
no goals
Theorem: Stream'.take_append_drop_take
Proof state before:
case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take (Nat.succ i) σ ++ take j fun i_1 => σ (i_1 + Nat.succ i)) = take (Nat.succ i + j) σ
Tactic:
rw [Nat.add_assoc i 1 j, Nat.add_comm 1 j, ←Nat.add_assoc i j 1]
Proof state after:
case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take (Nat.succ i) σ ++ take j fun i_1 => σ (i_1 + Nat.succ i)) = take (i + j + 1) σ
Theorem: Stream'.take_append_drop_take
Proof state before:
case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take (Nat.succ i) σ ++ take j fun i_1 => σ (i_1 + Nat.succ i)) = take (i + j + 1) σ
Tactic:
simp [take, ←ih]
Proof state after:
case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take j fun i_1 => σ (i_1 + Nat.succ i)) = take j fun i_1 => tail σ (i_1 + i)
Theorem: Stream'.take_append_drop_take
Proof state before:
case succ
α : Type u_1
σ✝ : Stream' α
j✝ i : ℕ
ih : ∀ {σ : Stream' α} {j : ℕ}, (take i σ ++ take j fun i_1 => σ (i_1 + i)) = take (i + j) σ
σ : Stream' α
j : ℕ
⊢ (take j fun i_1 => σ (i_1 + Nat.succ i)) = take j fun i_1 => tail σ (i_1 + i)
Tactic:
congr
Proof state after:
no goals
Theorem: Stream'.take_succ_to_concat
Proof state before:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take (i + 1) σ = List.concat (take i σ) (σ i)
Tactic:
rw [←take_append_drop_take]
Proof state after:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take i σ ++ take 1 (drop i σ) = List.concat (take i σ) (σ i)
Theorem: Stream'.take_succ_to_concat
Proof state before:
α : Type u_1
σ : Stream' α
i : ℕ
⊢ take i σ ++ take 1 (drop i σ) = List.concat (take i σ) (σ i)
Tactic:
simp only [take, head, nth, drop, zero_add, List.concat_eq_append]
Proof state after:
no goals
Theorem: Stream'.sum_eq_head_plus_sum_tail
Proof state before:
α : Type ?u.12375
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ (i + 1) = head σ + sum (tail σ) i
Tactic:
simp only [sum, take, head, nth, Nat.add_eq, add_zero, Nat.sum_cons]
Proof state after:
no goals
Theorem: Stream'.sum_succ
Proof state before:
α : Type ?u.12759
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ (i + 1) = sum σ i + σ (i + 1)
Tactic:
simp [sum, take_succ_to_concat, Nat.add_assoc]
Proof state after:
no goals
Theorem: Stream'.sum_eq_corec
Proof state before:
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ)
Tactic:
funext i
Proof state after:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ) i
Theorem: Stream'.sum_eq_corec
Proof state before:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, σ) => (acc + head σ, tail σ))
      (head σ, tail σ) i
Tactic:
simp only [corec, map, nth]
Proof state after:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
Theorem: Stream'.sum_eq_corec
Proof state before:
case h
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
Tactic:
induction' i with i ih
Proof state after:
case h.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ Nat.zero = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) Nat.zero).fst

case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
⊢ sum σ Nat.zero = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) Nat.zero).fst
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ sum σ (Nat.succ i) = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) (Nat.succ i)).fst
Tactic:
simp only [sum_succ, iterate, ← ih, add_right_inj]
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = head (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).snd
Tactic:
simp only [iterate_eq_Nat_iterate, head, nth]
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
ih : sum σ i = (iterate (fun x => (x.fst + head x.snd, tail x.snd)) (head σ, tail σ) i).fst
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
clear ih
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
have (g : ℕ × Stream' ℕ → ℕ) (y) : 
    Prod.snd ((fun x => (g x, tail x.snd))^[i] (y, tail σ))
    = ((fun x => tail x)^[i] (tail σ)) := by
  induction i generalizing y σ <;> simp [*]
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = Prod.snd ((fun x => (x.fst + Prod.snd x 0, tail x.snd))^[i] (σ 0, tail σ)) 0
Tactic:
rw [this]
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
this :
  ∀ (g : ℕ × Stream' ℕ → ℕ) (y : ℕ), ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Tactic:
clear this
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x => tail x)^[i] (tail σ) 0
Tactic:
simp [tail, nth]
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x i => x (i + 1))^[i] (fun i => σ (i + 1)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ σ (i + 1) = (fun x i => x (i + 1))^[i] (fun i => σ (i + 1)) 0
Tactic:
suffices ∀ k,
    σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
  from this 1
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
⊢ ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Tactic:
intro k
Proof state after:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i k : ℕ
⊢ σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i k : ℕ
⊢ σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
Tactic:
induction' i with i ih generalizing k
Proof state after:
case h.succ.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ k : ℕ
⊢ σ (Nat.zero + k) = (fun x i => x (i + 1))^[Nat.zero] (fun i => σ (i + k)) 0

case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = (fun x i => x (i + 1))^[Nat.succ i] (fun i => σ (i + k)) 0
Theorem: Stream'.sum_eq_corec
Proof state before:
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
i : ℕ
g : ℕ × Stream' ℕ → ℕ
y : ℕ
⊢ ((fun x => (g x, tail x.snd))^[i] (y, tail σ)).snd = (fun x => tail x)^[i] (tail σ)
Tactic:
induction i generalizing y σ <;> simp [*]
Proof state after:
no goals
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ.zero
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ k : ℕ
⊢ σ (Nat.zero + k) = (fun x i => x (i + 1))^[Nat.zero] (fun i => σ (i + k)) 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = (fun x i => x (i + 1))^[Nat.succ i] (fun i => σ (i + k)) 0
Tactic:
simp [Nat.add_assoc, ←ih (1+k)]
Proof state after:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = σ (i + (1 + k))
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (Nat.succ i + k) = σ (i + (1 + k))
Tactic:
show σ (i + 1 + k) = _
Proof state after:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (i + 1 + k) = σ (i + (1 + k))
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ.succ
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ σ (i + 1 + k) = σ (i + (1 + k))
Tactic:
congr 1
Proof state after:
case h.succ.succ.e_a
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ i + 1 + k = i + (1 + k)
Theorem: Stream'.sum_eq_corec
Proof state before:
case h.succ.succ.e_a
α : Type ?u.13176
σ✝ : Stream' α
σ : Stream' ℕ
k✝ i : ℕ
ih : ∀ (k : ℕ), σ (i + k) = (fun x i => x (i + 1))^[i] (fun i => σ (i + k)) 0
k : ℕ
⊢ i + 1 + k = i + (1 + k)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Stream'.sum_dropEveryNth
Proof state before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)
Tactic:
have :
    (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst 
    = head σ := by
  rcases n with ⟨⟩|⟨⟩|⟨⟩|_ <;> rfl
Proof state after:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
this :
  (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)
Theorem: Stream'.sum_dropEveryNth
Proof state before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
this :
  (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)
Tactic:
sorry
Proof state after:
no goals
Theorem: Stream'.sum_dropEveryNth
Proof state before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
⊢ (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
Tactic:
rcases n with ⟨⟩|⟨⟩|⟨⟩|_ <;> rfl
Proof state after:
no goals
Theorem: Stream'.sum_corec
Proof state before:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ sum (corec f g x) =
    corec Prod.fst
      (fun x =>
        match x with
        | (acc, x) => (acc + f x, g x))
      (f x, g x)
Tactic:
simp only [sum_eq_corec, head_corec, tail_corec]
Proof state after:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd)) (f x, corec f g (g x)) =
    corec Prod.fst (fun x => (x.fst + f x.snd, g x.snd)) (f x, g x)
Theorem: Stream'.sum_corec
Proof state before:
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd)) (f x, corec f g (g x)) =
    corec Prod.fst (fun x => (x.fst + f x.snd, g x.snd)) (f x, g x)
Tactic:
apply corec_bisim (fun (acc₁, σ) (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x)
Proof state after:
case hf
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      a.fst = a'.fst

case hg
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      match (a.fst + head a.snd, tail a.snd) with
      | (acc₁, σ) =>
        match (a'.fst + f a'.snd, g a'.snd) with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x

case a
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ match (f x, corec f g (g x)) with
  | (acc₁, σ) =>
    match (f x, g x) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Theorem: Stream'.sum_corec
Proof state before:
case hf
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      a.fst = a'.fst
Tactic:
rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hf.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ (acc, corec f g x).fst = (acc, x).fst
Theorem: Stream'.sum_corec
Proof state before:
case hf.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ (acc, corec f g x).fst = (acc, x).fst
Tactic:
rfl
Proof state after:
no goals
Theorem: Stream'.sum_corec
Proof state before:
case hg
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ ∀ (a : ℕ × Stream' ℕ) (a' : ℕ × α),
    (match a with
      | (acc₁, σ) =>
        match a' with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x) →
      match (a.fst + head a.snd, tail a.snd) with
      | (acc₁, σ) =>
        match (a'.fst + f a'.snd, g a'.snd) with
        | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
rintro ⟨acc, _⟩ ⟨_, x⟩ ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hg.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ match ((acc, corec f g x).fst + head (acc, corec f g x).snd, tail (acc, corec f g x).snd) with
  | (acc₁, σ) =>
    match ((acc, x).fst + f (acc, x).snd, g (acc, x).snd) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Theorem: Stream'.sum_corec
Proof state before:
case hg.mk.mk.intro.refl.refl
α : Type u_1
σ : Stream' α
x✝ : α
f : α → ℕ
g : α → α
acc : ℕ
x : α
⊢ match ((acc, corec f g x).fst + head (acc, corec f g x).snd, tail (acc, corec f g x).snd) with
  | (acc₁, σ) =>
    match ((acc, x).fst + f (acc, x).snd, g (acc, x).snd) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
simp only [head_corec, tail_corec, and_self]
Proof state after:
no goals
Theorem: Stream'.sum_corec
Proof state before:
case a
α : Type u_1
σ : Stream' α
x : α
f : α → ℕ
g : α → α
⊢ match (f x, corec f g (g x)) with
  | (acc₁, σ) =>
    match (f x, g x) with
    | (acc₂, x) => acc₁ = acc₂ ∧ σ = corec f g x
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: Stream'.iterate_add_eq_mul
Proof state before:
α : Type ?u.25506
σ : Stream' α
y z x : ℕ
⊢ (fun x_1 => x_1 + x)^[y] z = x * y + z
Tactic:
induction' y with y ih generalizing z
Proof state after:
case zero
α : Type ?u.25506
σ : Stream' α
z✝ x z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.zero] z = x * Nat.zero + z

case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.succ y] z = x * Nat.succ y + z
Theorem: Stream'.iterate_add_eq_mul
Proof state before:
case zero
α : Type ?u.25506
σ : Stream' α
z✝ x z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.zero] z = x * Nat.zero + z
Tactic:
simp only [Nat.zero_eq, Function.iterate_zero, id_eq, mul_zero, zero_add]
Proof state after:
no goals
Theorem: Stream'.iterate_add_eq_mul
Proof state before:
case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ (fun x_1 => x_1 + x)^[Nat.succ y] z = x * Nat.succ y + z
Tactic:
simp only [Function.iterate_succ, Function.comp_apply, ih, ←Nat.add_one]
Proof state after:
case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ x * y + (z + x) = x * (y + 1) + z
Theorem: Stream'.iterate_add_eq_mul
Proof state before:
case succ
α : Type ?u.25506
σ : Stream' α
z✝ x y : ℕ
ih : ∀ {z : ℕ}, (fun x_1 => x_1 + x)^[y] z = x * y + z
z : ℕ
⊢ x * y + (z + x) = x * (y + 1) + z
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Stream'.even_eq_mul_two
Proof state before:
α : Type u_1
σ✝ σ : Stream' α
⊢ even σ = fun i => σ (i * 2)
Tactic:
funext i
Proof state after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ even σ i = σ (i * 2)
Theorem: Stream'.even_eq_mul_two
Proof state before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ even σ i = σ (i * 2)
Tactic:
simp [even, corec, map, head, nth, tail, iterate_stream_eq_index_iterate, iterate_add_eq_mul 2]
Proof state after:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ (2 * i) = σ (i * 2)
Theorem: Stream'.even_eq_mul_two
Proof state before:
case h
α : Type u_1
σ✝ σ : Stream' α
i : ℕ
⊢ σ (2 * i) = σ (i * 2)
Tactic:
rw [Nat.mul_comm]
Proof state after:
no goals
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
α : Type u_1
σ : Stream' α
⊢ dropEveryNth 2 σ = even σ
Tactic:
simp [even, dropEveryNth, corec']
Proof state after:
α : Type u_1
σ : Stream' α
⊢ corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 0) =
    corec (fun s => head s) (fun s => tail (tail s)) σ
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
α : Type u_1
σ : Stream' α
⊢ corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 0) =
    corec (fun s => head s) (fun s => tail (tail s)) σ
Tactic:
apply corec_bisim (fun ⟨σ, n⟩ σ' => σ = σ' ∧ n = 0)
Proof state after:
case hf
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      head a.fst = head a'

case hg
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ, n) => σ = tail (tail a') ∧ n = 0

case a
α : Type u_1
σ : Stream' α
⊢ match (σ, 0) with
  | (σ_1, n) => σ_1 = σ ∧ n = 0
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
case hf
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      head a.fst = head a'
Tactic:
rintro ⟨σ, n⟩ σ' ⟨⟨⟩, ⟨⟩⟩
Proof state after:
case hf.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ head (σ, 0).fst = head σ
Theorem: Stream'.dropEveryNth_two_eq_even
Proof state before:
case hf.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ head (σ, 0).fst = head σ
Tactic:
simp [drop, head, nth]
Proof state after:
no goals