alternative definition of list.is_prefix

Stream: general

[Kenny Lau]

Could we have a subtype instead of an existential here, as the data is lost in the latter?

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

the data isn't lost, you can recover it by dropping the first n elements of the larger list

[Mario Carneiro]

where n is the length of the smaller list

[Kenny Lau]

right, but has this been done in mathlib?

[Mario Carneiro]

The existential is used because I want it to be a prop

[Kenny Lau]

I mean, the choice function for this existential isn't in mathlib

[Mario Carneiro]

theorem prefix_iff_eq_append (l₁ l₂ : list α) : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
⟨λ h, let ⟨r, e⟩ := h in begin
  rwa append_inj_right ((take_append_drop (length l₁) l₂).trans e.symm) _,
  simp [min_eq_left, length_le_of_sublist (sublist_of_prefix h)],
end, λ e, ⟨_, e⟩⟩

theorem suffix_iff_eq_append (l₁ l₂ : list α) : l₁ <:+ l₂ ↔ take (length l₂ - length l₁) l₂ ++ l₁ = l₂ :=
⟨λ ⟨r, e⟩, begin
  rwa append_inj_left ((take_append_drop (length l₂ - length l₁) l₂).trans e.symm) _,
  simp [min_eq_left, nat.sub_le, e.symm],
  apply nat.add_sub_cancel_left
end, λ e, ⟨_, e⟩⟩