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

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.

Answer 2

You may want to try to strengthen the property before proving your theorem. Using the SSReflect proof language, you can try the following route.

Lemma index_find_prop {a:Type} P (x:a) l : 
  forall i j, (INDEX_FIND i P l) = Some (j, x) -> P x = true.
Proof. 
elim: l => [//=|x' l' IH i j].
rewrite /INDEX_FIND.
case Px': (P x').
- by case=> _ <-.
- exact: IH. 
Qed.

Lemma opt_snd_inv A B X x :
  option_map (@snd A B) X = Some x -> exists j, X = Some (j, x).
Proof.
case: X => ab; last by [].
rewrite (surjective_pairing ab) /=.
case=> <-.
by exists ab.1.
Qed.

Theorem find_prop {a:Type} P l (x:a):
  (FIND P l) = Some x -> (P x)=true.
Proof.
rewrite /FIND => /(@opt_snd_inv _ _ (INDEX_FIND 0 P l) x) [j].
exact: index_find_prop. 
Qed. 

I'm confident there are shorter proofs ;)