Beginner question: list.diff

Stream: new members

[Martin Trifonov]

Hello all,
My name is Martin, I'm an undergraduate cs student at hu berlin, I'm new to lean and I'm trying to write a proof that has to do with list operations.
I am stuck and was wondering if anyone could help:
Given (a b : ℕ) (as bs : list ℕ) I am trying to prove the following:
((bs.erase a).diff as).erase b) = (((bs.erase a).erase b).diff as)

I am under the impression that this proposition is true, because of the following lemmas in mathlib:
list.diff_cons tells me that I should be able to expand out both sides of the equality into a long chain of erase operations:
something like
(((bs.erase a).erase a').erase a'' ... .erase b) = (((bs.erase a).erase b).erase a' ... .erase a'')
and list.erase_comm tells me that I'm free to change the order of the erase operations.

However, I don't know how to express this in lean.

[Eric Wieser]

Hi Martin - would you mind adjusting your message to use #backticks to make it easier to read?

[Martin Trifonov]

Sure! I hope this helps

[Eric Wieser]

Are you using #lean4 or lean 3? Nat makes it look like lean4, which probably won't have docs#list.erase_comm or docs#list.diff_cons yet...

[Martin Trifonov]

I'm using lean 3, I just wrote nat because I didn't know about the backticks ^^

[Floris van Doorn]

This seems to be a missing lemma about list.diff:

import data.list.basic

namespace list
variables {α : Type*} [decidable_eq α]
lemma diff_cons_right (l₁ l₂ : list α) (a : α) : l₁.diff (a::l₂) = (l₁.diff l₂).erase a :=
begin
  induction l₂ with b l₂ ih generalizing l₁ a,
  { simp_rw [diff_cons, diff_nil] },
  { rw [diff_cons, diff_cons, erase_comm, ← diff_cons, ih, ← diff_cons] }
end

end list

[Floris van Doorn]

This lemma gives you what you want, when combined with list.diff_cons

[Floris van Doorn]

#5941

[Martin Trifonov]

amazing, thank you!