## Stream: Coq users

### Topic: ✔ need some help with a simpl proof

#### yicx (Nov 06 2022 at 21:55):

Hi,

Here is that part:
======================================================
Fixpoint n_add_nat (n:nat) (l:list nat) : list nat :=
match l with
| nil => n :: nil
| n' :: l' =>
if Nat.eqb n n'
then l'
else n' :: n_add_nat n l'
end.

match l with
|[] => []
end.

repeat_n_add (l ++ l) = [].
======================================================

n_add_nat: add a nat into a list, if it is already in the list delete that one, if it is not in the list , add the number to the list
repeat_n_add: recursively did the same thing to all the element.

e.g.

repeat_n_add_same: for any arbitrary list, doing repeat_n_add(l ++ l) we get nothing

I have been stuck on this for a while, I think this is true but I cannot process further in coq, can anyone drop a hint?

Many thanks

#### Pierre Castéran (Nov 07 2022 at 09:12):

Hi, @yicx, I'm not sure it's just a simple proof.
After a few tests, I proved that repeat_n_add l returns a (duplicate-free) list of numbers which occurr an odd number of times in l (the order of enumeration doesn't matter).

Compute repeat_n_add [1;2;3;2;2;4;5;5] => [4; 3; 2; 1]

Note that this property trivially implies your lemma. Here is a skeleton of the proof ( Admitted means Exercise).

Lemma L0 : forall l x y,
count_occ Nat.eq_dec (n_add_nat y l) x =
if Nat.eq_dec y x
then match count_occ Nat.eq_dec l x with
0 => 1
| S p => p
end
else  count_occ Nat.eq_dec l x.

Lemma Even_Odd_dec n : {Nat.Even n} + {Nat.Odd n}.

Lemma L1 l:
forall x, count_occ Nat.eq_dec (repeat_n_add l) x =
if Even_Odd_dec (count_occ Nat.eq_dec l x)
then 0
else 1.

Lemma L2 : forall l x, Nat.Even (count_occ Nat.eq_dec (l++l) x).

Lemma L3: forall l, repeat_n_add (l++l)= [].

Nat.eqb).

#### Notification Bot (Nov 09 2022 at 21:37):

yicx has marked this topic as resolved.

#### yicx (Nov 09 2022 at 21:37):

thank you, the idea that I can find some way other than induction is more than enough, have a wonderful day!

#### Pierre Castéran (Nov 10 2022 at 06:21):

yicx said:

thank you, the idea that I can find some way other than induction is more than enough, have a wonderful day!

You're welcome. To be precise, induction is massively used in the proof of lemmas L0 to L3.
It’s very usual, when stuck in an attempt to prove simply a property by induction, to prove (often by induction) a more general property.

Indeed, in the proof of your lemma, every attempt based on the idea "every x in l is cancelled by
the same x in the second copy of l" failed (not compatible with your function). :thinking: . Hence the idea to use count_occand arithmetic :smile: . Note that L2is based on a diagonalization of stdlib's List.count_occ_app.

Last updated: Dec 05 2023 at 04:01 UTC