## Stream: Coq users

### Topic: Induction Principal for Set, represented by list.

#### Mukesh Tiwari (Dec 01 2022 at 08:33):

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 *)
++ (* false *)
+ intros [|(ya, yb) Y] (pa, pb) Ha;
simpl.
++ (* false from Ha *)
++ unfold set_eq in * |- *.
split.
destruct Ha as [Hal Har].
``````

#### Karl Palmskog (Dec 01 2022 at 08:42):

@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`.

#### Mukesh Tiwari (Dec 01 2022 at 09:38):

@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.
``````

#### Pierre Courtieu (Dec 01 2022 at 09:42):

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: Jun 18 2024 at 08:01 UTC