基於函數暗示證明引理

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。節奏緩慢，非常教學。