0

我想证明下面的引理。我正在尝试使用“破坏”策略，但我无法证明这一点。请任何人指导我如何证明这样的引理。我可以为 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.
4

1 回答 1

3

首先，让我争论风格。您可以这样编写函数 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）。

注意我之前没有intros s1 s2 C.做induction s1.。这是相当重要的一个原因：如果你这样做（尝试！），你的归纳假设将受到太多限制，因为它会谈论一个特定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 是 a String _ _，因此假设存在矛盾，由inversion C.;

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

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

      2. s2 是 a 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). 其中之一是 using f_equal.which 要求您证明构造函数的参数之间的成对相等。您也可以rewrite (IHs1 _ C).在该目标上使用 then use reflexivity。

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

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

这介绍了归纳的基础知识（参见“列表上的归纳”段落）。

这比我更好地解释了为什么以及如何概括你的归纳假设。您将学习如何解决我所做的目标，方法是在开始归纳之前intros s1 s2 C.放回s2目标中，使用 tactic generalize (dependent)。

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

于 2012-06-12T22:47:38.877 回答