theorem_proving_in_lean4

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

theorem_proving_in_lean4
自动定理证明侧重于“发现”方面。解析定理证明器、表定理证明器、快速可满足性求解器等提供了在命题和一阶逻辑中确定公式有效性的方法。其他系统为特定语言和领域提供搜索程序和决策程序，例如整数或实数上的线性或非线性表达式。诸如 SMT（“可满足性模理论”）之类的架构将领域通用搜索方法与领域特定程序相结合。计算机代数系统和专门的数学软件包提供了执行数学计算、建立数学界限或查找数学对象的方法。计算也可以被视为证明，这些系统也有助于建立数学主张。
自动推理系统追求强大和高效，通常以牺牲可靠性为代价。这样的系统可能存在错误，而且很难确保它们提供的结果是正确的。相比之下，交互式定理证明侧重于定理证明的“验证”方面，要求每个主张都得到适当公理基础的证明支持。这设定了一个非常高的标准：每个推理规则和计算的每个步骤都必须通过诉诸先前的定义和定理来证明，一直到基本公理和规则。事实上，大多数这样的系统都提供了完全详尽的“证明对象”，可以传达给其他系统并进行独立检查。构建这样的证明通常需要更多的用户输入和交互，但它允许您获得更深入和更复杂的证明。
精益定理证明器旨在通过将自动化工具和方法置于支持用户交互和构建完全指定的公理证明的框架中来弥补交互式和自动化定理证明之间的差距。目标是同时支持数学推理和复杂系统推理，并验证这两个领域的主张。
Lean 的底层逻辑具有计算解释，Lean 也可以被视为一种编程语言。更确切地说，它可以被视为一种具有精确语义的程序编写系统，以及对程序计算的功能进行推理的系统。Lean 还具有充当其自己的元编程语言的机制，这意味着您可以使用 Lean 本身实现自动化并扩展 Lean 的功能.

Dependent Type Theory（类型理论：任何一个表达式都是一个类型）

依赖类型理论的重要特征

  1. each term has computational behavior
  2. each term supports a notion of nomalization
  3. term 包含很多信息，可以从中推断出信息
    Lean 是基于依赖类型理论Calculus of Constructions，with a countable hierarchy of non-cumulative universes and inductive types，有编译器(生成可执行二进制文件)和interactive interpreter

Simple Type Theory

Lean natural number is a 任意精度的无符号整数

1
2
3
4
5
6
7
8
/-
    def 声明new constant symbols
    #check,#eval 辅助性命令一般#开头
    类型理论：a -> b 表示从a到b的函数类型
    描述f是关于x的函数 f x(e.g. Nat.succ 2)
    arrows associate to the right （Nat -> Nat -> Nat 是等同于Nat -> (Nat -> Nat)）
    函数的partially apply： Nat.add 3等同于Nat.add 3 n 返回了一个函数等待第二个参数n
-/

Type as objects

不理解类型理论，不知道def定义的意思
不理解操作在type universes上是多态polymorphic（感觉是多个类型参数结果是一个类型）的，例子List a，表示不论a在哪个类型中，List a都有意义

1
2
3
4
5
6
7
8
9
10
11
12
-- Lean的底层基础无限类型层次，Type 0是小范围的类型，Type 1是更大的类型，包含Type 0作为一个元素，以此类推
#check Type     -- Type 1
#check Type 1   -- Type 2
-- Lean依赖类型理论扩展的方式
    -- 1. 类型本身，它们的类型是Type

----------------------------------------------------------
-- 定义polymorphic constants（使用universe或者在定义时提供universe parameters）
universe u
def F (\a : Type u) : Type u := Prod \a \a
------------------------------------------
def G.{v} (\a : Type v) :Type v:= Prod \a \a

Function Abstraction and Evaluation

creating a function from another expression is a process known as lambda abstraction

1
2
3
4
5
6
7
-- fun 也可以用 λ 代替
#check (fun x => x+1) -- Nat -> Nat,此处leave off type notation省略了类型注释
/-  fun (x : type) => t 其中()可以省略
    对于x：\a 变量，可以构造表达式t:\b
    λ (x: \a) => t 表示函数from \a to \b 将x 映射到t
    其中x 是bound variable，占位符，whose scope does not extend beyond the expression t
-/

alpha equivalent : expression that are the same up to renaming of bound variables are called alpha equivalent, and considered as “the same”.

definitionally equal： two terms that reduce to the same value are called definitionally equal

Definitions

1
2
3
4
5
6
7
8
9
10
11
12
13
def self_name (arg1 arg2 : arg_Type) (arg3 :arg_type) : return_Type := expression
-- 虽然返回类型Lean可以推断，但最好还是显示指出
def fun1 := fun x:Nat => x+x -- def 定义函数就是有名字的fun或λ
def fun2 (x:Nat)  : Nat := x+x
def fun21 (x:Nat)  := x+x

def fun3 : Nat -> Nat := fun x => x+x
def fun3 (x: Nat): Nat -> Nat := fun x => x+x --这个第一个x会提示没有用到
def f := 1

def compose (α β γ :Type) (f: α → β ) (g : γ → α ) (x: γ ):β := f (g x)

#eval compose Nat Nat Nat fun1 fun3 f --4

Local Definitions

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
-- ;或换行都可以
def curiosity :=
    let x := 1+2
    let y := x+1;let z:=y+1
    x+y+z
#eval curiosity -- 12

/-
    ((fun a => t2) t1) 与 (let a := t1;t2)不一样；前者a是对t1的缩写，后者是a是一个变量，是一个整体

    #eval (fun a:Nat => a+a) 1+1 -- 3
    #eval (fun a:Nat => a*a) 1+1 -- 2
    #eval (fun a:Nat => a*a) (1+1) -- 4
    #eval let a:=1+1;a*a --4

    -- 迷惑？？？：bar0会 进行type check，但是bar不会进行！！！！
    def bar0 := let a:=Nat; fun x:a =>x+2
    def bar := (fun a => fun x : a => x + 2) Nat
-/

Varibles and Sections

section可以没有名字

1
2
3
4
5
6
7
8
section outer
variable (\a \b \g :Type)
variable (x: \a) (y: \b) --作用域在section中，包括里面的section也起作用
section
variable (x: \b) 
-- 与外部相同的定义会覆盖外部
end
end outer

NameSpaces

namespase 必须有名字，有且仅有一个匿名在root level

namespaces organize data and sections declare variables for insertion in definitions;sections are also useful for delimiting限制 the scope of commands such as “set_option” and “open”；对于variable 和 open命令，随着namespace关闭也失效

1
2
3
4
5
6
7
8
9
namespace foo
    namespace bar
    end bar
end foo

open foo --可以在当前使用非嵌套foo的短名

namespace foo
end foo

What makes dependent type dependent

看不懂举的例子是什么意思？？？？？？？不明白传值的时候哪个对应哪个！！！
type can depend on parameters
dependent function type(dependent arrow type) : (a:\a)->\b 其中\b 的值依赖于a (e.g. (a:\a) -> \b a)

Dependent products are also called sigma types, and you can also write them as Σ a : α, β a. You can use ⟨a, b⟩ or Sigma.mk a b to create a dependent pair. The ⟨ and ⟩ characters may be typed with \langle and \rangle or < and >, respectively.

implicit arguments

1
2
3
4
5
6
7
8
9
10
11
12
13
-- sorry produces a proof of anything or provides an object of any data type at all,但是不能用来证明False,会报错
-- _  placeholder代表implicit argument，表示自动填充
-- 可以从传入的某个参数确定一些类型参数，此时类型参数可以用_代替

-- 也可以在定义时，用 {}将可以推断的参数括起来，在传入时就无需显示指明

-- (e : T) to specify the type T of an expression e ,这样写告诉Lean的elaborator 在解决隐式参数时使用T作为e的Type

--  @List  -- 描述相同的方法，不过所用的参数都变成了explicit

-- Numerals are overloaded in Lean
#check 2 -- Nat
#check (2 : Int) -- Int

Lean 的实例化隐式参数(instantiating implicit arguments)可以用来infer function types , predicates , proofs
elaboration : the process of instantiating these “holes” or “placeholders”

Propositions and Proofs

Propositions as Types

proposition represents a sort of data type. if proposition p is true then the type associated with p is inhabited.constructing t : p tell us p is indeed true.

1
2
3
4
5
6
-- Prop is Sort 0
-- Type u is Sort (u+1)
-- if p q: Prop, then p \r q :Prop

-- if p : Prop , t1 t2:p 则 t1 t2是相等的
-- (fun x => t) s and t[s/x] as definitionally equal这个后者直接写这样会报错，所以不理解

Working with Propositions as Types

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
/-
    -- 'theorem' command is really a version of 'def' command 对于类型检查器没有任何区别 Lean tags proof as irreducible 不可归约？， which serves as a hint to the parser（elaborator）that is generally no need to unfold them when processing a file.为何不需要展开?
    -- Lean 并行处理证明和进程，因为proof的 irrelevance，一个proof 的正确性无需另一个定理的细节
-/

-- #print theorem_name -- show you the proof of a theorem

-- 显示指明临时假设的类型 #show
variable {p : Prop}
variable {q : Prop}
theorem t1 : p \r q \r p :=
    fun hp : p =>
    fun hq : q =>
    show p from hp -- 原先只写 hp 就可以

axiom hp : p -- 等价于声明 p is true, as witnessed by hp

the axiom declaration postulates假设 the existence of an element of the given type and may compromise影响 logical consistency.

Propositional Logic

The order of operations is as follows:
not > and > or > \imp > \iff其中\imp（\r）右结合
连接词的定义在库 Prelude.core中

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
-- example command states a theorem without naming it or storing it in the permanent context,只是检查了term的类型

--  Curry-Howard isomorphism同构：and 和 prod是一种同构
-- 当相关类型是推纳类型且可以从context中推断出来，就可以使用Lean的匿名构造符号 \langle \rlangle 或者 \< \>
#check (⟨hp, hq⟩ : p ∧ q)

-- e.bar 是 Foo.bar.e 的缩写，不需要打开一个namespase
variable (ls : List Nat)
#check ls.length
#check List.length ls 

-- for auto construction \< \>
example (h : p \and q): q \and p \and q := \< h.right, h \>
-- 或者 \< h.right , \< h.left, h.right\>\>
-- 或者 And.intro h.right h -- h.left = And.left
-- Or.elim (h :p \or q) (left :p \r c) (right :q \r c) :c简写 h.elim (left) (right)

-- or 有两个构造器constructors，so 不能匿名构造，但仍然可以简写
-- 什么是constructors？？？
1
2
3
-- ex falso sequitur quodlibet False \r c从错误中能推出任意事实
example (hp : p) (hnp : \neg p) : q := Flase.elim (hnp hp) -- absurd hp hnp

Introfucing Auxilisry Subgoals

1
2
3
4
5
6
7
8
9
-- have (h : p) := s;t 和 (fun (h : p) =>t) s 是一样的；s是p的证明，t是(h:p)期望假设的证明

/-
    suffices to show： resoning backwards from a goal
-/
    example (h : p∧ q) : q ∧ p :=
  have hp : p := h.left
  suffices hq:q from And.intro hq hp -- leave us with two goals,1 . by proving the original goal of q \and p with additional hypothesis hq : q, 2. have to show q
  show q from And.right h

Classical Logic

namespace Classical 中是典型逻辑，添加了excluded middle

1
2
3
4
5
6
7
8
open Classical
variable (p : Prop)
#check em p -- p ∨ ¬ p

-- 反证法形式化
#check byContradiction -- (\neg p -> False) -> p
-- 通过案例
#check byCases -- (p -> q) (\neg p -> q) -> q

Quantifiers And Equality

The Universal Quantifier

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
-- x : \a ,p x 表示 p that holds of x
-- 任意 x : \a, p x 

/-
introduction:

Given a proof of p x, in a context where x : α is arbitrary, we obtain a proof ∀ x : α, p x.

Given a term t of type β x, in a context where x : α is arbitrary, we have (fun x : α => t) : (x : α) → β x.

elimination:

Given a proof ∀ x : α, p x and any term t : α, we obtain a proof of p t.

Given a term s : (x : α) → β x and any term t : α, we have s t : β t.
-/

the expressions which differ up to renaming of bound variables are considered to be equivalent

1
2
3
4
5
-- 可以都用x来表示
example (α : Type)(p q : α → Prop): (∀ x : α , p x ∧ q x) → ∀ x : α , p x :=
  fun (h :∀ x : α , p x ∧ q x) =>
  (fun (z : α ) =>  -- 在此处重命名了变量
  show p z from (h z).left)

It is the typing rule for dependent arrow types, and the universal quantifier in particular, that distinguished Prop from other types.依赖箭头的类型是箭头两边的最大类型，如果箭头右边是 Sort 0类型，则依赖箭头类型就是Sort 0

Suppose we have α : Sort i and β : Sort j, where the expression β may depend on a variable x : α. Then (x : α) → β is an element of Sort (imax i j), where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.
Prop as the type of proposition rather than data,and it is what makes Prop impredicative
类型的幂： Notice that if α is any type, we can form the type α → Prop of all predicates on α （the “power type of α”）

Equality

rfl is the notation for (Eq.refl _) 将显示参数变成了隐式参数

1
2
3
4
5
6
7
8
9
10
11
12
13
example : 2+3 = 5 := rfl -- Eq.refl _

-- Eq.subst h1 h2 {motive : \a -> Prop }(h1 : a = b) (h2 :motive a): motive b可以用 h1 \t h2代替,Eq.subst 推断 \a -> Prop 需要instanse of higher-order unification，但这个问题是不可决定的（为什么？），有时会失败，\t 更有效

#check congrArg  --congrArg.{u, v} {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : a₁ = a₂) : f a₁ = f a₂
#check congrFun --congrFun.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) : f a = g a
#check congr --congr.{u, v} {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : α} (h₁ : f₁ = f₂) (h₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂

-- 乘法分配率
    -- 左结合
#check Nat.mul_add
#check Nat.left_distrib -- a *(b+c) = a*b +a*c
    -- 右结合 省略

Calculational Proof

1
2
3
4
5
6
7
8
9
10
11
12
13
/-
calc 
    <expr>_0 'op_1' <expr>_1 ':=' <proof>_1
    --expr<>_0可以单独一行，下面用'_'
    /-
    <expr>_0 
    '_'      'op_1' <expr>_1 ':=' <proof>_1
    -/
    '_'      'op_2' <expr>_2 ':=' <proof>_2
    ...
    '_'      'op_n' <expr>_n ':=' <proof>_n
-- each <proof>_i is a proof for <expr>_{i-1} op_i <expr>_i
-/
1
2
3
4
5
6
7
8
9
/-
`rw` tactics: 重写目标

use a given equality (which can be a hypothesis, a theorem name, or a complex term) to "rewrite" the goal. If doing so reduces the goal to an identity `t = t` ,the tatic applies reflexivity to prove it

`simp` tactics:更机智的重写目标,自动选择和重复的重写

rewrites the goal by applying the given identities repeatedly, in any order, anywhere they are applicable in a term. it also uses other rules that have been previously declared to the system, and applies commutativity wisely to avoid looping. 
-/
1
--`存在Exists.intro` : Existential introduction. If a : α and h : p a, then ⟨a, h⟩ is a proof that ∃ x : α, p x

The Existential Quantifier

the library includes both an introduction rule and an elimination rule
对于introduction rule : to prove Exists x : \a, p x, need suitable term t and a proof of p t
只需要显示提供任意一个可取的值，以及该值下成立的假设即可，

1
2
3
4
5
6
7
8
9
-- set_option pp.explicit true 后使用#print 可以display implicit argument
/-
-- Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p
-- implicit argument {p : α → Prop}意味着Lean能自动推出原命题，但是根据提供的值可以有很多假设：Lean use the context to infer which one is appropriate
example : ∃ x : Nat, x > 0 :=
  have h : 1 > 0 := Nat.zero_lt_succ 0
    Exists.intro 1 h
    -- ⟨1, h⟩
-/
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
/-
-- Exists.elim.{u} {α : Sort u} {p : α → Prop} {b : Prop}(h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b
-/
variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  Exists.elim h
    (fun w =>
     fun hw : p w ∧ q w =>
     show ∃ x, q x ∧ p x from ⟨w, hw.right, hw.left⟩)
/-`match .\a -> prop.. with | ...` :拆分组件(组件自命名，可拆的数目多种多样自助)
    the `match` statement destructs the exstential assertion into the components `w` and `hw`, which can be then used in the body of the statement to prove the proposition.
-/
variable (α : Type) (p q : α → Prop)

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩

--
variable (α : Type) (p q : α → Prop)
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hpw, hqw⟩ => ⟨w, hqw, hpw⟩
  -- | ...=> ...
/- `let` : pattern-matching ,similar to `match h with | <> => <>`-/
example {α : Type}{p q : α → Prop} (h : ∃ x ,p x ∧ q x ): ∃ x , q x ∧ p x:=
  let ⟨ w, hpw, hqw⟩:= h
  ⟨ w,hqw,hpw⟩

更多证明语言

this 代表上一个have匿名

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
variable (f : Nat → Nat)
variable (h : ∀ x : Nat, f x ≤ f (x + 1))
example : f 0 ≤ f 3 :=
  have : f 0 ≤ f 1 := h 0
  have : f 0 ≤ f 2 := Nat.le_trans this (h 1) -- this : f 0 ≤ f 1
  show f 0 ≤ f 3 from Nat.le_trans (by assumption) (h 2) -- (by assumption)如果目标可以inferred，就用assumption代
  
  -- by assumption的替代品那你，显示指出goal，notation "‹" p "›" => show p by assumption --`\f< \f>`

example : f 0 ≥ f 1 → f 1 ≥ f 2 → f 0 = f 2 :=
   fun p :(f 0 ≥ f 1) =>
    fun _ :(f 1 ≥ f 2) => -- 这个placeholder
    have :  f 0 ≥ f 2 :=
      Nat.le_trans ‹f 1 ≥ f 2 › ‹f 0 ≥ f 1 ›
    have :f 0 ≤ f 2 :=
      Nat.le_trans (h 0 ) (h 1)

    Nat.le_antisymm this ‹f 0 ≥ f 2 ›

Tactics

by tactics

Entering Tactic Mode

1
2
3
4
/-
`exact` is a variant of `apply` ,which signals that the expression given should fill the goal exactly.

-/

tatics 可能会产生多个子目标，并且tag them,可以在窗口中看到

1
2
3
4
5
6
7
8
9
10
11
12
-- In the case of `apply` tactic, the tags are inferred from the parameters' names used in the And.intro declaration. 

-- can structure your tatics using the notation `case <tag> => <tatics>`,我认为这样可以改变解决默认的解决顺序
    -- 也可以\. 结构化证明过程
-- And.intro {a b : Prop} (left : a) (right : b) : a ∧ b
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  case right =>
    apply And.intro
    case left => exact hq
    case right => exact hp
  case left => exact hp

Basic Tactics

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
/-
tactic `intro` : introduces a hypothesis, a variable of any type, is a command for constructing function abstraction interactively  (i.e., terms of the form fun x => e) 也可以像`match`一样提供多个参数,也可已使用`intros`
intro 
| \<\> => ...
| \<\> => ...

也可以不提供任何参数：in which case, it chooses names and introduces as many variables as it can.结果是Lean自动生成名字(不能访问)，可以通过  use the combinator `unhygienic` to disable this restriction.

-/
example : ∀ a b c : Nat, a = b → a = c → c = b := by
  intros -- 相当于跟着a✝² b✝ c✝ a✝¹ a✝ 
  rename_i a b c h1 h2
  apply Eq.trans
  apply Eq.symm
  assumption
  assumption

example : ∀ a b c : Nat, a = b → a = c → c = b := by unhygienic
  intros -- 相当于跟着 a b c a_1 a_2
  apply Eq.trans
  apply Eq.symm
  exact a_2
  exact a_1
/-
tactic `rename_i `:`rename_i x_1 ... x_n` :
renames the last n inaccessible names using the given names.
-/

/-
tactic `assumption` : 
looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.
-/

/-
The `rfl` tactic is syntactic sugar for `exact rfl`
-/

/-
The `revert` tactic is an reverse to `intro`, 把假设转为目标
-/

/-`generalize` tactic replace an arbitrary expression in the goal by a fresh variable: 将目标中的任意表达式替换成新变量 `generalize [h :]expre = variable`,但替换可能会导致goal不可证明-/
example : 2 + 3 = 5 :=by
  generalize h : 3 = x -- goal: 2 + x = 5
  rw[← h] -- 2 +3 = 5已经证明完毕了

/-`admit` :tactic
 is the analogue相似 of the `sorry` tactics-/

/-`cases` : 
decompose any element of an inductively defined type,子目标解决顺序任意；对于子目标使用相同策略的证明有用，和`match`的语法类似 cases h(具有多个可能值) with ,我认为区别在于match需要用函数构造，而cases直接使用tag作为函数名了
其中h的选择：可以是某个定理名（来自库或文件），也可以是某个变量表达式
-/
| <tag1> => <tactics1> -- tag是Lean在声明中的参数名
| <tag2> => <tactics2>
-/
  -- cases h(有多种可能) with
  -- | inl hp => apply Or.inr hp -- inl是tag，hp是参数（根据此情况需要传入的参数）
  -- | inr hq => apply Or.inl; exact hq
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  cases h with
  | intro left right => apply And.intro right left

example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => apply And.intro right left


-- 使用相同策略
example (p : Prop): p ∨ p → p := by
  intro h
  cases h
  repeat assumption

/-combinator `tac1 <;> tac2` ： 
<;> operator provides a parallel version of the sequencing operation: tac1 is applied to the current goal, and then apply the tactic `tac2` to each subgoal produced by tactic `tac1`
-/
example (p : Prop) : p ∨ p → p := by
  intro h
  cases h <;> assumption

/-`constructor`: apply the first applicable constructor of an inductively defined type

-/
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => constructor; exact right; exact left -- constructor
example (p q : Prop) : p ∧ q → q ∧ p := by
  intros h
  match h with
  | And.intro left right => constructor<;> assumption -- tac1 <;> tac2

-- case and constructor
example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := by
  intros h
  cases h with
  | intro w hpw => constructor ; apply Or.inl; exact hpw

/-`contradiction`:
contradiction closes the main goal if its hypotheses are "trivially contradictory".
example (h : False) : q := by
  contradiction
-/

-- “combine” `intro h` with `match h ...`
example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := by
  apply Iff.intro
  . intro h
    match h with
    -- 可以推断出来
    | And.intro _ (Or.inl _) => apply Or.inl (⟨by assumption ,by assumption⟩ ) -- 自动推断 by assumption
    | And.intro hp (Or.inr hr) => apply Or.inr (⟨hp ,hr⟩ )
  . intro -- intro 和match 合二为一了
    | Or.inl ⟨hp, hq⟩ => constructor; exact hp; apply Or.inl; exact hq
    | Or.inr ⟨hp, hr⟩ => constructor; exact hp; apply Or.inr; exact hr

Structuring Tactic Proofs

apply and exact 可以传入任意term,e.g. (using have show这两个属于 term-style的term…) can invoke tactic mode by inserting a by block,也有show 的tactic

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := 
  by intro h
  by exact
    have hp : p := h.left
    have hqr : q ∨ r := h.right
    show (p ∧ q) ∨ (p ∧ r) by -- 此处是show .. by 是term-style
      cases hqr with
      | inl hq => exact Or.inl ⟨hp, hq⟩
      | inr hr => exact Or.inr ⟨hp, hr⟩

/-`show` tactic:
declares the type of the goal that is about to be solved,while remaining in tactic mode
`show t` finds the first goal whose target unifies with t. It makes that the main goal, performs the unification, and replaces the target with the unified version of t.重写目标为定义上相等的东西
-/
example (n : Nat) : n + 1 = Nat.succ n := by
  show Nat.succ n = Nat.succ n
  rfl

/-`have` tactic:
intoduces a new subgoal,
have name_label : xxx := ... 
1. can omit the label in the `have` tactic, in which case, the default label `this` is used
2. can omit types in the `have` tactic 
-/ 
example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
  intro ⟨hp, hqr⟩
  show (p ∧ q) ∨ (p ∧ r)
  cases hqr with
  | inl hq =>
    have hpq: p ∧ q := And.intro hp hq-- 定义label
    apply Or.inl
    exact hpq
  | inr hr =>
    have : p ∧ r := And.intro hp hr -- 省略label
    apply Or.inr
    exact this

/-`let` tactic:
introduce local definitions
the difference between `let` and `have` is that `let` introduces a local definition in the contextt, so that the definition of the local declaration can be unfolded in the proof.
-- let a : Nat := 3 * 2 -- 类型可以省略
-/

/- notation`.` : 
空格敏感，依赖于对齐来检测whether the tactic block ends.

不用`.` 也可以使用{} 和 ; 来确定block
-/

看起来有结构的方式: . case label => {}

1
2
3
4
5
6
7
8
9
10
11
12
/-
apply foo
  . <proof of first goal>
  . <proof of second goal>
  
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
 
  { <proof of first goal>  }
  { <proof of second goal> }
  
-/

Tactic Combinators( are operations that form new tactics from old ones)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
/-
The `first | t₁ | t₂ | ... | tₙ` applies each `tᵢ` until one succeeds, or else fails

`skip` tactic does nothing and succeeds

-/
example (p q : Prop) (hp : p) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

example (p q : Prop) (hq : q) : p ∨ q := by
  first | apply Or.inl; assumption | apply Or.inr; assumption

/-
`try` tac runs tac and succeeds even if tac failed.
!! `repeat (try tac)` will loop forver,because `try tac` will always succeed
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  -- 第一个constructor 将goal 变为 case left : p 和 case right : q ∧ r
  -- 第二个constructor只在case right 才会执行
  constructor <;> (try constructor) <;> assumption
end

/-`all_goals tac` : 
applies tac to all open goals
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  all_goals (try constructor)
  all_goals assumption

/-`any_goals tac`:
与`all_goal`类似，except it succeeds if its argument succeed on at least one goal
 -/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
  repeat any_goals constructor
  all_goals assumption
  -- repeat (first | constructor | assumption )

/-`focus t `combinator ensures that `t` only effects the current goal,temporarily hiding the others from the scope.So, if t ordinarily only effects the current goal, focus (all_goals t) has the same effect as t. 
-/
example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor
  case right => constructor ; all_goals assumption
  case left => focus (all_goals apply hp) -- 等价于 focus (apply hp)

Rewriting

1
2
3
4
/-`rewrite [t]`: t is a term whose type asserts an equality.
1. 有多个可以替换时默认选择第一个进行替换
2. noatation `rw [t] at h` : 在h中rw
-/

Using the Simplifier

A number of identities in Lean’s library have been tagged with the [simp] attribute, and the simp tactic uses them to iteratively rewrite subterms in an expression.也可以使用at h指定在h中应用
simp 对于交换和结合顺序的解释:the simplifier uses these two facts to rewrite an expression, as well as left commutativity. 对于local modifier告诉simplifier使用右结合， It may seem that commutativity and left-commutativity are problematic, in that repeated application of either causes looping。But the simplifier detects identities that permute their arguments, and uses a technique known as ordered rewriting.
也许是最后的goal会变成右结合，但simp会报错made no progress

1
2
3
4
-- 例子
example (w x y z : Nat) (p : Nat → Prop)
        : x * y + (z * w) * x = x * w * z + y * x := by
  simp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
/-`simp`
1. do propositional rewriting. using hypothesis p, it rewrites p ∧ q to q and p ∨ q to true
2. 对于新的定义，也可以使用simp，可以在定义时标注 @[simp] （表示定理具有 [simp] 属性； 第二种方式是拉出来写 `attribute [simp] theorem_name`）就可以在使用`simp`时不显式指明定理
-/

example (p q : Prop) (hp : p) : p ∧ q ↔ q := by
  simp [*] -- 重写：p ∧ q = q
example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
  simp -- 使用了带有simp属性的等式

example (x y z : Nat) (p : Nat → Prop) (h : p (x * y))
        : p ((x + 0) * (0 + y * 1 + z * 0)) := by
  simp at *; assumption


def mk_symm (xs : List α) :=
 xs ++ xs.reverse
theorem reverse_mk_symm (xs : List α)
        : (mk_symm xs).reverse = mk_symm xs := by
  simp [mk_symm]

example (xs ys : List Nat)
        : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
  simp [reverse_mk_symm]

attribute [simp] reverse_mk_symm -- 这个属性一直存在(只要导入了含有属性声明的文件，约束属性作用域的办法： using the `local` modifier)
-- attribute [local simp] reverse_mk_symm -- 局部属性，outside the section, the simplifier will no longer use this theorem by default

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p (mk_symm ys ++ xs.reverse) := by
  simp at h; assumption


/-“wildcard 通配符” *：
 代表所有的hypotheses and the goal
 e.g. simp [*]
 -/

Split Tactic

The split tactic is useful for breaking nested if-then-else and match expressions in cases. For a match expression with n cases, the split tactic generates at most n subgoals.
拆分多种subgoal和match差不多

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
/-`simp_arith`:
 is shorthand for simp with arith := true and decide := true. This enables the use of normalization by linear arithmetic.
-/
section
def f (x y z: Nat): Nat :=
  match x , y ,z with
  | 0, _, _ => y
  | _, 0, _ => z
  | _, _, 0 => x
  | _, _, _ => 1
example (x y z : Nat) : x ≠ 0 → y ≠ 0 → z ≠ 0 → z = w → f x y w = 1 := by
  intros -- f x y w = 1
  simp [f]    /-(match x, y, w with
              | 0, x, x_1 => y
              | x, 0, x_1 => w
              | x_1, x_2, 0 => x
              | x, x_1, x_2 => 1) =
              1-/
  split ;repeat (first | contradiction| rfl)

  -- split <;> first | contradiction | rfl

  -- split
  -- case h_1 => contradiction
  -- case h_2 => contradiction
  -- case h_3 => contradiction
  -- case h_4 => rfl
end

by default, simp include all theorems that have been marked with the attribute [simp].
Writing simp only excludes these defaults, allowing you to use a more explicitly crafted list of rules. In the examples below, the minus sign and only are used to block the application of reverse_mk_symm.

1
2
3
4
5
6
7
8
9
example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp [-reverse_mk_symm] at h; assumption -- -负号

example (xs ys : List Nat) (p : List Nat → Prop)
        (h : p (xs ++ mk_symm ys).reverse)
        : p ((mk_symm ys).reverse ++ xs.reverse) := by
  simp only [List.reverse_append] at h; assumption -- only的应用
1
2
3
4
5
6
7
8
9
10
/-`simp` tactic 的useful configuration options:
{contextual := true, arith := true, decide := true, ...}
-/
-- 用x= 0 化简  y + x = y ，用x ≠ 0 化简 x ≠ 0
example : if x = 0 then y + x = y else x ≠ 0 := by
  simp (config := { contextual := true })

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
  simp_arith -- is a shorthand for `simp (config := {arith := true})`

Extensible Tactics

command syntax to define new tactics
command macro_rules to specify what should be done when the new tactic is used.
You can provide different expansions, and the tactic interpreter will try all of them until one succeeds.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
--define a new tactic `my_tac`
syntax "my_tac" : tactic
macro_rules
  | `(tactic| my_tac)=> `(tactic| assumption)
example (h : p) : p := by
  my_tac

-- extend `my_tac`
macro_rules
  | `(tactic| my_tac) => `(tactic|  rfl)

example (x : α ): x = x:=by my_tac

-- extend `my_tac`
macro_rules
  | `(tactic | my_tac) => `(tactic| apply And.intro <;>my_tac )
example (x : α) (h : p) : x = x ∧ p := by
  my_tac

Interacting with Lean

Although the names of theorems and definitions have to be unique, the aliases that identify them do not._root_ is an explicit description of the empty prefix.

protected keyword用在定义时，可以禁止更短的别名（必须使用嵌套的全名）

1
2
3
4
5
6
7
8
9
10
11
12
13
14
-- `open` 后面可以加括号指明至对于括号里面的打开命名空间,也就是可以直接使用括号里面的短别名
open Nat (succ zero gcd)
#check zero
#check add -- error
#check Nat.add --对的

-- 让Nat.mul的别名为times, Nat.plus的别名为plus
open Nat renaming mul → times, add → plus
#eval plus (times 2 2) 3  -- 7

/-`exprot`:
在当前namespace中创建短别名，如果export在一个命名空间外使用，则创建的别名是the top level
-/
export Nat (succ zero gcd)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
/-`instance`command:
assiggn the notation 小于等于 to some relation
-/
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
  ∃ t, l₁ ++ t = l₂

instance : LE (List α) where
  le := isPrefix
-- 变成局部
/-
def instLe : LE (List α) :=
  { le := isPrefix }

section
attribute [local instance] instLe

example (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

end
-/
theorem List.isPrefix_self (as : List α) : as ≤ as :=
  ⟨[], by simp⟩

More on Implicit Arguments

1
2
3
4
/-annotion : 
`{}` 
`\{{ and \}}` : weaker than `{}`,表示一个占位符应该只被添加在下一个显示参数之前
-/

Notation and Precedence

语法扩展命令

1
2
3
4
/-introduing new `prefix` `infix` `postfix` operators-/
infixl :  65 "+" => HAdd.hAdd -- 65 is the precedence level
-- initial_command_name(describing the operator kind) : parsing precedence(natural number) : "a_token" => a_fuction(the operator should be translated to )
-- 其中`precedence` 代表how "tightly" an operator binds to its arguments,encoding the order of operations(1024优先级可以简写为`max`)
1
2
3
/-`notation`:
接受一系列的tokens和命名的term placeholders with precedences
-/

(剩下的不懂)

Coercions

强制转换,也有自动检测和插入强制转换的机制

1
2
3
4
variable (m n : Nat)
variable (i j : Int)
#check (m + i) --↑m + i : Int
#check Int.ofNat m -- Int

Displaying Information

1
2
#check @Eq
#print -- (展示type of the symbol and definition of a definition or theorem; 展示indicates that fact, and shows the type of a constant or an axiom)

Setting Options

1
2
3
-- set_option <name> <value>
-- `set_option pp.all true` carries out these settings all at once, whereas `set_option pp.all` false reverts to the previous values.
-- pp.notation :使用defined notation to display output

Using the Library

import 可以传递，But the act of opening a namespace, which provides shorter names, does not carry over. In each file, you need to open the namespaces you wish to use.
标准库1
Lean4标准库2

Auto Bound Implicit Arguments

Lean4 的新特性: 对于是single lower case or greek letter的未绑定标识符，Lean会自动绑定为implicit argument
可以通过set_option autoImplicit false禁止此特性

1
2
3
4
5
6
7
-- Sort 类型比Type更general
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

#check @compose
-- {β : Sort u_1} → {γ : Sort u_2} → {α : Sort u_3} → (β → γ) → (α → β) → α → γ

Implicit Lambdas

在fun 的语法中，也可以使用{} 表示隐式参数,@fun 就必须传入所有（显式和隐式）参数

Sugar for Simple Functions

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
-- 在Lean4中对于中缀操作符：使用 · as a placeholder
#check (· + 1)
-- fun a => a + 1
#check (2 - ·)
-- fun a => 2 - a
#eval [1, 2, 3, 4, 5].foldl (·*·) 1
-- 120

def f (x y z : Nat) :=
  x + y + z

#check (f · 1 ·)
-- fun a b => f a 1 b

#eval [(1, 2), (3, 4), (5, 6)].map (·.1)
-- [1, 3, 5]

-- 需要括号打断· 和 ·
#check (Prod.mk · (· + 1)) --fun x => (x, fun x => x + 1) : ?m.49894 → ?m.49894 × (Nat → Nat)

Named Arguments

命名参数用来不按顺序传参，provide the value for an implicit parameter when lean failed to infer it.
可以使用.. to provide missing explicit arguments as _,前提是这些显示参数是Lean可以自动推断出来

Inductive Types

具体类型(除了universes)和类型构造器(除了dependent arrows)都是inductive types的实例

1
2
3
4
5
6
-- Inductive type is built up from a specified list of constructors
inductive Foo where
  | constructor₁ : ... → Foo
  | constructor₂ : ... → Foo
  ...
  | constructorₙ : ... → Foo

Enumerated Types

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
/-使用match expression定义Weekday的函数-/
inductive Weekday where
 | sunday : Weekday
 | monday : Weekday
 | tuesday : Weekday
 | wednesday : Weekday
 | thursday : Weekday
 | friday : Weekday
 | saturday : Weekday
 deriving Repr -- instruct Lean to generate a function that converts Weekday objects into text.
open Weekday

def numberOfDay (d : Weekday) : Nat :=
  match d with
  | sunday    => 1
  | monday    => 2
  | tuesday   => 3
  | wednesday => 4
  | thursday  => 5
  | friday    => 6
  | saturday  => 7

#eval numberOfDay Weekday.sunday  -- 1
#eval numberOfDay Weekday.monday  -- 2

/-使用match定义函数：-/
namespace Hidden
def and (a b : Bool) : Bool :=
  match a with
  | true  => b
  | false => false
end Hidden

Constructors With Arguments

Remember that the standard library defines notation α × β for Prod α β and (a, b) for Prod.mk a b.

Notice that the product type depends on parameters α β : Type which are arguments to the constructors as well as Prod. Lean detects when these arguments can be inferred from later arguments to a constructor or the return type, and makes them implicit in that case.
Lean 可以自动推断参数类型后使其隐式化

in this section : each constructor relies only on previously specified types.

1
2
3
inductive Prod (α : Type u)(β : Type v)
| mk  (a :α) (b :β)   : Prod α β -- 可以对参数命名
-- mk : α → β → Prod α β

A type, like Prod, that has only one constructor is purely conjunctive ：the constructor simply packs the list of arguments into a single piece of data, essentially a tuple where the type of subsequent arguments can depend on the type of the initial argument. We can also think of such a type as a “record” or a “structure”. In Lean, the keyword structure can be used to define such an inductive type as well as its projections, at the same time.只有一个构造器的纯粹or类型：将参数打包成一个数据，后续参数都依赖于第一个参数, 这样的类型可以看作是record或者structure

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
/-
介绍了
1. inductive type : Prod
2. mk : constructor
3. fst , snd : projections
4. eliminators `rec` `recOn`
-/
structure Prod (α : Type u) (β : Type v) where
  mk :: (fst : α) (snd : β)

structure Color where
  (red : Nat)(green : Nat)(blue : Nat) -- 不用()用换行也行
  deriving Repr

-- dependent Product sugma 
-- Sigma.mk.{u, v} {α : Type u} {β : α → Type v} (fst : α) (snd : β fst) : Sigma β
namespace Hidden
inductive Sigma {α : Type u} (β : α → Type v) where
  | mk : (a : α) → β a → Sigma β
end Hidden


Inductively Defined Propositions

归纳类型定义的类型可以生存在任何类型的universe中，包括Prop

1
2
3
inductive Or (a b: Prop) where
| inl : a -> Or a b 
| inr : b -> Or a b

Roughly speaking, what characterizes inductive types in Prop is that one can only eliminate to other types in Prop. This is consistent with the understanding that if p : Prop, an element hp : p carries no data.

∃ x : α, p is syntactic sugar for Exists (fun x : α => p).

1
2
inductive Exists {α : Type u} (p : α → Prop) where
  | intro (w : α) (hw : p w) : Exists p

The notation {x : α // p x}也表示一个类型 is syntactic sugar for Subtype (fun x : α => p x)表示对所有的x \a，p x都成立. It is modeled after subset notation in set theory: the idea is that {x : α // p x} denotes the collection of elements of α that have property p.

Defining the Natural Numbers

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat
  deriving Repr

def add (a   b : Nat): Nat :=
  match a with
  | Nat.zero => b
  | Nat.succ a' => Nat.succ (add a' b)

-- 归纳证明例子
open Nat
theorem add_comm (m n : Nat) : m + n = n + m :=
  Nat.recOn (motive := fun x => m + x = x + m) n
   (show m + 0 = 0 + m by rw [Nat.zero_add, Nat.add_zero])
   (fun (n : Nat) (ih : m + n = n + m) =>
    show m + succ n = succ n + m from
    calc m + succ n
      _ = succ (m + n) := rfl
      _ = succ (n + m) := by rw [ih]
      _ = succ n + m   := sorry)

-- sorry 处依旧可以用归纳证明 succ n + 0,  succ n + succ m

Other Recursive Data Types

Inductive Types with Parameters

1
2
3
inductive List (α : Type u) where
  | nil : List α
  | cons : α → List α → List α

Inductive Types with Recursion

1

Tactics for Inductive Types

cases (当open Classical, can use the law of the exclude middle for any proposition at all),

1
2
3
-- 排中律Decidable.em
theorem em (p : Prop) [Decidable p] : p ∨ ¬p :=
  byCases Or.inl Or.inr

induction tactic: 用来归纳证明

  1. 证明归纳
  2. 支持 user-defined induction principle with multiple targets
    语法与cases一样，except that the argument can only be a term in the local context,也可以用case 替换 |
    1
    2
    3
    4
    theorem zero_add (n : Nat) : 0 + n = n := by
      induction n with
      | zero => rfl -- case zero => rfl
      | succ n ih => rw [Nat.add_succ, ih]
    1
    2
    3
    /-`funext` tactic:

    -/

Inductive Families

1
2
3
4
5
6
-- 其中...表示一系列的参数类型，叫做`indices`
inductive foo : ... → Sort u where
  | constructor1 : ... → foo ...
  | constructor₂ : ... → foo ...
  ...
  | constructorₙ : ... → foo ...

Axiomatic Details

Mutual and Nested Inductive Types

mutual: 同时定义两个，相互关联

1
2
3
4
5
6
7
8
9
mutual
    inductive Tree (α : Type u) where
      | node : α → TreeList α → Tree α

    inductive TreeList (α : Type u) where
      | nil  : TreeList α
      | cons : Tree α → TreeList α → TreeList α
end

Nested : 使用其他type

1
2
inductive Tree (α : Type u) where
  | mk : α → List (Tree α) → Tree α -- 用List(Tree \a )代替TreeList

Induction and Recursion

Pattern Matching

1
2
3
4
5
6
7
8
9
10
/-`zero` and `succ` notation 具有 [match_pattern] attribute, they can be used in pattern matching
-/
-- def的多cases形式
def sub1 : Nat → Nat
  | zero   => zero
  | succ x => x
-- 不用zero和succ
def sub1' : Nat → Nat
  | 0 => 0
  | x +1 => x

认为模式匹配是多情况定义
Pattern matching works with any inductive type, such as products and option types
fun_name.match_1:看定义

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
-- 一个参数示例
def sub2 : Nat → Nat
  | zero => 0
  | succ zero => 0
  | succ (x + 1)=> x
#check sub2.match_1 -- 这里面写出了sub2的完整定义
#check sub2 -- Nat →  Nat

def sub2' : Nat → Nat :=
  fun x =>
  match x with
  | zero => 0
  | 1 => 0
  | x + 2 => x

-- 两个参数示例
def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m+1, 0   => 1
  | m+1, n+1 => 2
-- 只对一个参数模式匹配
def and : Bool → Bool → Bool
  | true, a=> a
  | false , _ => false -- 这里的_表示wildcard pattern或者匿名变量，并不代表implicit argument

/-出现在`:` 之前的参数不参与pattern matching，Lean also allows parameters to occur after `:`,but it cannot pattern match on them-/
-- α 不参与 pattern matching
def tail1 {α : Type u} : List α → List α
  | []      => []
  | a :: as => as
-- α也没有参与 pattern matching，只对list进行了分割
def tail2 : {α : Type u} → List α → List α
  | α, []      => []
  | α, a :: as => as

Wildcards and Overlapping Patterns

the notion of a wildcard

对于patterns overlap的情况，Lean use the first applicable equation

1
2
3
4
5
6
7
8
9
10
def foo : Nat → Nat → Nat
  | 0,   n   => 0
  | m, 0   => 1
  | m, n => 2

-- `_`作为通配符
def foo : Nat → Nat → Nat
  | 0,   _   => 0-- m n 的值没有用到，可以写成_
  | _, 0   => 1
  | _, _ => default -- default是Inhabited类型的默认值

function programming languages support incomplete patterns.We can simulate the arbitrary value approch using the Inhabited type class.

we will see that Lean can be instructed that suitable base types are inhabited, and can automatically infer that other constructed types are inhabited. On this basis, the standard library provides a default element, default, of any inhabited type.inhabited 类型有默认值，可以传递?

1
2
3
4
5
6
7
/-`Option`: simulate the incomplete patterns.The idea is to return `some a`for the provided patterns, and use `none` for the incomplete cases

-/
def f2 : Nat → Nat → Option Nat
  | 0, _  => some 1
  | _, 0  => some 2
  | _, _  => none     -- the "incomplete" case

Structural Recursion and Induction

  1. structurally recursive definitions
  2. well-founded recursive definitions
  3. mutually recursive definitions
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    -- 模式匹配
    /-
    As we have seen, a `pattern` is either a variable, a constructor applied to other patterns, or an expression that normalizes to something of that form (where the non-constructors are marked with the [match_pattern] attribute). The appearances of constructors prompt case splits, with the arguments to the constructors represented by the given variables.
    `pattern`:
    1. 变量
    2. 构造器
    3. 表达式
    4.  explicit terms in patterns that are needed to make an expression type check，though they do not play a role in pattern matching. These are called "inaccessible patterns" for that reason. 
    -/
    def foo (a : α) : (b : β) → γ
      | [patterns₁] => t₁
      ...
      | [patternsₙ] => tₙ

    In other situations, however, reductions hold only propositionally, which is to say, they are equational theorems that must be applied explicitly. The equation compiler generates such theorems internally. They are not meant to be used directly by the user; rather, the simp tactic is configured to use them when necessary.

1
2
3
4
5
6
7
8
9
10
11
theorem zero_add : ∀ n, add zero n = n
  | zero => rfl
  | succ n => congrArg succ (zero_add n) -- 递归
  -- | succ n => by simp [add, zero_add] 
-- 要证明 add zero (succ n) = succ n  =>
--f :=succ x = x + 1;
-- h:=  add zero n = n 结果 succ (add zero n)  = succ n
-- 另一种写法
theorem zero_add : ∀ n, add zero n = n
  | zero => by simp [add]
  | succ n => by rw[add, zero_add]

与模式匹配的定义一样：parameters to a structural recursion or induction 可能出现在冒号之前Such parameters are simply added to the local context before the definition is processed

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
open Nat
def add (m : Nat) : Nat → Nat
  | zero => m
  | succ n => succ (add m n)

-- 也可以使用match
def add' (m n: Nat) :  Nat :=
  match n with
  | zero => m
  | succ n => succ (add m n)

/-
`let rec`和`where`在`def`中的应用
-/
def fibFast (n : Nat) : Nat :=
  (loop n).2
where
  loop : Nat → Nat × Nat
    | 0   => (0, 1)
    | n+1 => let p := loop n; (p.2, p.1 + p.2)

def fibFast' (n : Nat): Nat:=
  let rec loop : Nat → Nat × Nat
    | 0 => (0,1)
    | n + 1 => let p := loop n; (p.2, p.2 + p.1)
  (loop n).2

/-`below` `brecOn`介绍：
To handle structural recursion, the equation compiler uses course-of-values recursion, using constants below and brecOn that are automatically generated with each inductively defined type
-/
variable (C : Nat → Type u)

#check (@Nat.below C : Nat → Type u)

#reduce @Nat.below C (3 : Nat)-- 存储C 0， C 1， C 2元素的数据结构

-- 下面是值过程递归的例子
#check (@Nat.brecOn C : (n : Nat) → ((n : Nat) → @Nat.below C n → C n) → C n)

The use of course-of-values recursion is one of the techniques the equation compiler uses to justify to the Lean kernel that a function terminates. It does not affect the code generator which compiles recursive functions as other functional programming language compilers. Recall that #eval fib <n> is exponential on . On the other hand, #reduce fib <n> is efficient because it uses the definition sent to the kernel that is based on the brecOn construction.brecOn的实现可能更有效率

– 不懂！ 这里面的::是什么语法

1
2
3
def append : List α → List α → List α
  | [] , bs => bs
  | a :: as , bs => a :: append as bs

Local recursive declarations

let ret定义local recursive

Inaccessible Patterns

use implicit arguments in patterns

Structure and Records

Type Classes