✔ need some help with a simpl proof · Coq users

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.

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?

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]
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).

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

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):

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.

Stream: Coq users

Topic: ✔ need some help with a simpl proof

yicx (Nov 06 2022 at 21:55):

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

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

yicx (Nov 09 2022 at 21:37):

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