基于函数的隐含证明引理

Question

我想证明下面的引理。我正在尝试使用“破坏”策略，但我 无法证明。请任何人指导我如何证明这样的引理。我可以为 EmptyString 证明它，但不能为变量 s1 和 s2 证明。谢谢

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

  Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.

  Fixpoint CompStrings (sa : string) (sb : string) {struct sb}: bool :=
  match sa with
  | EmptyString => match sb with
                  | EmptyString => true
                  | String b sb'=> false
                  end
  | String a sa' => match sb with
                   | EmptyString => false
                   | String b sb'=> CompStrings sa' sb'
                   end
 end.

 Lemma Eq_lenght : forall (s1 s2 : string), 
                 (CompStrings s1 s2) = true -> (Eq_nat (length s1) (length s2)) = true.

Answer 1

首先，让我谈谈风格。您可以这样编写函数 CompStrings：

Fixpoint CompStrings' (sa : string) (sb : string) {struct sb}: bool :=
  match sa, sb with
  | EmptyString,  EmptyString => true
  | EmptyString,  _
  | _,            EmptyString => false
  | String a sa', String b sb'=> CompStrings sa' sb'
  end.

我觉得它更容易阅读。这是一个与你相同的证据，以防你怀疑：

Theorem CompStrings'ok: forall sa sb, CompStrings sa sb = CompStrings' sa sb.
Proof.
  intros. destruct sa, sb; simpl; reflexivity.
Qed.

---

现在，这将是一个双重答案。首先，我将向您提示证明的方向。然后，我会给你一个完整的证据，我鼓励你在自己尝试之前不要阅读。

首先，我假设 length 的这个定义，因为你没有提供它：

Fixpoint length (s: string): nat :=
  match s with
  | EmptyString => O
  | String _ rest => S (length rest)
  end.

因为我也没有 Eq_nat，所以我继续证明长度在命题上是相等的。适应 Eq_nat 应该相当简单。

Lemma Eq_length' : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  induction s1.
  (* TODO *)
Admitted.

所以这里是开始！您想证明关于归纳数据类型字符串的属性。问题是，您将希望通过案例分析继续进行，但如果您只使用destructs 进行分析，它将永远不会结束。这就是我们继续使用induction 的原因。也就是说，您需要证明 if s1 is the EmptyString, then the property holds 和 if the property holds for a substring, then it holds for the string with one character added。这两种情况都比较简单，在每种情况下都可以在 s2 上进行案例分析（即使用destruct）。

请注意，我在做induction s1. 之前没有做intros s1 s2 C.。这是相当重要的一个原因：如果你这样做（尝试！），你的归纳假设将受到太多限制，因为它会谈论一个特定的s2，而不是被它量化。当您开始通过归纳进行证明时，这可能会很棘手。所以，一定要尝试继续这个证明：

Lemma Eq_length'_will_fail : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  intros s1 s2 C. induction s1.
  (* TODO *)
Admitted.

最终，您会发现您的归纳假设无法应用于您的目标，因为它涉及到一个特定的s2。

---

我希望你已经尝试过这两个练习。

现在，如果您遇到困难，这里有一种方法可以证明第一个目标。

不要作弊！ :)

Lemma Eq_length' : forall (s1 s2 : string),
  CompStrings s1 s2 = true ->
  length s1 = length s2.
Proof.
  induction s1.
  intros s2 C. destruct s2. reflexivity. inversion C.
  intros s2 C. destruct s2. inversion C. simpl in *. f_equal.
  exact (IHs1 _ C).
Qed.

用通俗易懂的话来说：

• 让我们通过对 s1 的归纳来证明属性 forall s2, CompStrings s1 s2 = true -> length s1 = s2：

  • 在s1是EmptyString的情况下，我们看看s2的形状：

    1. s2是EmptyString，那么两个长度都等于0，所以reflexivity.；

    2. s2是String _ _，所以假设存在矛盾，如inversion C.所示；

  • 在 s1 是 String char1 rest1 的情况下，让我们看看 s2 的形状，假设其余属性为 true：

    1. s2是EmptyString，所以假设存在矛盾，由inversion C.表示；

    2. s2 是String char2 rest2，然后是length s1 = S (length rest1) 和length s2 = S (length rest2)，因此我们需要证明S (length rest1) = S (length rest2)。此外，假设 C 简化为C: CompStrings rest1 rest2 = true。这是使用归纳假设证明length rest1 = length rest2，然后以某种方式使用该结果来证明目标的最佳时机。

请注意，对于最后一步，有很多方法可以继续证明 S (length rest1) = S (length rest2)。其中之一是使用f_equal.，它要求您证明构造函数的参数之间的成对相等。您也可以使用rewrite (IHs1 _ C).，然后在该目标上使用自反性。

希望这不仅可以帮助您解决这个特定目标，还可以帮助您初步了解归纳证明！

---

要结束这一点，这里有两个有趣的链接。

This presents the basics of induction (see paragraph "Induction on lists").

This explains, better than me, why and how to generalize your induction hypotheses. 你将学习如何解决我在intros s1 s2 C. 所做的目标，方法是在开始归纳之前将s2 放回目标中，使用策略generalize (dependent)。

一般来说，我建议阅读whole book。它节奏缓慢，非常具有指导意义。