人工智能数学验证工具LEAN4【入门介绍2】加法世界-数学归纳法,证明自然数是加法交换幺半群

发布时间:2024年01月22日

视频链接,创作不易记得投币哦:人工智能数学验证工具LEAN4【入门介绍2】加法世界-数学归纳法,自然数是加法交换幺半群_哔哩哔哩_bilibili

import Game.Levels.Addition.L03add_comm


World "Addition"
Level 4
Title "add_assoc (associativity of addition)"

namespace MyNat

Introduction
"
? We've been adding up two numbers; in this level we will add up three.

? What does $x+y+z$ *mean*? It could either mean $(x+y)+z$, or it
? could mean $x+(y+z)$. In Lean, $x+y+z$ means $(x+y)+z$.

? But why do we care which one it means; $(x+y)+z$ and $x+(y+z)$ are *equal*!

? That's true, but we didn't prove it yet. Let's prove it now by induction.
"

LemmaDoc MyNat.add_assoc as "add_assoc" in "+" "`add_assoc a b c` is a proof
that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints
as `a + b + c`, because the notation for addition is defined to be left
associative. "

/-- On the set of natural numbers, addition is associative.
In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have
$ (a + b) + c = a + (b + c). $ -/
Statement add_assoc (a b c : ?) : a + b + c = a + (b + c) := by
? Hint "Remember that when Lean writes `a + b + c`, it means `(a + b) + c`.
? If you are not sure where the brackets are in an expression, just hover
? your cursor over it and look at what gets highlighted. For example,
? hover over both `+` symbols on the left hand side of the goal and
? you'll see where the invisible brackets are."
? induction c with d hd
? · rw [add_zero, add_zero]
? ? rfl
? · rw [add_succ, add_succ, hd, add_succ]
? ? rfl

-- Adding this instance to make `ac_rfl` work.
instance : Lean.IsAssociative (α := ?) (· + ·) := ?add_assoc?

LemmaTab "+"

Conclusion
"
A passing mathematician congratulates you on proving that naturals
are an additive commutative monoid.

Let's practice using `add_assoc` and `add_comm` in one more level,
before we leave addition world.
"

文章来源:https://blog.csdn.net/weixin_44347105/article/details/135723500
本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。