标识符

首先，我们需要一个用于索引到地图中的键的类型。在Lists.v中，我们为类似的目的引入了一个新的类型id；在这里以及其他软件基础中，我们将使用Coq标准库中的字符串类型。

为了比较字符串，我们定义了函数eqb_string，它在内部使用Coq的字符串库中的函数string_dec。

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

（函数string_dec来自Coq的字符串库。如果您检查string_dec的结果类型，您将看到它实际上并没有返回bool，而是返回一个类似{x = y} + {x <> y}的类型，称为sumbool，可以被认为是“携带证据的布尔值”。形式上，元素{x = y} + {x <> y}要么是证明x和y相等，要么是证明它们不相等，再加上一个标记，表明它们相等。但就目前而言，你可以把它看作是一个花哨的东西。）

现在我们需要一些字符串相等的基本属性。。。

Theorem eqb_string_refl : forall s : string, true = eqb_string s s.
Proof.
  intros s. unfold eqb_string.
  destruct (string_dec s s) as [Hs_eq | Hs_not_eq].
  - reflexivity.
  - destruct Hs_not_eq. 
  reflexivity.
Qed.

两个字符串根据eqb_string相等，如果它们根据=。So=反映在eqb_string中，在IndProp中讨论的“反射”意义上。

Theorem eqb_string_true_iff : forall x y : string,
  eqb_string x y = true <-> x = y.
Proof.
  intros x y.
  unfold eqb_string.
  destruct (string_dec x y) as [Hs_eq | Hs_not_eq].
  - rewrite Hs_eq. 
  split. 
  reflexivity. 
  reflexivity.
  - split.
    + intros contra. 
    discriminate contra.
    + intros H. 
    exfalso. 
    apply Hs_not_eq. 
    apply H.
Qed.

同样地：

Theorem eqb_string_false_iff : forall x y : string,
  eqb_string x y = false <-> x <> y.
Proof.
  intros x y. 
  rewrite <- eqb_string_true_iff.
  rewrite not_true_iff_false. 
  reflexivity. 
  Qed.

这一推论只需重写即可得出：

Theorem false_eqb_string : forall x y : string,
  x <> y -> eqb_string x y = false.
Proof.
  intros x y. 
  rewrite eqb_string_false_iff.
  intros H. 
  apply H. 
  Qed.