Prove a property of finding the same elements in two lists

Question

I'm new to Coq. I have a function findshare which finds the same elements in two lists. Lemma sameElements proves that the result of function findshare on the concatenation of two lists is equal to the concatenation of the results of the function applied to each one of them. I'm a bit stuck in proving lemma 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

You are having trouble because the statement you have is not quite correct: it entails a contradiction. More precisely, it implies that [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.

You should be able to prove the lemma by swapping tl with l1, l2 and l1 ++ l2, and proceeding by induction on l1.