defining an arithmetic natural sequence

Stream: new members

[Bulhwi Cha]

-- this code is written in Lean 4
import Mathlib.Tactic.Ring

-- define an arithmetic natural sequence
def is_arith_nat_seq (a : ℕ → ℕ) : Prop :=
    ∃ d : ℕ, ∀ n : ℕ, a (n + 1) = a n + d

def is_not_arith_nat_seq (a : ℕ → ℕ) : Prop := ¬ is_arith_nat_seq a

postfix:max "is an arithmetic natural sequence"     => is_arith_nat_seq
postfix:max "is not an arithmetic natural sequence" => is_not_arith_nat_seq

-- define the sequence of odd natural numbers
def odd : ℕ → ℕ := fun n : ℕ => 2 * n + 1

#reduce odd 0 -- output: 1
#reduce odd 1 -- 3
#reduce odd 2 -- 5

-- `odd` is an arithmetic natural sequence
theorem odd_is_arith_nat_seq : odd is an arithmetic natural sequence :=
  show ∃ d : ℕ, ∀ n : ℕ, odd (n + 1) = odd n + d
    from Exists.intro (2 : ℕ)
    (show ∀ n : ℕ, odd (n + 1) = odd n + 2
      from fun n : ℕ => calc
      odd (n + 1) = 2 * (n + 1) + 1 := rfl
      _           = (2 * n + 2) + 1 := congrArg Nat.succ (Nat.mul_add 2 n 1)
      _           = (2 * n + 1) + 2 := Nat.add_right_comm (2 * n) 2 1
      _           = odd n + 2       := rfl)

/- do not switch the order of the quantifiers
   in the definition of `is_arith_nat_seq` -/
theorem do_not_switch_quantifiers :
        ∃ b : ℕ → ℕ, (∀ n : ℕ, ∃ d : ℕ, b (n + 1) = b n + d)
                      ∧ b is not an arithmetic natural sequence :=
  let b : ℕ → ℕ := fun n : ℕ => n ^ 2

  have switch_quantifiers : ∀ n : ℕ, ∃ d : ℕ, b (n + 1) = b n + d :=
    fun n : ℕ =>
    show ∃ d : ℕ, b (n + 1) = b n + d
      from Exists.intro (2 * n + 1 : ℕ)
      (show b (n + 1) = b n + (2 * n + 1)
        from calc
        b (n + 1) = (n + 1) ^ 2       := rfl
        _         = n ^ 2 + 2 * n + 1 := by ring
        _         = b n + (2 * n + 1) := rfl)

  have b_is_not_arith_nat_seq : b is not an arithmetic natural sequence :=
    fun hyp : ∃ d : ℕ, ∀ n : ℕ, b (n + 1) = b n + d =>
    show False
      from Exists.elim hyp
      (fun d : ℕ =>
      fun d_is_common_difference : ∀ n : ℕ, b (n + 1) = b n + d =>
      have b_1_is_b_0_plus_d : b 1 = b 0 + d := d_is_common_difference 0
      have d_is_1 : d = 1 := calc
        d = b 1 - b 0 := by rw [b_1_is_b_0_plus_d, Nat.add_sub_self_left]
        _ = 1         := rfl
      have b_2_is_b_1_plus_d : b 2 = b 1 + d := d_is_common_difference 1
      have d_is_3 : d = 3 := calc
        d = b 2 - b 1 := by rw [b_2_is_b_1_plus_d, Nat.add_sub_self_left]
        _ = 3         := rfl
      have one_is_3     : 1 = 3 := by rw [← d_is_1, d_is_3]
      have one_is_not_3 : 1 ≠ 3 := by norm_num
      show False from one_is_not_3 one_is_3)

  show ∃ b : ℕ → ℕ, (∀ n : ℕ, ∃ d : ℕ, b (n + 1) = b n + d)
                    ∧ b is not an arithmetic natural sequence
    from Exists.intro (b : ℕ → ℕ)
    (show (∀ n : ℕ, ∃ d : ℕ, b (n + 1) = b n + d)
          ∧ b is not an arithmetic natural sequence
      from And.intro switch_quantifiers b_is_not_arith_nat_seq)

[Bulhwi Cha]

@shimsw20 and I wrote the above code for practice. We defined arithmetic natural sequences, proved that the sequence of odd natural numbers is one of them, and showed that you shouldn't switch the order of the quantifiers in the definition of is_arith_nat_seq.

Our proof style is adapted from the draft of @Clara Löh's "Exploring Formalisation. A Primer in Human-Readable Mathematics in Lean 3 with Examples from Simplicial Topology."

[Kevin Buzzard]

Nice!