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の定義を展開し、仮説を立てて書き直すだけです。

仮説を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.

ただし、通常そのような結合を操作しない限り、私が行ったように仮説を分離する方がおそらく良いスタイルです。そうしないと、接続詞が証明の邪魔になり、常にそれらを破壊/構築する必要があります。

編集：私はそれを明確にしなかったので、あなたはこの証明のために誘導を必要としません。たとえば、文字列リストの形状に対して再帰的なケース分析を行う必要があるという目標を述べた場合は、誘導を使用する必要があります。

于 2012-06-18T12:19:58.187 に答える