Trivialities about lists

Stream: Is there code for X?

[Martin Dvořák]

Do we have them?

import Mathlib

variable {α : Type}

lemma nmem_replicate_of_neq {a b : α} (hab : a ≠ b) (n : ℕ) :
    a ∉ List.replicate n b := by
  sorry

open scoped List

lemma sublist_append_nmem_left {d : α} {l x y : List α}
    (dnix : d ∉ x) (subl : d :: l <+ x ++ y) :
    d :: l <+ y := by
  sorry

[Damiano Testa]

I could not find them (which does not mean much), but discovered docs#List.replicate_subset_singleton which gives this proof for the first:

lemma nmem_replicate_of_neq {a b : α} (hab : a ≠ b) (n : ℕ) :
    a ∉ List.replicate n b := by
  apply Set.not_mem_subset (List.replicate_subset_singleton n b)
  erw [List.mem_singleton]
  assumption

where

• apply cannot be changed to refine,
• erw cannot be changed to rw.

This makes me suspect that something weird is going on.

[Timo Carlin-Burns]

nmem_replicate_of_neq is the contrapositive of docs#eq_of_mem_replicate

[Martin Dvořák]

Oh there is also docs#List.mem_replicate for the most general statement.

[Kevin Buzzard]

Damiano Testa said:

I could not find them (which does not mean much), but discovered docs#List.replicate_subset_singleton which gives this proof for the first:

lemma nmem_replicate_of_neq {a b : α} (hab : a ≠ b) (n : ℕ) :
    a ∉ List.replicate n b := by
  apply Set.not_mem_subset (List.replicate_subset_singleton n b)
  erw [List.mem_singleton]
  assumption

where

• apply cannot be changed to refine,
• erw cannot be changed to rw.

This makes me suspect that something weird is going on.

The proof abuses defeq: List.replicate_subset_singleton n b uses \subseteq on lists, but you're using Set.not_mem_subset on it, which expects \subseteq on sets. Everything is thus unfolded and the chaos thus ensues.

import Mathlib

variable {α : Type*}

lemma List.not_mem_subset {α : Type*} {a : α} {s t : List α} (h : s ⊆ t) (ha : a ∉ t) : a ∉ s := by
  sorry

lemma nmem_replicate_of_neq {a b : α} (hab : a ≠ b) (n : ℕ) :
    a ∉ List.replicate n b := by
  refine List.not_mem_subset (List.replicate_subset_singleton n b) ?_
  rw [List.mem_singleton]
  assumption

[Damiano Testa]

Kevin, thanks: I had completely overlooked the Set namespace! Now everything is clear!

[Martin Dvořák]

Here is a proof of the second lemma:

lemma List.sublist_append_nmem_left {α : Type} {d : α} {l x y : List α}
    (dnix : d ∉ x) (subl : d :: l <+ x ++ y) :
    d :: l <+ y := by
  induction x with
  | nil => exact subl
  | cons a _ ih =>
    apply ih (dnix ∘ List.Mem.tail a)
    cases subl <;> aesop

Do we want it in Mathlib?

[Yaël Dillies]

Surely that can be made an iff?

[Martin Dvořák]

Yes! Do you want to suggest a name for it?

[Yaël Dillies]

List.cons_sublist_append_iff_right?

[Martin Dvořák]

Did you intentionally avoid d ∉ x in the lemma name?

[Yaël Dillies]

I think it's pretty clear from context but could be added if disambiguation is needed

[Martin Dvořák]

All right, I'll use the name you suggested.

[Martin Dvořák]

#10629

[Eric Wieser]

Can you add a more general version, (h : l₂.Disjoint l₄) (h' : l₂ ≠ []) : l₁ ++ l₂ <+ l₃ ++ l₄ ↔ l₁ ++ l₂ <+ l₃?

[Eric Wieser]

(and then the obvious symmetric version)

[Martin Dvořák]

docs#List.Disjoint

[Eric Wieser]

I guess ¬l₂ <+ l₄ and ¬l₄ <+ l₂ would be a tighter constraint

[Martin Dvořák]

Eric Wieser said:

Can you add a more general version

Maybe in addition to my lemma, not as its replacement. Even when I add both

lemma lllllllllllll {l₃ l₄ : List α} (h : l₂.Disjoint l₄) (h' : l₂ ≠ []) :
    l₁ ++ l₂ <+ l₃ ++ l₄ ↔ l₁ ++ l₂ <+ l₃ :=
  sorry

lemma llllllllllllll {l₃ l₄ : List α} (h : l₁.Disjoint l₃) (h' : l₁ ≠ []) :
    l₁ ++ l₂ <+ l₃ ++ l₄ ↔ l₁ ++ l₂ <+ l₄ :=
  sorry

exact? still won't solve my original problem.

[Eric Wieser]

Indeed, I'm suggesting you add those lemmas to provide a one- or two- line proof of your version

[Martin Dvořák]

Eric Wieser said:

I guess ¬l₂ <+ l₄ and ¬l₄ <+ l₂ would be a tighter constraint

What about them?

[Eric Wieser]

They should work instead of l₂.Disjoint l₄, right?

[Patrick Massot]

Aren't all those list lemmas better suited for Std than for Mathlib?

[Eric Wieser]

It's probably more pleasant to prove them in mathlib first, then check if they still compile in Std once you're done