coq - Theorem that finding in a list works properly

Question

I am proving theorem about finding in a list. I got stuck at proving that if you actually found something then it is true. What kind of lemmas or strategy may help for proving such kind of theorems? I mean it looks like induction on the list is not enough in this case. But still the theorem is surely true.

(*FIND P = OPTION_MAP (SND :num # α -> α ) ° INDEX_FIND (0 :num) P*)
Require Import List.
Require Import Nat.

Fixpoint INDEX_FIND {a:Type} (i:nat) (P:a->bool) (l:list a) :=
match l with 
| nil => None
| (h::t) => if P h then Some (i,h) else INDEX_FIND (S i) P t
end.

Definition FIND {a:Type} (P:a->bool) (l:list a)
:= (option_map snd) (INDEX_FIND 0 P l).

Theorem find_prop {a:Type} P l (x:a):
(FIND P l) = Some x 
->
(P x)=true.
Proof.
unfold FIND.
unfold option_map.
induction l.
+ simpl.
  intro H. inversion H.
+ simpl.
  destruct (P a0).
  - admit.
  - admit.
Admitted.

(this is a translation of definition from HOL4 which also lacks such kind of theorem)

HOL version of the theorem:

Theorem find_prop:
FIND (P:α->bool) (l:α list) = SOME x ? P x
Proof
  cheat
QED

question from:https://stackoverflow.com/questions/65843830/theorem-that-finding-in-a-list-works-properly

Answer 1

It looks like what you are missing is an equation relating P a0 and its destructed value. This can be obtained with the variant of destruct documented there destruct (P a0) eqn:H.