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

Question

Я новичок в Coq.У меня есть функция findshare, которая находит одинаковые элементы в двух списках.Лемма sameElements доказывает, что результат функции findshare при конкатенации двух списков равен конкатенации результатов функции, примененной к каждому из них.Я немного застрял в доказательстве леммы sameElements.

Require Import List .
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 tl (l1++l2)) =
  (findshare tl (l1))++ (findshare tl (l2)).
Proof.

Answer 1

У вас проблемы, потому что ваше утверждение не совсем верно: оно влечет за собой противоречие.Точнее, это означает, что [1; 2] = [2; 1]:

Require Import List .
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 tl (l1++l2)) =
  (findshare tl (l1))++ (findshare tl (l2)).
Admitted.

Import ListNotations.

Lemma contra : False.
Proof.
pose proof (sameElements [1] [2] [2;1]).
simpl in H.
discriminate.
Qed.

Вы должны быть в состоянии доказать лемму, поменяв местами tl с l1, l2 и l1 ++ l2 и действуя по индукции наl1.