Zulip Chat Archive

Stream: new members

Topic: Beginner question: list.diff

Martin Trifonov (Jan 28 2021 at 17:26):

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 (Jan 28 2021 at 17:30):

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

Martin Trifonov (Jan 28 2021 at 17:32):

Sure! I hope this helps

Eric Wieser (Jan 28 2021 at 17:33):

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 (Jan 28 2021 at 17:34):

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

Floris van Doorn (Jan 28 2021 at 18:33):

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 :=
  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 list

Floris van Doorn (Jan 28 2021 at 18:34):

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

Floris van Doorn (Jan 28 2021 at 18:42):


Martin Trifonov (Jan 28 2021 at 19:25):

amazing, thank you!

Last updated: Dec 20 2023 at 11:08 UTC