Mathematics_in_Lean

发表于 更新于 分类于 阅读次数： Waline： 本文字数： 766 阅读时长 ≈ 3 分钟

Mathematics in lean ：基于mathlib库，建造复杂表达式的方式：1.自己写，2.提供instruction 指导如何构建
Theorem Proving in Lean: 侧重底层逻辑框架和Lean的核心语法

Log

Linear algebra写法

2 basic

1
2
3
4
5
-- le_div_iff₀这个theorem，以及rm[]
-- 使用方面linarith(线性计算)，和ring(交换)
-- 以及证明时可以把用的定理直接提出来，theorem
-- have h:引入假设，calc 分步计算，让过程更加清晰，因为写出了要证明的每一步的结果
-- tatics： apply , repeat

3.1 Impication and the Universal Quantifier

In lean,in a sequence of implications there are implicit parentheses grouped to the right.

it is common in Lean to use curly brackets to make quantified variables implicit when they can be inferred from subsequent hypotheses.So we can just do lemma to the hypothese without mentioning the objects.即用{}括起来的在调用时不需要显示指出。

5.2 Induction and Recursion

1
2
3
4
5
6
7
8
9
-- 归纳
-- inductive types (which are types generated infuctively by a given list of constructors)
-- e.g. the natual numbers are declared as follows( in Prelude.lean)
inductive Nat where
  | zero : Nat -- constructor
  | succ (n : Nat): Nat -- constructor
---------------------------------------------------------

@[simp] -- specifys that the defining equation should be added to the database of identities that the simplifier uses by default

6.1 Defining Structures

structure can specify not only data types but also constraints that the data must satisfy(In lean,these are represented as fields of type Prop).
def 可以用来定义structure实例
subtype类型({x: alpha // p x}表示for all a in alpha，p x is true) construction combines a piece of data with a property.

structure的好处：But even though we can use products, subtypes, and Sigma types instead of structures, using structures has a number of advantages. Defining a structure abstracts away the underlying representation and provides custom names for the functions that access the components. This makes proofs more robust: proofs that rely only on the interface to a structure will generally continue to work when we change the definition, as long as we redefine the old accessors in terms of the new definition. Moreover, as we are about to see, Lean provides support for weaving structures together into a rich, interconnected hierarchy, and for managing the interactions between them.

1
2
structure structure_name where
  ...

annotation when define a structure：

structure can bundle together data,so as the and符号

1
2
-- 此注解表示自动生成定理: 当结构体的两个实例组成部分对应相同时，这两个实例相等
@[ext] -- extensionality,tells Lean to automatically generate theorems that can be used to prove that two instances of a structure are equal when their components are equal.

define particular instances of structure

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
def inst_name : struc_name where
  ...
  -- e.g. x:=1
---------------------------------
def inst_name : struct_name :=
  ...
  --e.g. <value1 , ,...> -- anonymous constructor notation
---------------------------------
def inst_name :=
  struc_name.mk ...valuek valuek+1 ...
  -- struc_name.mk 是constructor，也可以自己命名，需要在define structure 的时候，比where多 了name和::
  -- structure struc_name where constructor_name ::
  --    ...
-- open a namespace
namespace namespace_name
...
end namespace_name

definations and theorems

about namespace: when namespace not open, can use anonymous projection notation,which allows us to write a.add b instead of namespace_name.add a b.

protected keyword

1
2
3
-- so that the theorem name is Point.add_comm,even when the namespace is open
protected theorem add_comm (a b :Point) :add a b = add b a:=by
  sorry

6.2 Algebraic Structures

abelian or commutative group : set A, operation •,假设a b ∈ A,则需要满足Closure （a · b ∈ A），Associativity（结合律），Identity element (必存在e∈A就是元 使得a · e = e · a = a)，Inverse element(对任意a，都有a · b = b · a = e)，Commutativity（交换律）
lattice ： 带有join和meet（leat upper bound 和greatest lower bound）偏序集合
ring ： 加法abelian group和an associative multiplication operation *，和identity 1，且multiplication distributes over addition.如果乘法是交换的则环是交换的

Lean theorem

multiple arrows：隐式右结合（associate to the right）

Lean使用快捷键

Ctrl-Shift-P ： get access to the Lean 4:show all abbreviations
Ctrl-Space : completion in the editior to guess the theorem name

写法

运算的特殊写法

  1. divisibility relation整除关系 |

提示写法

“apply?”可以在右边得到suggestions

重复证明过程的写法

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
--1. 使用hypothesis ：任意
--2. 使用repeat
example : min a b = min b a := by
  have h : ∀ x y : ℝ, min x y ≤ min y x := by
    intro x y
    apply le_min
    apply min_le_right
    apply min_le_left
  apply le_antisymm
  apply h
  apply h
-----------------------
example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left

name_of_theorem

A_of_B_of_C: established something of the form A from hypothese of the form B and C,where A,B,C approximate the way we might read the goals out loud,e.g. x+y<… probably start with add_lt.

example use by & not use by

1
2
3
4
5
6
7
example (a b : R) : a - b = a + -b :=by
  rw[sub_eq_add_neg a b]
end

example (a b : R) : a - b = a + -b :=
  sub_eq_add_neg a b
end

语法记录

Command

1
2
3
4
5
6
7
8
9
10
11
12
--
section ... end
-- 变量声明
variable(v1 v2 v3 ... : type) 
-- 检查类型，或描述用法
#check ...
#check a -- a:R
#check mul_comm -- mul_comm.{u_1} {G : Type u_1} [CommMagma G] (a b : G) : a * b = b * a

#check norm_num -- 常量计算与比较，Normalize numerical expressions. Supports the operations + - * / ⁻¹ ^ and % over numerical types such as ℕ, ℤ, ℚ, ℝ, ℂ and some general algebraic types, and can prove goals of the form A = B, A ≠ B, A < B and A ≤ B, where A and B are numerical expressions. It also has a relatively simple primality prover.

-- Nat.gcd m n :最大公约数,在显示的时候会显示出来m.gcd.n

rfl is short for “reflexivity”.

calc先定义阶段目标再填写过程

1
2
3
4
5
6
7
8
example:(a+b)*(a+b) = a*a+2*a*b +b*b:
    calc
        xx :by
            xx
        _=xxx:=by
            xx
        _=xxxx:=by
            xxxx

have 先提出假设h进行证明，之后可以使用h推断goal

1
2
3
4
theorem zero_mul(a: R):0*a  =0 := by
    have h: 0*a+0*a = 0*a+0 :=by
        rw[←add_mul,add_zero,add_zero]
    rw[add_left_cancel h]

rw[…,…,…]替换

  1. 变量

定理

左箭头表示a=b:用a替换b

1
2
3
4
nth_rw <第几个>[]替换
rw[mul_assoc]--a*b*c = a*(b*c)
rw[mul_assoc]--a*(b*c)=a*b*c
sub_self -- a-a=0

<⬅>mul_assoc
mul_comm <v1,v2>

tactic：ring

automation for that follow purely from the ring axioms

1
2
example: c*b*a = b*(a*c):= by
    ring

a ring consists of a collection of
objects,
R,(R with + is an abelian group,with 0 as the additive identity , with negation as inverse)
operations + *,and (multiplication is associative with identity 1,and multiplication distributes over addition)
constants 0 and 1,and
an operation x->-x

Lean is good not only for proving things about concrete mathematical structures like the natural numbers and the integers, but also for proving things about abstract structures, characterized axiomatically, like rings. Moreover, Lean supports generic reasoning about both abstract and concrete structures, and can be trained to recognize appropriate instances.