coq - 在列表中查找正常工作的定理

Question

我正在证明关于在列表中查找的定理。我一直在证明，如果你真的发现了什么，那么它就是真的。什么样的引理或策略可能有助于证明这类定理？我的意思是，在这种情况下，列表上的归纳似乎是不够的。但是这个定理仍然是肯定的。

(*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.

（这是 HOL4 定义的翻译，也缺少这种定理）

定理的 HOL 版本：

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

Answer 1

看起来您缺少的是一个相关的等式P a0及其破坏值。这可以通过那里 destruct (P a0) eqn:H记录的 destruct 变体获得。

Answer 2

在证明您的定理之前，您可能想尝试加强该属性。使用 SSReflect 证明语言，您可以尝试以下路线。

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. 

我相信有更短的证明；）