Email Gateway (Mar 15 2021 at 13:37): Email Gateway (Mar 15 2021 at 13:37):From: Jakub Kądziołka <kuba@kadziolka.net>
Hello,
I have proven the following lemma, which splits the result of remove1
into the items before and after the removed element. I feel like it
might be generally useful.
lemma remove1_split:
assumes "a ∈ set xs"
shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r"
using assms proof (induction xs)
case (Cons x xs)
show ?case
proof cases
assume "x = a"
show ?thesis
apply (rule exI[of _ "[]"])
using x = a by simp
next
assume "x ≠ a"
then have "a ∈ set xs"
using a ∈ set (x # xs)
by simp
then obtain l r where *: "xs = l @ a # r ∧ remove1 a xs = l @ r"
using Cons.IH by auto
show ?thesis
apply (rule exI[of _ "x # l"])
apply (rule exI[of _ r])
using x ≠ a * by auto
qed
qed simp
Regards,
Jakub Kądziołka
Email Gateway (Mar 15 2021 at 14:36):From: Peter Lammich <lammich@in.tum.de>
Hello,
the lemma remove1_append is actually very similar, and sledgehammer
finds a very simple proof of your lemma:
lemma remove1_split:
assumes "a ∈ set xs"
shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r"
by (metis assms remove1.simps(2) remove1_append split_list_first)
This does not mean that this lemma is useless, as it may provide a
handier split than using remove1_append directly.
Email Gateway (Mar 16 2021 at 07:18):From: Tobias Nipkow <nipkow@in.tum.de>
I have added the lemma with Peter's/sh's proof. Although a simple consequence,
it does indeed look helpful.
Thanks
Tobias
smime.p7s
Last updated: Apr 19 2024 at 16:20 UTC