證明 - Coq - 我需要感應嗎？

Question

我有一個場景，我想證明一個引理，包括一些字符串和列表變量。可能它需要'歸納'，但任何人都可以幫助我證明下面給出的引理。如果需要其他代碼，我也可以提供。

Definition DLVRI (IA IT : string) 
       (FA ICL FCL IUL FUL FTL : strlist) : bool := 
match (TestA IA FA), 
     (TestC ICL FCL), 
     (TestD IT IUL FUL FTL) with 
| true, true, true => true 
| _ , _ , _ => false 
end.    

(** 
Lemma TestDL : forall (IA IT : string), 
       forall (FA ICL FCL IUL FUL FTL : strlist), 
       (TestA IA FA) = true /\ 
       (TestC ICL FCL) = true /\ 
       (TestD IT IUL FUL FTL) = true. 
Proof. 
*) 
    (* OR *) 

Lemma TestDL : forall (IA IT : string), 
       forall (FA ICL FCL IUL FUL FTL : strlist), 
       (TestA IA FA) = true /\ 
       (TestC ICL FCL) = true /\ 
       (TestD IT IUL FUL FTL) = true 
       -> DLVRI IA IT FA ICL FCL IUL FUL FTL = true. 

Answer 1

這是一段代碼，展示瞭如何解決類似的目標。

Require Import String. 

Parameter TestA: string -> list string -> bool. 
Parameter TestC: list string -> list string -> bool. 
Parameter TestD: string -> list string -> list string -> list string -> bool. 

Definition DLVRI (IA IT : string) 
    (FA ICL FCL IUL FUL FTL : list string) : bool := 
    match (TestA IA FA), (TestC ICL FCL), (TestD IT IUL FUL FTL) with 
    | true, true, true => true 
    | _ , _ , _ => false 
end. 

Lemma TestDL: 
    forall 
    (IA IT : string) 
    (FA ICL FCL IUL FUL FTL : list string), 
    TestA IA FA = true -> 
    TestC ICL FCL = true -> 
    TestD IT IUL FUL FTL = true -> 
    DLVRI IA IT FA ICL FCL IUL FUL FTL = true. 
Proof. 
    intros ???????? TA TC TD. unfold DLVRI. rewrite TA, TC, TD. reflexivity. 
Qed. 

這是一個非常簡單的證明：只是展開DLVRI的定義，並用假設重寫。

我沒有用假設3取代假設(TestA IA FA) = true /\ (TestC ICL FCL) = true /\ (TestD IT IUL FUL FTL) = true。如果你不希望這樣做，那麼證明變爲：

intros ???????? HYP. destruct HYP as [TA [TC TD]]. unfold DLVRI. rewrite TA, TC, TD. reflexivity. 

但是，它可能是更好的風格和我一樣的假設分開，除非你平時操縱這些conjuctions。否則，連詞妨礙了證明，你總是必須破壞/構造它們。

---

編輯：由於我沒有說清楚，你不需要爲這個證明感應。例如，如果您需要對字符串列表的形狀進行遞歸案例分析，則需要使用歸納。