数字表 Lists of Numbers

概括成对的定义，我们可以这样描述数字列表的类型：“一个列表要么是空列表，要么是一个数字和另一个列表的一对。”

Inductive natlist

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

Definition mylist

例如，下面是一个三元素列表：

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

与pairs一样，用熟悉的编程符号编写列表更方便。下面的声明允许我们使用：：作为中缀cons运算符，方括号作为构造列表的“outfix”符号。

Notation "x :: l"

Notation "x :: l" := (cons x l)
                   (at level 60, right associativity).

Notation "[ ]"

Notation "[ ]" := nil.

Notation "[ x ; .. ; y ]"

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].

“在60级”部分告诉Coq如何将包含：：和其他中缀运算符的表达式括起来。例如，由于我们将+定义为50级加号函数的中缀符号，

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

（在.v文件中读取诸如"[1 + 2 :: [3]]" 之类的表达式时可能会有点混淆。3左右的内括号表示列表，但在HTML呈现中不可见的外括号用于指示“coqdoc”工具，带括号的部分应显示为Coq代码，而不是运行文本。）

上面的第二个和第三个符号声明介绍了列表的标准方括号符号；第三个的右侧展示了Coq的语法，用于声明n元符号并将其转换为二进制构造函数的嵌套序列。

重复 Repeat

接下来，让我们看几个用于构造和操作列表的函数。首先，repeat函数接受一个数字n和一个计数，并返回一个长度计数列表，其中每个元素都是n。

Fixpoint repeat

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

长度 Length

length函数计算列表的长度。

Fixpoint length

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

追加 Append

app函数连接（附加）两个列表。

Fixpoint app

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

由于该应用程序将被广泛使用，它再次方便有一个中缀运营商为它。

Notation "x ++ y"

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 and Tail

下面是两个使用列表编程的小示例。hd函数返回列表的第一个元素（“head”），而tl则返回除第一个元素（“tail”）之外的所有元素。由于空列表没有第一个元素，因此在这种情况下，我们传递一个要返回的默认值。

Definition hd

Definition hd (default : nat) (l : natlist) : nat :=
  match l with
  | nil ⇒ default
  | h :: t ⇒ h
  end.

Definition tl

Definition tl (l : natlist) : natlist :=
match l with
| nil ⇒ nil
| h :: t ⇒ t
end.
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.

Exercises

28: 2 stars, standard, especially useful (list_funs)

完成以下非零、oddmembers和countoddmembers的定义。看看测试，了解这些函数应该做什么。

Fixpoint nonzeros

Fixpoint nonzeros (l:natlist) : natlist
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_nonzeros:
nonzeros [0;1;0;2;3;0;0] = [1;2;3].
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint nonzeros (l:natlist) : natlist:=
match l with
|nil => nil
|h :: t => if h =? 0 then nonzeros t
          else h :: nonzeros t
end.

Example test_nonzeros:
nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. reflexivity. Qed.

Fixpoint oddmembers

Fixpoint oddmembers (l:natlist) : natlist
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_oddmembers:
oddmembers [0;1;0;2;3;0;0] = [1;3].
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint oddmembers (l:natlist) : natlist :=
match l with
|nil => nil
|h :: t => if odd h then h ::oddmembers t
         else oddmembers t
end.
Example test_oddmembers:
oddmembers [0;1;0;2;3;0;0] = [1;3].
Proof. reflexivity. Qed.

Definition countoddmembers

Definition countoddmembers (l:natlist) : nat
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_countoddmembers1:
countoddmembers [1;0;3;1;4;5] = 4.
(* FILL IN HERE *) Admitted.
Example test_countoddmembers2:
countoddmembers [0;2;4] = 0.
(* FILL IN HERE *) Admitted.
Example test_countoddmembers3:
countoddmembers nil = 0.
(* FILL IN HERE *) Admitted.

Coq代码

Definition countoddmembers (l:natlist) : nat:=
length (oddmembers l).

Example test_countoddmembers1:
  countoddmembers [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.

Example test_countoddmembers2:
  countoddmembers [0;2;4] = 0.
Proof. reflexivity. Qed.

Example test_countoddmembers3:
  countoddmembers nil = 0.
Proof. reflexivity. Qed.

29: 3 stars, advanced (alternate)

完成以下[alternate]的定义，它将两个列表交错为一个，在第一个列表中的元素和第二个列表中的元素之间交替。有关更多具体示例，请参见下面的测试。

（注：一种自然而优雅的书写方式[alternate]将无法满足Coq的要求，即所有[Fixpoint]定义“明显终止”如果您发现自己陷入了这种困境，请寻找一种更详细的解决方案，同时考虑两个列表的元素。一种可能的解决方案包括定义一种新的对，但这不是唯一的方法。）

Fixpoint alternate (l1 l2 : natlist) : natlist
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_alternate1:
  alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
  (* FILL IN HERE *) Admitted.

Example test_alternate2:
  alternate [1] [4;5;6] = [1;4;5;6].
  (* FILL IN HERE *) Admitted.

Example test_alternate3:
  alternate [1;2;3] [4] = [1;4;2;3].
  (* FILL IN HERE *) Admitted.

Example test_alternate4:
  alternate [] [20;30] = [20;30].
  (* FILL IN HERE *) Admitted.

Coq代码

Fixpoint alternate (l1 l2 : natlist) : natlist:=
match l1,l2 with
|nil,nil => nil
|nil,h :: t => l2
|h' :: t',nil => l1
|h'' :: t'',h''' :: t''' =>h'' :: ([h'''] ++ alternate t'' t''')
end.

Example test_alternate1:
alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.

Example test_alternate2:
alternate [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.

Example test_alternate3:
alternate [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.

Example test_alternate4:
alternate [] [20;30] = [20;30].
Proof. reflexivity. Qed.

Bags via Lists

一个包（或多集）就像一个集合，只是每个元素可以出现多次而不是一次。一袋数字的一种可能表示形式是列表。

Definition bag := natlist.

Multiset[sum]类似于set[union]：[sum a b]包含[a]和[b]的所有元素。（数学家通常在多集上对[union]的定义稍有不同——使用max而不是sum——这就是为什么我们不将此操作称为[union]）对于[sum]，我们给您提供了一个标头，它不为参数提供显式名称。此外，它使用关键字[Definition]而不是[Fixpoint]，因此即使您有参数的名称，也无法递归地处理它们。用这种方式表述这个问题的目的是鼓励您思考[sum]是否可以用另一种方式实现——也许可以使用一个或多个已经定义的函数。

30: 3 stars, standard, especially useful (bag_functions)

完成以下函数的定义

bags的[计数]、[总和]、[添加]和[成员]。）

Fixpoint count

Fixpoint count (v : nat) (s : bag) : nat
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Coq代码

Fixpoint count (v : nat) (s : bag) : nat:=
match s with
|nil => O
|h ::t =>if h =? v then S (count v t)
          else count v t
end.
(** All these proofs can be done just by [reflexivity]. *)

Example test_count1:              count 1 [1;2;3;1;4;1] = 3.
Proof. reflexivity. Qed.
Example test_count2:              count 6 [1;2;3;1;4;1] = 0.
Proof. reflexivity. Qed.

Definition sum

Definition sum : bag -> bag -> bag
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_sum1:              count 1 (sum [1;2;3] [1;4;1]) = 3.
 (* FILL IN HERE *) Admitted.

Coq代码

Definition sum : bag -> bag -> bag:=
app.

Example test_sum1:              count 1 (sum [1;2;3] [1;4;1]) = 3.
Proof. reflexivity. Qed.

Definition add

Definition add (v : nat) (s : bag) : bag
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_add1:                count 1 (add 1 [1;4;1]) = 3.
 (* FILL IN HERE *) Admitted.
Example test_add2:                count 5 (add 1 [1;4;1]) = 0.
 (* FILL IN HERE *) Admitted.

Coq代码

Definition add (v : nat) (s : bag) : bag:=
v :: s.

Example test_add1:                count 1 (add 1 [1;4;1]) = 3.
Proof. reflexivity. Qed.
Example test_add2:                count 5 (add 1 [1;4;1]) = 0.
Proof. reflexivity. Qed.

Definition member

Definition member (v : nat) (s : bag) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_member1:             member 1 [1;4;1] = true.
 (* FILL IN HERE *) Admitted.

Example test_member2:             member 2 [1;4;1] = false.
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint member' (v : nat) (s : bag) : bool :=
match s with
|nil => false
|h :: t =>if h=? v then true
             else member' v t
end.

Definition member (v : nat) (s : bag) : bool :=
member' v s.

Example test_member1:             member 1 [1;4;1] = true.
Proof. reflexivity. Qed.

Example test_member2:             member 2 [1;4;1] = false.
Proof. reflexivity. Qed.

31: 3 stars, standard, optional (bag_more_functions)

这里有一些更多的bag功能供您练习。

当将“移除”应用于没有要移除的编号的bag时，应将相同的bag原封不动地返回。（此练习是可选的，但是学习高级课程的学生需要在以后的练习中填写remove_one的定义。）

Fixpoint remove_one (v : nat) (s : bag) : bag

Fixpoint remove_one (v : nat) (s : bag) : bag
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_remove_one1:
  count 5 (remove_one 5 [2;1;5;4;1]) = 0.
  (* FILL IN HERE *) Admitted.
Example test_remove_one2:
  count 5 (remove_one 5 [2;1;4;1]) = 0.
  (* FILL IN HERE *) Admitted.
Example test_remove_one3:
  count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
  (* FILL IN HERE *) Admitted.
Example test_remove_one4:
  count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
  (* FILL IN HERE *) Admitted.

Coq代码

Fixpoint remove_one (v : nat) (s : bag) : bag :=
match s with
|nil => nil
|h :: t => if h =? v then t
          else h :: remove_one v t
end.

Example test_remove_one1:
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.

Example test_remove_one2:
count 5 (remove_one 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.

Example test_remove_one3:
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
Proof. simpl. reflexivity. Qed.

Example test_remove_one4:
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
Proof. reflexivity. Qed.

Fixpoint remove_all (v:nat) (s:bag) : bag

Fixpoint remove_all (v:nat) (s:bag) : bag
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_remove_all1: count 5 (remove_all 5 [2;1;5;4;1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all2: count 5 (remove_all 5 [2;1;4;1]) = 0.
(* FILL IN HERE *) Admitted.
Example test_remove_all3: count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
(* FILL IN HERE *) Admitted.
Example test_remove_all4: count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
(* FILL IN HERE *) Admitted.

Coq代码

Fixpoint remove_all (v:nat) (s:bag) : bag :=
match s with
|nil => nil
|h :: t => if h =? v then remove_all v t
          else h :: remove_all v t
end.
   
Example test_remove_all1:  count 5 (remove_all 5 [2;1;5;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all2:  count 5 (remove_all 5 [2;1;4;1]) = 0.
Proof. reflexivity. Qed.
Example test_remove_all3:  count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
Proof. reflexivity. Qed.
Example test_remove_all4:  count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
Proof. reflexivity. Qed.

Fixpoint subset (s1 : bag) (s2 : bag) : bool

Fixpoint subset (s1 : bag) (s2 : bag) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Example test_subset1: subset [1;2] [2;1;4;1] = true.
 (* FILL IN HERE *) Admitted.
Example test_subset2: subset [1;2;2] [2;1;4;1] = false.
 (* FILL IN HERE *) Admitted.

Coq代码

 Fixpoint subset (s1 : bag) (s2 : bag) : bool:=
match s1,s2 with
|nil,nil => true
|nil,h::t => true
|h'::t',nil => false
|h''::t'',h'''::t''' => if member h'' s2 then subset t'' (remove_one h'' s2) 
else false
end.

Example test_subset1:  subset [1;2] [2;1;4;1] = true.
Proof. simpl. reflexivity. Qed.
Example test_subset2:  subset [1;2;2] [2;1;4;1] = false.
Proof. simpl. reflexivity. Qed.

32: 2 stars, standard, especially useful (add_inc_count)

向bag中添加值应将该值的计数增加1。把它作为一个定理陈述并证明它。

(*
Theorem bag_theorem : ...
Proof.
...
Qed.
*)
(* Do not modify the following line: *)
Definition manual_grade_for_add_inc_count : option (nat×string) := None.

【Coq】11 Lists II 数字表

数字表 Lists of Numbers

Inductive natlist

Definition mylist

Notation "x :: l"

Notation "[ ]"

Notation "[ x ; .. ; y ]"

重复 Repeat

Fixpoint repeat

长度 Length

Fixpoint length

追加 Append

Fixpoint app

Notation "x ++ y"

从头到尾 Head and Tail

Definition hd

Definition tl

Exercises

28: 2 stars, standard, especially useful (list_funs)

Fixpoint nonzeros

Coq代码

Fixpoint oddmembers

Coq代码

Definition countoddmembers

Coq代码

29: 3 stars, advanced (alternate)

Coq代码

Bags via Lists

30: 3 stars, standard, especially useful (bag_functions)

Fixpoint count

Coq代码

Definition sum

Coq代码

Definition add

Coq代码

Definition member

Coq代码

31: 3 stars, standard, optional (bag_more_functions)

Fixpoint remove_one (v : nat) (s : bag) : bag

Coq代码

Fixpoint remove_all (v:nat) (s:bag) : bag

Coq代码

Fixpoint subset (s1 : bag) (s2 : bag) : bool

Coq代码

32: 2 stars, standard, especially useful (add_inc_count)

Coq代码