【coq】函数语言设计笔记 01

参考博客： https://www.cnblogs.com/TheFutureIsNow/p/11569756.html

定义一个类型
在coq中，一个变量的类型往往表示为 var_name : var_type，即变量名后面的一个冒号后是变量的类型
Enumerated Types-枚举类型

Inductive type_name : Type :=
constructor 1
constructor 2
...
constructor n.   (*注意最后一个constructor的后面还有一个 . *)

即创建一个名为 type_name 的类型，该类型的变量的取值只能是{constructor 1, …, constructor n}之中的一个。

eg：

Inductive day : Type :=| monday| tuesday| wednesday| thursday| friday| saturday| sunday.

上面语句创建了一个名为 day 的类型，该类型中的变量取值范围为：{monday，tuesday，wednesday，thursday，friday，saturday，sunday}

定义一个函数
有了类型，可以在这个类型上定义一个函数：

Definition func_name (agrv1 : type1, argv2 : type1...) : ret_type :=
match argv1 with
|　case 1 => ret1
|　case 2 => ret2
|　...
end.

创建一个函数名为func_name的函数，其形参分别为argv1，argv2，并且形参的变量类型分别为type1和type2，最后的返回值的类型为ret_type
eg：


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

Compute语句
定义好了函数之后，可以使用关键字Compute 来计算函数的返回值

Compute (next_weekday friday).

计算的结果为：monday : day

Example语句
eg：

Example test_next_weekday:(next_weekday (next_weekday saturday)) = tuesday.

上面的语句会做两件事：
作出一个假设“Saturday后的两个工作日是Tuesday”；
然后赋予这个假设一个名称，以便后面可以继续参考。
在做出了假设之后，可以调用coq来进行验证：
Proof. simpl. reflexivity. Qed.
上面的语句可以简单的理解为：“刚才所做的断言可以通过观察等式两边经过某种简化后得到相同的值来证明。”

New Type From Old
在定义一个新的类型的时候，也可以调用之前定义好了的类型：

Inductive bit : Type :=| B0| B1.
Inductive nybble : Type :=| bits (b0 b1 b2 b3 : bit).
(*上面的语句定义了一个元组类型*)
Check (bits B1 B0 B1 B0).
(* ==> bits B1 B0 B1 B0 : nybble *)

在定义一个函数的时候可以调用其他函数来完成函数的功能，不过在调用其他函数的时候需要注意变量的类型需要与函数声明中的类型保持一致
eg：

Inductive bool: Type :=| true| false.
Definition andb (b1:bool) (b2:bool) : bool:=match b1 with| true=> b2| false=> falseend.
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool:=match b1 with| true=> andb b2 b3| false=> falseend.
Example test_andb31: (andb3 truetruetrue) = true.
Proof. simpl. reflexivity.  Qed.
Example test_andb32: (andb3 falsetruetrue) = false.
Proof. simpl. reflexivity.  Qed.

coq的函数定义是枚举各个可能的case然后定义每个case下的返回值，但有时并不需要枚举所有的case。这种情况下可以用 "_"符号来代替所有除了前面所枚举过的case的其他case。
eg：

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

（*color类型是一个从已经定义好的类型上重新定义的新的类型*）
（*color类型的变量可能的取值有：black, white, primary red, primary green, primary bule*）
Definition isgreen (c: color) : bool:=match c with| primary green => true| _ => falseend.

Check语句
coq中的每个表达式都有相应的类型，用于描述其计算类型。可以使用check命令来调用coq打印一个表达式的类型
eg：

Definition negb (b:bool) : bool:=match b with| true=> false| false=> trueend.
Check true.
(*打印的内容为：true: bool*)
Check (negb true).
(*打印的内容为：negb true: bool*)
Check negb.
(*打印的内容为：negb : bool-> bool*)

定义自然数
几乎前面所定义的所有类型都是通过枚举定义的，这与此处所定义的自然数类型不同。因为并不能通过一个一个的枚举自然数所有可能取的值，所以这里通过两条规则来规约自然数类型的变量：

0是一个自然数，对应的自然数值为0
如果n‘是自然数，那么S n’就是自然数，对应的自然数值为n’+1

Module NatPlayground.
Inductive nat : Type :=| O| S (n : nat).
End NatPlayground.

这样的定义方法中：自然数 0 表示为[O]，1 表示为[S O]，2 表示为[S (S O)]，然后以此类推…
为了构造一个自然数的集合，上面的构造语句相当于定义了下面几个构造规则：
• 函数[O] 和 [S] 是自然数集合[nat]的构造函数 ;
• 表达式[O]是集合 [nat]中的一个元素;
• 如果表达式[n]属于集合[nat], 则表达式 [S n]也属于集合[nat];
• 通过上面个两条规则构造出来的表达式只属于集合[nat].
由于自然数是一种非常普遍的数据类型，所以Coq为解析和打印提供了一点点内置的魔术类型，可以用普通的十进制数字来代替由构造函数[S]和[O]定义的“一元”符号。coq在默认情况下打印十进制数字:
Check (S (S (S (S O)))).
(打印结果为：4: nat)
在这样的自然数定义下可以定义相应的函数：


Definition pred (n : nat) : nat :=match n with| O => O| S n' => n'end.
(** The second branch can be read: "if [n] has the form [S n']forsome [n'], then return [n']."  *)
Definition minustwo (n : nat) : nat :=match n with| O => O| S O => O| S (S n') => n'end.
Compute (minustwo 4).(* ===> 2: nat *)

定义一个递归调用函数
在coq中定义递归调用的函数的语句与定义普通的函数的语句不同：定义递归调用的函数需要使用关键字Fixpoint来定义

Fixpoint func_name (argv1 : type1, argv2:type2...) : ret_type :=
match argv1 with
| case1 => ret1
| case2 => ret2
| ...
end.
eg:

Fixpoint evenb (n:nat) : bool:=match n with| O        => true| S O      => false| S (S n') => evenb n'end.
Fixpoint plus (n : nat) (m : nat) : nat :=match n with| O => m| S n' => S (plus n' m)end.
(** Adding three to two now gives us five, aswe'd expect. *)
Compute (plus 31).
(** The simplification that Coq performs to reach this conclusion canbe visualized asfollows: *)
(*  [plus (S (S (S O))) (S (S O))]
==> [S (plus (S (S O)) (S (S O)))]by the second clause of the [match]
==> [S (S (plus (S O) (S (S O))))]by the second clause of the [match]
==> [S (S (S (plus O (S (S O)))))]by the second clause of the [match]
==> [S (S (S (S (S O))))]by the first clause of the [match]
*)

Notation语句
coq中可以使用Notation来对某些函数进行重命名从而简化运算语句
Notation语句类似于C语言中的 #Define 语句
eg：

Notation "x + y":= (plus x y)(at level 50, left associativity): nat_scope.
Notation "x - y":= (minus x y)(at level 50, left associativity): nat_scope.
Notation "x * y":= (mult x y)(at level 40, left associativity): nat_scope.
Check ((0+ 1) + 1).

在Notation语句中的关键字[level]、[associativity]以及[nat_scope]用于描述Coq解释程序如何处理这些Notation语句。
其中[level]数值越低，则运算的优先级越高；[associativity]解释该运算操作是左结合还是右结合。
Notation语句并不会改变运算操作的定义，coq解释程序会使用 [plus x y] 来代替[x+y]

定义递归函数时的复杂case
在定义函数的时候可以在一个变量里的case里面讨论另一个变量的case，如下，定义一个自然数小于或等于的函数：


Fixpoint leb (n m : nat) : bool:=match n with| O => true| S n' =>      match m with| O => false| S m' => leb n'm'endend.
Example test_leb1:             (leb 22) = true.
Proof. simpl. reflexivity.  Qed.
Example test_leb2:             (leb 24) = true.
Proof. simpl. reflexivity.  Qed.
Example test_leb3:             (leb 42) = false.
Proof. simpl. reflexivity.  Qed.

定义递归函数的时候需要注意，case 的左边的参数一定要严格的大于右边的参数：

(*Fibonacc series*)
(*wrong definition!*）
Fixpoint fibonacc (n:nat) : nat :=match n with| S(S n') => plus (fibonacc n') (fibonacc (S n')) | _ => (S O)end.
(*
error message:
fibonacc : nat -> nat
n : nat
n0 : nat
n' : natRecursive call to fibonacc has principal argument equal to "S n'" instead of
one of the following variables: "n0""n'".
*)
(*correct definition*)
Fixpoint fibonacc (n:nat) : nat :=match n with| O => 1| S n' =>match n' with| O => 1| S n''=> plus (fibonacc n') (fibonacc n'')    endend.
Example test_fibonacc1: (fibonacc 2) = 2.
Proof. simpl. reflexivity.  Qed.
Example test_fibonacc2: (fibonacc 5) = 8.
Proof. simpl. reflexivity.  Qed.

【coq】函数语言设计笔记 01 - basics相关推荐

c语言软件的思想,C语言设计思想01
C语言设计思想01 为什么只有设计师才能发明流行的新语言先回顾一下知名编程语言的作者和创造时间: Fortran 语言,50年代,IBM 研究员: Lisp 语言,50年代,MIT 的教授和学生: ...
【历史上的今天】6 月 5 日：洛夫莱斯和巴贝奇相遇；公钥密码学先驱诞生；函数语言设计先驱出生
整理 | 王启隆透过「历史上的今天」,从过去看未来,从现在亦可以改变未来. 今天是 2022 年 6 月 5 日,世界环境日.1972 年 6 月 5 日至 16 日,联合国人类环境会议在斯德哥尔摩 ...
[C++程序语言设计笔记一]面向对象编程抽象，继承，重写基本介绍
今天是个不错的日子,不仅有人收了我做徒弟从此传授我有关C++的一些知识,由于前一段时间喜欢上了外挂的研究也用到了一些MFC的知识及一些Windows APIs编程,但是对C++还是没有从根本上认识.我 ...
C语言学习笔记01：C语言基础语法_变量类型_类型转换
文章目录 C语言第一天课程笔记 1. 内容安排 2. 课堂笔记 2.1 计算机硬件 2.2 计算机软件 2.3 编程语言和编译器 2.4 编程语言发展 2.5 C语言标准 2.6 C语言学习理由 2. ...
独立式环境与宿主式环境————《标准C语言指南》读书笔记01
独立式环境与宿主式环境----<标准C语言指南>读书笔记01 在编写和转换一个C程序之前,需要考虑它的执行环境,因为这关系到源文件的内容(程序应当如何编写),也关系到转换后的程序能否正常执 ...
r语言c函数怎么用,R语言学习笔记——C#中如何使用R语言setwd()函数
在R语言编译器中,设置当前工作文件夹可以用setwd()函数. > setwd("e://桌面//") > setwd("e:\桌面\") > ...
c语言中如何用sqar函数,简易函数信号发生器设计_毕业论文.doc
简易函数信号发生器设计 PAGE PAGE 2 简易函数信号发生器设计摘要:信号发生器又称信号源或振荡器,在生产实践和科技领域中有着广泛的应用.这次的设计分为五个模块:单片机控制及显示模块.数模转换 ...
R语言与函数估计学习笔记（函数模型的参数估计）
R语言与函数估计学习笔记毫无疑问,函数估计是一个比参数估计要复杂得多的问题,当然也是一个有趣的多的问题.这个问题在模型未知的实验设计的建模中十分的常见,也是我正在学习的内容的一部分. 关于函数估计我 ...
C 语言的可变参数表函数的设计
首先在介绍可变参数表函数的设计之前,我们先来介绍一下最经典的可变参数表printf函数的实现原理. 一.printf函数的实现原理在C/C++中,对函数参数的扫描是从后向前的.C/C++的函数参数是 ...
c语言中void arrout,c语言学习笔记(数组、函数
<c语言学习笔记(数组.函数>由会员分享,可在线阅读,更多相关<c语言学习笔记(数组.函数(53页珍藏版)>请在人人文库网上搜索. 1.数组2010-3-29 22:40一维数 ...

【coq】函数语言设计笔记 01 - basics

【coq】函数语言设计笔记 01 - basics相关推荐

最新文章

热门文章

【coq】函数语言设计 笔记 01 - basics

【coq】函数语言设计 笔记 01 - basics相关推荐

最新文章

热门文章

【coq】函数语言设计笔记 01 - basics

【coq】函数语言设计笔记 01 - basics相关推荐