Coq学习笔记（一）

BASICS
- 函数编程
- 枚举类型
- - 引例：Days of the week（定义一个类型）
- 一些基础语法定义
- - Type
  - Check命令
  - 多元组
  - Modules
  - Compute命令
  - 定义一个新常量
BOOLEANS
- 布尔表达式的构造
- - 相关定义
  - 布尔表达式的相关运算律
  - 用Example检查计算结果是否符合预期
课堂实例
- 自然数和链表的递归构造
- - 自然数
  - 链表的构造
参考书目课后题答案

OMG,没学离散数学之前觉得这就是门数学，学了之后被逻辑和编程同时吊打，这里根据一些资料把之前学的coq相关规则回顾一遍，毕竟要准备期末考试复习了，这学期东西又难又是在线上教学，一定要好好加油鸭。（鬼姐姐根本没在怕的）
所用参考书目为《Logic Foundations》

BASICS

函数编程

函数编程强调让我们了解如何将输入映射到输出，同时将函数（方法）作为一级值（类似于数字，集合都属于数学中某一级别的值），也就是将函数作为数据来处理。
函数式编程思想也包括我们在OOP中涉及到的多态，代码重用，但是函数式编程是通过函数将程序模块化。

枚举类型

coq内置特性非常少，并没有像高级语言一样已经定义了常用的数据类型，而是提供了一种强大的机制来从头定义新的数据类型。
当然coq标准库提供了原始的数据类型，但我们这里选择显式地重述定义。

引例：Days of the week（定义一个类型）

defining a new set of data values-a type

Coq < Inductive day:Type:=
Coq < |monday
Coq < |tuesday
Coq < |wednesday
Coq < |thursday
Coq < |friday
Coq < |saturday
Coq < |sunday.
day is defined
day_rect is defined
day_ind is defined
day_rec is defined

coq代码中经常会用数据：类型的格式展现一个数据和其相应的类型
“：=”在coq中表示等于，用"."结束语句
这里定义了一个新的类型，名字是day，有七个成员
用coq定义一个函数对这些数据进行操作

Definition next_weekday (d:day) : day :=match d with| monday => tuesday| tuesday => wednesday| wednesday => thursday| thursday => friday| friday => monday| saturday => monday| sunday => mondayend.

1 定义函数 Definition fun_name (输入）：（返回），注意这里的输入输出依然采用数据名称：数据类型的格式，但是一旦命名的数据名称必须在环境中使用（比如d），对于输入，一般都需要使用一个数据，需要说明数据，但是类型可有可无，对于输出，必须说明其类型（coq可以进行类型判断，但是我们一般会包括他们，使阅读更加容易）
2 在定义每个情况的输出类型时，必须定义所有可能的情况，比如这里需要列举所有星期对应的返回值。
定义好一个函数后，我们使用Compute命令对结果进行查询。

Compute (next_weekday friday).
Compute (next_weekday (next_weekday saturday)).

调用函数的时候和高级语言格式很接近。
执行结果：

一些基础语法定义

Type

每个表达式都有一个类型

New Types from Old
就像前面定义的Days of week一样，我们定义的都是枚举类型的例子

Check命令

确定输入内容的类型

简单的类型

Coq < Check True.
True: PropCoq < Check 3.
3: natCoq < Check 3+2.
3 + 2: nat

有序数对

Coq < Check (2,3=5).
(2, 3 = 5): nat * Prop

函数类型
1 使用关键字fun构造一个新函数，它将替换λlambda微积分（之前的博客有提到）和类似理论的符号。
they are written with arrows.

Coq < Check (fun x:nat=>x=3).
fun x : nat => x = 3: nat -> Prop
Coq < Check (forall x:nat,x<3\/(exists y:nat,x=y+3)).
forall x : nat, x < 3 \/ (exists y : nat, x = y + 3): Prop

2 let的使用（为函数提供一个临时的名字，之前的博客提到过）

Check (let f := fun x => (x * 3,x) in f 3).
let f := fun x : nat => (x * 3, x) in f 3 : nat * nat

3 构造枚举类函数时其成员也可以定义成一个函数（constructor)

Inductive reb:Type :=
|red
|green
|blue.Inductive color :Type:=
|black
|white
|primary (p:reb).
Check primary red.
Check primary blue.

多元组

多个参数的单个构造函数用于创建元组类型
比如我们在用二进制编码时，可以将某一位定义是取值为0或1的函数，那样我们表示一个字节时相当于八位的元组，很像在高级语言中的数组

Inductive bit:Type :=
|B0
|B1.
Inductive byte:Type :=
| bits(b0 b1 b2 b3 b4 b5 b6 b7:bit).
Check (bits B0 B1 B0 B1 B0 B1 B0 B1).

下划线的使用，我们用下划线代替未定义的变量，比如我们要检查定义的字节是否各位为全0

Definition all_zero (input:byte):bool:=
match input with
|(bits B0 B0 B0 B0 B0 B0 B0 B0)=>true
|(bits _ _ _ _ _ _ _ _)=>false
end.
Compute all_zero(bits B1 B1 B1 B1 B1 B1 B1 B1).

Modules

本课程中涉及很少

Compute命令

定义一个新常量

Coq < Definition example:=fun x=>x*x.
example is definedCoq < Compute example 1.= 1: natCoq < Compute example 3.= 9: nat

BOOLEANS

布尔表达式的构造

布尔表达式的相关运算律

用Example检查计算结果是否符合预期

Coq < Example test1: orb true false=false.
test1 < Proof. simpl. reflexivity. Qed.

课堂实例

自然数和链表的递归构造

自然数

自然数的构造
1 自然数的内部表示

Inductive nat:Type:=
|o
|S(n:nat).
(*O和S只是一种表达方式，O是归纳基础，S是构造算子，我们甚至可以这样定义*)
Inductive nat':Type:=
|Lilghost
|darling (d:nat').
Check darling(darling(darling Lilghost)).

递归定义：O是归纳基础，S是构造算子

Coq < Check 1.
1: nat
Coq <  Check S(S(S O)).
3: nat

coq内部用一进制表示自然数（上边那个是O不是0）
我们使用命令

Print nat.

可以输出nat的内部表示

Coq < Print nat.
Inductive nat : Set :=  O : nat | S : nat -> natFor S: Argument scope is [nat_scope]

Unset Printing Notations.
Set Printing Notations.

表示打开其内部表示

Coq < Unset Printing Notations.Coq < Check 3.
S (S (S O)): nat

2 一些关于自然数的函数

前置函数
利用递归函数确定给定自然数是否为偶数

3 定义自然数的加法
加法的定义：取m的n次后继
定义递归函数时用Fixpoint命令

Fixpoint plus n m :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Compute plus 2 3.
Notation "x + y":=(plus x y).
Compute 2+3.

使用Notation能用符号表示函数

练习：使用递归定义自然数乘法，减法
练习答案：

Coq < Fixpoint plus n m:=
Coq < match n with
Coq < |O=>m
Coq < |S n'=>S (plus n' m)
Coq < end.
plus is defined
plus is recursively defined (decreasing on 1st argument)Coq <  Fixpoint mulit n m:=
Coq < match n with
Coq < |1=>m
Coq < |S n'=>plus m (mulit n' m)
Coq < |O=>O
Coq < end.
mulit is defined
mulit is recursively defined (decreasing on 1st argument)Coq < Compute mulit 3 5.= 15: natCoq < Notation "n * m":=(mulit n m).Coq < Compute 3*0.= 0: natCoq < Compute 5*9.= 45: nat

Coq < Fixpoint sub n m :=
Coq < match n,m with
Coq < |O,_=>O
Coq < |_,O=> n
Coq < |S x',S y'=>sub x' y'
Coq < end.
sub is defined
sub is recursively defined (decreasing on 1st argument)Coq < Compute sub 5 2.= 3: nat

递归是函数式编程的基本理念，保证函数的终止性，没有传统过程语言的循环结构

链表的构造

Inductive natlist : Set :=
| nil : natlist
| cons : nat -> natlist -> natlist.Definition l1 := cons 2 (cons 1 nil).(* syntax tree of l1 is: cons |+-----+-----+ |           |2         cons|+---+---+|       |1      nil
*)Definition l2 := cons 3 nil.Compute l1.Notation "[ ]" := nil.
Notation "[ a ; .. ; b ]" := (cons a .. (cons b nil) .. ).Compute l1.Fixpoint plus s t := match s with| [] => t| cons a s' => cons a (plus s' t)end.Compute plus [3] [2;1].Notation "x + y" := (plus x y).Compute l2 + l1.Fixpoint rev s := match s with| [] => []| cons a s' => (rev s') + [a]end.Compute rev (l2 + l1).

练习：计算链表长度，自然数链表元素求和。

Coq < Fixpoint plus n m:=
Coq < match n with
Coq < |O=>m
Coq < |S n'=>S(plus n' m)
Coq < end.
plus is defined
plus is recursively defined (decreasing on 1st argument)Coq < Inductive list:Set:=
Coq < |nil:list
Coq < |cons :nat->list->list.
list is defined
list_rect is defined
list_ind is defined
list_rec is definedCoq <  Definition l1:=cons 2(cons 1(cons 3 nil)).
l1 is definedCoq <  Fixpoint nons s :=
Coq <  match s with
Coq < |nil=>O
Coq < |cons a s'=>plus 1 (nons s')
Coq < end.
nons is defined
nons is recursively defined (decreasing on 1st argument)Coq < Compute nons l1.= 3: natCoq <  Fixpoint sum s :=
Coq < match s with
Coq < |nil=>O
Coq < |cons a s'=>plus a (sum s')
Coq < end.
sum is defined
sum is recursively defined (decreasing on 1st argument)Coq < Compute sum l1.= 6: nat

参考书目课后题答案

EX1：standard (nandb)

Definition negb b:=
match b with
|true=>false
|false=>true
end.Definition nandb (b1:bool) (b2:bool) : bool :=
match b1 with
|false=>true
|true=>negb b2
end.
Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb2: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb3: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_nandb4: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.

EX2： standard (andb3)

Definition andb n m:=
match n with
|true=>m
|false=>false
end.Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1 with
|false=>false
|true=>andb b2 b3
end.
Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.

EX3 standard (factorial)

Fixpoint muti m n:=
match m with
|O=>O
|S m'=>(plus n (muti m' n))
end.Fixpoint factorial (n:nat) : nat:=
match n with
|O=>1
|S n'=>(muti n (factorial n'))
end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.Fixpoint eqb (n m:nat):bool:=
match n with
|O=>match m with |O=>true|S m'=>falseend
|S n'=>match m with|O=>false|S m'=>(eqb n' m')end
end.Compute (eqb 3 5).

Fixpoint eqb (n m:nat):bool:=
match n with
|O=>match m with |O=>true|S m'=>falseend
|S n'=>match m with|O=>false|S m'=>(eqb n' m')end
end.Definition ltb (n m : nat) : bool:=
match (minus n m)with
|O=>(negb(eqb n m))
|_=>false
end.
Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
Example test_ltb1: (ltb 2 2) = false.
Proof. simpl. reflexivity. Qed.
Example test_ltb2: (ltb 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_ltb3: (ltb 4 2) = false.
Proof. simpl. reflexivity. Qed.

终于结束第一部分了，接下来是coq独特的证明功能，本篇代码中间隐藏了数个小彩蛋，鬼姐姐们可以找找噢。

离散数学——coq学习笔记（一）相关推荐

《离散数学》学习笔记
截图来自于https://www.icourse163.org/course/UESTC-1002268006 集合论基础不含任何元素的集合是空集空集是绝对唯一的对于一个具体的范围考虑的所有对 ...
离散数学自考学习笔记
11月30日 12月1日
离散数学学习笔记-Day4
离散数学学习笔记-Day4: 1.集合集合的基数:集合A中的元素个数,记为 |A|. 2.集合中元素的基本特性: 1)集合中元素是无序的 2)集合中元素是不同的 3.包含⊆: 真包含⊂:一个集合是 ...
离散数学学习笔记——集合运算的基本等式
离散数学学习笔记--集合运算的基本等式集合运算的基本等式集合运算的基本等式设 UUU 为全集,A,B,CA, B, CA,B,C 为任意集合. (1) A∪A=A,A∩A=A.A \cup A= ...
计算机专业常用图论,同等学力申硕计算机专业--数学公式集合（新增学习笔记）...
组合数学部分: 基础公式: 定义:从n个不同的元素中, 取r个并按次序排列, 称为从n中取r个的一个排列, 全部这样的排列数记为P(n, r). 定义: 从n个不同的元素中, 取r个但是不考虑次序时候 ...
MATLAB学习笔记2：MATLAB基础知识（下）
阅读前请注意: 1. 该学习笔记是华中师范大学HelloWorld程序设计协会2021年寒假MATLAB培训的学习记录,是基于培训课堂内容的总结归纳.拓展阅读.博客内容由 @K2SO4钾撰写.编辑, ...
LearnOpenGL学习笔记—PBR：IBL
LearnOpenGL学习笔记-PBR:IBL 0 引入 1 渲染方程的求解 2 hdr文件转成cubemap 3 预计算漫反射积分 4 预计算镜面反射积分 4.1 预滤波HDR环境贴图 4.1.1 ...
2021-06-22 离散数学图论复习笔记
离散数学图论复习笔记仅记了自己不太熟悉容易弄混的概念,不懂的可以回到知乎连接查看. 一.图的类型无序对--(a,b),AB之间的线无序积--A&B,AB之间线的集合有序对--<a ...
MySQL学习笔记(三）查询
写在前面:本篇为作者自学总结,学习内容为课堂所学和网络学习笔记汇总,对于内容引用部分在文中和文末注明. 文章仅供参考,如需深入了解,请查阅MySQL参考手册.附上下载链接: 链接:https://pa ...
【人工智能学习笔记】人工智能里的数学——概述
系列文章目录 [人工智能学习笔记]人工智能里的数学--概述 [人工智能里的数学]一元函数微分学 [人工智能里的数学]线性代数基础 [人工智能里的数学]多元函数微分学前言与软件开发相比,人工智能领域 ...

离散数学——coq学习笔记（一）