2021-11-11 17:22 已编辑华东师范大学前端工程师

关注

【Coq】16 Poly II 作为数据的函数

作为数据的函数 Functions as Data

与大多数现代编程语言一样——特别是其他“函数”语言，包括OCaml、Haskell、Racket、Scala、Clojure等——Coq将函数视为一级公民，允许它们作为参数传递给其他函数、作为结果返回、存储在数据结构中等。

高阶函数 Higher-Order Functions

操纵其他函数的函数通常称为高阶函数。这里有一个简单的例子：

Definition doit3times {X : Type} (f : X->X) (n : X) : X :=
  f (f (f n)).

这里的参数f本身就是一个函数（从X到X）；doit3times的主体将f应用于某个值n的三倍。

Check @doit3times : forall X : Type, (X -> X) -> X -> X.

Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity. Qed.

Example test_doit3times': doit3times negb true = false.
Proof. reflexivity. Qed.

滤器 Filter

下面是一个更有用的高阶函数，它获取一个X列表和X上的谓词（从X到bool的函数）并“过滤”该列表，返回一个新列表，其中只包含谓词返回true的元素。

Fixpoint filter {X:Type} (test: X->bool) (l:list X) : list X :=
  match l with
  | [] => []
  | h :: t =>
    if test h then h :: (filter test t)
    else filter test t
  end.

例如，如果我们将筛选器应用于谓词偶数和一个数字列表l，它将返回一个仅包含l的偶数成员的列表。

Example test_filter1: filter even [1;2;3;4] = [2;4].
Proof. reflexivity. Qed.

Definition length_is_1 {X : Type} (l : list X) : bool :=
  (length l) =? 1.

Example test_filter2:
    filter length_is_1
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

我们可以使用过滤器从列表一章中给出countoddmembers函数的简明版本。

Definition countoddmembers' (l:list nat) : nat :=
  length (filter odd l).

Example test_countoddmembers'1:   countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.
Example test_countoddmembers'2:   countoddmembers' [0;2;4] = 0.
Proof. reflexivity. Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity. Qed.

匿名函数 Anonymous Functions

在上面的例子中，被迫定义函数长度_is_1并给它起个名字，以便能够将其作为参数传递给过滤器，这可能有点令人伤心，因为我们可能永远不会再使用它。此外，这不是一个孤立的例子：当使用高阶函数时，我们通常希望将永远不会使用的“一次性”函数作为参数传递；必须为这些函数中的每一个都指定一个名称将是乏味的。

幸运的是，有更好的办法。我们可以“动态”构造一个函数，而无需在顶层声明它或给它命名。

Example test_anon_fun':
  doit3times (fun n => n * n) 2 = 256.
Proof. reflexivity. Qed.

表达(fun n => n * n)可以理解为“给定一个数n，产生n×n的函数。”

下面是一个过滤器示例，重写为使用匿名函数

Example test_filter2':
    filter (fun l => (length l) =? 1)
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity. Qed.

51: 2 stars, standard (filter_even_gt7)

使用filter（而不是Fixpoint）编写Coq函数filter_偶数_gt7，该函数将自然数列表作为输入，并返回偶数大于7的自然数列表。

Definition filter_even_gt7 (l : list nat) : list nat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
 (* FILL IN HERE *) Admitted.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5;2;6;19;129] = [].
 (* FILL IN HERE *) Admitted.

Coq代码

Definition filter_even_gt7 (l : list nat) : list nat :=
 filter (fun n => even n && leb 7 n) l.

Example test_filter_even_gt7_1 :

 filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
Proof. reflexivity. Qed.

Example test_filter_even_gt7_2 :
 filter_even_gt7 [5;2;6;19;129] = [].
Proof. reflexivity. Qed.

52: 3 stars, standard (partition)

使用筛选器编写Coq函数分区：

分区：∀ X:类型，

(X → bool) → list X → list X × list X

给定一个集合X，一个类型为X的谓词→ bool和一个列表X，分区应该返回一对列表。该对的第一个成员是包含满足测试的元素的原始列表的子列表，第二个成员是包含未通过测试的元素的子列表。两个子列表中元素的顺序应与其在原始列表中的顺序相同。

Definition partition {X : Type}
                    (test : X -> bool)
                    (l : list X)
                  : list X * list X
 (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_partition1: partition odd [1;2;3;4;5] = ([1;3;5], [2;4]).
(* FILL IN HERE *) Admitted.
Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
(* FILL IN HERE *) Admitted.

Coq代码

Definition partition {X : Type}
                     (test : X -> bool)
                     (l : list X)
                   : list X * list X:=
((filter (fun n => test n) l),(filter (fun n => negb (test n)) l)).


Example test_partition1: partition odd [1;2;3;4;5] = ([1;3;5], [2;4]).
Proof. reflexivity. Qed.
Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
Proof. reflexivity. Qed.

地图 Map

另一个方便的高阶函数叫做map。

Fixpoint map {X Y : Type} (f : X->Y) (l : list X) : list Y :=
  match l with
  | []     => []
  | h :: t => (f h) :: (map f t)
  end.

它接受一个函数f和一个列表l=[n1，n2，n3，…]，并返回列表[fn1，fn2，fn3，…]，其中f依次应用于l的每个元素。例如：

Example test_map1: map (fun x => plus 3 x) [2;0;2] = [5;3;5].
Proof. reflexivity. Qed.

输入和输出列表的元素类型不必相同，因为map有两个类型参数X和Y；因此，它可以应用于数字列表和从数字到布尔值的函数，以生成布尔值列表：

Example test_map2:
  map odd [2;1;2;5] = [false;true;false;true].
Proof. reflexivity. Qed.

它甚至可以应用于数字列表和从数字到布尔值列表的函数，以生成布尔值列表：

Example test_map3:
    map (fun n => [even n;odd n]) [2;1;2;5]
  = [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity. Qed.

53: 3 stars, standard (map_rev)

显示地图和rev通勤路线。你可能需要定义一个辅助引理。

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  (* FILL IN HERE *) Admitted.

54: 2 stars, standard, especially useful (flat_map)

函数映射使用类型为X → Y的函数将列表X映射到列表Y。我们可以定义一个类似的函数，flat_map，它使用类型为X → list Y的函数f将列表X映射到列表Y。你的定义应该通过“展平”f的结果来起作用，如下所示：

 flat_map (fun n => [n;n+1;n+2]) [1;5;10]
      = [1; 2; 3; 5; 6; 7; 10; 11; 12].

Fixpoint flat_map {X Y: Type} (f: X -> list Y) (l: list X)
                   : list Y
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_flat_map1:
  flat_map (fun n => [n;n;n]) [1;5;4]
  = [1; 1; 1; 5; 5; 5; 4; 4; 4].
 (* FILL IN HERE *) Admitted.

列表不是map有意义的唯一归纳类型。以下是选项类型的映射：

Definition option_map {X Y : Type} (f : X -> Y) (xo : option X)
                      : option Y :=
  match xo with
  | None => None
  | Some x => Some (f x)
  end.

55: 2 stars, standard, optional (implicit_args)

filter和map的定义和使用在许多地方使用隐式参数。用括号替换隐式参数周围的大括号，然后在必要时填写显式类型参数，并使用Coq检查是否正确执行了此操作。（此练习不需要提交；在该文件的副本上进行此练习可能是最简单的，您可以在以后将其丢弃。）

折叠 Fold

一个更强大的高阶函数称为fold。这个函数是“reduce”操作的灵感来源，该操作是Google map/reduce分布式编程框架的核心。

Fixpoint fold {X Y: Type} (f : X->Y->Y) (l : list X) (b : Y)
                         : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

直观地说，折叠操作的行为是在给定列表中的每对元素之间插入给定的二进制运算符f。例如，fold plus[1；2；3；4]直观地表示1+2+3+4。为了精确起见，我们还需要一个“起始元素”，作为f的初始第二个输入。那么比如说,

 fold plus [1;2;3;4] 0
 yields
       1 + (2 + (3 + (4 + 0))).

还有一些例子：

Check (fold andb) : list bool -> bool -> bool.

Example fold_example1 :
  fold mult [1;2;3;4] 1 = 24.
Proof. reflexivity. Qed.

Example fold_example2 :
  fold andb [true;true;false;true] true = false.
Proof. reflexivity. Qed.

Example fold_example3 :
  fold app  [[1];[];[2;3];[4]] [] = [1;2;3;4].
Proof. reflexivity. Qed.

56: 1 star, advanced (fold_types_different)

请注意，折叠的类型由两个类型变量X和Y参数化，参数f是一个二进制运算符，它接受X和Y并返回Y。您能想到X和Y不同的情况吗？

(* FILL IN HERE *)

构造函数的函数 Functions That Construct Functions

到目前为止，我们讨论的大多数高阶函数都将函数作为参数。让我们看一些示例，这些示例涉及将函数作为其他函数的结果返回。首先，这里有一个函数，它接受一个值x（从某个类型x中提取），并将一个函数从nat返回到x，该函数在每次调用时都会生成x，而忽略其nat参数。

Definition constfun {X: Type} (x: X) : nat -> X :=
  fun (k:nat) => x.

Definition ftrue := constfun true.

Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.

Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.

事实上，我们已经看到的多参数函数也是将函数作为数据传递的示例。要了解原因，请回忆一下plus的类型。

Check plus : nat -> nat -> nat.

每个→ 在这个表达式中，类型实际上是一个二进制运算符。这个操作符是右关联的，所以加号的类型实际上是nat -> (nat -> nat)的简写--也就是说，它可以理解为“加号是一个单参数函数，它接受一个nat并返回一个单参数函数，它接受另一个nat并返回一个nat。”在上面的例子中，我们总是将加号同时应用于它的两个参数，但如果我们愿意，我们可以只提供第一个。这称为部分应用程序。

Definition plus3 := plus 3.
Check plus3 : nat -> nat.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity. Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity. Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity. Qed.

【学习】函数语言程序设计文章被收录于专栏

函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】