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

Software Foundations Vol.I : 使用结构化的数据(Lists)

Software Foundations Vol.I : 使用结构化的数据(Lists)


数值序对

在 Inductive 类型定义中,每个构造子(Constructor)可以有任意多个参数 —— 可以没有(如 true 和 O),可以只有一个(如 S),也可以更多 (如 nybble,以及下文所示):

Inductive natprod : Type :=
| pair (n1 n2 : nat).Check (pair 3 5) : natprod.Definition fst (p : natprod) : nat :=match p with| pair x y ⇒ xend.
Definition snd (p : natprod) : nat :=match p with| pair x y ⇒ yend.
Compute (fst (pair 3 5)).
(* ===> 3 *)

由于二元组十分常用,不妨以标准的数学记法 (x,y) 取代 pair x y。 通过 Notation 向 Coq 声明该记法:

Notation "( x , y )" := (pair x y).

这种新的表示法既可以在表达式中使用,也可以在模式匹配中使用.

Compute (fst (3,5)).
Definition fst' (p : natprod) : nat :=match p with| (x,y) ⇒ xend.
Definition snd' (p : natprod) : nat :=match p with| (x,y) ⇒ yend.
Definition swap_pair (p : natprod) : natprod :=match p with| (x,y) ⇒ (y,x)end.

对一个括号内的元组(如:(x,y)),并非与先前所见的多重匹配语法(如 x,y)混淆.

这种差异虽然不大,但是了解到这一点还是非常必要的.例如,下面的定义就是不正确的:

(* Can't match on a pair with multiple patterns: *)
Definition bad_fst (p : natprod) : nat :=match p with| x, y ⇒ xend.(* Can't match on multiple values with pair patterns: *)
Definition bad_minus (n m : nat) : nat :=match n, m with| (O , _ ) ⇒ O| (S _ , O ) ⇒ n| (S n', S m') ⇒ bad_minus n' m'end.

如果我们以稍显古怪的方式陈述序对的性质,那么有时只需 reflexivity(及其内建的简化)即可完成证明。

Theorem surjective_pairing' : ∀ (n m : nat),(n,m) = (fst (n,m), snd (n,m)).
Proof.reflexivity. Qed.

但是,如果我们用一种更为自然的方式来陈述此引理的话,只用 reflexivity 还不够。

Theorem surjective_pairing_stuck : ∀ (p : natprod),p = (fst p, snd p).
Proof.simpl. (* 啥也没有归约! *)
Abort.

我们还需要向 Coq 展示 p 的具体结构,这样 simpl 才能对 fst 和 snd 做模式匹配。通过 destruct 可以达到这个目的

Theorem surjective_pairing : forall (p : natprod),p = (fst p, snd p).
Proof.intros p. destruct p as [n m]. - simpl. reflexivity. 
Qed.

数值列表

通过推广序对的定义,数值'列表'类型可以这样描述: “一个列表要么是空的,要么就是由一个数和另一个列表组成的序对。”

Inductive natlist : Type :=| nil| cons (n : nat) (l : natlist).

例如,这是一个三元素列表:

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

和序对一样,使用熟悉的编程记法来表示列表会更方便些。 以下两个声明能让我们用 :: 作为中缀的 cons 操作符, 用方括号作为构造列表的“外围(outfix)”记法。

Notation "x :: l" := (cons x l)(at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

注解 "right associativity" 告诉 Coq 当遇到多个 :: 时如何给表达式加括号,如此一来下面三个声明做的就是同一件事:

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

"at level 60" 告诉 Coq 当遇到表达式和其它中缀运算符时应该如何加括号。 例如,plus 函数定义了 + 中缀符号,它的优先级是 50:

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

+会比 :: 结合的更紧密,所以 1 + 2 :: [3] 会被解析成 (1 + 2) :: [3] 而非 1 + (2 :: [3])。

Repeat

接下来看几个用来构造和操作列表的函数。第一个是 repeat 函数,它接受一个数字 n 和一个 count,返回一个长度为 count,每个元素都是 n 的列表。

Fixpoint repeat (n count : nat) : natlist :=match count with| O ⇒ nil| S count' ⇒ n :: (repeat n count')end.

Length

length 函数用来计算列表的长度。

Fixpoint length (l:natlist) : nat :=match l with| nil ⇒ O| h :: t ⇒ S (length t)end.

Append

app 函数用来把两个列表联接起来。

Fixpoint app (l1 l2 : natlist) : natlist :=match l1 with| nil ⇒ l2| h :: t ⇒ h :: (app t l2)end.

由于下文中 app 随处可见,不妨将其定义为中缀运算符。

Notation "x ++ y" := (app x y)(right associativity, at level 60).
Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

Head与Tail

下面介绍列表上的两种运算:hd 函数返回列表的第一个元素(即“head”); tl 函数返回列表除去第一个元素以外的部分(即“tail”)。由于空表没有表头, 我们必须传入一个参数作为返回的默认值。

Definition hd (default:nat) (l:natlist) : nat :=match l with| nil ⇒ default| h :: t ⇒ hend.
Definition tl (l:natlist) : natlist :=match l with| nil ⇒ nil| h :: t ⇒ tend.
Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

用列表实现口袋(Bag)

bag(或者叫 multiset 多重集)类似于集合,只是其中每个元素都能出现不止一次。 口袋的一种可行的表示是列表。

Definition bag := natlist.

有关列表的论证

和数字一样,有些列表处理函数的简单事实仅通过化简就能证明。

Theorem nil_app : ∀ l:natlist,[] ++ l = l.
Proof. reflexivity. Qed.

...由于 [] 被替换进了 app 定义中相应的“被检”分支 (即经由匹配“仔细检查”过值的表达式),整个匹配得以被简化。

和数字一样,有时对一个列表做分类讨论(是否是空)是非常有用的。

Theorem tl_length_pred : ∀ l:natlist,pred (length l) = length (tl l).
Proof.intros l. destruct l as [| n l'].- (* l = nil *)reflexivity.- (* l = cons n l' *)reflexivity. Qed.

在这里 nil 的情况能够工作是因为定义了 tl nil = nil, 而 destruct 策略中 as 注解引入的两个名字,n 和 l',分别对应了 cons 构造子的两个参数(正在构造的列表的头和尾)。

然而一般来说,许多关于列表的有趣定理都需要用到归纳法来证明。

对列表进行归纳

比起对自然数的归纳,归纳证明 natlist 这样的数据类型更加陌生。 不过基本思路同样简单。每个 Inductive 声明定义了一组数据值, 这些值可以用声明过的构造子来构造。

归纳定义的集合中元素的形式 '只能是' 构造子对其它项的应用。这一事实同时也给出了一种对归纳定义的集合进行论证的方法:一个自然数要么是 O,要么就是 S 应用到某个'更小'的自然数上;一个列表要么是 nil, 要么就是 cons 应用到某个数字和某个'更小'的列表上,诸如此类。

  • 首先,证明当 l 为 nil 时 P l 成立。

  • 然后,证明当 l 为 cons n l' 时 P l 成立,其中 n 是某个自然数,l' 是某个更小的列表,假设 P l' 成立.

由于较大的列表总是能够分解为较小的列表,最终这个较小的列表会变成 nil,这两点合在一起就完成了 P 对一切列表 l 成立的证明。下面是个具体的例子:

Theorem app_assoc : forall l1 l2 l3 : natlist,(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.intros l1 l2 l3. induction l1 as [| n l1' IHl1'].- (* l1 = nil *)reflexivity.- (* l1 = cons n l1' *)simpl. rewrite -> IHl1'. reflexivity. 
Qed.

其使用自然语言描述为:

'定理':对所有的列表 l1, l2, 和 l3, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)。
'证明': 通过对 l1 使用归纳法。

首先, 假设 l1 = []。我们必须证明:
$$([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)$$

这可以通过展开 ++ 的定义得到。

然后, 假设 l1 = n::l1',有:
$$(l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)$$

(归纳假设)。我们必须证明:
$$((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3)$$

根据 ++ 的定义, 上式等价于:
$$n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3))$$

该式可通过我们的归纳假设立即证得。 ☐

反转列表

举一个更加深入的例子来说明对列表的归纳证明:假设使用 app 来定义一个列表反转函数 rev:

Fixpoint rev (l:natlist) : natlist :=match l with| nil ⇒ nil| h :: t ⇒ rev t ++ [h]end.
Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

为了比目前所见的证明多一点挑战性, 来证明反转一个列表不会改变它的长度。

Theorem rev_length_firsttry : ∀ l : natlist,length (rev l) = length l.
Proof.intros l. induction l as [| n l' IHl'].- (* l = nil *)reflexivity.- (* l = n :: l' *)(* 这种情况比较棘手。我们从一般的化简开始。 *)simpl.(* 现在我们好像卡住了:目标是要证明涉及 ++ 的等式,但是我们在上下文和全局环境下并没有任何有用的等式!通过用 IH 来重写目标,我们可以推进一点... *)rewrite <- IHl'.(* ...但也仅此而已。 *)
Abort.

不妨单独提出引理,阐述 ++ 与 length 形成的等式关系, 以从我们卡住的地方推进证明。

Theorem app_length : ∀ l1 l2 : natlist,length (l1 ++ l2) = (length l1) + (length l2).
Proof.(* 课上已完成 *)intros l1 l2. induction l1 as [| n l1' IHl1'].- (* l1 = nil *)reflexivity.- (* l1 = cons *)simpl. rewrite → IHl1'. reflexivity. 
Qed.

现在可以完成最初的证明了。

Theorem rev_length : ∀ l : natlist,length (rev l) = length l.
Proof.intros l. induction l as [| n l' IHl'].- (* l = nil *)reflexivity.- (* l = cons *)simpl. rewrite → app_length.simpl. rewrite → IHl'. rewrite plus_comm.reflexivity.
Qed.

'定理':对于所有 l,length (rev l) = length l。
'证明':首先,观察到 length (l ++ [n]) = S (length l) 对一切 l 成立, 这一点可通过对 l 的归纳直接得到。
当 l = n'::l' 时,通过再次对 l 使用归纳, 然后同时使用之前观察得到的性质和归纳假设即可证明。 ☐

Search 搜索

我们已经见过很多需要使用之前证明过的结论(例如通过 rewrite)来证明的定理了。 但是在引用别的定理时,我们必须事先知道它们的名字。

当然,即使是已被证明的定理本身 我们都不能全部记住,更不用提它们的名字了。

Coq 的 Search 指令在这时就非常有用了。执行 Search foo 会让 Coq 显示所有涉及到 foo 的定理。

例如,去掉下面的注释后, 会看到一个我们证明过的所有关于 rev 的定理的列表:

(*  Search rev. *)

Options 可选类型

假设我们想要写一个返回某个列表中第 n 个元素的函数。如果我们为它赋予类型 nat → natlist → nat,那么当列表太短时我们仍须返回某个数...

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=match l with| nil ⇒ 42| a :: l' ⇒ match n with| 0 ⇒ a| S n' ⇒ nth_bad l' n'endend.

这种方案并不好:如果 nth_bad 返回了 42,那么不经过进一步处理的话, 无法得知该值是否真的出现在了输入中。

因为无法判断是什么因素让它返回了 42.它可能是列表过短时的返回值,同时也可能是(此时列表足够长)在列表中找到的值

Inductive natoption : Type :=| Some (n : nat)| None.

可以修改前面 nth_bad 的定义,使其在列表太短时返回 None, 在列表足够长且 a 在 n 处时返回 Some a。将这个新函数称为 nth_error 来表明它可以产生带错误的结果。

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=match l with| nil ⇒ None| a :: l' ⇒ match n with| O ⇒ Some a| S n' ⇒ nth_error l' n'endend.
Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.

Coq 的条件语句和其它语言中的一样,不过加上了一点更为一般化的特性。

由于 bool 类型不是内建的,因此 Coq 实际上支持在'Any'带有两个构造子的, 归纳定义的类型上使用条件表达式。

当断言(guard)求值为 Inductive 定义中的第一个构造子时,它被认为是真的;当它被求值到第二个构造子时, 则被认为是假的。

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=match l with| nil ⇒ None| a :: l' ⇒ if n =? O then Some aelse nth_error' l' (pred n)end.

以下函数从 natoption 中取出一个 nat,在遇到 None 时它将返回提供的默认值。

Definition option_elim (d : nat) (o : natoption) : nat :=match o with| Some n' ⇒ n'| None ⇒ dend.

Partial Maps 偏映射

下面的例子演示了如何在 Coq 中定义基础的数据结构。这是一个简单的 '偏映射' 数据类型,它类似于大多数编程语言中的映射或字典数据结构。

首先,定义一个新的归纳数据类型 id 来用作偏映射的“键”。

Inductive id : Type :=| Id (n : nat).

本质上来说,id 只是一个数。但通过 Id 标签封装自然数来引入新的类型, 能让定义变得更加可读,同时也给了我们更多的灵活性。

还需要一个 id 的相等关系测试:

Definition eqb_id (x1 x2 : id) :=match x1, x2 with| Id n1, Id n2 ⇒ n1 =? n2end.

现在定义偏映射的类型:

Inductive partial_map : Type :=| empty| record (i : id) (v : nat) (m : partial_map).

此声明可以理解为:“有两种方式可以构造一个 partial_map:
用构造子 empty 表示一个空的偏映射,
或将构造子 record 应用到一个键、一个值和一个既有的 partial_map 来构造一个带“键-值”映射 的 partial_map。”

update 函数用于在部分映射中覆盖给定的键以取缔原值(如该键尚不存在, 则新建其记录)。

Definition update (d : partial_map)(x : id) (value : nat) : partial_map :=record x value d.

最后,find 函数按照给定的键搜索一个 partial_map。若该键无法找到, 它就返回 None;若该键与 val 相关联,则返回 Some val。 若同一个键被映到多个值,find 就会返回它遇到的第一个值。

Fixpoint find (x : id) (d : partial_map) : natoption :=match d with| empty ⇒ None| record y v d' ⇒ if eqb_id x ythen Some velse find x d'end.
http://www.hskmm.com/?act=detail&tid=25239

相关文章:

  • Software Foundations Vol.I : 归纳证明(Induction)
  • Software Foundations Vol.I : Coq函数式编程(Basics)
  • 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