Theorem: dropEveryNth_three_eq_fun (ListPowersProblem.lean)

State before:
α✝ : Type u_1
σ : Stream' α✝
⊢ dropEveryNth 3 σ = fun i => σ (i + i / 2)
Tactic:
rw [dropEveryNth, fun_to_corec fun i => σ (i + i/2)]
State after:
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 3 - 2) =
    corec (fun i => σ (i + i / 2)) (fun x => x + 1) 0

State before:
α✝ : Type u_1
σ : Stream' α✝
⊢ corec
      (fun x =>
        match x with
        | (σ, snd) => head σ)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 3 - 2) =
    corec (fun i => σ (i + i / 2)) (fun x => x + 1) 0
Tactic:
apply corec_bisim (fun ⟨σ', c⟩ i => σ' = (σ.drop <| i + i/2) 
  ∧ c = (i+1) % 2)
State after:
case hf
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      (match a with
        | (σ, snd) => head σ) =
        σ (a' + a' / 2)

case hg
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ', c) => σ' = drop (a' + 1 + (a' + 1) / 2) σ ∧ c = (a' + 1 + 1) % 2

case a
α✝ : Type u_1
σ : Stream' α✝
⊢ match (σ, 3 - 2) with
  | (σ', c) => σ' = drop (0 + 0 / 2) σ ∧ c = (0 + 1) % 2

State before:
case hf
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      (match a with
        | (σ, snd) => head σ) =
        σ (a' + a' / 2)
Tactic:
rintro ⟨_, _⟩ i ⟨⟨⟩, ⟨⟩⟩
State after:
case hf.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, snd) => head σ) =
    σ (i + i / 2)

State before:
case hf.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, snd) => head σ) =
    σ (i + i / 2)
Tactic:
simp only [head, nth, drop, zero_add]
State after:
no goals

State before:
case hg
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ', c) => σ' = drop (a' + 1 + (a' + 1) / 2) σ ∧ c = (a' + 1 + 1) % 2
Tactic:
rintro ⟨_, _⟩ i ⟨⟨⟩, ⟨⟩⟩
State after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ match
    match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, 0) => (tail (tail σ), 3 - 2)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ', c) => σ' = drop (i + 1 + (i + 1) / 2) σ ∧ c = (i + 1 + 1) % 2

State before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ match
    match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, 0) => (tail (tail σ), 3 - 2)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ', c) => σ' = drop (i + 1 + (i + 1) / 2) σ ∧ c = (i + 1 + 1) % 2
Tactic:
simp
State after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (i + 1 + 1) % 2

State before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (i + 1 + 1) % 2
Tactic:
rw [Nat.add_mod (i+1) 1]
State after:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      ((i + 1) % 2 + 1 % 2) % 2

State before:
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, (i + 1) % 2) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      ((i + 1) % 2 + 1 % 2) % 2
Tactic:
cases h : (i+1)%2
State after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2

case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.succ n✝ + 1 % 2) % 2

State before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2
Tactic:
have hdvd : 2 ∣ i+1 := Nat.dvd_of_mod_eq_zero h
State after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2

State before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.zero) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.zero + 1 % 2) % 2
Tactic:
simp [tail, drop, nth, Nat.succ_div_of_dvd hdvd]
State after:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (fun i_1 => σ (i_1 + 1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i / 2 + 1)))

State before:
case hg.mk.intro.refl.refl.zero
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
⊢ (fun i_1 => σ (i_1 + 1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i / 2 + 1)))
Tactic:
funext j
State after:
case hg.mk.intro.refl.refl.zero.h
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ σ (j + 1 + 1 + (i + i / 2)) = σ (j + (i + 1 + (i / 2 + 1)))

State before:
case hg.mk.intro.refl.refl.zero.h
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ σ (j + 1 + 1 + (i + i / 2)) = σ (j + (i + 1 + (i / 2 + 1)))
Tactic:
congr 1
State after:
case hg.mk.intro.refl.refl.zero.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ j + 1 + 1 + (i + i / 2) = j + (i + 1 + (i / 2 + 1))

State before:
case hg.mk.intro.refl.refl.zero.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
h : (i + 1) % 2 = Nat.zero
hdvd : 2 ∣ i + 1
j : ℕ
⊢ j + 1 + 1 + (i + i / 2) = j + (i + 1 + (i / 2 + 1))
Tactic:
ring
State after:
no goals

State before:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.succ n✝ + 1 % 2) % 2
Tactic:
simp [tail, drop, nth]
State after:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ ((fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))) ∧ n✝ = (Nat.succ n✝ + 1) % 2

State before:
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ ((fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))) ∧ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
constructor
State after:
case hg.mk.intro.refl.refl.succ.left
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))

case hg.mk.intro.refl.refl.succ.right
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2

State before:
case hg.mk.intro.refl.refl.succ.left
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))
Tactic:
funext j
State after:
case hg.mk.intro.refl.refl.succ.left.h
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ σ (j + 1 + (i + i / 2)) = σ (j + (i + 1 + (i + 1) / 2))

State before:
case hg.mk.intro.refl.refl.succ.left.h
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ σ (j + 1 + (i + i / 2)) = σ (j + (i + 1 + (i + 1) / 2))
Tactic:
congr 1
State after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)

State before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Tactic:
have hdvd : ¬2 ∣ i+1 := by
  apply Nat.not_dvd_of_mod_neq_zero 
  intro h'
  rw [h] at h'
  contradiction
State after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)

State before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + (i + 1) / 2)
Tactic:
rw [Nat.succ_div_of_not_dvd hdvd]
State after:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + i / 2)

State before:
case hg.mk.intro.refl.refl.succ.left.h.e_a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
hdvd : ¬2 ∣ i + 1
⊢ j + 1 + (i + i / 2) = j + (i + 1 + i / 2)
Tactic:
ring
State after:
no goals

State before:
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ ¬2 ∣ i + 1
Tactic:
apply Nat.not_dvd_of_mod_neq_zero
State after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ (i + 1) % 2 ≠ 0

State before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
⊢ (i + 1) % 2 ≠ 0
Tactic:
intro h'
State after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : (i + 1) % 2 = 0
⊢ False

State before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : (i + 1) % 2 = 0
⊢ False
Tactic:
rw [h] at h'
State after:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : Nat.succ n✝ = 0
⊢ False

State before:
case a
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
j : ℕ
h' : Nat.succ n✝ = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case hg.mk.intro.refl.refl.succ.right
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
cases' Nat.mod_two_eq_zero_or_one (i + 1) with h' h'
<;> rw [h'] at h
State after:
case hg.mk.intro.refl.refl.succ.right.inl
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 0 = Nat.succ n✝
h' : (i + 1) % 2 = 0
⊢ n✝ = (Nat.succ n✝ + 1) % 2

case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 1 = Nat.succ n✝
h' : (i + 1) % 2 = 1
⊢ n✝ = (Nat.succ n✝ + 1) % 2

State before:
case hg.mk.intro.refl.refl.succ.right.inl
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 0 = Nat.succ n✝
h' : (i + 1) % 2 = 0
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
contradiction
State after:
no goals

State before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : 1 = Nat.succ n✝
h' : (i + 1) % 2 = 1
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
simp at h
State after:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2

State before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ n✝ = (Nat.succ n✝ + 1) % 2
Tactic:
rw[←h]
State after:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ 0 = (Nat.succ 0 + 1) % 2

State before:
case hg.mk.intro.refl.refl.succ.right.inr
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h' : (i + 1) % 2 = 1
h : 0 = n✝
⊢ 0 = (Nat.succ 0 + 1) % 2
Tactic:
rfl
State after:
no goals

State before:
case a
α✝ : Type u_1
σ : Stream' α✝
⊢ match (σ, 3 - 2) with
  | (σ', c) => σ' = drop (0 + 0 / 2) σ ∧ c = (0 + 1) % 2
Tactic:
exact ⟨rfl, rfl⟩
State after:
no goals