1+1=2の証明

#🌱

「1+1=2を証明するにはどうするか」が気になってメモ

普通の証明はペアノの公理を使うらしい

どうして1+1=2なの？ペアノの公理に従ってLeanで説明しよう - YouTube

GitHub: lean4_textbook/Lean4Textbook/NatDef.lean at main · ondanaoto/lean4_textbook

普通の説明だと多分よくわからなさそうなのでLeanで証明されているものを見てみる

Leanの場合の1+1=2の証明

mathlib ver3の場合の定義。関係しそうなところだけ抽出。

code:src/algebra/ring/defs.lean

34 variables {α : Type u} {β : Type v} {γ : Type w} {R : Type x}

110 section has_one_has_add

111

112 variables has_one α has_add α

113

114 lemma one_add_one_eq_two : 1 + 1 = (2 : α) := rfl

115

116 end has_one_has_add

ref: one_add_one_eq_two(mathlib ver3)

mathlib4の場合の定義

code:Mathlib/Data/Nat/Cast/Defs.lean

theorem one_add_one_eq_two AddMonoidWithOne R : 1 + 1 = (2 : R) := by

rw ← Nat.cast_one, ← Nat.cast_add

apply congrArg

decide

ref: one_add_one_eq_two(mathlib ver4)

AddMonoidWithOneがなんなのとか色々わからないことはある。なのでMathlib4のドキュメントを見る。

AddMonoidWithOneの定義: Mathlib.Data.Nat.Cast.Defs

one_add_one_eq_twoの定義: Mathlib.Data.Nat.Cast.Defs

Natの定義: Init.Prelude > Nat

モノイド(半群)は結合律、単位律を満たす構造

code:memo

@simp, norm_cast

theorem cast_one AddMonoidWithOne R : ((1 : ℕ) : R) = 1 := by

rw cast_succ, Nat.cast_zero, zero_add

-- ↑1 = 1

@simp, norm_cast

theorem cast_add AddMonoidWithOne R (m n : ℕ) : ((m + n : ℕ) : R) = m + n := by

induction n with

| zero => simp

-- ↑(m + n) = ↑m + ↑n

| succ n ih => rw add_succ, cast_succ, ih, cast_succ, add_assoc

apply(Lean)

one_add_one_eq_twoで検索 in leanprover-community/mathlib

congrArg

decide(Lean 4)

2 + 2 = 4の証明

Natural Number Game 「Level 8 / 8 : 2+2=4」という問題があって、そこで「2+2=4」が証明できる

code:lean

example : (2 : ℕ) + 2 = 4 := by

rw two_eq_succ_one -- succ 1 + succ 1 = 4

rw succ_eq_add_one -- 1 + 1 + (1 + 1) = 4

rw one_eq_succ_zero -- succ 0 + succ 0 + (succ 0 + succ 0) = 4

rw add_succ -- succ (succ 0 + 0) + succ (succ 0 + 0) = 4

rw add_succ -- succ (succ (succ 0 + 0) + (succ 0 + 0)) = 4

rw add_zero -- succ (succ (succ 0) + succ 0) = 4

rw add_succ -- succ (succ (succ (succ 0) + 0)) = 4

rw add_zero -- succ (succ (succ (succ 0))) = 4

rw ← one_eq_succ_zero -- succ (succ (succ 1)) = 4

rw ← two_eq_succ_one -- succ (succ 2) = 4

rw ← three_eq_succ_two -- succ 3 = 4

rw ← four_eq_succ_three -- 4 = 4

rfl -- no goals