My first proof, any feedbacks on this ?

Stream: new members

[Lorenzo Carrascosa]

Hi everyone, for my first proof with lean4, I'm working on parasitic number and one of the first result I needed was the equivalence between doing a rotation 1 of a list of digits and a formula without any list operators.

Do you have some advices or feedbacks on this ?

import Mathlib.Tactic

/-- A structure to represent a parasitic number.

A parasitic number `n` in base `b` with multiplier `m` satisfies the property that when you
multiply `n` by `m`, the digits of the resulting number, when rotated to the left by one position,
are the same as the digits of `n`.
-/
structure ParasiticNumber (b m : ℕ) where
  /-- The parasite number. -/
  n : ℕ
  h_b : b > 1
  h_n : n > 0
  h_m : m > 1
  /-- The property of a parasitic number. -/
  h_parasitic : n * m = Nat.ofDigits b (Nat.digits b n |>.rotate 1)

def ParasiticNumber.length {b m : ℕ} (p : ParasiticNumber b m) : ℕ :=
  Nat.digits b p.n |>.length

/-- An equivalent property of h_parasitic which uses algebraic manipulation instead of list operations.
-/
theorem ParasiticNumber.algebraic_property {b m : ℕ} (p : ParasiticNumber b m) :
  p.n * m = (p.n / b) + (p.n % b) * b^(p.length - 1) := by
  set d := p.n % b with hd
  set y := p.n / b with hy
  set l := p.length with hl
  set n := p.n with hn
  set n' := n * m with hn'
  have h_parasitic := p.h_parasitic
  rw [← hn'] at h_parasitic
  have h_len : (b.digits y).length = (b.digits n).length - 1 := by
    rw [Nat.digits_def' p.hb p.hn, List.length_cons, Nat.add_sub_cancel]
  calc
    n' = Nat.ofDigits b ((b.digits n).rotate 1) := by rw [h_parasitic]
    _ = Nat.ofDigits b ((d :: b.digits y).rotate 1) := by rw [Nat.digits_def' p.hb p.hn]
    _ = Nat.ofDigits b ((b.digits y) ++ [d]) := by
      rw [List.rotate_eq_drop_append_take]
      · rfl
      · exact Nat.succ_le_succ (Nat.zero_le (b.digits y).length)
    _ = Nat.ofDigits b (b.digits y) + b^(b.digits y).length * Nat.ofDigits b [d] :=
      by rw [Nat.ofDigits_append]
    _ = y + d * b^(l - 1) := by
      rw [Nat.ofDigits_digits, Nat.ofDigits_singleton, h_len]
      ring_nf
      rfl

[Michael Rothgang]

Here's one trick: you can combine consecutive rw calls into one: rw [foo]; rw [bar] is (almost always) equivalent to rw [foo, bar].

[Lorenzo Carrascosa]

thank you.