证明在列表中找到相同元素的另一个属性

Question

根据我的问题here，我有一个函数findshare，它可以在两个列表中找到相同的元素。实际上，keepnotEmpty 是我在对引理sameElements 的初始版本进行了一些更改之后在我的程序中需要的引理。引理keepnotEmpty 证明如果函数findshare 在两个列表的串联上的结果不为空，那么应用于每个列表的函数结果的串联也不为空。我很困惑如何证明引理keepnotEmpty。谢谢。

Require Import List .
Import ListNotations.
Fixpoint findshare(s1 s2: list nat): list nat:=
      match s1 with
        | nil => nil
        | v :: tl =>
           if ( existsb  (Nat.eqb v)  s2)
            then v :: findshare tl s2
            else findshare tl s2
      end.
Lemma sameElements l1 l2 tl :
        (findshare(l1++l2) tl) =
         (findshare l1 tl) ++ (findshare l2 tl ).
  Proof.
  Admitted.

Lemma keepnotEmpty l1 l2 tl :
  (findshare tl (l1++l2)) <> nil -> (findshare tl (l1) ++ (findshare tl (l2))<>nil).
Proof.

Answer 1

您需要对列表的tl 和属性oneNotEmpty 进行归纳来证明lemmakeepnotEmpty。

Lemma oneNotEmpty (l1 l2:list nat):
l1<>nil -> (l2++l1)<>nil.
Proof.
Admitted.

 Lemma keepnotEmpty l1 l2 tl :
 (findshare tl (l1++l2))<> nil -> (findshare tl (l1) ++ (findshare tl (l2))<>nil).
Proof.
induction tl. simpl; intro. congruence.
simpl.
rewrite existsb_app. 
destruct_with_eqn(existsb (Nat.eqb a) l1).
destruct_with_eqn(existsb (Nat.eqb a) l2);
simpl; intros H1 H2;  congruence.
destruct_with_eqn(existsb (Nat.eqb a) l2).
simpl. intros. apply (oneNotEmpty);
intro. inversion H0.
simpl; assumption. 
Qed.