Proof - Coq - Do I need induction?

Question

I have a scenario where I want to prove a lemma including a number of string and list variables. Probably, it needs 'induction', but can anybody help me proving the lemma given below. If the rest of code is needed, I can provide that too.

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

Here is a snippet that shows how to solve a similar goal.

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.

It is a really simple proof: just unfold the definition of DLVRI, and rewrite with hypotheses.

None that I replaced the hypothesis (TestA IA FA) = true /\ (TestC ICL FCL) = true /\ (TestD IT IUL FUL FTL) = true by three hypotheses. If you do not wish to do that, then the proof becomes:

intros ???????? HYP. destruct HYP as [TA [TC TD]]. unfold DLVRI. rewrite TA, TC, TD. reflexivity.

However, it is probably better style to separate the hypotheses as I did, unless you usually manipulate such conjuctions. Otherwise, conjunctions get in the way of proofs and you always have to destruct/construct them.

---

EDIT: Since I didn't make it clear, you do not need induction for this proof. You would need to use induction if you stated a goal that needed to do recursive case analysis on the shape of a string list for instance.