Coq 学习

根据课程进度持续更新

Wings 收录于类别软件

2025-03-14 2025-03-14 约 1759 字预计阅读 8 分钟次阅读条评论

软件所的形式化课直接教 Coq, 牛. 跟着课堂内容记录一下学习的过程, 整理的东西可能需要穿插着看.

环境

配一个 nvim 的环境还比较麻烦. 插件是 Coqtail, 主机需要安装 pynvim 并且配置使用主机的 python¹.

默认快捷键和我的 codecompanion 有些冲突, 暂时没去调整.

以及 auto save 的 delay 不能开太小, 否则他的 buffer 会闪一下然后回去.

差一个 coq-lsp, 需要 ocaml, 再说.

基本的配置是这样的:

lua

return {
  "whonore/Coqtail",
  dependencies = {
    "AstroNvim/astrocore",
    opts = {
      options = {
        g = {
          python3_host_prog = "/usr/bin/python",
        },
      },
    },
  },
}

类型

非常强类型, 类型都有类型

可以使用 Check 检查表达式的类型, 比如:

coq

Check 1.
Check 1+1.
Check _ + _.
Check Nat.add.

输出结果依次如下:

text

1
     : nat

1 + 1
     : nat

?n + ?m
     : nat
where
?n : [ |- nat]
?m : [ |- nat]

add
     : nat -> nat -> nat

输出里的 nat 是自然数, 他是 Coq 标准库中的一个模块里定义好的东西.

第三个 Check 的 _ + _ 表示检查记号Notation + 的类型, 也是 nat. 不过这里可以看到左右两个表达式(_), 都必须是 nat 类型. 而 Nat.add 是一个函数, 他接受两个参数, 返回一个值, 函数式编程, 前两个 nat 分别是前两个参数的类型, 最后 to 的一个 nat 是函数返回值的类型. 这个 nat -> nat -> nat 也是一种类型, -> 是右结合, 所以 nat -> nat -> nat 就是 nat -> (nat -> nat) 的类型. Coq 定义的函数是柯里化Currying的, 比如这里 add 有两个参数, 只给他一个参数他就输出另一个函数, 这个函数的类型是 nat -> nat, 表示参数是一个 nat, 返回一个 nat.

coq

Check Nat.add 1

text

Nat.add 1
     : nat -> nat

定义类型

枚举类型, 例如交通灯

coq

Inductive traffic_light: Type :=
| Red
| Yellow
| Green.

Inductive 是定义类型的标识符, 后面跟着类型名比如 traffic_light, 之后 : Type 表示这个类型的类型是 Type, 最后接构造的定义. 定义由若干个构造子constructor组成, 这里就是简单的三个标识符 Red, Yellow, Green.

coq

Check Red.
Check traffic_light.

text

Red
     : traffic_light

traffic_light
     : Set

技巧

为什么 Check 的 traffic_light 的类型是 Set 而不是 Type 见 Type

此外, 还可以归纳定义类型, 比如皮亚诺Peano²公理定义自然数.

皮亚诺公理

$0$ 是自然数；
每一个确定的自然数 $a$，都有一个确定的后继数 $a’$，$a’$ 也是自然数；
对于每个自然数 $b$、$c$，$b=c$ 当且仅当 $b$ 的后继数 $=c$ 的后继数；
$0$ 不是任何自然数的后继数；
任意关于自然数的命题，如果证明：它对自然数 $0$ 是真的，且假定它对自然数 $a$ 为真时，可以证明对 $a’$ 也真。那么，命题对所有自然数都真。

定义如下:

coq

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

其中,

O 是一个构造子, 表示自然数 $0$ (公理第 1 条)
S 是一个构造子, 这个构造子是一个函数, 意思是如果 n 是 mynat, 那么 S n 也是 mynat, 可以看作是后继函数, 说明了每个自然数都有唯一的后继 (公理第 2 条)
在 Coq 里, 归纳定义的构造子一定是单射, 即每个值都有唯一的构造子. 也就是说, 一个值只能对应一个构造子 (公理第 3 条)
在 Coq 里, 构造子是互不相交的, O 不能是 S n 可以构造出来的, 满足 $0$ 不是任何自然数的后继 (公理第 4 条)
在 Coq 里, 归纳定义时会自动生成归纳原理, 可以 Print mynat_ind 来查看:

text

mynat_ind =
fun (P : mynat -> Prop) (f : P O) (f0 : forall n : mynat, P n -> P (S n)) =>
fix F (m : mynat) : P m :=
  match m as m0 return (P m0) with
  | O => f
  | S n => f0 n (F n)
  end
     : forall P : mynat -> Prop,
       P O -> (forall n : mynat, P n -> P (S n)) -> forall m : mynat, P m

由于还没有学到, 这个函数不是很看得懂, 但是看最后的 P O -> (forall n : mynat, P n -> P (S n)) -> forall m : mynat, P m 能看出个大概: P 是一个性质, 对于 O 成立, 并且对于所有的 n, 如果 P n 成立, 那么 P 对 n 的后继 S n 也成立 (P (S n) 成立), 那么 P 对所有 mynat 的 m 都成立. 这就是公里第 5 条.

预定义类型

Coq 标准库中定义了一些类型

nat

text

Locate nat.
Print nat.

text

Inductive Coq.Init.Datatypes.nat

Inductive nat : Set :=  O : nat | S : nat -> nat.

Arguments S _%nat_scope

技巧

Locate 用于定位模块, Print 用于查看类型定义

同时也定义了一些自然数的运算, 比如加减乘除:

coq

Locate "_ + _".
Print "_ + _".

text

Notation "x + y" := (Init.Nat.add x y) : nat_scope (default interpretation)
Notation "x + y" := (sum x y) : type_scope

Notation "x + y" := (Init.Nat.add x y)

Init.Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat

Arguments Init.Nat.add (n m)%nat_scope

暂时先不管函数定义的内容, 可以看到, + 是一个记号notation, 是 Init.Nat.add 函数的 “语法糖”. 定义记号的方法类似 Print 打印出来的那一行 Notation "x + y" := (Init.Nat.add x y), 关键字是 Notation.

这个 Init.Nat 是 Coq 的一个模块, 里面定义了一些基本的算术运算. 要写成函数的形式, 需要 Nat.add 1 1 这样, 或者事先 Import Nat. (可以省略 Init 前缀), 即可 add 1 1.

PeanoNat

另外还有一个 Coq.Peano.PeanoNat / PeanoNat 模块, 主要提供基于 Peano 归纳定义的定理和性质, 比如自反性 PeanoNat.Nat.le_refl, 传递性 PeanoNat.Nat.le_trans, 反对称性 PeanoNat.Nat.le_antisym.

用的话需要 Require Import PeanoNat.. 还没学到怎么用, 老师屏幕里出现了 PeanoNat, 问 gpt 了解一下.

bool

coq

Print bool.
Check true.
Check false.

text

Inductive bool : Set :=  true : bool | false : bool.

true
     : bool

false
     : bool

显而易见, 不解释了

list

另一种类型是列表, 他能够表示相同类型的一列东西. 比如:

coq

Require Import List.

Check 1::2::3::nil.
Check (1::2::nil)::(2::3::nil)::nil

Print "_ :: _".

其中, :: 是列表连接的记号 (定义在 List 库中, 所以需要 Require Import List.). nil 是表尾构造子.

text

1 :: 2 :: 3 :: nil
     : list nat

(1 :: 2 :: nil) :: (2 :: 3 :: nil) :: nil
     : list (list nat)

Notation "x :: y" := (cons x y)

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.

Arguments list A%type_scope
Arguments nil {A}%type_scope
Arguments cons {A}%type_scope a l%list_scope
  (where some original arguments have been renamed)

可以看到, 构造出来的列表, 类型是 list A, 其中 A 表示元素的类型, 比如 nat, 或者 list nat.

prod

coq

Print prod.
Check pair.
Check (1, 2, 3).
Print "(".

text

Inductive prod (A B : Type) : Type :=  pair : A -> B -> A * B.

Arguments prod (A B)%type_scope
Arguments pair {A B}%type_scope _ _

pair
     : ?A -> ?B -> ?A * ?B
where
?A : [ |- Type]
?B : [ |- Type]

(1, 2)
     : nat * nat

Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
  (default interpretation)

(1, nil, true)
     : nat * list ?A * bool
where
?A : [ |- Type]

元组的构造子是 pair, 类型是 A -> B -> A * B, 返回的 A * B 意思是 A B 类型的笛卡尔集. ( 和 ) 是 pair 的记号, 可以用来构造任意多元素的元组.

option

原来 rust 的 Option 来自这里!

coq

Check Some 1.
Check None.

text

Inductive option (A : Type) : Type :=
    Some : A -> option A | None : option A.

Arguments option A%type_scope
Arguments Some {A}%type_scope a
  (where some original arguments have been renamed)
Arguments None {A}%type_scope

Some
     : ?A -> option ?A
where
?A : [ |- Type]

Some 1
     : option nat

None
     : option ?A
where
?A : [ |- Type]

Type

类型也有类型, 为 Type. 这样的类型还能有多级, 而最低级的类型是 Set.

暂时只能感性理解一下.

函数

函数根据类型的不同, 分为普通函数和递归函数.

普通函数

coq

Definition next_light (n: traffic_light) :traffic_light :=
  match n with
  | Red => Green
  | Yellow => Red
  | Green => Yellow
  end.

类型可以推导, 不需要显示定义, 和 rust 的 match 一样, 也有 _ 来表示其他的 (同样也要放到最后).

coq

Definition next_light2 n :=
  match n with
  | Red => Green
  | _ => Red
  end.

定义函数的类型可以是多态, 比如如下定义:

coq

Definition self {A : Type} (x : A) : A := x.
Definition self {A : Type} (x : A) := x.
Definition self {A : Type} x : A := x.

self 函数返回自身. 而且只要在一处指定了类型, Coq 能够自动推导其他地方的类型. 比如最后一条仅指定了参数的类型是 A, Coq 能够推导出返回值的类型也是 A. 倒数第二条反过来也可以.

花括号的指定泛型可以自动推导, 若是圆括号则必须手动指定:

coq

Definition self {A : Type} x : A := x.
Check self 1.
Fail Check self nat 1.

Definition self2 (A : Type) x : A := x.
Check self2 bool true.
Fail Check self2 true.

text

self is defined

self 1
     : nat

The command has indeed failed with message:
Illegal application (Non-functional construction): 
The expression "self nat" of type "Set"
cannot be applied to the term
 "1" : "nat"

self2 is defined

self2 bool true
     : bool

The command has indeed failed with message:
The term "true" has type "bool" while it is expected to have type "Type".

技巧

Fail 检查这条命令是否失败, 并给出错误信息.

递归函数

递归函数作用在归纳构造的类型上. 关键字是 Fixpoint, 表示推导的最后会到达不动点.

coq

Fixpoint sum_all_nat (l : list nat) : nat :=
  match l with
  | nil => 0
  | cons hd tl => hd + sum_all_nat tl
  end.

递归函数需要结构上的递减, 如下面这个函数定义将会报错:

coq

Fixpoint foo(x: nat): nat :=
  match x with
  | 0 -> 0
  | S x' => foo((x' * 2) - (x' * 3))
end.

text

Recursive definition of foo is ill-formed.
In environment
foo : nat -> nat
x : nat
x' : nat
Recursive call to foo has principal argument equal to 
"x' * 2 - x' * 3" instead of "x'".
Recursive definition is:
"fun x : nat => match x with
                | 0 => 0
                | S x' => foo (x' * 2 - x' * 3)
                end".

这个函数虽然实际上是递减的, 但是从表达式上来看无法得知结构上的递减, 所以 coq 会拒绝这个. 如果需要可以自己构造证明. (暂时没学到)

如果不只一个参数, 则需要说明哪个参数结构上递减, 或者 Coq 能够推导出.

coq

Fixpoint power (a b : nat) : nat :=
  match b with
  | 0 => 1
  | S b' => a * power a b'
  end.
Print power.

Fixpoint myle (n m : nat) : bool :=
  match n, m with
  | 0, _ => true
  | S _, 0 => false
  | S n', S m' => myle n' m'
  end.
Print myle.

Fixpoint myle2 (n m : nat) {struct m} : bool :=
  match n, m with
  | 0, _ => true
  | S _, 0 => false
  | S n', S m' => myle2 n' m'
  end.
Print myle2.

text

power is defined

power is recursively defined (guarded on 2nd argument)

power =
fix power (a b : nat) {struct b} : nat :=
  match b with
  | 0 => 1
  | S b' => a * power a b'
  end
     : nat -> nat -> nat

Arguments power (a b)%nat_scope

myle is defined

myle is recursively defined (guarded on 1st argument)

myle =
fix myle (n m : nat) {struct n} : bool :=
  match n with
  | 0 => true
  | S n' => match m with
            | 0 => false
            | S m' => myle n' m'
            end
  end
     : nat -> nat -> bool

Arguments myle (n m)%nat_scope

myle2 is defined

myle2 is recursively defined (guarded on 2nd argument)

myle2 =
fix myle2 (n m : nat) {struct m} : bool :=
  match n with
  | 0 => true
  | S n' => match m with
            | 0 => false
            | S m' => myle2 n' m'
            end
  end
     : nat -> nat -> bool

Arguments myle2 (n m)%nat_scope

可以看到, power 自动推导出了第二个参数是结构递减的, myle 两个参数都是递减, Coq 默认按第一个来. myle2 则是手动 {struct m} 说明让 Coq 按第二个参数结构递减来.

函数式编程

由于已经了解过一点点, 所以只简单记录

$\lambda x.M$

$x$ 是参数, $M$ 是函数体.

绑定变量

$x$ 在 $\lambda x.M$ 中是绑定变量
$x$ 如果在 $M$ 或者 $N$ 中是绑定变量, 那么在 $MN$ 中是绑定变量

自由变量

$x$ 在 $x$ (表达式) 中是自由变量
$x$ 在 $\lambda y.M$ ($x \ne y$ 并且 $x$ 在 $M$ 中是自由变量 ) 中是自由变量
$x$ 如果在M或者N中是自由变量, 那么在 $MN$ 中是自由变量 (不管在那个域里是自由变量, 都是自由变量)

绑定变量和自由变量不冲突

$\alpha$ 转换$\alpha$ conversion, 就是变量重命名, 原表达式的意思不会改变

$$(\lambda x.M) \to_\alpha(\lambda y.M\{y/x\}), \text{if } y \notin \mathrm{var}(M)$$

$M\{y/x\}$ 的意思是在 $M$ 中, 用 $y$ 替换掉 $x$

$\beta$ 规约$\beta$ reduction, 可以理解成 “作用” 一次, 即把参数带入函数做一次计算

$$(\lambda x.M)N \to_\beta M[N/x]$$

$M[N/x]$ 的意思是在 $M$ 中, 用 $N$ 替换掉 $x$, 即进行了一次规约.

TODO: 剩下的看了课件再来整理整理.

目录

目录

Coq 学习

根据课程进度持续更新

环境

类型

定义类型

预定义类型

nat

bool

list

prod

option

Type

函数

普通函数

递归函数

函数式编程