Доказательство другого свойства нахождения тех же элементов в списках

Question

После моего вопроса здесь у меня есть функция 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 списков, чтобы доказать лемму keepnotEmpty.

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.