lists

Stream: general

[Andrew Ashworth]

theorem append_inj : ∀ {s₁ s₂ t₁ t₂ : list α}, s₁ ++ t₁ = s₂ ++ t₂ → length s₁ = length s₂ → s₁ = s₂ ∧ t₁ = t₂
| []      []      t₁ t₂ h hl := ⟨rfl, h⟩
| (a::s₁) []      t₁ t₂ h hl := list.no_confusion $ eq_nil_of_length_eq_zero hl
| []      (b::s₂) t₁ t₂ h hl := list.no_confusion $ eq_nil_of_length_eq_zero hl.symm
| (a::s₁) (b::s₂) t₁ t₂ h hl := list.no_confusion h $ λab hap,
  let ⟨e1, e2⟩ := @append_inj s₁ s₂ t₁ t₂ hap (succ.inj hl) in
  by rw [ab, e1, e2]; exact ⟨rfl, rfl⟩

why is length s1 = length s2 required explicitly as a hypothesis?

[Mario Carneiro]

It's not true otherwise

[Andrew Ashworth]

ahh. i guess you'd only have a weaker conclusion without the length requirement, that two lists exist that are subsets of s1 ++ t1

[Mario Carneiro]

Of course that's a trivial consequence, s1 and t1 are such

[Simon Hudon]

If you don't want the length assumption, you could prove s0 ++ t0 = s1 ++ t1 -> s0 = t0 -> s1 = t1

[Mario Carneiro]

I guess that follows from this pretty easily, since if s0 = t0 then length s0 = length t0

[Simon Hudon]

Yeah, you're right! What was I thinking :stuck_out_tongue:

[Andrew Ashworth]

yeah it's something i'm having an issue with, I'm trying to prove that list reversal is injective from scratch

[Mario Carneiro]

The easiest way is to note that reverse is an involution

[Andrew Ashworth]

lemma rev_involutive : ∀ l : list ℕ, rev (rev l) = l
| nil := rfl
| (x::xs) := by simp [*, rev, rev_step, rev_distrib]

[Mario Carneiro]

actually, another way, using that theorem, is to use the mirror version that assumes length t1 = length t2; then you get that concat is injective since the right parts have length 1

[Andrew Ashworth]

somebody had a prose proof in a conference paper i'm reading of how you can automatically prove injectivity of list reversal, and it's not working for me, haha

[Andrew Ashworth]

the concat def is really slick in core lib, i was trying to avoid using it

[Andrew Ashworth]

EDIT: I can't read good, they assume the lengths are equal in the pseudocode figure

[Topologic]

I'm trying to get a sense of the built in methods associated to the list type. I know the basic stack methods for it.

• concatenate is ++
• (a :: l) is push

Now, do the following operations need to be defined by hand?

• delete the ith entry
• add in x : T in the ith entry
• get the ith entry
• splice the list
• length of the list

[Jason Rute]

(deleted)

[Jason Rute]

I answered in the duplicate topic #Is there code for X? > Lists

[Bolton Bailey]

Note that docs#list.append and docs#list.concat are reversed from their normal definitions (we should probably fix this, but it's in lean rather than mathlib).