基于函数暗示证明引理

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要么，我继续证明长度propositionally相等。适应Eq_nat应该是相当微不足道的。

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

所以这里是开始！你想证明一个关于归纳数据类型字符串的属性。事情是，你会希望通过案例分析来进行，但如果你只是用destruct这样做，它就永远不会结束。这就是我们继续执行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. 

要提出，在理解方面：

• 让我们通过归纳证明财产forall s2, CompStrings s1 s2 = true -> length s1 = s2上S1：

  • 在S1是EmptyString的情况下

    ，让我们看看s2的形状：

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

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

  • 在s1是String char1 rest1的情况下

    ，让我们来看看S2的形状，假设物业真正休息：

    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.您将学习如何解决，我通过将回到目标s2开始感应，使用战术generalize (dependent)以前那样intros s1 s2 C.的目标。

一般来说，我建议您阅读whole book。节奏缓慢，非常教学。