Hi everyone,

I want to prove the lemma `seq_equality_problem`

but I feel list induction is not sufficient and I need a more general set induction principal. One reason to think about this is that according my definition of `set_eq`

: `[(1, 2)] and [(1, 2); (1, 2); (1, 2)] (duplication)`

are same, `[(1, 2); (2, 3); (3, 4)] and [(3, 4); (1, 2); (2, 3)] (permutation)`

. Any idea how to prove it?

```
From Coq Require Import List.
Require Import Utf8.
Definition subset (l₁ l₂ : list (nat * nat)) : Prop :=
∀ x, In x l₁ -> In x l₂.
Definition set_eq (l₁ l₂ : list (nat * nat)) : Prop :=
subset l₁ l₂ ∧ subset l₂ l₁.
Fixpoint elim_dup (p1 : nat * nat) (l : list (nat * nat)) :=
match l with
| nil => p1 :: nil
| p2 :: l' =>
match p1, p2 with
| (s1, t1), (s2, t2) =>
if Nat.eqb s1 s2 then
elim_dup (s1, Nat.add t1 t2) l'
else p2 :: elim_dup p1 l'
end
end.
Lemma seq_equality_problem :
forall X Y p, set_eq X Y ->
set_eq (elim_dup p X) (elim_dup p Y).
Proof.
induction X as [|(au, bu) X Ihx].
+ intros [|(ya, yb) Y] (pa, pb) Ha;
simpl.
++ (* easy *)
admit.
++ (* false *)
admit.
+ intros [|(ya, yb) Y] (pa, pb) Ha;
simpl.
++ (* false from Ha *)
admit.
++ unfold set_eq in * |- *.
split.
destruct Ha as [Hal Har].
```

@Mukesh Tiwari is there an obvious reason why it has to be proven in this order and this way? The usual approach would be to prove a lemma:

```
forall x X p, In x X <-> In x (elim_dup p x)
```

(or similar) and then use this to prove the `set_eq`

.

@Karl Palmskog Thanks Karl! My lemma is not true, when `p`

happens to be a member of `X`

.

```
Let X := [(1, 2)].
Let Y := [(1, 2); (1, 2); (1, 2)].
Lemma eq_proof_x_y : set_eq X Y.
Proof.
unfold set_eq, subset, X, Y;
cbn; split; firstorder.
Qed.
Lemma eq_proof_elim_dup :
~set_eq (elim_dup (1, 2) X) (elim_dup (1, 2) Y).
Proof.
intro H.
unfold set_eq, subset, X, Y in H;
cbn in H; firstorder.
pose proof (H (1, 4) (or_introl eq_refl)).
destruct H1.
congruence.
exact H1.
Qed.
```

I suppose the induction you want is the one where we only add new elements to the list. But:

- This principle must be restricted to properties that are compatible with
`set_eq`

, and proved with the standard list induction. - to prove that something is compatible with
`set_eq`

, you will also need the regular list induction principle.

Here you are proving that`elim_dup`

is compatible with`eq_dec`

, thus it must be done with the standard list induction principle.

Moreover your theorem is not true as stated: counter-example `In x (elim_dup x nil)`

is true (because `elim_dup x nil`

reduces to `[x] (which os probably what you want to change)`

, whereas `In x nil`

is false.

Last updated: Jan 27 2023 at 01:03 UTC