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