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.

Fixpoint repeat_n_add (l:list nat):list nat:=

match l with

|[] => []

|n::l' => n_add_nat n (repeat_n_add l')

end.

Compute repeat_n_add [1;2;3;2].

Compute repeat_n_add [1;2;3;2;2].

Lemma repeat_n_add_same: forall (l:list nat),

repeat_n_add (l ++ l) = [].

Admitted.

======================================================

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.

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

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

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

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]
Compute repeat_n_add [1;2;3;5;2;2;2;4;4;4;4;5;5] => [5;3;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.
Admitted.
Lemma Even_Odd_dec n : {Nat.Even n} + {Nat.Odd n}.
Admitted.
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.
Admitted.
Lemma L2 : forall l x, Nat.Even (count_occ Nat.eq_dec (l++l) x).
Admitted.
Lemma L3: forall l, repeat_n_add (l++l)= [].
Admitted.
```

Note: In your definition of `n_add_nat`

, you may use `Nat.eq_dec`

(more informative than

`Nat.eqb`

).

yicx has marked this topic as resolved.

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

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_occ`

and arithmetic :smile: . Note that `L2`

is based on a diagonalization of stdlib's `List.count_occ_app`

.

Last updated: Jun 24 2024 at 12:02 UTC