結合律

結合律(associativity)

code:lean

-- Leanではa + b + cは(a + b) + cの意味になる

-- (a + b) + c = a + (b + c)

-- Level 4 / 5 : add_assoc (associativity of addition)

theorem add_assoc (a b c : ℕ) : a + b + c = a + (b + c) := by

induction a with h hd

-- → Goal: 0 + b + c = 0 + (b + c)

-- → Goal: b + c = 0 + (b + c)

-- → Goal: b + c = b + c

rfl

-- →

-- Assumptions: hd: h + b + c = h + (b + c)

-- Goal: succ h + b + c = succ h + (b + c)

-- →

-- Assumptions: hd: h + b + c = h + (b + c)

-- Goal: succ (h + b) + c = succ h + (b + c)

-- →

-- Assumptions: hd: h + b + c = h + (b + c)

-- Goal: succ (h + b + c) = succ h + (b + c)

-- →

-- Assumptions: hd: h + b + c = h + (b + c)

-- Goal: succ (h + b + c) = succ (h + (b + c))

-- →

-- Assumptions: hd: h + b + c = h + (b + c)

-- Goal: succ (h + (b + c)) = succ (h + (b + c))

rfl

-- → No Goals

確認用

Q. 結合律

調査用

Wikipedia.icon

Wikipedia.icon