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

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: Oct 01 2023 at 18:01 UTC