当前位置: 首页 > news >正文

Software Foundations Vol.I : Coq函数式编程(Basics)

好久没写随笔了,随便投投.这里的内容主要取至《软件基础》第一卷https://coq-zh.github.io/.

我补充了一部分习题的答案,在https://github.com/mesonoxian-yao/softwareFoudations-volume1-coqLearn可以看看.

Software Foundations Vol.I : Coq函数式编程(Basics)


数据与函数

枚举类型

Coq 的一个不同寻常之处在于它'极小'的内建特性集合。 比如,Coq 并未提供通常的原语(atomic)类型(如布尔、整数、字符串等), 而是提供了一种极为强大的,可以从头定义新的数据类型的机制 —— 上面所有常见的类型都是由它定义而产生的实例。

当然,Coq 发行版同时也提供了内容丰富的标准库,其中定义了布尔值、 数值,以及如列表、散列表等许多通用的数据结构。 不过这些库中的定义并没有任何神秘之处,也没有原语(Primitive)的特点。 为了说明这一点,我们并未在本课程中直接使用标准库中的数据类型, 而是在整个教程中重新定义了其中的绝大部分。

下面是一个例子,说明了Coq中如何使用Inductive与Definition:

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

Inductive: 其中,Inductive通过归纳声明了一个Type,类似于如下:

Inductive type_name:Type:=| x1| x2.

Definition: Definition为声明各类函数与关系提供了途径:

Definition func(para:type_name):=match para with| x1=>x2end.

而为了计算函数,下面的例子展示了如何使用Compute代入函数:

Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

Compute: Compute把右侧的参数提供给左侧的函数:

Compute (func x1).

下面的例子为我们揭示了如何使用Example来表示某个猜想,并且通过Proof证明它:

Example test_next_weekday:(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.

布尔值

下面综合上面的语法,为逻辑谓词及布尔值运算相关内容提供了案例.

布尔型类型声明如下:

Inductive bool : Type :=| true| false.

谓词定义如下:

Definition negb (b:bool) : bool :=match b with| true ⇒ false| false ⇒ trueend.
Definition andb (b1:bool) (b2:bool) : bool :=match b1 with| true ⇒ b2| false ⇒ falseend.
Definition orb (b1:bool) (b2:bool) : bool :=match b1 with| true ⇒ true| false ⇒ b2end.

这里需要注意的是,对于coq,有以下语法对应关系:

  • ⇒: =>
  • →: ->
  • ↔: <->
  • ∃: exists
  • ∃!: exists!
  • ∀: forall
  • ∀!: forall!
  • ∧: /\
  • ∨: /
  • ≠: <>
  • ×: *

下面是一些附加的验证:

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.

同时,下面通过Notation指令为既定的定义提供了新的符号记法.

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

Notation: 通过Notation对已有定义进行简化处理.

Notation "- x" := (func x).
Example test_example2 : -x1=x2.
Proof. simpl. reflexivity. Qed.

值得注意的是,在双引号中,能够与变量组合的符号应该是coq内部支持的,而非自己定义.

类型

Coq 中的每个表达式都有类型,它描述了该表达式所计算的东西的类别。 Check 指令会让 Coq 显示一个表达式的类型。

Check true.
(* ===> true : bool *)

如果在被 Check 的表达式后加上一个分号和你想验证的类型,那么 Coq 会 验证该表达式是否属于你提供的类型。当两者不一致时,Coq 会报错并终止执行。

Check true:bool.
Check (negb true):bool.

像 negb 这样的函数本身也是数据值,就像 true 和 false 一样。 它们的类型被称为'函数类型',用带箭头的类型表示。

Check negb:bool->bool.

negb 的类型写作 bool → bool,读做“bool 箭头 bool”, 可以理解为“给定一个 bool 类型的输入,该函数产生一个 bool 类型的输出。” 同样,andb 的类型写作 bool → bool → bool,可以理解为 “给定两个 bool 类型的输入,该函数产生一个 bool 类型的输出。”

由旧类型构造新类型

下面是通过Constructor构造新类型的方式:

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

其中primary为Constructor表达式.

  • 我们从有限的一组'构造子'开始。例如 red、primary、true、false、monday 等等都是构造子。
  • '构造子表达式'通过将构造子应用到一个或多个构造子表达式上构成。例如 red、true、primary、primary red、red primary、red true、 primary (primary primary) 等等
  • 每个 Inductive 定义都刻画了一个构造子表达式的子集并赋予了它们名字,如 bool、rgb 或 color。

具体来说,rgb 和 color 的定义描述了如何构造这两个集合中的构造子表达式:

  • 构造子表达式 red、green 和 blue 属于集合 rgb;
  • 构造子表达式 black 和 white 属于集合 color;
  • 若 p 是属于 rgb 的构造子表达式,则 primary p(读作“构造子 primary 应用于参数 p)是属于集合 color 的构造子表达式;且
  • 通过这些方式构造的构造子表达式'只属于'集合 rgb 和 color。

我们可以像之前的 day 和 bool 那样用模式匹配为 color 定义函数。

Definition monochrome (c : color) : bool :=match c with| black ⇒ true| white ⇒ true| primary p ⇒ falseend.

鉴于 primary 构造子接收一个参数,匹配到 primary 的模式应当带有一个 变量或常量。变量可以取任意名称,如上文所示;常量需有适当的类型,例如:

Definition isred (c : color) : bool :=match c with| black ⇒ false| white ⇒ false| primary red ⇒ true| primary _ ⇒ falseend.

其中_为通配的哑(dummy)变量

元组

一个多参数的单构造子可以用来创建元组类型,下面提供了一个例子,其描述了使用半字节表示四个比特:

Inductive bit : Type :=| B0| B1.
Inductive nybble : Type :=| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0): nybble.

这里的 bit 构造子起到了对它内容的包装作用。 解包可以通过模式匹配来实现

Definition all_zero (nb : nybble) : bool :=match nb with| (bits B0 B0 B0 B0) ⇒ true| (bits _ _ _ _) ⇒ falseend.
Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : bool *)

模块

如果将一组定义放在 Module X 和 End X 标记之间,那么在文件中的 End 之后,我们就可以通过像 X.foo 这样的名字来引用,而不必直接用 foo 了

Module logic_sys.End logic_sys.

Module: 使用Module可以创建模块来管理声明定义:

Module logic_sys.
(*...*)
End logic_sys.Compute (logic_sys.func logic_sys.x1).

数值

枚举集合都是有限的,而一般自然数都是无限的,为了表示自然数,需要用一种更强大的方式声明它们.

为了在 Coq 中表示一进制数,我们使用两个构造子。 大写的 O 构造子用来表示“零”

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

在这种定义下, 0 被表示为 O, 1 则被表示为 S O, 2 则是 S (S O),以此类推

也可以把 O 写为 tick,这些记号的'解释'完全取决于我们如何用它进行计算。

Inductive nat' : Type :=| stop| tick (foo : nat').

编写一个函数来对上述自然数的表示进行模式匹配。 例如,以下为前趋函数

Definition pred (n : nat) : nat :=match n with| O ⇒ O| S n' ⇒ n'end.

第二个分支可以读作:“如果 n 对于某个 n' 的形式为 S n', 那么就返回 n'。”

为了让自然数使用起来更加自然,Coq 内建了一小部分解析打印功能: 普通的十进制数可视为“一进制”自然数的另一种记法,以代替 S 与 O 构造子; 反过来,Coq 也会默认将自然数打印为十进制形式:

Check (S (S (S (S O)))).
(* ===> 4 : nat *)Definition minustwo (n : nat) : nat :=match n with| O ⇒ O| S O ⇒ O| S (S n') ⇒ n'end.Compute (minustwo (S (S (S (S O))))).
(* ===> 2 : nat *)

注意:现在上面描述的内容必须通过Datatypes.nat来实现了.

构造子 S 的类型为 nat → nat,与 pred 和 minustwo 之类的函数相同:

Check S : nat→nat.
Check pred : nat→nat.
Check minustwo : nat→nat.

以上三个对象均可作用于自然数,并产生nat结果,但第一个 S 与后两者有本质区别:pred 和 minustwo 这类函数是通过给定的'计算规则'定义的

简单的模式匹配不足以描述很多有趣的数值运算,我们还需要递归定义。 例如:给定自然数 n,欲判定其是否为偶数,则需递归检查 n-2 是否为偶数。 关键字 Fixpoint 可用于定义此类函数。

Fixpoint evenb (n:nat) : bool :=match n with| O ⇒ true| S O ⇒ false| S (S n') ⇒ evenb n'end.

Fixpoint: 通过Fixpoint,可以在函数中递归地使用函数来声明.

Fixpoint fix_func(para:type_name):type_name:=match para with| x1=>x2| x2=>x1| y x1=>x1| y x2=>x2| y (y n)=>(fix_func n)end.Compute (fix_func (y(y(y(y(x1)))))).
(*logic_sys.x2:logic_sys.type_name*)

我们可以使用类似的 Fixpoint 声明来定义 odd 函数, 不过还有种更简单方式:

Definition oddb (n:nat) : bool :=negb (evenb n).
Example test_oddb1: oddb (S O) = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb (S (S (S (S O)))) = false.
Proof. simpl. reflexivity. Qed.

当然,也可以用递归定义多参函数。

Fixpoint plus (n : nat) (m : nat) : nat :=match n with| O ⇒ m| S n' ⇒ S (plus n' m)end.

三加二等于五,不出意料。

Compute (plus (S (S (S O))) (S (S O))).
(* ===> 5 : nat *)

Coq 所执行的化简步骤如下所示:

(*   plus 3 2
i.e. plus (S (S (S O))) (S (S O))==> S (plus (S (S O)) (S (S O)))(根据第二个 match 子句)==> S (S (plus (S O) (S (S O))))(根据第二个 match 子句)==> S (S (S (plus O (S (S O)))))(根据第二个 match 子句)==> S (S (S (S (S O))))(根据第一个 match 子句)
i.e. 5  *)

为了书写方便,如果两个或更多参数具有相同的类型,那么它们可以写在一起。

在下面的定义中,(n m : nat) 的意思与 (n : nat) (m : nat) 相同。

Fixpoint mult (n m : nat) : nat :=match n with| O ⇒ O| S n' ⇒ plus m (mult n' m)end.Example test_mult1: (mult (S (S (S O))) (S (S (S O)))) = (S (S (S (S (S (S (S (S (S O))))))))).
Proof. simpl. reflexivity. Qed.

你可以在两个表达式之间添加逗号来同时匹配它们:

Fixpoint minus (n m:nat) : nat :=match n, m with| O , _ ⇒ O| S _ , O ⇒ n| S n', S m' ⇒ minus n' m'end.
End NatPlayground2.
Fixpoint exp (base power : nat) : nat :=match power with| O ⇒ S O| S p ⇒ mult base (exp base p)end.

可以通过引入加法、乘法和减法的Notation来让数字表达式更加易读。

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) : nat.

(level、associativity 和 nat_scope 标记控制着 Coq 语法分析器如何处理上述记法。

Coq 几乎不包含任何内置定义,甚至连数值间的相等关系都是由用户来实现。

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'endend.

上面的例子既为我们提供了一个多分支match1的很好的例子,又为我们提供了一个用于说明eq关系的案例

类似地,leb 函数检验其第一个参数是否小于等于第二个参数,以布尔值表示。

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 2 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: leb 2 4 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: leb 4 2 = false.
Proof. simpl. reflexivity. Qed.

提供一种中缀记法:

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.

基于化简的证明

前几节中的每个 Example 都对几个函数在某些特定输入上的行为做出了准确的断言。这些断言的证明方法都一样: 使用 simpl 来化简等式两边,然后用 reflexivity 来检查两边是否具有相同的值。

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.intros n. simpl. reflexivity. Qed.

在前面的例子中,其实并不需要调用 simpl ,因为 reflexivity 在检查等式两边是否相等时会自动做一些化简,simpl 只是为了看到中间状态

在 Coq 中,关键字 Example 和 Theorem(以及 Lemma、Fact 和 Remark等)都表示完全一样的东西。

关键字 intros、simpl 和 reflexivity 都是'策略(Tactic)'的例子。 策略是一条可以用在 Proof(证明)和 Qed(证毕)之间的指令,它告诉 Coq 如何来检验我们所下的一些断言的正确性。

其它类似的定理可通过相同的模式证明。

Theorem plus_1_l : ∀ n:nat, 1 + n = S n.
Proof.intros n. reflexivity. Qed.
Theorem mult_0_l : ∀ n:nat, 0 × n = 0.
Proof.intros n. reflexivity. Qed.

上述定理名称的后缀 _l 读作“在左边”。

基于改写的证明

该定理并未对自然数 n 和 m 所有可能的值做全称断言,而是讨论了仅当 n = m 时这一更加特定情况。箭头符号读作“蕴含”。

Theorem plus_id_example : ∀ n m:nat,n = m →n + n = m + m.

由于n与m都为nat,所以无法通过形式上的简化来证明此定理,因此,观察发现,若将n替换为m或m替换为n,那么就可以证明,这种策略被叫做rewrite.

Proof.(* 将两个量词移到上下文中: *)intros n m.(* 将前提移到上下文中并改写为H *)intros H.(* 用前提改写目标: *)rewrite → H.reflexivity. Qed.

rewrite 中的箭头与蕴含无关:它指示 Coq 从左往右地应用改写。 若要从右往左改写,可以使用 rewrite <-

intros: intros用于将量词,前提引入到上下文中.同时,也可以将形如a->b结构的a拆分出来作为H.

Theorem th1 : forall n:nat,n = n ->n = n.
Proof.intros n.reflexivity.
Qed.

Admitted 指令告诉 Coq 我们想要跳过此定理的证明,而将其作为已知条件, 这在开发较长的证明时很有用。

Admitted: 告诉coq,此处的证明作为已知条件.

Check 命令也可用来检查以前声明的引理和定理。

Check: 用于判断类型,断言,引理,定理等是否正确.

Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)
Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)

除了上下文中现有的假设外,还可以通过 rewrite 策略来运用前期证明过的定理。

如果前期证明的定理的语句中包含量词变量,Coq 会通过匹配当前的证明目标来尝试实例化(Instantiate)它们。

Theorem mult_n_0_m_0 : ∀ n m : nat,(n × 0) + (m × 0) = 0.
Proof.intros n m.rewrite <- mult_n_O.rewrite <- mult_n_O.reflexivity. Qed.

利用分类讨论来证明

并非一切都能通过简单的计算和改写来证明,未知的、假定的值,如数值、布尔值、列表等会阻碍化简。

例如:

Theorem plus_1_neq_0_firsttry : ∀ n : nat,(n + 1) =? 0 = false.
Proof.intros n.simpl. (* 无能为力! *)
Abort.

这里通过Abort来放弃证明.

原因在于:根据 eqb 和 + 的定义,其第一个参数先被 match 匹配。 但此处 + 的第一个参数 n 未知,而 eqb 的第一个参数 n + 1 是复合表达式,二者均无法化简。

欲进行规约,则需分情况讨论 n 的所有可能构造。告诉 Coq 分别对 n = 0 和 n = S n' 这两种情况进行分析的策略,叫做 destruct。

Theorem plus_1_neq_0 : ∀ n : nat,(n + 1) =? 0 = false.
Proof.intros n. destruct n as [| n'] eqn:E.- reflexivity.- reflexivity. Qed.

eqn:E记号告知Coq以E来命名这些假设.destruct 策略会生成两个子目标,我们必须接下来证明这两个子目标。

eqn: 对相关假设进行命名

destruct: 通过destruct来构造子证明对目标constructor进行分类讨论的策略

as [| n'] 这种标注被称为 '引入模式'。它告诉 Coq 应当在每个子目标中 使用什么样的变量名。总体而言,在方括号之间的是一个由 | 隔开的 '列表的列表'(译者注:list of lists)。

在上面的例子中,第一个元素是 一个空列表,因为 O 构造子是一个空构造子(它没有任何参数)

第二行和第三行中的 - 符号叫做'标号',它标明了这两个生成的子目标所对应的证明部分。

destruct 策略可用于任何归纳定义的数据类型,下面证明对布尔值而言取反是自身的逆运算

Theorem negb_involutive : ∀ b : bool,negb (negb b) = b.
Proof.intros b. destruct b eqn:E.- reflexivity.- reflexivity. 
Qed.

这里的 destruct 没有 as 子句,因为此处 destruct 生成的子分类均无需绑定任何变量

有时在一个子目标内调用 destruct,产生出更多的证明义务(Proof Obligation) 也非常有用。这时候,我们使用不同的标号来标记目标的不同“层级”,比如:

Theorem andb_commutative : ∀ b c, andb b c = andb c b.
Proof.intros b c. destruct b eqn:Eb.- destruct c eqn:Ec.+ reflexivity.+ reflexivity.- destruct c eqn:Ec.+ reflexivity.+ reflexivity.
Qed.

除了 - 和 + 之外,还可以使用 ×(星号)或任何重复的标号符(如 -- 或 ***)作为标号。我们也可以用花括号将每个子证明目标括起来:

Theorem andb_commutative' : ∀ b c, andb b c = andb c b.
Proof.intros b c. destruct b eqn:Eb.{ destruct c eqn:Ec.{ reflexivity. }{ reflexivity. } }{ destruct c eqn:Ec.{ reflexivity. }{ reflexivity. } }
Qed.

花括号还允许我们在一个证明中的多个层级下使用同一个标号。 使用大括号、标号还是二者结合都纯粹是个人偏好问题。

Theorem andb3_exchange :∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof.intros b c d. destruct b eqn:Eb.- destruct c eqn:Ec.{ destruct d eqn:Ed.- reflexivity.- reflexivity. }{ destruct d eqn:Ed.- reflexivity.- reflexivity. }- destruct c eqn:Ec.{ destruct d eqn:Ed.- reflexivity.- reflexivity. }{ destruct d eqn:Ed.- reflexivity.- reflexivity. }
Qed.

在本章结束之前,我们最后再说一种简便写法。或许你已经注意到了, 很多证明在引入变量之后会立即对它进行情况分析:

       intros x y. destruct y as [|y] eqn:E.

这种写法是如此的常见以至于 Coq 为它提供了一种简写:我们可以在引入 一个变量的同时对他使用'引入模式'来进行分类讨论

Theorem plus_1_neq_0' : ∀ n : nat,(n + 1) =? 0 = false.
Proof.intros [|n].- reflexivity.- reflexivity. 
Qed.

以下两种形式是等价的:

intros x y. destruct y as [|y] eqn:E.intros [|y].

如果没有需要命名的constructor参数,我们只需写上 [] 即可进行情况分析。

Theorem andb_commutative'' :∀ b c, andb b c = andb c b.
Proof.intros [] [].- reflexivity.- reflexivity.- reflexivity.- reflexivity.
Qed.

关于记法

回忆一下中缀加法和乘法的记法定义:

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

对于 Coq 中的每个记法符号,我们可以指定它的 '优先级' 和 '结合性'。 优先级 n 用 at level n 来表示.Coq 使用 0 到 100 的优先级等级,同时支持 '左结合'、'右结合' 和 '不结合' 三种结合性

每个记法符号还与 '记法范围(Notation Scope)'相关。Coq 会尝试根据上下文来猜测 你所指的范围

不动点Fixpoint与结构化递归

以下是加法定义的一个副本:

Fixpoint plus' (n : nat) (m : nat) : nat :=match n with| O ⇒ m| S n' ⇒ S (plus' n' m)end.

当 Coq 查看此定义时,它会注意到“plus' 的第一个参数是递减的”。 这意味着我们对参数 n 执行了'结构化递归'。

换言之,我们仅对严格递减的 n 值进行递归调用。这一点蕴含了“对 plus' 的调用最终会停止”。

这项要求是 Coq 的基本特性之一,它保证了 Coq 中定义的所有函数对于所有输入都会终止。

http://www.hskmm.com/?act=detail&tid=25237

相关文章:

  • Python 在自然语言处理中的应用与发展
  • Python 在网络爬虫与数据采集中的应用
  • 15_spring_data_neo4j简单教程
  • CF2152G Query Jungle(线段树,重链剖分,*)
  • 代码随想录算法训练营第九天 | leetcode 151 卡特55
  • [题解] 分竹子
  • 分数规划
  • CSS - transition 粗浅记忆
  • 【MC】LittleTiles模组结构数据解析和版本迁移方案
  • 容器魔方导致盒子满了
  • 课程学习笔记——[大一秋]遗传学
  • P3067 [USACO12OPEN] Balanced Cow Subsets G
  • Vivado 2025 界面中文设置
  • 词汇学习——专业词汇
  • P4556 [Vani有约会] 雨天的尾巴 [模板] 线段树合并
  • P4550 收集邮票
  • P8110 [Cnoi2021] 矩阵
  • P9751 [CSP-J 2023] 旅游巴士
  • P9234 [蓝桥杯 2023 省 A] 买瓜
  • P1044 [NOIP 2003 普及组] 栈
  • P1080 [NOIP 2012 提高组] 国王游戏
  • 音响没声音
  • P1654 OSU!
  • DynamoDB十年演进:云原生数据库的技术革新
  • 完整教程:MySQL全量、增量备份与恢复
  • 10/5
  • 10/4
  • 嵌入式MCU
  • porting perf性能观测工具
  • Windows常用快捷指令