Доказательство - 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.

coq proof
person Khan    schedule 18.06.2012    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вот фрагмент, который показывает, как решить аналогичную цель.

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.

Однако, вероятно, лучше разделить гипотезы, как это сделал я, если только вы обычно не манипулируете такими связями. В противном случае союзы будут мешать доказательствам, и вам всегда придется их разрушать / строить.

РЕДАКТИРОВАТЬ: Поскольку я не разъяснил, вам не нужна индукция для этого доказательства. Вам нужно будет использовать индукцию, если вы указали цель, которая требует, например, проведения рекурсивного анализа случаев в форме списка строк.

person Ptival    schedule 18.06.2012
comment
Это большая помощь. Спасибо, Роберт. - person Khan; 18.06.2012