## Stream: new members

### Topic: defining an arithmetic natural sequence

#### Bulhwi Cha (Aug 11 2022 at 16:21):

-- 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 (Aug 11 2022 at 16:22):

@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 (Aug 11 2022 at 16:40):

Nice!

Last updated: Dec 20 2023 at 11:08 UTC