Доказательство - 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 и перепишите гипотезы.

Ничего, что я заменил гипотезу (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.

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

---

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