1

我有一个场景，我想证明一个引理，包括许多字符串和列表变量。可能，它需要“归纳”，但任何人都可以帮助我证明下面给出的引理。如果需要其余代码，我也可以提供。

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.
4

1 回答 1

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 的定义，并用假设重写。

没有，我用(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.

然而，像我一样分开假设可能是更好的风格，除非你通常操纵这样的连词。否则，连词会妨碍证明，您总是必须破坏/构造它们。

编辑：由于我没有说清楚，因此您不需要对这个证明进行归纳。例如，如果您声明需要对字符串列表的形状进行递归案例分析的目标，则需要使用归纳法。

于 2012-06-18T12:19:58.187 回答