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
[(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
@Karl Palmskog Thanks Karl! My lemma is not true, when
p happens to be a member of
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:
set_eq, and proved with the standard list induction.
set_eq, you will also need the regular list induction principle.
elim_dupis 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