选项 Options

假设我们要编写一个函数，返回某个列表的第n个元素。如果我们给它类型nat→ natlist→ nat，那么当列表太短的时候，我们必须选择一些数字返回…

Fixpoint nth_bad

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

这个解决方案不太好：如果nth_bad返回42，我们无法在没有进一步处理的情况下判断该值是否实际出现在输入上。更好的替代方法是更改nth_bad的返回类型，以包含错误值作为可能的结果。我们称这种类型为natoption。

Inductive natoption

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

然后，当列表太短时，我们可以更改上面对nth_bad的定义，使其返回None；当列表有足够的成员且a出现在位置n时，可以更改为a。我们将这个新函数称为nth_error，以表明它可能导致错误。正如我们在这里看到的，归纳定义的构造函数可以大写。

Fixpoint 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'
             end
end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

（在HTML版本中，这些示例的样板示例被省略。如果您想查看，请单击方框。）

下面的函数将nat从natoption中拉出，在None情况下返回提供的默认值。

Definition option_elim

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

39: 2 stars, standard (hd_error)

使用相同的想法，修复前面的[hd]函数，这样我们就不必为[nil]情况传递默认元素。

Definition hd_error

Definition hd_error (l : natlist) : natoption
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_hd_error1 : hd_error [] = None.
(* FILL IN HERE *) Admitted.

Example test_hd_error2 : hd_error [1] = Some 1.
(* FILL IN HERE *) Admitted.

Example test_hd_error3 : hd_error [5;6] = Some 5.
(* FILL IN HERE *) Admitted.

Coq代码

Definition hd_error (l : natlist) : natoption:=
match l with
 | nil => None
 | h :: t =>Some h
 end.

Example test_hd_error1 : hd_error [] = None.
Proof. reflexivity. Qed.

Example test_hd_error2 : hd_error [1] = Some 1.
Proof. reflexivity. Qed.

Example test_hd_error3 : hd_error [5;6] = Some 5.
Proof. reflexivity. Qed.

40: 1 star, standard, optional (option_elim_hd)

此练习将新[hd_error]与旧[hd]关联起来。

Theorem option_elim_hd

Theorem option_elim_hd : forall (l:natlist) (default:nat),
hd default l = option_elim default (hd_error l).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem option_elim_hd : forall (l:natlist) (default:nat),
hd default l = option_elim default (hd_error l).
Proof.
intros l default. induction l as [| n l' IHl'].
- simpl. reflexivity.
- simpl. reflexivity.
Qed.