Last active
July 5, 2023 19:59
-
-
Save righ1113/28cbabc0bdfae8436d2b1e3b36645dd2 to your computer and use it in GitHub Desktop.
各桁の和が3の倍数なら、元の数も3の倍数 in Lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
完成しました。