2012-06-18 36 views
1

我有一个场景,我想证明一个引理,包括一些字符串和列表变量。可能它需要'归纳',但任何人都可以帮助我证明下面给出的引理。如果需要其他代码,我也可以提供。证明 - Coq - 我需要感应吗?

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. 

回答

0

这是一段代码,展示了如何解决类似的目标。

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。否则,连词妨碍了证明,你总是必须破坏/构造它们。


编辑:由于我没有说清楚,你不需要为这个证明感应。例如,如果您需要对字符串列表的形状进行递归案例分析,则需要使用归纳。

+0

它的帮助很大。谢谢罗伯特。 – Khan