各桁の和が3の倍数な整数は3の倍数 in Idris

MultiOf3.idr

module MultiOf3

%default total


-- isMm3 y x : -3y + x
data Mm3 : (y : Nat) -> Type where
  isMm3 : (y : Nat) -> Nat -> Mm3 y

-- 3の倍数か判定する
isMultiOf3Sub : Nat -> Bool
isMultiOf3Sub Z             = True
isMultiOf3Sub (S Z)         = False
isMultiOf3Sub (S (S Z))     = False
isMultiOf3Sub (S (S (S n))) = isMultiOf3Sub n
isMultiOf3 : Either Nat (y ** Mm3 y) -> Bool
isMultiOf3 (Left n)                   = isMultiOf3Sub n
               -- 3の倍数なのでkは捨てる
isMultiOf3 (Right (k ** (isMm3 k n))) = isMultiOf3Sub n

-- 各桁の和（の関係性）を求める
myPlus3 : Either Nat (y ** Mm3 y) -> Either Nat (y ** Mm3 y)
myPlus3 (Left n)                   = Left (S (S (S n)))
myPlus3 (Right (k ** (isMm3 k n))) = Right (k ** (isMm3 k (S (S (S n))) ))
sumDigitToN : Either Nat (y ** Mm3 y) -> Nat
sumDigitToN (Left n)                   = n
sumDigitToN (Right (k ** (isMm3 k n))) = n
sumDigit : Nat -> Nat -> Either Nat (y ** Mm3 y)
sumDigit _ Z             = Left Z
sumDigit _ (S Z)         = Left (S Z)
sumDigit _ (S (S Z))     = Left (S (S Z))
sumDigit a (S (S (S n))) =
  -- nの一桁目が6以下ならば+3を外に出す、でなければ -3a + sumDigit n にする
  if (modNatNZ n 10 SIsNotZ) `lte` 6
    then myPlus3 (sumDigit n n)
    else Right (a ** (isMm3 a (sumDigitToN (sumDigit n n))))
-- おまけfoldr (+) 0 $ map ((\x=> minus x 48) . toNat) $ the (List Int) $ (map cast . (unpack . show)) n


-- ----------補題1----------
lemma1 : (n:Nat) -> isMultiOf3 (Left n) = True
  -> isMultiOf3 (Left (S (S (S n)))) = True
lemma1 _ prf = prf

-- ----------補題2----------
lemma2_1 : (nn : Either Nat (y ** Mm3 y))
  -> isMultiOf3 (myPlus3 nn) = True
    -> isMultiOf3 nn = True
lemma2_1 (Left _)                   prf = prf
lemma2_1 (Right (_ ** (isMm3 _ _))) prf = prf

lemma2_2 : (nn : Either Nat (y ** Mm3 y))
  -> isMultiOf3Sub (sumDigitToN nn) = True
    -> isMultiOf3 nn = True
lemma2_2 (Left _)                   prf = prf
lemma2_2 (Right (_ ** (isMm3 _ _))) prf = prf

lemma2 : (n:Nat) -> (isMultiOf3 (sumDigit (S (S (S n))) (S (S (S n))))) = True
  -> (isMultiOf3 (sumDigit n n)) = True
lemma2 n prf with ((modNatNZ n 10 SIsNotZ) `lte` 6) proof p
  lemma2 n prf | True  = lemma2_1 (sumDigit n n) prf
  lemma2 n prf | False = lemma2_2 (sumDigit n n) prf


-- 各桁の和が3の倍数なら、元の数も3の倍数
theorem : (n:Nat)
  -> (isMultiOf3 (sumDigit n n)) = True -> isMultiOf3 (Left n) = True
theorem Z             _   = Refl
theorem (S Z)         prf = absurd prf
theorem (S (S Z))     prf = absurd prf
theorem (S (S (S n))) prf = lemma1 n $ theorem n $ lemma2 n prf