Proving Simple Lemma for Lists

Stream: Is there code for X?

[Ramneet Singh]

I have the following goal state:

T: Type
 a b: list T
c d: T
h: [d] = a ++ [c] ++ b
⊢ a = list.nil \and b = list.nil \and c=d

What tactic or theorem can I use? This seems like it should be easy to show but I haven't been able to.

[Ramneet Singh]

I have written the following proof:

variable {T : Type}

lemma singleton_length_one (a : T) : [a].length=1 := by
{
  apply (iff.elim_right (list.length_eq_one)),
  use a,
}

lemma singleton_eq_append_implies_empty (a b: list T) (c d : T) : ([d] = a ++ [c] ++ b) → (a = []) := by
  {
    intro h,
    have h1 : (a ++ [c] ++ b).length = a.length + 1 + b.length := by
    {
      rw list.length_append (a ++ [c]) b,
      rw list.length_append a [c],
      have h2 : [c].length=1 := singleton_length_one c,
      rw h2,
    },
    have h2 : [d].length=1 := singleton_length_one d,
    have h3 : [d].length = (a ++ [c] ++ b).length := by {exact congr_arg list.length h},
    rw h2 at h3,
    rw h1 at h3,
    have h4 : a.length=0 := by
    {
      have h5 := iff.elim_left nat.add_eq_one_iff (iff.elim_left eq_comm h3),
      cases h5,
      {
        by_contra,
        have h6 := and.elim_left h5,
        have h7 : a.length + 1 > 0 := by {exact ne_zero.pos (list.length a + 1),},
        have h8 : ¬ (a.length + 1 = 0) := by {exact ne_of_gt h7,},
        exact h (false.rec (list.length a = 0) (h8 h6)),
      },
      {
        have h6 := and.elim_left h5,
        exact nat.succ.inj h6,
      },
    },
    exact list.length_eq_zero.mp h4,
  }

I would be grateful if someone could review this and suggest improvements to the tactics/style.

[Ruben Van de Velde]

How about this

lemma singleton_eq_append_implies_empty (a b: list T) (c d : T) : ([d] = a ++ [c] ++ b) → (a = []) := by
  {
    intro h,
    rw [←list.length_eq_zero, ←le_zero_iff],
    apply_fun list.length at h,
    simp only [list.length_append, list.length_singleton, list.append_assoc, list.singleton_append] at h,
    apply le_of_add_le_add_right,
    rw [←h],
    simp,
  }

[Ruben Van de Velde]

And fwiw, docs#list.length_singleton

[Martin Dvořák]

I should probably refactor and generalize my lemma:
https://github.com/madvorak/grammars/blob/93af02643431b3165b19594415c40b80eaa987ae/src/classes/unrestricted/closure_properties/star.lean#L1424

[Martin Dvořák]

Also, since you will be working with triples of lists in your project, have a look at this section:
https://github.com/madvorak/grammars/blob/93af02643431b3165b19594415c40b80eaa987ae/src/utilities/list_utils.lean#L26

[Ramneet Singh]

Thanks @Ruben Van de Velde and @Martin Dvořák ! This helps a lot :))