各桁の和が3の倍数なら、元の数も3の倍数 in Lean

multiOf3.lean

open nat
#check succ


-- isMm3 y x : -3y + x
inductive Mm3 (y : ℕ)
| isMm3 : ℕ → Mm3
open Mm3
#check isMm3 3 5

-- 3の倍数か判定する
def isMultiOf3Sub : ℕ → bool
| zero                   := tt
| (succ zero)            := ff
| (succ (succ zero))     := ff
| (succ (succ (succ n))) := isMultiOf3Sub n
def isMultiOf3 : sum ℕ (sigma (λ y, Mm3 y)) → bool
| (sum.inl n)                        := isMultiOf3Sub n
               -- 3の倍数なのでkは捨てる
| (sum.inr (sigma.mk _ (isMm3 k n))) := isMultiOf3Sub n
#reduce isMultiOf3 (sum.inl 5)
#reduce isMultiOf3 (sum.inl 12)

-- 各桁の和（の関係性）を求める
def myPlus3 : sum ℕ (sigma (λ y, Mm3 y)) → sum ℕ (sigma (λ y, Mm3 y))
| (sum.inl n)                        := (sum.inl (succ (succ (succ n))) )
| (sum.inr (sigma.mk _ (isMm3 k n))) :=
    (sum.inr (sigma.mk _ (isMm3 k (succ (succ (succ n))))))
def sumDigitToN : sum ℕ (sigma (λ y, Mm3 y)) → ℕ
| (sum.inl n)                        := n
| (sum.inr (sigma.mk _ (isMm3 k n))) := n
variables a b : ℕ
def sumDigit : ℕ → sum ℕ (sigma (λ y, Mm3 y))
| zero                   := sum.inl zero
| (succ zero)            := sum.inl (succ zero)
| (succ (succ zero))     := sum.inl (succ (succ zero))
| (succ (succ (succ n))) :=
  -- nの一桁目が6以下ならば+3を外に出す、でなければ -3a + sumDigit n にする
  if (n % 10) < 7
    then myPlus3 (sumDigit n)
    else sum.inr (sigma.mk a (isMm3 a (sumDigitToN (sumDigit n))))
#check sumDigit
#reduce sumDigit 2 20
#check sigma.mk a (λ y, isMm3 y 7)


-- ----------補題1----------
lemma lemma1 : ∀ (n : ℕ),
  isMultiOf3 (sum.inl n) = tt
    → isMultiOf3 (sum.inl (succ (succ (succ n)))) = tt :=
begin
  intros n prf,
  apply prf
end
-- ----------補題1----------

-- ----------補題2----------
/-

◆コールグラフ
lemma2
  ┗ lemma2_1
      ┗ lemma2_1_1
          ┗ lemma2_1_1_1
      ┗ lemma2_1_2
          ┗ lemma2_1_1_1
  ┗ lemma2_2
      ┗ lemma2_1_1
          ┗ lemma2_1_1_1
      ┗ lemma2_1_2
          ┗ lemma2_1_1_1

-/
lemma lemma2_1_1_1 : ∀ (n : ℕ),
  isMultiOf3Sub (succ (succ (succ n))) = tt → isMultiOf3Sub n = tt
| _ prf := prf

lemma lemma2_1_1 : ∀ (n : ℕ),
  isMultiOf3 (sum.inl (succ (succ (succ n)))) = tt
    → isMultiOf3 (sum.inl n) = tt
| n :=
  begin
    rw isMultiOf3,
    rw isMultiOf3,
    apply (λ prf, lemma2_1_1_1 n prf)
  end

lemma lemma2_1_2 : ∀ (k n : ℕ),
  isMultiOf3 (myPlus3 (sum.inr ⟨k, isMm3 k n⟩)) = tt
    → isMultiOf3 (sum.inl n) = tt
| k n :=
  begin
    rw isMultiOf3,
    rw myPlus3,
    apply (λ prf, lemma2_1_1_1 n prf)
  end

lemma lemma2_1 : ∀ (nn : sum ℕ (sigma (λ y, Mm3 y))),
  isMultiOf3 (myPlus3 nn) = tt
    → isMultiOf3 nn = tt
| (sum.inl n)                        prf := lemma2_1_1 n prf
| (sum.inr (sigma.mk _ (isMm3 k n))) prf := lemma2_1_2 k n prf

variable c : (ite (11 % 10 < 7) true false)
variable d : (11 % 10 < 7)
#check c
#check implies_of_if_pos c d
variables aa bb : Prop
variable e : (ite (11 % 10 < 7) true false) = (ite (11 % 10 < 7) false false)
-- #check congr_arg (λ (q : ite (11 % 10 < 7) aa bb), implies_of_if_pos q d) e

lemma lemma2_2 : ∀ (nn : sum ℕ (sigma (λ y, Mm3 y))),
  isMultiOf3Sub (sumDigitToN nn) = tt
    → isMultiOf3 nn = tt
| (sum.inl n)                        prf := lemma2_1_1 n prf
| (sum.inr (sigma.mk _ (isMm3 k n))) prf := lemma2_1_2 k n prf

lemma lemma2 : ∀ (n : ℕ),
  isMultiOf3 (sumDigit zero (succ (succ (succ n)))) = tt
    → isMultiOf3 (sumDigit zero n) = tt
| n :=
  begin
    rw sumDigit,
    by_cases h : ((n % 10) < 7),
      {
        rw if_pos,
        apply (λ prf, lemma2_1 (sumDigit zero n) prf),
        apply h
      },
      {
        rw if_neg,
        rw isMultiOf3,
        apply (λ prf, lemma2_2 (sumDigit zero n) prf),
        apply h
      }
  end
-- ----------補題2----------

-- 各桁の和が3の倍数なら、元の数も3の倍数
theorem theoremMultiOf3 : ∀ (n : ℕ),
  isMultiOf3 (sumDigit zero n) = tt → isMultiOf3 (sum.inl n) = tt
| zero                   _   := rfl
| (succ zero)            prf := by contradiction
| (succ (succ zero))     prf := by contradiction
| (succ (succ (succ n))) prf := lemma1 n (theoremMultiOf3 n (lemma2 n prf))

未完成です。

完成しました。